L2 — Netlist ↔ RTL equivalence

Node — the synchronous machine: flops plus combinational logic over a Boolean vector, Mealy(N) (00), well-defined only under the standing well-formedness hypothesis that survives the digital crossing (01). Edge up — the CEC (a horizontal equivalence, not an abstraction step): Mealy(N) ≈ρ ⟦RTL⟧ — the netlist machine equals the RTL machine under a register correspondence ρ, via licensed deletions (02), ρ (03), the equivalence certificates (04), and the hard cones (05). Note the proof-order inversion: this edge consumes L3's object ⟦RTL⟧, so it is proved after L3 despite sitting below it in the tower — numbering is artifact altitude, not logical dependency. (The book's top-down reading order happens to agree: L3's chapters precede these.)

Background

Synthesis compiled the emitted RTL into the netlist the flow hardens: 51,359 standard-cell instances (drawn from 96 cell types) with mangled names and aggressively restructured logic, growing further in place-and-route as clock trees, hold buffers, and physical cells are inserted. This layer proves the compilation preserved meaning — not by trusting the tool, but by checking certificates the tool's run can be made to emit. The route: define the netlist's semantics (00), check it is electrically sane (01), delete the instances that compute nothing under explicitly licensed theorems (02), extract the register correspondence from the flow's own run (03), and prove per-register-boundary equivalence by certificate, with exploratory SAT confined to where no certificate exists (04, 05).

Statement

There is a register correspondence ρ — a bijection between RTL state elements and netlist flops, up to opt_dff-eliminated constants and resizer cloning (its existence is exactly F5) — such that, after the three licensed deletions,

Mealy(N) / (delete PHYSICAL · collapse clock to the global tick · collapse buffers)
    is bisimilar under ρ to   ⟦RTL⟧,   from matched reset states.

Established by certificates, with exploratory SAT confined to where no certificate exists. The N here is the shared object of the overview's tower: one parse of ChipTop.mapped.v (and its post-P&R successor) serves L1's LVS target, L1's STA subject, and this theorem's left-hand side.

Subcomponents

Interfaces

Consumes: the hardened netlist, RTL, ⟦·⟧ (L3), the synthesis flow, per-cell Boolean functions (L0). Exports: to L1, N with identified registers/clock/reset; to L3, the licence to reason about ⟦RTL⟧ instead of the netlist.

Axioms introduced

None surviving. S1 (netlist semantics) is derived — per-cell Boolean shadows (L1/06) + the bridge theorem (M5) + LVS (L1) yield it as a conclusion (00) — and X1 (parser fidelity) is an ordinary verified-parser obligation; both are in Axioms' Discharged table. F5 (does ρ exist?) is the layer's load-bearing unknown, decidable by 03's experiment.

The layer's shape

Everything reduces to the register boundary. Only ports and state elements need correspondence — internal restructuring is exactly what CEC absorbs — so the RTL-to-netlist gap is the question "do the flops correspond?" (F5), and every other file supports answering or exploiting it: 00–01 make the two sides comparable objects, 02 shrinks the problem 13×, 04 checks the cones between corresponded registers, 05 handles the cones where checking needs a different calculus. The methodological corollary: never reconstruct word structure from bits — words live on the RTL side of ρ; and never compare against an independently-written model — structural similarity is what makes any of this tractable.

The proof, structured

Take one tiny sequential circuit — a flop q whose next value is ¬((a·b)+c) — and follow that object down through the layers: a behavioural expression, then a cell netlist, then transistors.

Definitions.

• R, I, O — the RTL register bits, input bits, output bits.
• ⟦RTL⟧ (from L3) — a Mealy machine on states 𝔹^R: a next-state function δ_r : 𝔹^R × 𝔹^I → 𝔹 for each r ∈ R, and output functions λ_o.
• N — the hardened netlist; F its flip-flops. Each cell instance denotes a Boolean function, its Liberty entry.
• N_f : 𝔹^F × 𝔹^I → 𝔹 — the function of flop f’s combinational fan-in cone (cell functions composed along the nets). These define Mealy(N).
• ρ : R → F — a bijection; ρ(r) is the flop holding bit r. For a netlist state s ∈ 𝔹^F, s∘ρ ∈ 𝔹^R is the RTL state read off the flops.
• s0, …, s7 — the intermediate networks at the boundaries of the synthesis (ABC) script, the eight snapshots cec/trail-cec.sh records. Flops are mapped (dfflibmap) before ABC, so every s_k is a combinational network over the same flop boundary F — this is the no-retiming fact. s0 = the front-end output (proc/flatten/memory/opt/techmap); then s1 after fx, s2 after mfs, s3 after strash, s4 after the rewrite/refactor/balance block, s5 after the fraig sweep, s6 after amap, s7 after &dch/&nf. Each s_k thus defines a cone function per flop; s_k ≡ s_{k+1} means these agree for every flop.

