Formal Verification Equivalence
Formal Equivalence Checking (LEC) is the mathematical verification technique that proves two representations of a digital design are functionally identical — comparing the RTL against the synthesized gate-level netlist, or the pre-layout netlist against the post-layout netlist, using Boolean algebra and SAT solvers rather than simulation, providing exhaustive proof of correctness without input vectors.
Why LEC Is Necessary
Every transformation step in the design flow — synthesis, scan insertion, clock tree synthesis, place-and-route optimization, engineering change orders (ECOs) — modifies the netlist. Each modification could introduce a functional error. Simulation cannot exhaustively verify that a 500-million-gate netlist is unchanged because the input space is astronomically large (2^n for n inputs). LEC provides mathematical proof of equivalence in hours instead of the years that exhaustive simulation would require.
How LEC Works
1. Key Point Mapping: The tool identifies corresponding state elements (flip-flops, latches, memories) between the reference (golden) and revised designs. Mapping uses net names, hierarchy, and structural analysis.
2. Combinational Cone Extraction: For each mapped key point pair, the tool extracts the combinational logic cone (all gates between the driving flip-flops and the output flip-flop) from both designs.
3. Boolean Comparison: Each pair of corresponding combinational cones is compared using BDD (Binary Decision Diagram) or SAT (Boolean Satisfiability) solvers. If the Boolean functions are identical for all possible input combinations, the pair is marked "equivalent." If a difference exists, the tool generates a counterexample (a specific input pattern that produces different outputs).
4. Reporting: The tool reports the number of equivalent, non-equivalent, and unmapped points. A fully-passing LEC run shows 100% equivalence with zero non-equivalent or unmapped points.
LEC Checkpoints in the Design Flow
| Checkpoint | Reference | Revised | What Changed |
|---|---|---|---|
| Post-Synthesis | RTL | Gate-level netlist | Logic synthesis optimization |
| Post-DFT | Pre-DFT netlist | Post-DFT netlist | Scan insertion, compression |
| Post-CTS | Pre-CTS netlist | Post-CTS netlist | Clock tree buffer insertion |
| Post-Route | Pre-route netlist | Post-route netlist | Buffer insertion, gate resizing |
| ECO | Pre-ECO netlist | Post-ECO netlist | Manual or automated changes |
Challenges at Scale
- Design Size: Modern SoCs have 500M+ gates. LEC must partition the problem into manageable chunks (hierarchical LEC, compose each block separately).
- Sequential Equivalence: When synthesis performs retiming (moving flip-flops across combinational logic for timing optimization), the key point mapping changes. Sequential equivalence checking using induction-based proofs is required, which is more computationally expensive.
Formal Equivalence Checking is the mathematical guarantee that the design was not corrupted during implementation — providing bit-exact proof that every logic transformation preserved the designer's original functional intent.