Formal Equivalence Checking (LEC) is the mathematical verification technique that proves two design representations are functionally identical — comparing RTL to gate-level netlist, pre-synthesis to post-synthesis, pre-ECO to post-ECO, or any two design states — by exhaustively proving that every output produces the same value for every possible input combination, without simulation or test vectors.
Why LEC Is Indispensable
Every transformation in the design flow (synthesis, optimization, DFT insertion, CTS, routing optimization, ECO) modifies the netlist. Each modification creates the risk of introducing a functional bug. Running full simulation after every transformation would take weeks. LEC proves equivalence in hours by mathematical analysis, providing exhaustive verification that no bugs were introduced.
How LEC Works
1. Key Point Mapping: The tool identifies corresponding points between the reference (golden) and implementation (revised) designs — primary inputs/outputs, register boundaries, and internal named signals. These "key points" partition the design into manageable combinational cones. 2. Combinational Equivalence: For each key point pair, the tool constructs a mathematical model (Binary Decision Diagram or SAT-based) of the combinational logic cone and proves that the output is identical for all input combinations. If the BDD/SAT proof succeeds, the point is "equivalent." If it fails, a counterexample (specific input vector causing different outputs) is reported. 3. Non-Equivalent Point Debugging: Non-equivalent points indicate either a real bug introduced during transformation or a mapping problem. The tool reports the distinguishing input pattern, enabling rapid root-cause identification.
LEC in the Design Flow
| Comparison | What It Catches |
|---|---|
| RTL vs. synthesized netlist | Synthesis optimization bugs, incorrect constraint application |
| Pre-DFT vs. post-DFT | Scan insertion errors, test-mode logic mistakes |
| Pre-CTS vs. post-CTS | Clock tree buffer insertion errors |
| Pre-route vs. post-route optimization | Timing-driven optimization mistakes |
| Pre-ECO vs. post-ECO | Manual or automated ECO implementation errors |
Challenges
- Retiming: Synthesis may move logic across register boundaries (retiming) for timing optimization. Standard combinational LEC fails on retimed designs because the register mapping changes. Sequential equivalence checking or retiming-aware LEC modes handle this.
- Datapath Optimization: Arithmetic optimizations (carry-lookahead replacement, multiplier restructuring) can make the two netlists structurally unrecognizable. Modern LEC tools use arithmetic-aware solvers.
- Clock Gating: Inserted ICG cells change the register enable structure. LEC must recognize ICG-inserted equivalences.
Formal Equivalence Checking is the mathematical safety net of the implementation flow — providing absolute proof that no functional bug was introduced at each transformation step, a guarantee that no amount of simulation can match.
Explore 500+ Semiconductor & AI Topics
From EUV lithography to CUDA optimization — search the full knowledge base or chat with our AI assistant.