Download Brochure
Contact Us
Contact Us
Contact Us
Contact Sales
  • Company
  • About Us
  • Investor Relations
  • Community
  • Newsroom
  • Resources
  • Careers & Culture
Contact Us
All Synopsys
+ Silicon Design & Verification + Silicon IP + Software Integrity + About Us
Support
SolvNetPlus Software Integrity Customer Community
Global Sites
日本語 简体中文 繁體中文 Русский

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:

  1. Setup
  2. Mapping
  3. 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:

Functional ECO Figure 1 | Synopsys

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 Formality Figure | Synopsys

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.

Related Solutions

Formality Equivalence Checking Solution

Formality ECO

ESP: Custom Design Formal Equivalence Checking Based on Symbolic Simulation