Synopsys Cloud
Any Tool. Any Scale. Any Time.
Request a Free Evaluation →
What is Equivalence Checking?
Definition
Equivalence checking is a portion of a larger discipline called formal verification. This technology uses mathematical modeling techniques to prove that two representations of design exhibit the same behavior. This approach should not be confused with functional verification, which uses exhaustive simulation to verify the correctness of a design.
Once a verified version of a design has been identified, equivalence checking can be used to determine if an alternate representation of the design behaves the same as the verified version. This technique does not use input vectors so it is more efficient.
Equivalence checking is useful to verify that a design’s function has not changed after an operation like synthesis, or after a functional ECO has been applied.
How does equivalence checking work?
There are three basic steps in equivalence checking:
- Setup
- Mapping
- Compare
Inputs to Setup include the verified reference design, library elements and the revised design. In this step the inputs are read in and data structures are created to facilitate the subsequent steps.
In Mapping, key points of the design are mapped and compared. Logic cones are typically used to organize compare points. A logic cone is a block of combinational logic that drives a compare point. Inputs to a logic cone include register output pins, primary input ports and black-box output pins. Compare points include registers, primary output ports and black-box input pins.
During Compare, the key mapped points are examined to determine if they are equivalent, non-equivalent, or inverted equivalent. Parts of the design that return an inconclusive result can be rerun with a higher level of effort to resolve.
The figure below illustrates the process:
Why is equivalence checking important?
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.
What are the benefits of equivalence checking?
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 vs. Sequence Equivalence Checking
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.
What solutions does Synopsys offer?
Synopsys offers Formality Equivalence Checking that uses formal and static techniques to determine if two versions of a design are functionally equivalent.
Synopsys also offers VC Formal, a solution that includes a comprehensive set of formal applications (Apps), including Property Verification (FPV), Automatic Extracted Properties (AEP), Coverage Analyzer (FCA), Connectivity Checking (CC), Sequential Equivalence Checking (SEQ), Register Verification (FRV), X-Propagation Verification (FXP), Testbench Analyzer (FTA), Regression Mode Accelerator (RMA), Datapath Validation (DPV), Functional Safety (FuSa) and a portfolio of Assertion IPs (AIP) for verification of standard bus protocols.
Lastly, Synopsys offers ESP, which is a Custom Design Formal Equivalence Checking Based on Symbolic Simulation. ESP is a formal equivalence checking tool commonly used for full functional verification of custom designs such as embedded memories, custom macros, standard cells and I/O cell libraries. It is used to ensure that two design representations are functionally equivalent. These designs maybe represented as Verilog Behavioral model, RTL, Gate, Switch or SPICE or .db netlist view.