Goal. for every r ∈ R (write f = ρ(r)) and all (s, i) ∈ 𝔹^F × 𝔹^I: N_f(s, i) = δ_r(s∘ρ, i) (and N_o = λ_o under ρ, for outputs). A combinational identity — the one-step ρ-commutation; the lift to trace equivalence is L3’s (foot of proof).

Each leaf (▸) is a tool run whose output is a certificate we can independently check, or a checker we assert correct. Status: ● holds · ◐ partial · ○ open.

Proof.

• 1. Mealy(N) is well-defined — each N_f is total. ◐
  • 1.1 · 00 each cell denotes its Liberty function (this fixes the cone composition; call it S1). ▸ celltopo derives each library master’s function from its transistor switch-network and asserts equality to Liberty; the derivation is the certificate (the conducting-path formula), independently checkable. ● 311/437 masters · ○ flops, tristate.
  • 1.2 · 01 N’s combinational graph is acyclic and single-driven (W1–W4), so composing 1.1 along the nets terminates in a total N_f. ▸ the W1–W4 checker — finite structural checks on N; checker asserted correct. ◐
• 2. ρ is a bijection R → F (F5). ▸ 03 the flop→name table read from the Q-nets; certificate checkable as injective and onto R. ● 10,873/10,915. Figure: DFF ≙ register q.
• 3. N ≡ N′ cone-wise, where N′ drops the physical / clock / buffer cells. ▸ 02 per class: physical cells drive no logic net; buffer/clock cells have function = identity (by 1.1) — one checkable certificate each. ◐
• 4. N′_f(s, i) = δ_r(s∘ρ, i) — via the pass trail. Figure: the AOI21 cone computes ¬((a·b)+c).
  • 4.1 adjacent snapshots are cone-equal, s_k ≡ s_{k+1}. ▸ 04 their miter as CNF, UNSAT by minisat (modules) / ABC cec (die); exact passes one miter each, mfs 6,172. The CNF is the certificate; correctness = an independent solver’s UNSAT (miter polarity falsification-tested). ● s0 … s7.
  • 4.2 hence s0 ≡ s7 (4.1, transitivity); and s7 ≡ N′, since the trailing buffer/upsize/dnsize are function-preserving and the P&R inserts are exactly step 3’s deletions. ●
  • 4.3 s0’s cones equal δ (the front end RTL → s0: proc / techmap / opt). ▸ no certificate yet. ○
  • ⇒ 4.2 gives N′_f = (s0-cone); with 4.3, = δ_r. Conditional on 4.3.
  • 05 arithmetic cones (mul / div) take the same 4.1 equalities via width-generic template theorems, where SAT starves. ◐
• 5. Goal. N_f = (by 3) N′_f = (by 4) δ_r(·∘ρ); well-defined by (1), quantified over all of R by the bijection (2). ∎ Sound modulo the open leaves 4.3 (front end) and the 1.1 master-coverage gap.

Lift (L3, not here). With the reset-bit certificate reset_f = reset_r (03, ○; the IBuf unreset residual is its failure mode), the Goal lifts to Mealy(N) ≈ρ ⟦RTL⟧ by one cycle-induction step in L3 — trivial because ρ shares the state.

Open problems

1. F5 — run 03's reproduction; both outcomes are results.
2. The ABC trail patch and checker (04) — the cheapest site anywhere in the project for the congruence-certificate architecture.
3. The mul/div parameter check (05) — confirms the multiplier stays iterative, keeping the hard problem class away.

First experiments

Instrument the synthesis (03) — the flow is ours to re-run, so ρ is logged, not excavated. Alongside: promote W1–W4 to lemmas (01), and state the SRAM macro contracts (02).

Effort

6–9 months; the most likely place for an early concrete result after L1's SDC work. Cost scales with the certificate trail length, not the design size.

Reading

Kuehlmann/Brand lineage on SAT sweeping; ABC's rewrite/refactor/resub. Kaufmann & Biere on PAC certificates for multipliers. CompCert for the verified-pass vs validated-pass calculus — they validated register allocation for exactly the reasons 04 validates the rewrite trail.