Equivalence Checking: Proving a Netlist Matches Its RTL

Simulation shows that two designs agree on the vectors that were applied. Equivalence checking shows that they agree on every vector, by asking whether a circuit built from both of them can ever produce a difference. The construction is small: wire the two designs to the same inputs, compare each pair of corresponding outputs with an exclusive-OR, and ask whether any XOR can be 1. If the answer is unsatisfiable, the designs are equivalent; if it is satisfiable, the satisfying assignment is a counterexample, and it is a concrete input vector that the designer can replay.

That reduction is exact and it is the entire theory. What makes equivalence checking practical or impractical is everything around it: whether the two designs have corresponding state elements at all, how the satisfiability question is solved, and whether the tool can be given enough structure to avoid solving a problem that is exponentially hard in the worst case.

The miter and why it is satisfiable in the wrong direction

The circuit formed by joining the two designs at their inputs and XORing corresponding outputs is called a miter. Its satisfiability question is: does there exist an input assignment making any output pair differ? Unsatisfiable means equivalent.

The asymmetry of the answer matters. A satisfiable miter proves non-equivalence, and the proof is constructive: the solver’s assignment is a counterexample, and a counterexample is checkable by simulation in one run. An unsatisfiable miter proves equivalence, and the proof is a refutation with no witness: there is nothing to replay, only a claim that the search space was exhausted. This is why a tool that says “equivalent” is trusted only as far as its solver is trusted, and why a standard sanity check is to test the checker: run the tool on a deliberately modified netlist and confirm it reports non-equivalence and produces the expected counterexample.

The miter also has a structural problem that makes it harder than either design alone. Both copies share inputs, so the two cones of logic are correlated in ways neither is correlated with itself, and the solver must reason about that correlation. Naive SAT solving on a miter of two large optimized netlists can blow up even when the designs are equivalent, which is why structural methods are applied first.

Structural matching does most of the work

Before any solver runs, the tool compares the two netlists structurally. If a node in one netlist has the same function as a node in the other (same gate type with inputs that have already been matched, or a wire that is literally the same net after name preservation), the two are recorded as equivalent and the comparison propagates forward.

This works because synthesis preserves a great deal of structure even through optimization. A gate that survived from the RTL keeps its inputs; an inverter inserted for drive strength has a name that identifies it; a buffer tree is a tree of buffers. Tools exploit name preservation, which is why RTL flows keep register and instance names through the synthesis step rather than letting the tool rename everything.

Where structural matching fails, functional matching takes over: two nodes are proven equivalent by satisfiability of a small local miter over their input cones, bounded in depth. If the two nodes’ functions match, the tool records the equivalence and continues. This is the same technique described in technology mapping for boolean matching, applied in the other direction: mapping asks which library cell implements a function, equivalence checking asks whether two implementations compute the same function.

Only the residual differences, those nodes that neither structural nor local functional matching could pair, go to the full miter and the SAT solver. In a well-behaved flow that set is small, which is the reason equivalence checking of a synthesized netlist is routine while the general problem is intractable.

Registers, and why the comparison is combinational

The comparison above assumes the two designs have corresponding registers in corresponding positions. In that case the tool treats each pair of registers as a shared primary input, compares the next-state functions and the outputs combinationally, and the induction is implicit: if the registers hold equal values in some cycle and the next-state functions are equal, they hold equal values in the next cycle too. This is combinational equivalence checking, and it is what runs between RTL and a netlist that was optimized without moving state.

The assumption is exactly what register retiming violates. Retiming moves registers across logic, duplicates them at fanout, and merges them where it can. After that step there is no register-to-register correspondence: one RTL register may correspond to three netlist registers, and the tool’s state mapping is undefined. The same is true of any transformation that changes the number of cycles a value takes to propagate, including resource sharing, which time-multiplexes one arithmetic unit across several operations and therefore changes latency.

For those cases the tool needs sequential equivalence checking, which proves that two circuits produce the same output sequence for the same input sequence from a common initial state. The general problem is much harder than the combinational one, because it requires reasoning about reachable states rather than about one combinational function, and in practice it is handled by either of two compromises: prove equivalence only for a bounded number of cycles from a reset state, or require that the two designs’ state sets are related by a function the tool can discover. Both are weaker than the combinational proof, and both are the reason retiming is often the last transformation applied and is trusted rather than re-proven.

The cost structure of the satisfiability problem

Modern solvers are conflict-driven clause-learning SAT solvers, or their word-level cousins that reason about bit-vectors and arrays directly. A miter is translated into clauses: each gate becomes a small clause set relating its output to its inputs, each pair of corresponding outputs feeds an XOR whose output is 1 exactly when the pair differs, and the solver is asked whether the OR of those XORs can be 1 while all the gate clauses hold.

The cost is dominated by the size of the search, not the size of the formula, and the search is sensitive to structure the translation destroys. Two designs that differ only in the association order of a wide AND, or in the order of bits within a word, produce miters whose clauses are easy to satisfy but whose equivalence proof requires the solver to discover the association and bit-order relations. Word-level solvers help precisely here, because a bit-vector addition is one constraint rather than a ripple-carry chain of clauses.

Three techniques make the difference between a proof in seconds and no proof at all.

Cut points. The tool picks internal nodes in one netlist and asserts them as additional constraints, splitting the miter into smaller sub-problems. A cut point that is functionally equal in both designs turns one large proof into several small ones. Choosing cut points badly can make the problem harder, so the choice is heuristic and iterated.

Constraints and don’t-cares. Synthesis exploits don’t-care conditions from the environment: an input combination that never occurs, a state that is unreachable. Those optimizations produce netlists that are not equivalent to the RTL as combinational functions, only under the constraints that justify them. The tool must be given the same constraints, or it will report a difference that is real in the miter and irrelevant in the system. This is the equivalence-checking version of the false-path problem in static timing analysis, and the failure mode is symmetric: a missing constraint produces a spurious counterexample, and an unjustified constraint produces a false proof.

Abstraction and case splitting. Registers whose values are known to be constant in a mode, or wide datapaths where only some bits matter, can be abstracted before the proof and refined if the abstraction turns out to be too coarse. This is where equivalence checking becomes an engineering activity rather than a solver invocation.

Where the boundary of trust sits

A typical flow runs equivalence checking at several points: after each synthesis step that preserves state correspondence, after technology mapping, and after any step the flow considers risky. The checks that are skipped are a decision about which transformations are trusted, and the decision has a cost that shows up later: a bug introduced by a transformation that was never checked appears as a functional failure in silicon with no obvious cause, because the RTL was simulated and the netlist was not.

The checks that are run are only as good as their constraints. A proof that a netlist is equivalent to its RTL under a set of assumptions proves exactly that, and the assumptions are usually supplied by the same person who wrote the RTL. The gap between “equivalent under the constraints” and “implements the intended function” is not closed by any tool; it is closed by simulation and by review of the constraints themselves.

There is also a scale limit that is worth stating plainly. Combinational equivalence of two large designs with extensive arithmetic optimization can exceed the resources of any solver, and the standard response is to partition the design at register boundaries and prove the partitions separately. When a partition cannot be proven, the tool reports it as inconclusive, which is not the same as failing: inconclusive means the search was abandoned, and the design may be perfectly correct. The distinction matters for how the result is recorded, and conflating the two is how a real difference gets filed as a tool limitation.