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

<svg viewBox="0 0 485 264" xmlns="http://www.w3.org/2000/svg" style="max-width:100%;height:auto" role="img"><rect x="0" y="0" width="485" height="264" rx="12" fill="#0d1117"/><g font-family="ui-monospace,SFMono-Regular,Menlo,Consolas,&quot;Liberation Mono&quot;,monospace" font-size="14"><text xml:space="preserve" x="20" y="31.7"><tspan fill="#c9d1d9"> Reference (Golden)     Implementation (Revised)</tspan></text><text xml:space="preserve" x="20" y="50.7"><tspan fill="#c9d1d9">      RTL                   Gate-Level Netlist</tspan></text><text xml:space="preserve" x="20" y="69.7"><tspan fill="#c9d1d9">       </tspan><tspan fill="#6e7681">↓</tspan><tspan fill="#c9d1d9">                         </tspan><tspan fill="#6e7681">↓</tspan></text><text xml:space="preserve" x="20" y="88.7"><tspan fill="#c9d1d9">   Read &amp; Elaborate          Read &amp; Elaborate</tspan></text><text xml:space="preserve" x="20" y="107.7"><tspan fill="#c9d1d9">       </tspan><tspan fill="#6e7681">↓</tspan><tspan fill="#c9d1d9">                         </tspan><tspan fill="#6e7681">↓</tspan></text><text xml:space="preserve" x="20" y="126.7"><tspan fill="#c9d1d9">   Map Key Points </tspan><tspan fill="#6e7681">←──────→</tspan><tspan fill="#c9d1d9"> Map Key Points</tspan></text><text xml:space="preserve" x="20" y="145.7"><tspan fill="#c9d1d9">       </tspan><tspan fill="#6e7681">↓</tspan><tspan fill="#c9d1d9">                         </tspan><tspan fill="#6e7681">↓</tspan></text><text xml:space="preserve" x="20" y="164.7"><tspan fill="#c9d1d9">       </tspan><tspan fill="#6e7681">└────────</tspan><tspan fill="#c9d1d9"> Compare </tspan><tspan fill="#6e7681">────────┘</tspan></text><text xml:space="preserve" x="20" y="183.7"><tspan fill="#c9d1d9">                    </tspan><tspan fill="#6e7681">↓</tspan></text><text xml:space="preserve" x="20" y="202.7"><tspan fill="#c9d1d9">            PASS (equivalent)</tspan></text><text xml:space="preserve" x="20" y="221.7"><tspan fill="#c9d1d9">                 or</tspan></text><text xml:space="preserve" x="20" y="240.7"><tspan fill="#c9d1d9">            FAIL (non-equivalent with counterexample)</tspan></text></g></svg>

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

Common LEC Issues

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.