Formal Equivalence Checking between High-Level and RTL Hardware Designs

Digital applications complexity makes it harder every day to discover and debug behavioral inconsistencies at register transfer level (RTL). Aiming to bring a solution, several techniques have appeared as alternatives to verify that a circuit description meets the requirements of its corresponding functional specification. Simulation is widely applied due to its convenience to uncover early design bugs, but is far from providing the exhaustiveness acquired through formal methods, for which improved and new tools continue to appear. On the other hand, formal verification can suffer from problems such as state-space explosion or modeling inaccuracy. Then, it is vital to develop new ways to check a design for consistency fast and comprehensively. In this paper, we propose a sequential equivalence checking (SEC) formalism and an algorithm, for use between a specification, written at electronic system level (ESL), and an implementation, written at RTL. Given that equivalence is checked between different levels of abstraction, it is no longer valid to perform SEC on single states, thus, we show a scheme to extract and compare complete sequences of states in order to determine if the design intention, which is described in the ESL specification, is contained and respected by the RTL implementation. The results obtained suggest that our methodology can be applied efficiently on real designs.