L2/04 — Equivalence by certificate

Background

The question "do these two circuits compute the same function?" — combinational equivalence checking, CEC — is the workhorse problem of hardware verification, and this chapter leans on thirty years of its technology, so the technology needs introducing. The foundation is the SAT solver: a program that takes a Boolean formula and either finds an assignment making it true or reports that none exists. SAT is the canonical intractable problem in theory, but modern solvers (the architecture is called CDCL — conflict-driven clause learning: search, hit a contradiction, learn a clause recording why, never repeat that mistake) routinely dispatch industrial instances with millions of variables. Equivalence reduces to SAT by the miter construction: wire the two circuits to the same inputs, XOR their outputs, and ask the solver whether the XOR can ever output 1. "Unsatisfiable" means no distinguishing input exists — the circuits are equivalent.

Two refinements turn this from possible into practical. First, equivalence tools do not attack the miter whole; they exploit the fact that the two circuits being compared are usually versions of the same design, littered with internal wires that compute identical functions. SAT sweeping finds them: simulate both circuits on random inputs, group internal nodes whose simulated values always agree (candidates), prove each candidate pair equivalent with a small local SAT call, and merge them — so the two circuits progressively fuse from the inputs forward, and no solver call is ever large. (The circuits are held in a normal form called an AIG — and-inverter graph, everything expressed as two-input ANDs plus inverters — which makes structural sharing cheap and mergers mechanical.) The crucial corollary runs backwards: sweeping starves without structural similarity, which is why this chapter insists the right comparand is the RTL that generated the netlist, never an independently written reference model.

Second — and this is the book's recurring trust move, stated here at its origin — a solver's "unsatisfiable" verdict need not be taken on faith. Solvers can emit a proof log (the standard formats are DRAT and its checkable-in-linear-time refinement LRAT): a step-by-step derivation of the contradiction that a small, simple, independently verified checker can replay. The solver stays a wild, heuristic, untrusted search engine; trust resides only in the checker. This search-vs-certificate split is how every SAT-shaped result in the project enters the proof, and this chapter pushes the same idea one level further: the synthesis optimiser's own rewrites are drawn from a finite, pre-verifiable library (the "222 NPN classes" below are the 4-input Boolean functions up to negating/permuting inputs and negating output — a complete catalogue), so if the tool is patched to log which rewrite it applied where, the entire optimisation trail becomes a checkable certificate and search at verification time disappears.

Statement

Given ρ (03) and the deletions (02): for every register/port boundary pair, the combinational cone in the reduced netlist computes the same function as the corresponding cone in the elaborated RTL — established by checking certificates, with exploratory SAT confined to where no certificate exists.

Per-cone equivalence + ρ + matched reset then compose into the bisimulation Mealy(N) ≈ρ ⟦RTL⟧.

Why CEC scales, and why that dictates the architecture

SAT sweeping works by proposing candidate-equivalent internal nodes via random simulation and proving each with a small local SAT call, using previously proven equivalences as rewrites. The candidates exist because both sides are the same design through one tool — structural similarity is the fuel. Two consequences:

• An independent reference model is the wrong architecture. Comparing a hand-written model against a synthesised netlist destroys the internal equivalence points; the miter becomes one enormous SAT problem. (This is quite apart from the register-mapping problem an independent model creates.) The RTL that generated the netlist is the right comparand.
• Register boundaries bound every miter. With ρ in hand, each proof obligation is one cone — an in-order core's are shallow — so even certificate-free fallback SAT stays tractable per cone.

Unmap rather than map: substitute each SKY130 cell's verified Boolean function (L1/06) to bring the hardened netlist down to generic gates, instead of technology-mapping the RTL side up. Free — L0 already produced the functions — and it removes tech mapping from the comparison entirely.

The certificate architecture: instrument ABC's trail

ABC's optimisations are local rewrites drawn from a finite precomputed library — the 222 NPN classes of 4-input functions for rewrite, plus refactor/balance/resub. Every application is a table lookup plus a structural substitution; the justification already exists as a table entry — ABC just doesn't write it down.

The plan, enabled by 03's reproduction of the flow (we control the run, so we can patch the tool):

1. Verify the NPN library once, exhaustively — 222 lemmas over 4-input functions, trivially checkable.
2. Log the trail: (cut, before, after, library-entry) per rewrite — a modest patch to an open-source tool.
3. Check the trail: each step is congruence (substitution at a cut, pointer-level if the representation is a hash-consed AIG (And-Inverter Graph — the two-input-AND-plus-inverter normal form equivalence tools operate on)) plus one library lemma. No search at check time.
4. Residual cones — anything the trail doesn't cover as a pure library rewrite: proc/techmap structural expansion, and ABC's mfs, the flow's only don't-care-licensed pass (measured below). For mfs the trail records each resubstitution with its don't-care condition, discharged by checking that condition or by a windowed SAT-with-DC-assumption; other residue falls back to per-cone SAT with LRAT proofs, checked not trusted.

