Knowledge Center
Knowledge Center

Combinatorial Equivalence Checking

Verify functionality between registers remains unchanged after a transformation


Equivalence checking takes two designs and ascertains if they have the same functionality. This is important in the design flow where the RTL design, usually described in Verilog or VHDL, is modified by tools and manual methods as it goes through physical implementation. The RTL model is treated as the golden model and this is verified through functional verification to ensure it has the intended behavior. Once this model has been verified, an automated and rigorous method is required to ensure that the derived models are functionally equivalent.
An RTL description defines the registers in a design and the logic that exists between them. During synthesis, the logic may be optimized, combined with the logic of other pieces of the design so that elements can be reused, have additional logic inserted for test purposes, or any number of other transformations. The registers may also become shared, but the circuit is not retimed, meaning that the outputs of the design should be the same for each and every clock.

Given that proviso, combinatorial equivalence checking takes the logic between registers and ascertains if this has the correct behavior. There can be no state-holding elements or feedback loops such that the outputs is a simple function of the current inputs.

More modern commercial equivalence checkers can also handle limited changes in the sequential nature of the design. For example, pipeline retiming changes the register pairs between which some logic exists, but produces the same results. Clock gating may also be added for power reduction that requires special handling.


Equivalence Checking of Digital Circuits: Fundamentals, Principles, Methods

Formal Equivalence Checking and Design Debugging (Frontiers in Electronic Testing)

Formal Equivalence Checking and Design Debugging (Frontiers in Electronic Testing)