Formal verification

Logical Equivalence Checking for RTL — and what “equivalent” really means

Logical equivalence checking (LEC) answers one question: do two versions of a design compute the same outputs for every legal input? It is the workhorse that lets you trust a synthesis netlist against its RTL, a manually retimed pipeline against its reference, or an ECO patch against the block it patched. But “equivalent” is a precise claim, and a sloppy equivalence run can report “equivalent” while having compared almost nothing. This page covers how LEC actually works — combinational vs sequential, miters, k-induction — and the honesty rule that separates a real proof from a vacuous one.

What LEC proves (and what it does not)

LEC is a formal method: when it succeeds, it proves equivalence over the entire input space, not just the vectors a testbench happened to drive. That is its whole value over simulation. A passing LEC result means there is no input pattern that makes the two designs disagree on the compared outputs.

What it does not prove is that either design is correct. LEC checks that B matches A; if A has a bug, B will faithfully reproduce it and LEC will happily call them equivalent. Equivalence is a relationship between two artifacts, not a verdict on intent. For intent you still need a verification plan with assertions and coverage. LEC's job is to let you change one artifact into another without re-verifying from scratch.

Combinational equivalence

The simplest and most common case. If two designs have the same state elements — same registers, same names, or a known correspondence — the problem decomposes into purely combinational cones of logic feeding each register and each output. For every such cone, you ask: is the Boolean function on the gold side identical to the function on the gate side?

You answer it by building a miter: instantiate both cones, tie their inputs together, XOR their outputs, and ask a SAT or BDD engine whether the XOR can ever be 1. If it cannot, the functions are equal. If it can, the solver hands you the exact input that distinguishes them — a counterexample you can drop straight into a waveform.

// A miter circuit: two designs, the same inputs, XOR their outputs.
// If the XOR can ever be 1, the designs differ -> a counterexample.
// If a solver proves the XOR is always 0, the outputs are equivalent.
module miter (input  logic [7:0] a, b, output logic differ);
    logic [7:0] y_spec, y_impl;
    spec u_spec (.a(a), .b(b), .y(y_spec));   // golden / RTL
    impl u_impl (.a(a), .b(b), .y(y_impl));   // revised / netlist
    assign differ = |(y_spec ^ y_impl);       // 0 == equivalent
endmodule

Combinational LEC scales remarkably well because modern SAT solvers exploit the structural similarity between a netlist and the RTL it was synthesized from. Synthesis preserves most of the register boundaries, so the register correspondence is usually easy to establish and the per-cone miters stay small.

Sequential equivalence and k-induction

Combinational LEC breaks down the moment the two designs do not share a register mapping — retiming moved a flop across a logic cloud, a pipeline gained a stage, a FSM was re-encoded, or clock gating changed when a register updates. Now you cannot match state one-to-one, and you have to reason about behavior over time: do the two machines produce the same output sequence for the same input sequence?

This is sequential equivalence checking (SEC), and it is genuinely harder. The standard open-tool approach is bounded model checking with k-induction: build a miter over the two state machines and prove the outputs agree for the first k cycles, then prove that if they agree for k consecutive cycles they agree on the next one. When both halves hold, equivalence is proven for all time. When only the bounded half holds, you have evidence up to depth k and nothing beyond it — which is exactly the kind of result you must report honestly rather than rounding up to “equivalent.”

Multipliers, large counters, and deep memories are where bounded SEC tends to run out of road: the induction step does not close within the depth or the time budget. An honest tool calls this inconclusive, not equivalent — more on that below.

Doing it with open tools: Yosys and EQY

You do not need a proprietary equivalence checker to get real evidence. The open flow is Yosys for the front end plus EQY (Equivalence checKY) to orchestrate the comparison, with SymbiYosys and a SAT backend doing the proving. EQY partitions the design into match points, builds miters at each, and dispatches them to the solver. For RTL-vs-netlist it reads the gold RTL and the gate netlist (with the standard-cell library models) and lines up the registers automatically.