This is the K(G₁) = K(G₂) congruence architecture the project sketched from the start, landing at its cheapest available site: local rewrites, precomputed justifications, open tool. It is the best available answer to avoid poorly-specified exploratory obligations.

Measured: the don't-care footprint of this flow

The certificate architecture above splits every synthesis rewrite into two bins: exact (a full-input-space Boolean identity over a bounded cut — certifiable locally, by composition, against the finite rewrite library) and don't-care-licensed (the rewritten cut equals the original only on the inputs that can occur (satisfiability DCs) or that are observed (observability DCs) — not certifiable by local pin-projection, because the licensing condition is a non-local property of the surrounding circuit). Only the second bin is the hard residue. So the operational question is: how big is it, on this design? We instrumented the flow and measured it.

The flow's ABC script, classified. The synthesis step hands ABC a script (runs/*/06-yosys-synthesis/AREA_0.abc) of eighteen passes. Every one is exact-equivalence except a single don't-care pass:

• exact — fx (algebraic factoring), strash (structural hashing), drw/drf (rewrite/refactor from the 222-NPN 4-input library), balance (associativity), the fraig_store/fraig_restore sweep (SAT-proven node merges), amap and &nf (technology covering — implement the AIG function by construction), &dch (structural choices — invoked bare, so proven-equivalent snapshots only, no don't-care merge), buffer/upsize/dnsize (function-preserving sizing);
• structural no-ops — retime -M 5, scleanup, and the sequential &get -n path. Yosys runs dfflibmap before ABC, so ABC receives a purely combinational network: its own stats report lat = 0. There are no latches to retime. Flop boundaries — ρ — are fixed before ABC touches anything; the flow performs no retiming at all. This is not a configuration we chose; it is visible in the log (ABC: Error: The network is combinational when retime runs) and it removes register-level non-locality from the problem entirely.
• don't-care-licensed — mfs (and only mfs): SAT-based resubstitution and redundancy removal using satisfiability and observability don't-cares. This is the whole of bin two.

So the design-wide don't-care residue is exactly one pass, and mfs reports its own footprint. Instrumenting it (cec/dc-instrument.sh, cec/dc-fullchip.sh — the flow's script with mfs -v, run pass-by-pass) gives:

Two things fall out. First, the footprint is small and self-reported: mfs names the exact nodes it changed, so the certificate does not have to discover the don't-care residue — the tool hands it over. Every node mfs did not touch is reached by exact rewrites alone and certifies locally.

Second, the genuinely non-local part is almost nothing. mfs's -W flag is the observability (transitive-fanout) cone depth; -W 0 leaves only satisfiability don't-cares, which are a property of a node's fan-in — still non-local, but input-side and bounded by the cone the local cut already sees. Re-running the whole flow with -W 0 reduces the full chip by 4,241 nodes versus 4,249 with observability on: the observability don't-cares — the ones whose licensing truly depends on what the rest of the circuit ignores, and which no enlargement of the local window can ever capture — account for 8 nodes in the entire design. The full 8% is satisfiability-DC. AMOALU shows the same (-W 0 identical, all 28 resubs satisfiability-based). IBuf looks larger (~10 nodes, ~0.8pp) precisely because it is carved out: a module observed only at its boundary has artificial observability don't-cares that vanish once it is wired into the closed chip — the same free-boundary effect as the IBuf reset residual in the Executed runs below, and the reason the honest number is the full-chip one. Observability don't-cares and unobserved boundary state are the same phenomenon seen from two sides, and in the closed design there is almost none of it.

Consequence for the certificate. The trail checker discharges every exact pass locally. For mfs, the trail records each resubstitution with its don't-care condition; the checker either verifies that condition or falls the cut back to a windowed SAT-with-DC-assumption. The measurement says that fallback is invoked on ~8% of nodes — and of those, all but a handful carry a satisfiability condition (which input patterns reach the cut: a bounded fan-in property the windowed check already has in scope), while the observability-dependent part, the only kind that resists any local window whatsoever, is 8 nodes in 52,775. The die-wide CEC does not merely factor into local checks in principle; on this design the non-local remainder is one instrumented pass, over 99.9% of it input-side and windowable, with a hard core of eight nodes.

Executed: re-checking mfs's don't-care SAT calls outside ABC

The measurement says the don't-care residue is one pass and it names its own footprint. The next step is to make that pass hand over the proof obligation it discharged, and re-check it without trusting ABC. We patched ABC to do exactly this (cec/abc-mfs-dclog.patch, ~50 lines; cec/DC-CERT-NOTES.md).

