Equivalence Checking

1. What LEC Proves

Logic Equivalence Checking is a formal method that takes two circuit representations — called the golden and the revised — and mathematically proves they implement the exact same Boolean function at every output point. It is not simulation: no test vectors are applied. Instead, the tool constructs a mathematical proof using Binary Decision Diagrams (BDDs), SAT solvers, or a combination of both.

The critical distinction: LEC verifies structural transformation correctness, not specification compliance. Given an RTL that correctly implements a FIFO, LEC can prove that the post-synthesis netlist is functionally identical to that RTL. But it cannot tell you whether the RTL's FIFO depth was the right choice — that is the domain of functional verification and formal property checking.

LEC produces one of three verdicts per output (key point):

2. RTL-to-Gate vs Gate-to-Gate Use Cases

LEC is applied at multiple stages of the ASIC flow, with different golden/revised pairs at each stage. Understanding the right pair to compare at each step is essential for building a robust sign-off flow.

The RTL-to-gate run is the most critical and runs immediately after synthesis. The gate-to-gate run after layout catches late-stage tool bugs. Both are mandatory for tapeout sign-off in any serious ASIC methodology.

3. Combinational vs Sequential LEC

LEC comes in two fundamentally different modes, each appropriate for different circuit transformations.

Combinational LEC

Combinational LEC treats every register (flip-flop and latch) as a cut-point: register outputs become pseudo primary inputs (PPIs) and register inputs become pseudo primary outputs (PPOs). The entire sequential circuit is thus decomposed into a set of purely combinational logic cones, each of which is verified independently.

This approach is extremely fast — modern BDD and SAT engines can verify millions of cones per hour. It works correctly as long as there is a one-to-one correspondence between registers in the golden and revised designs: the same register in both designs is assigned the same initial state, and the synthesis tool did not move logic across register boundaries.

Sequential LEC

Sequential LEC is required when register-to-register correspondence cannot be established — most commonly after register retiming. Retiming is a synthesis optimization that moves registers forward or backward across combinational logic to balance pipeline stages and improve timing. After retiming, a register in the revised design may correspond to no single register in the golden design; it may represent the combination of state from multiple old registers.

Sequential LEC handles this by bounded unrolling: it unrolls the circuit over K time steps and proves that for any input sequence of length K, both designs produce identical output sequences. The value of K is set high enough to cover the state-machine depth. This is exponentially more expensive than combinational LEC and is applied selectively to blocks where combinational LEC fails to establish register mapping.

4. Key Points: The Partitioning Concept

The key point is the foundational concept of LEC. A key point is any circuit node that divides the design into independent combinational cones for equivalence checking. The tool verifies one cone at a time: it proves that the function computed at the revised key point is identical to the function computed at the corresponding golden key point, given the same values at all upstream key points.

What Qualifies as a Key Point?

• Registers (flip-flops and latches): The most important class. Every register in the design becomes a key point automatically. Its output is a PPI (pseudo primary input) and its input is a PPO (pseudo primary output).
• Primary inputs (PIs): Top-level input ports of the design — treated as primary inputs in both golden and revised.
• Primary outputs (POs): Top-level output ports — the ultimate verification targets.
• Black boxes: When a sub-block is marked as a black box (IP core, memory macro), its output pins become PPIs. The tool assumes both golden and revised black boxes are functionally identical and verifies only the logic surrounding them.
• User-defined cut-points: Engineers can manually add cut-points to help the tool handle complex logic cones that are causing UNVERIFIED results due to resource limits.

How Mapping Works

The tool performs name-based matching first: it looks for registers with the same hierarchical name in both golden and revised. Synthesis tools may rename registers during optimization; to help the tool, designers use dont_rename or set_dont_rename constraints, or the tool uses structural/functional heuristics to match renamed points. When automatic matching fails for a register, the tool marks it UNMATCHED, which cascades into UNVERIFIED results for all cones involving that register.

5. Synopsys Formality Workflow

