Logic Equivalence Checking
Logic Equivalence Checking (LEC) is the formal verification technique that mathematically proves two circuit representations compute identical logic functions — comparing RTL to gate-level netlist, pre-synthesis to post-synthesis, or pre-layout to post-layout netlist to guarantee that no functional errors were introduced by synthesis, optimization, DFT insertion, or ECO modifications, providing exhaustive proof of correctness that simulation alone cannot achieve.
Why LEC Is Essential
- Synthesis transforms RTL (behavioral) into gates → thousands of optimizations applied.
- Each optimization could introduce a bug → simulation covers only a fraction of input space.
- LEC proves ALL possible inputs produce identical outputs → complete verification.
- Required at every major transformation: synthesis, DFT, P&R optimization, ECO.
LEC Flow
Key Points
- LEC compares at mapped comparison points:
- Primary outputs.
- Flip-flop data inputs (next-state logic cones).
- Black-box inputs.
- Each comparison point: Tool builds BDD or SAT representation → checks equivalence.
- If equivalent: Mathematical proof that no input can produce different outputs.
- If non-equivalent: Tool produces counterexample input vector.
LEC Checkpoints in Design Flow
| Checkpoint | Reference | Implementation | What Changed |
|---|---|---|---|
| Post-synthesis | RTL | Synthesized netlist | Logic optimization |
| Post-DFT | Pre-DFT netlist | DFT-inserted netlist | Scan chains, BIST |
| Post-layout | Pre-layout netlist | Post-layout netlist | Placement optimization |
| Post-ECO | Pre-ECO netlist | Post-ECO netlist | Engineering changes |
Common LEC Issues
| Issue | Cause | Resolution |
|---|---|---|
| Unmapped points | Name changes during optimization | Adjust mapping directives |
| Black boxes | Missing IP models | Provide Liberty/behavioral model |
| Non-equivalent | Synthesis bug or intended change | Analyze counterexample |
| Abort (complexity) | Logic cone too large for SAT solver | Partition, add intermediate points |
| Sequential elements mismatch | Retiming, register merging | Enable sequential LEC mode |
Formal Engines
- BDD (Binary Decision Diagrams): Canonical form → equivalence = structural comparison. Memory-limited for large cones.
- SAT (Boolean Satisfiability): Prove no assignment makes outputs differ. More scalable.
- Hybrid: BDD for small cones, SAT for large. Modern tools use portfolio of engines.
Sequential Equivalence
- Standard LEC is combinational: Assumes same state → checks same output.
- Sequential LEC: Proves equivalence across multiple clock cycles.
- Needed when: Retiming (registers moved), FSM re-encoding, pipeline stage changes.
- More complex: Requires induction or bounded model checking.
Logic equivalence checking is the mathematical guarantee that the chip you manufacture matches the design you verified — without LEC, every synthesis run, DFT insertion, and layout optimization would require re-running the entire simulation regression (weeks of compute), and even then couldn't provide the exhaustive proof that formal LEC delivers in hours, making LEC an indispensable pillar of the modern digital design verification flow.