What is Equivalence Checking?

In any typical complex SoC design, there are many tools in the flow that perform operations on the design. Besides logic synthesis, there are power optimization steps, testability insertion and functional ECOs to address design issues or design changes.

All of these steps can introduce subtle modifications in design behavior that can be missed by simulation, since simulation is only as complete as the test bench that drives it. Since equivalence checking is based on a vectorless formal proof approach, this technology can catch a wide range of errors introduced during this process. This significantly enhances the confidence in the end result.

Equivalence checking provides a powerful addition to any design flow. The ability to apply formal methods to verify the consistency of a design gives insight into the quality of the result that is not dependent on the completeness of the test bench. Specific benefits include:

• Higher efficiency. Less reliance on slower gate-level simulation.
• Higher confidence. Less concerns that the tool chain or ECOs have introduced subtle errors.
• Higher quality. This technique can highlight poor RTL coding in the design.
• Higher predictability. Less chance of missing bugs.

Logic equivalence checking (LEC) looks at the combinatorial structure of the design to determine if the structure of two alternative implementations will exhibit the same behavior. If operations such as retiming are applied to a design, the structure of the design will no long map between the two representations.

Sequence equivalency checking (SEC) takes timing into account and examines the equivalency of two design representations over multiple clock cycles.