Synopsys Formality is the industry-standard LEC tool at most semiconductor companies. It is invoked via Tcl scripts, typically called from a Makefile target or an automation framework after each synthesis step.

Basic RTL-to-Gate Formality Script

## formality_rtl2gate.tcl
## Run: fm_shell -f formality_rtl2gate.tcl | tee formality.log

## ── 1. Set up the run ──────────────────────────────────────
set_svf ../synth/design.svf              ; # Synopsys Verification File from DC
set search_path [list ../rtl /libs/std_cell/db]

## ── 2. Read the golden (RTL) ───────────────────────────────
read_verilog -golden -sva {
  ../rtl/alu.sv
  ../rtl/ctrl.sv
  ../rtl/top.sv
}
set_top golden {r:/WORK/top}

## ── 3. Read the revised (netlist) ──────────────────────────
read_verilog -revised {
  ../synth/output/top_netlist.v
}
read_db -revised /libs/std_cell/saed14.db
set_top revised {i:/WORK/top}

## ── 4. Match and verify ─────────────────────────────────────
match
verify

## ── 5. Report ───────────────────────────────────────────────
report_passing_points  > reports/passing.rpt
report_failing_points  > reports/failing.rpt
report_aborted_points  > reports/aborted.rpt

if {[get_status] == "SUCCEEDED"} {
  puts "LEC CLEAN: All points verified"
} else {
  puts "LEC FAILED: See failing.rpt"
  exit 1
}

Key Formality Commands Reference

SVF (Synopsys Verification File)

When Design Compiler synthesizes the design, it generates an SVF file that records every name change, constant folding, and structural decision the tool made. Formality reads this file via set_svf and uses it to guide key point matching. Always use the SVF — without it, Formality falls back to purely name-based matching, which frequently fails on optimized netlists and produces spurious NE results.

6. Cadence Conformal Workflow

Cadence Conformal (also called Conformal LEC or LEC) is the primary alternative to Formality and is dominant at companies using the Cadence synthesis flow (Genus). The command language differs from Formality but the underlying concepts are identical.

Basic RTL-to-Gate Conformal Script

## conformal_rtl2gate.do
## Run: lec -dofile conformal_rtl2gate.do -xl -nogui | tee conformal.log

// ── 1. Read the golden (RTL) ────────────────────────────────
read design -golden -sv        \
  ../rtl/alu.sv                \
  ../rtl/ctrl.sv               \
  ../rtl/top.sv
set root module top -golden

// ── 2. Read the revised (netlist + libraries) ───────────────
read library -revised /libs/tsmc28/tsmc28.lib
read design -revised -verilog  \
  ../synth/output/top_netlist.v
set root module top -revised

// ── 3. Set functional mode (ignore scan) ────────────────────
add pin constraints 0 scan_en -both
add pin constraints 0 test_mode -both

// ── 4. Flatten hierarchy for matching ───────────────────────
set flatten model -both

// ── 5. Match and verify ─────────────────────────────────────
map key points
set system mode lec

// ── 6. Compare and report ───────────────────────────────────
add compare point -all
compare
report compare results -summary
report compare results -non_equivalent -file ne_points.rpt

Key Conformal Commands

7. Debugging Non-Equivalent Points

When Formality or Conformal reports NE points, the next step is to determine whether this is a true bug (the synthesis tool introduced a functional difference) or a false negative (a tool limitation, mapping error, or missing constraint that caused a false alarm).

Step 1 — Read the Counterexample

Every NE point comes with a counterexample: a set of input values for which golden and revised produce different outputs. This is not a simulation waveform — it is an algebraic witness generated by the SAT solver. In Formality use report_failing_points -verbose; in Conformal use report compare data -ne.

## Formality — examine an NE point interactively
start_gui                         ; # launch the Formality GUI

## Or from script:
set ne_pts [get_failing_points]
foreach pt $ne_pts {
  puts "NE point: $pt"
  report_failing_points -verbose $pt
  ; # shows counterexample input vector + expected/actual output
}

Step 2 — Classify the NE Point