To license each reduction, mfs builds a two-copy care-aware miter (Abc_MfsCreateSolverResub): two copies of the window, tied on the candidate divisors, with the node's output forced to disagree. UNSAT means no two care-set inputs agree on the divisors yet differ on the node — the node is determined by those divisors on the care set — so the reduction is valid; ABC then reads the replacement function off that same refutation by Craig interpolation. The refutation is the certificate. The patch, gated by an environment variable, dumps the complete CNF of that miter (assumptions baked in as unit clauses) for every applied reduction, plus a manifest tying each to its node and window support. An off-the-shelf solver re-deriving UNSAT removes ABC's SAT engine from the trust base for the whole don't-care step.

Run through the flow via abc -exe, then discharged by minisat and z3 (cec/dc-log.sh, cec/dc-check.py):

Coverage is exact at every scale: the dumped remove/replace counts equal mfs's own Remove/Resub accounting to the unit — IBuf 206/174, and the whole chip 2,917/3,255 — so all 2,917 observability-based removes, the genuinely non-local reductions, are among them. Every don't-care SAT call the flow made is reproduced by a solver outside ABC, and every one is UNSAT (a SAT here would be an ABC soundness bug; none occurred).

This discharges the "re-do the don't-care SAT calls" obligation. Two layers remain, and the manifest is built to reach them: emitting a DRAT/LRAT proof from the external solver upgrades each verdict to a checked proof; and mapping the dumped window variables back to netlist nets (the manifest records the support net ids) closes the "faithful window" obligation — that the dumped miter models the real netlist's don't-cares — against 00's semantics. What is already true is the sharp part: the die-wide don't-care residue is one pass, its every reduction is logged as a bounded local refutation, and those refutations check outside the tool that produced them.

The exact passes: per-pass equivalence, checked outside ABC

mfs is the only pass that needs a don't-care argument; every other pass in the script — fx, strash, the rewrite/refactor/balance block, the fraig sweep, amap, &dch/&nf — preserves the function on all inputs, so each is a plain equivalence with no care set. That invites the obvious check: verify each pass against the one before it.

Why per-pass rather than one shot: the monolithic RTL≡netlist miter is exactly the compute-bound object from the runs above — the two sides are dozens of passes apart, structurally dissimilar, so SAT sweeping starves. Consecutive networks are one pass apart and nearly identical, so the same sweeping collapses each adjacent miter in milliseconds. Snapshotting the network after every pass and checking neighbors turns the one hard CEC into a chain of trivial ones — precisely the "trail of intermediate netlists" the certificate architecture calls for, at its cheapest.

cec/trail-cec.sh does this: it snapshots after each pass (&get -n for uniform signal names; s0 via non-destructive write_blif, since fx needs an SOP network), exports each adjacent miter (miter -c, whose single output can be 1 exactly when the two circuits differ), and discharges it with minisat — outside ABC — keeping ABC's own cec as a cross-check. The polarity is falsification-tested (an AND-vs-OR miter yields SAT), so a false "equivalent" cannot pass.

For AMOALU and IBuf, every boundary is independently UNSAT and ABC's cec agrees:

s0_start -> s1_fx      : UNSAT (equivalent)   | abc: are equivalent
s1_fx    -> s2_mfs     : UNSAT (equivalent)   | abc: are equivalent
s2_mfs   -> s3_strash  : UNSAT (equivalent)   | abc: are equivalent
s3_strash-> s4_rewrite : UNSAT (equivalent)   | abc: are equivalent
s4_rewrite->s5_fraig   : UNSAT (equivalent)   | abc: are equivalent
s5_fraig -> s6_amap    : UNSAT (equivalent)   | abc: are equivalent
s6_amap  -> s7_nf      : UNSAT (equivalent)   | abc: are equivalent

For the whole ChipTop, all seven boundaries are equivalent too, each in 0.06–64 s (~3.3 min total) — tractable exactly where the monolithic RTL≡netlist miter is not. The chain composes: s0 ≡ s1 ≡ … ≡ s7, so the pre-ABC network equals the final mapped netlist. The mfs boundary (s1→s2) passes this whole-network check too — it is output-preserving — while its internal don't-care reductions get the finer, per-reduction certificate of the previous section.

One honest scaling seam. On the modules the external solver discharges each boundary; on the full chip the boundaries are checked by ABC's own cec, because a plain external solver does not scale on the raw die-wide miter — minisat exceeds two minutes on a 69k-variable boundary, for want of the structural node-sharing that cec's fraig sweeping supplies and a bare CNF discards. So at full-chip scale this step still trusts ABC's checker (not its optimiser). Closing that — a structure-aware CEC that emits a DRAT/LRAT proof a small checker can replay — is the remaining hardening; the decomposition has already done the hard part, cutting the die-wide problem into seven individually-tractable steps.

