Introduction
In VLSI design, equivalence checking is a key part of the broader discipline known as formal verification. Unlike functional verification, which relies on exhaustive simulation with test vectors, equivalence checking uses mathematical modelling to prove that two versions of a design behave identically under all circumstances.
This approach ensures that even after transformations like synthesis, optimizations, or functional ECOs, a design’s functionality remains unchanged without the overhead of running countless simulations.
What is Equivalence Checking?
Equivalence checking verifies whether an alternative representation of a design matches a previously verified reference version. For example, after synthesizing RTL to a gate-level netlist or applying a functional ECO, equivalence checking can confirm that the new design behaves the same as the original.
Because it does not rely on input vectors, this method is faster and more efficient than traditional simulation-based verification.
How Equivalence Checking Works
Equivalence checking generally follows three main steps:
1. Setup
The first step involves loading the reference design, the revised or implementation design, and the necessary library elements. Data structures are created to manage the subsequent comparison process efficiently.
2. Mapping
Key points in the design, known as compare points, are identified and linked between the two designs. These often involve logic cones, which are blocks of combinational logic that drive the compare points. Inputs to a logic cone typically include:
- Register outputs
- Primary input ports
- Black-box outputs
Compare points usually consist of:
- Registers
- Primary output ports
- Black-box inputs
3. Comparison
At this stage, the tool examines each mapped point to determine equivalence. Results can fall into one of several categories:
- Equivalent: Both designs match at this point.
- Non-equivalent: A discrepancy exists.
- Inverted equivalent: Behaviour matches but with inverted logic.
Inconclusive points can be analysed further with additional effort or higher-level mapping techniques.
Why Equivalence Checking Matters
Modern SoC designs are highly complex and pass through numerous automated steps including logic synthesis, power optimization, testability insertion, and ECOs. Each of these steps can subtly alter design behaviour.
Simulation alone may not catch all such changes, because it is limited by the completeness of the test bench. Equivalence checking, with its vector less formal approach, can detect subtle errors that simulation might miss, ensuring high confidence in the final design.
Benefits of Equivalence Checking
Incorporating equivalence checking into your design flow provides several advantages:
- Efficiency: Reduces reliance on time-consuming gate-level simulations.
- Confidence: Detects subtle errors introduced by transformations or ECOs.
- Design Quality: Highlights potential issues in RTL coding or design structure.
- Predictability: Reduces the risk of missing hidden bugs before tape-out.
Types of Equivalence Checking
Logic Equivalence Checking (LEC)
LEC focuses on combinational logic and structural mapping. It verifies that two implementations will behave the same in terms of logic output. However, structural changes like retiming may prevent direct mapping between designs, requiring more advanced handling.
Sequential Equivalence Checking (SEC)
SEC goes a step further by considering timing and clock cycles. It evaluates the equivalence of designs over multiple cycles, making it ideal for designs with sequential logic and pipelined operations.
Conclusion
Equivalence checking, whether logic-based or sequential, is an essential step in modern VLSI verification. It provides mathematical assurance of design correctness, ensures consistency across transformations, and strengthens confidence in the final silicon.