Every stage of a chip's journey — from RTL coding through synthesis, optimization, and physical implementation — transforms the design structurally. Each transformation carries the risk of silently altering the intended logic. Catching such discrepancies after tape-out means costly silicon re-spins. Logic Equivalence Check (LEC) exists to prevent exactly that.

LEC is a cornerstone of formal verification in modern VLSI flows. Rather than relying on simulation vectors, it uses mathematical proof engines to exhaustively confirm that two representations of a design are functionally identical — for every possible input combination, without exception.

What Is Formal Verification — and Where Does LEC Fit?

Formal verification is a class of mathematical techniques used to prove properties about a digital design without relying on test stimuli. Unlike simulation — which only exercises the design for the specific input vectors you provide — formal methods analyze all possible input conditions by construction.

This makes formal verification especially powerful for proving the absence of bugs, not just their presence. Simulation can find bugs; formal verification can prove they don't exist.

Within the formal verification family, Logic Equivalence Check addresses a specific and practical question: Do these two representations of the same design behave identically? It does not verify that the design is correct in an absolute sense — it verifies that a transformation has not changed what was already there.

Logic Equivalence and the Concept of Logic Cones

Two designs are said to be logically equivalent when they produce identical output values for every combination of inputs — regardless of how their internal gate structures differ. A two-level AND-OR tree and a single complex-gate cell can be equivalent even though they look nothing alike structurally.

For designs with millions of gates, checking equivalence as a single monolithic problem is computationally infeasible. This is where the concept of logic cones becomes essential.

What Is a Logic Cone?

A logic cone is the complete set of combinational logic and sequential elements that collectively determine the value of a specific output or internal key point. For any given output pin, its cone includes every gate, mux, and flip-flop that can influence it.

By decomposing the design into individual cones, the LEC tool transforms an enormous monolithic problem into many smaller, parallelizable sub-problems. Each cone in the reference design is matched to its counterpart in the implementation, and equivalence is checked cone-by-cone with mismatches reported precisely at the output they affect.

The Three Types of LEC in a VLSI Design Flow

LEC is not a one-time checkpoint — it is applied repeatedly as the design evolves. Each application targets a specific transformation stage.

RTL-to-RTL Equivalence Checking

When engineers refactor RTL for better synthesis quality, fix bugs, or restructure state machines, RTL-to-RTL LEC confirms no functional intent was lost. The original RTL is frozen as the reference; the revised RTL is the implementation.

RTL-to-Netlist Equivalence Checking

Synthesis transforms RTL into a gate-level netlist using technology mapping, constant propagation, and logic optimization — all of which alter structure while theoretically preserving behavior. RTL-to-Netlist LEC is the formal proof that synthesis did its job correctly.

Netlist-to-Netlist Equivalence Checking

After place-and-route, power optimization, clock tree synthesis, or ECO changes, the netlist differs from its pre-optimization form. Netlist-to-Netlist LEC confirms that physical implementation has not altered the logic — a formal sign-off requirement before tape-out.

Equivalence vs. Non-Equivalence: A Concrete Example

Consider an output Z defined in RTL as the logical AND of two inputs A and B. During synthesis, the tool implements this using a NAND gate followed by an inverter — structurally different but functionally identical. LEC proves equivalence: both produce Z = A·B for all inputs.

// RTL (Reference)
assign Z = A & B;

// Netlist — different structure, same behavior
nand U1 (.A(A), .B(B), .Z(n1));
inv  U2 (.A(n1),       .Z(Z));

// LEC result: EQUIVALENT ✓

Now introduce an unintended inversion — a wrong port connection during ECO entry, or a synthesis constraint that accidentally complements a signal. The LEC tool reports a counterexample: the specific input combination where the two designs produce different output values.

Diagnosing and Fixing Logic Non-Equivalence

A failing LEC run is not a dead-end — it is a precise diagnostic. Modern LEC tools provide counterexamples, cone-level schematic tracing, and hierarchy-aware debugging that significantly narrow the root cause.

Common Root Causes

Synthesis constraint errors are a frequent culprit. If a constraint incorrectly models a false path or don't-care condition, the synthesis tool may legally transform logic that should have been preserved. Correcting the constraint and re-running synthesis typically resolves these cases.

Reset and initial-state mismatches arise when the reference and implementation disagree on reset polarity, synchrony, or initial flip-flop values. Ensuring consistent reset definitions — and correct reset mapping rules in the LEC tool — is essential.

ECO-introduced errors are among the most common causes in late-stage flows. Manual ECO changes or incremental synthesis passes can inadvertently toggle a signal polarity. The counterexample from LEC directly points to the affected cone.

Mapping and hierarchy issues — misaligned black-box definitions, renamed signals, or flattened hierarchies — can cause false mismatches. Proper design hierarchy alignment and careful black-box configuration resolves these.

LEC Debugging Workflow

Start by examining the counterexample to understand which output is failing and under what conditions. Use the tool's cone-tracing feature to identify the exact gate or net where divergence first appears. Cross-reference with recent changes — synthesis re-runs, ECO scripts, or constraint modifications. Fix the root cause, re-run LEC, and confirm clean.

Frequently Asked Questions