# eqy: an EQY problem file pairing RTL against its synthesized netlist.
[gold]
read -sv rtl/alu.v
prep -top alu

[gate]
read_verilog netlist/alu_syn.v
read_verilog -lib sky130_fd_sc_hd.v   # cell models for the gate side
prep -top alu

[strategy sby]
use sby
depth 5      # sequential: prove equivalence up to k=5 cycles

This is the same flow ChipVerify AI runs to compare a synthesized sky130 netlist against its RTL as part of the RTL-to-GDSII preview on open PDKs. It is pre-signoff evidence — that the synthesis step did not change behavior — produced on open tools. It is not a foundry signoff and does not replace a commercial signoff flow; it is a structural, formally-grounded check you can run on every commit.

The honesty rule: a proof over zero points is vacuous

Here is the failure mode that quietly turns a green LEC report into a lie. Equivalence is only meaningful relative to a set of equivalence points — the output ports and matched registers whose functions you actually compared. If the tool fails to match any points — because port names changed, a module did not elaborate, the netlist parsed partially, or the two designs have disjoint interfaces — then it compared nothing. Every (empty) miter trivially proves true, and a naive tool prints “EQUIVALENT.”

That result is vacuous, not equivalence. Zero compared points is the LEC equivalent of a testbench that runs zero vectors and reports “all tests passed.” A trustworthy LEC must require that at least one real equivalence point was matched and proven, and must surface the count of matched-and-proven points alongside the verdict. ChipVerify AI enforces this directly: a run that matches no equivalence points is reported as inconclusive, never as equivalent. The same anti-vacuity discipline applies to assertion-based checks, where a property that can never fire is a false sense of safety rather than a passing one.

What “inconclusive” honestly means

A real LEC run has three outcomes, and the third one matters as much as the first two:

• Equivalent — at least one equivalence point was matched, and every matched point was proven equal over the full input space (or, for SEC, k-induction closed). This is a positive proof, not an absence of failures.
• Not equivalent — a miter was satisfiable; the solver returns a concrete counterexample input that makes the two designs disagree. This is the most actionable result: you get a waveform that reproduces the divergence.
• Inconclusive — the proof did not complete: bounded depth was reached without closing induction, the solver timed out, a module failed to elaborate, or zero points matched. This is not a pass. Reporting it as equivalence is the single most dangerous thing an equivalence tool can do, because downstream engineers treat “equivalent” as permission to skip re-verification.

The discipline is simple to state and easy to violate: equivalence is a claim you earn by proving matched points, and anything short of that — including a clean-looking run that secretly compared nothing — must degrade to inconclusive.

Where LEC fits in your flow

• RTL vs synthesis netlist — the classic use: confirm the synthesizer preserved behavior. Combinational LEC almost always closes here.
• ECO verification — prove a late metal/logic patch did exactly what was intended and nothing else.
• RTL vs RTL refactor — prove a readability or timing refactor did not change function. Watch for matched-point count: a rename can make the tool think nothing corresponds.
• After clock or reset restructuring — pair LEC with clock-domain-crossing analysis, because LEC compares function under a single clocking assumption and will not catch metastability hazards on its own.

FAQ

Is LEC the same as a formal property check?

No. Property checking proves an assertion holds about onedesign. LEC proves a relationship between two designs. They share the same SAT/BMC machinery, and both must guard against vacuity — a property that never fires and a miter over zero points are the same disease.

Does equivalence mean my chip will work?

It means the second design behaves like the first. If the first is golden and your equivalence points cover every output, that is strong evidence the transformation was safe. It says nothing about timing, power, CDC, or whether the golden reference itself is correct — and it is pre-signoff evidence, not a foundry signoff.

Why did my run say “inconclusive” on a multiplier?

Wide combinational multipliers and deep sequential structures blow past the SAT or k-induction budget. That is an honest limit of bounded open tools, not a bug. The right response is to report the bound reached, not to round up to equivalent.