Apply the following decision tree to each NE point:

1. Is the counterexample reachable? — If the input combination is physically impossible (e.g., requires two one-hot signals high simultaneously), the NE is a false negative. Add a constraint to exclude it: set_constant in Formality or add pin constraints in Conformal.
2. Is the key point mapping correct? — Run report_matching_points and verify that the register in the golden is matched to the logically correct register in the revised. A mis-match will cause all downstream cones to appear NE even when the design is correct. Use set_user_match (Formality) or add key point -mapping (Conformal) to correct the mapping.
3. Is there a missing SVF/ECO directive? — Some synthesis operations (e.g., constant propagation that eliminates logic) require the SVF to guide the tool. A missing or stale SVF can cause legitimate optimizations to appear as bugs.
4. Is this a true functional difference? — If the counterexample is reachable, the mapping is correct, and constraints are applied, the NE represents a real synthesis bug. File a CAR (Corrective Action Request) with the EDA vendor or adjust synthesis constraints to prevent the optimization.

Waivers and Sign-Off

Any NE or UNVERIFIED point that is accepted at sign-off must have a written waiver explaining:

• Why the point is not a functional concern (unreachable input, known tool limitation, intentional difference)
• What alternative verification was done to gain confidence (simulation, formal property check)
• Who approved the waiver (sign-off requires engineering manager + verification lead)

8. Common Non-Equivalence Causes

Experience across many ASIC projects reveals four recurring root causes of LEC failures. Understanding them helps you resolve NE points quickly and set up flows that avoid them in the first place.

1. Reset Handling Differences

RTL typically uses synchronous reset (reset applied only on the clock edge) or asynchronous reset (reset applied immediately, independent of the clock). Synthesis tools sometimes infer the wrong reset type, or the standard-cell library has flip-flops with only one type of reset that the tool maps to. If the golden RTL has always_ff @(posedge clk) if (rst) q <= 0; but the netlist uses a flip-flop with an asynchronous reset pin, Formality will see a functional difference because the reset sensitivity differs.

// RTL: synchronous reset — LEC golden
always_ff @(posedge clk) begin
  if (rst_n == 1'b0)
    q <= 8'h00;
  else
    q <= d;
end

// Formality workaround: constrain rst_n=1 to eliminate reset path from
// the functional comparison (verify only the data path)
set_constant r:/WORK/top/rst_n 1

2. Clock Gating (ICG Cells)

Power-aware synthesis inserts Integrated Clock Gating (ICG) cells. An ICG cell is a latch-based gate that generates a glitch-free gated clock. From the LEC tool's perspective, the ICG output is a new "clock" signal that was not present in the RTL — the registers driven by it have a different clock sensitivity in the netlist than in the RTL. Most tools have built-in ICG awareness: Formality's analyze_clocks and Conformal's set clock commands identify ICG cells and handle them correctly, but the tool must be told the ICG cell name so it can match the gating function.

3. Scan Insertion

DFT scan insertion replaces each regular flip-flop with a scan flip-flop that has an additional scan-in (SI) input and scan-enable (SE) input. In functional mode (SE=0), the flip-flop behaves identically to the original. LEC must be run with SE constrained to 0 to perform a functional-mode comparison. Failing to constrain SE will cause every scan flop to appear NE because the tool sees an extra input that doesn't exist in the RTL.

## Formality: constrain scan_enable=0 for functional LEC
set_constant i:/WORK/top/scan_en 0

## Conformal: same effect
add pin constraints 0 scan_en -revised

4. Register Retiming

When the synthesis tool applies retiming to balance pipeline stages, it physically moves flip-flops across combinational logic. The number of registers may change, register names change, and the functional behavior at any single cycle boundary changes — even though the end-to-end latency and throughput of the pipeline are preserved. Combinational LEC will report massive NE because it cannot establish register mapping. The solution is to either disable retiming for blocks that must pass combinational LEC, or run sequential LEC on those blocks. Most teams disable retiming by default and enable it selectively with set_dont_retime constraints.

FAQ