So the ABC trajectory is covered end to end: the exact passes by adjacent-miter equivalence (external on modules, ABC-cec in minutes on the die), and the one don't-care pass by both this whole-network check and its 6,172 externally-replayed SAT refutations. What remains is the front end — s0 back to the RTL (proc/techmap structural expansion, the "naive netlist" of the next section) and, above it, L3's elaboration semantics. The ABC middle — historically the heuristic, untrusted part — is now a chain of small equivalence checks anyone can replay.

The naive netlist: useful oracle, wrong comparand

read_verilog; hierarchy; proc; memory_map; techmap — no opt, no abc — produces a "naive" netlist whose function is fixed by the language and whose structure is fixed by Yosys's techmap.v, a small readable rule library one could formalise. Caveats: proc is not a no-op (proc_rmdead prunes unreachable branches), and well-definedness is conditional on L3's 15 always @* latch-inference checks — the obligation is shared between layers.

But as a CEC comparand it is the worst case: its ripple-carry adders share nothing structurally with ABC's output, so sweeping starves. Its role is differential testing and semantics cross-validation (L3's CEC cross-check), not the equivalence proof itself. The trail architecture makes this moot: with the trail, the comparand is each intermediate netlist against the next, and structural similarity is maximal at every step.

Executed: the equivalence check as run

Ahead of the instrumented-trail endgame, the equivalence was run with off-the-shelf machinery (eqy and yosys equiv_*), matching by name via ρ (03) with no hint file, to find out what the obligation actually costs on this design. Three results, one coherent picture.

A cone closes cleanly. AMOALU — the atomic-memory-op ALU, a purely combinational Rocket cone — synthesised standalone to SKY130 cells and checked against its RTL yields Equivalence successfully proven, all 32 output bits. The whole pipeline runs end to end: slang elaboration → standalone synthesis → cells read against Liberty → equiv_make name-match → SAT → proven. This is scoped-cec in check-l3, and it is the proof that the pipeline itself is sound — no confound, a real PASS on real Rocket logic.

A sequential cone exposes the reset issue, not a bug. IBuf (instruction buffer, 53 flops) matched every flop by Q-net and proved 198 of 212 cones on the first pass. The residual is not a logic discrepancy: 115 of the unproven cells are primary outputs driven by the unreset data registers buf_pc/buf_data, whose two copies start at independent free values, so every output that reads them differs at cycle 0. A carved-out module observed at its boundary from an arbitrary state genuinely is not output-equivalent; the correct statement is equivalence under matched initial register state — ρ as an assumed initial condition, standard SEC practice — which needs the reset sequence modelled. The matching (F5) is untouched; what is open is a clean whole-module sequential verdict.

The whole chip confirms matching but not a clean verdict — by either route. eqy's per-flop partitioning matched ~10,900 cones by name (ρ at full scale) but its serial combine is a multi-hour grind. The yosys-native single-miter route (equiv_make/equiv_simple/equiv_induct) matched 642 cones by name, but equiv_simple proved only 6 of them — the same free-register-init wall as IBuf, dominating even the combinational check when the whole design's registers start free — and equiv_induct exhausted memory without closing. So a clean full-chip number needs either the per-partition route run to completion (compute) or reset-sequence modelling (the IBuf lesson at scale). The scoped AMOALU pass remains the standing evidence the pipeline is correct; the full-chip verdict is cec-fullchip, still open, and blocked on compute/reset-modelling rather than on any doubt about the method.

The lesson for the architecture below: matched-reset (the ## Statement's hypothesis, and 03's reset-correspondence clause) is not a formality — it is exactly what these runs show is needed to turn per-cone combinational equivalence into a whole-design verdict. The certificate route inherits the same requirement; the trail proves the cones, and the reset correspondence composes them.

Obligations

1. The NPN library verification (one-time, mechanical).
2. The ABC patch and trail format; the trail checker against 00's semantics.
3. The composition theorem: per-cone equivalences + ρ + reset correspondence ⟹ bisimulation.
4. LRAT checking for residual cones — standard machinery, imported not built.

Interface (trust anchor). The soundness of these certificates is the S-miter seam (miterCNF_sound): that the miter CNF faithfully encodes inequivalence, so a refutation proves the machines equal. It is the one seam that is not an inter-layer arrow but a trust anchor — every PassCert and l2_commutes rest on it — and the one dischargeable outright: a verified Tseitin encoding turns it from axiom into theorem.

Effort

The patch and checker: months. The composition theorem: weeks once 00/03 exist. The certificate route's cost scales with the trail length, not the design size — which is the point.