formal equivalence checking
**Formal Equivalence Checking (LEC)** is the **mathematical verification technique that proves two circuit representations are functionally identical** — most commonly used to verify that synthesis, place-and-route, and ECO (Engineering Change Order) transformations have not altered the logical behavior of a design, providing exhaustive correctness guarantees that simulation cannot match.
Unlike simulation, which tests a finite number of input vectors, LEC uses formal methods (BDD-based or SAT-based) to prove equivalence for all possible input combinations. This makes LEC the gold standard for verifying that physical implementation matches the RTL specification.
**LEC Flow Stages**:
| Stage | Reference | Revised | Purpose |
|-------|----------|---------|----------|
| **RTL vs. Synthesis** | RTL (Verilog/VHDL) | Gate-level netlist | Verify synthesis correctness |
| **Synthesis vs. P&R** | Pre-layout netlist | Post-layout netlist | Verify P&R changes |
| **Pre-ECO vs. Post-ECO** | Before change | After change | Verify targeted fix |
| **Signoff** | RTL | Final GDS netlist | End-to-end verification |
**Key Concepts**: LEC operates by identifying **compare points** — corresponding flip-flops, ports, or latches in both designs — and proving that for identical primary inputs, each compare point produces identical outputs. The tool maps corresponding points using names, structural analysis, or user guidance.
**Non-Equivalent (NEQ) Debugging**: When LEC reports non-equivalence, the tool provides a **counterexample** — a specific input pattern that produces different outputs. Common causes of NEQ: synthesis optimizations that change logic structure beyond what LEC can map automatically, clock gating insertion changing register enable conditions, scan chain insertion modifying multiplexer logic, and manual ECO changes with unintended side effects.
**Challenges at Advanced Nodes**: **Setup complexity** — advanced low-power designs with multiple power domains, retention registers, and isolation cells require careful LEC setup to handle cells that behave differently during normal operation vs. power-down modes. **Runtime** — large designs (100M+ gates) may require partitioning and hierarchical LEC to manage compute requirements. **Sequential equivalence** — retiming optimizations (moving registers across combinational logic) change the cycle-by-cycle behavior while preserving multi-cycle functionality, requiring sequential equivalence checking rather than combinational LEC.
**LEC in the Design Flow**: LEC runs are typically automated in the signoff checklist. The synthesis tool generates a setup file that guides the LEC tool on how to map the two representations. Teams maintain a LEC waiver database for known acceptable differences (e.g., test-mode-only logic, debug features).
**Formal equivalence checking provides the mathematical certainty that no bug was introduced during implementation — in an era where a single gate-level error in a billion-gate SoC could cause a costly silicon respin, LEC is the indispensable proof that the chip you fabricate matches the chip you designed.**