formal verification equivalence
**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.