Formal Equivalence in ASIC Signoff

Why Formal Equivalence Belongs in Signoff

ASIC signoff is a claim that the design taped out behaves exactly as intended. Simulation alone cannot fully back that claim, because even a large regression suite covers only the states its testbench happens to reach. Formal equivalence checking makes a much stronger statement: given two representations of the design, it mathematically proves that every reachable state produces identical behavior.

That proof is what allows teams to move between design stages, such as RTL to gate level or gate level to engineering change order revisions, without re-running exhaustive simulation. When equivalence checking is part of the signoff checklist, every transformation that could silently corrupt functionality is covered by an exhaustive, tool-generated proof rather than by sampling. This is also why signoff reviews routinely ask for a clean equivalence report alongside timing and physical checks.

What Equivalence Checking Proves

A logic equivalence checker compares a golden model, usually the RTL, against a revised model, usually the synthesized netlist. It builds internal decision procedures that reason about the Boolean function of every output and every state element. If the functions match, the tool proves equivalence and reports each compare point as verified. Compare points typically include primary outputs, register inputs, and floating outputs that the flow deliberately excludes.

The result is a per-point proof, not a statistical confidence level. This distinction matters during signoff because reviewers can trace every output of the revised design back to a proven match. It also matters for audits: a clean equivalence log demonstrates that no logic change between two checkpoints altered observable behavior, which is exactly the guarantee that formal methods were designed to provide.

Combinational Versus Sequential Equivalence

Most signoff flows rely on combinational equivalence checking. The tool maps registers one to one between the golden and revised models and then proves that the combinational logic driving each corresponding pair of registers and outputs is identical. This approach is fast and scales to very large netlists, but it depends on the register correspondence being valid. Sequential equivalence checking drops that assumption and reasons about the state machines themselves.

It is the right choice when retiming, register merging, or architectural changes move state around, because it proves behavior equivalent without requiring matched registers. Teams usually reserve sequential checking for the cases where combinational mapping fails or for design steps known to restructure state, keeping the standard flow fast and deterministic for routine iterations.

Setting Up Signoff-Quality Comparison Points

The quality of an equivalence run is decided long before the proof starts, during setup. Key compare points must be declared: primary inputs and outputs, cut points through large combinational cones, and any manually specified mapping where automatic matching would be ambiguous. Scan chains, test logic, and clock domain structures need explicit handling so that design-for-test insertion does not create false mismatches.

Undriven inputs, tie cells, and constant propagation settings must match the intent of the synthesis flow. A disciplined flow stores this setup in version-controlled configuration files that travel with the design, so every run from the same checkpoint uses identical assumptions. When setup is reproducible, a reported non-equivalent point reflects a real logic difference rather than a difference in tool assumptions between runs.

Handling Clock Gating and Optimizations

Modern synthesis applies clock gating, register replication, and logic restructuring that can confuse naive comparison. Clock gating cells replace the direct clock connection to a register, so the checker must recognize the gating function as preserving the register's enabled behavior. Register replication means one golden register now corresponds to several revised copies, and the tool must expand the mapping accordingly.

Datapath optimizations may restructure arithmetic into different but functionally equal trees. Well-configured equivalence tools absorb these transformations automatically, but every absorbed transformation is a place where configuration errors can hide. Signoff practice is to review the mapping summary, not just the final pass or fail line, so that an unexpectedly low compare point count is investigated instead of celebrated.

Debugging Non-Equivalent Points

When the checker reports a non-equivalent compare point, the deliverable is not just the failing point but a counter-example: an input sequence under which the two models diverge. Teams use that trace in the simulator to reproduce the mismatch on the RTL and the netlist simultaneously, which turns an abstract proof failure into a familiar waveform debug session. The first triage questions are structural.

Did the mapping match the intended registers? Was a cut point placed that hides the divergence? Did an engineering change order update one model and not the other? Experience shows that a large fraction of reported mismatches trace to setup, constraint, or stale-model issues rather than genuine synthesis bugs, so systematic triage pays for itself quickly.

Running Equivalence Checks Across Design Stages

Equivalence checking earns its place in signoff by running at every stage where logic could change. After initial synthesis, it proves the netlist faithful to the RTL. After each engineering change order, it proves the edit did what the author intended and nothing else. After low-power insertion, it proves that power gating and isolation cells preserve functional behavior in the active state.

After test logic insertion, it proves the functional mode is untouched. Each run is cheap relative to re-simulating the affected area, and the accumulated chain of clean proofs documents an unbroken functional argument from source RTL to the final netlist. Signoff auditors value exactly that chain, because it closes the gap that simulation coverage reports leave open.

Integrating Formal with Timing and Physical Signoff

Equivalence checking does not stand alone. It verifies logical function, while static timing analysis verifies that the proven logic meets timing across corners and modes, and physical verification confirms the layout implements the proven netlist. A signoff package is strongest when these three lines of evidence reference the same netlist checkpoint, so there is no ambiguity about which version was proven, timed, and checked.

Teams that tie equivalence runs to specific netlist revisions in version control can reconstruct, months later, exactly which logical proof guarded a given tapeout. This traceability is increasingly important as design teams grow and responsibility for a netlist passes through several hands between synthesis and tapeout.

Building a Repeatable Equivalence Flow

A reliable equivalence flow is automated, versioned, and boring in the best sense. Scripts drive the tool with fixed setup files, publish structured reports, and archive proof results alongside the netlist revision. Every run records the tool version, the setup hash, and the compare point summary, so a later reviewer can reproduce the proof exactly. Failures block the flow from advancing the design state, which keeps a broken netlist from silently reaching timing or physical signoff.

Teams should also run periodic regression checks of the equivalence flow itself, using known-good and deliberately broken checkpoints, to confirm the setup still detects real mismatches. A proof flow that has never been tested against a known failure is not yet signoff grade.

Common Pitfalls and How to Avoid Them

Several pitfalls recur in equivalence-based signoff. Treating a pass with an unexplained drop in compare point count as clean can hide compare points that were never verified. Allowing ad hoc, per-user setup files breaks reproducibility and makes mismatches unreproducible. Ignoring unused or dangling logic can leave real behavior outside the proof envelope. Running equivalence only at the end of the flow, instead of after every logic-affecting step, converts small, easy debug sessions into one large and painful one.

Finally, skipping the archived proof report saves a little disk and loses the audit trail. Each pitfall is avoidable with disciplined setup control, staged runs, and archived evidence, and each avoidance directly strengthens the final signoff claim.