Overview — the mathematical content

Background

The introduction set the scene — the tower of trust, how the industry establishes correctness today, the validation-not-design plan, the Chipyard/Rocket target, and the six layers in prose. This page is the mathematical front door: the statement the project is trying to establish, the named objects at the layer seams, and the dispatch of the proof into layers with their prices. Project structure and tooling live in the repository's root README; the flow's jargon is in the glossary, and textbook on-ramps for the fields the tower spans are in the reading list.

The top-level statement

Let d be a fabricated die, F a program image, E an environment (supply, clock, temperature, radiation, asynchronous inputs). Write obs(d,F,E) for the observable trace at the pads and Sys(F) for the pad-trace semantics of the system specification — both defined by L5, not primitive. (How F gets into the machine — resident boot ROM, the debug module, or the serial TileLink port — is part of L5's boundary decision, not an aside: every load path is a pad-trace prefix.)

     Envelope(d, E)                                     ← L0/04, V1–V7
  ∧  Axioms                                             ← axioms.md
  ⟹  P[ obs(d,F,E) ⊑ Sys(F) ]  ≥  1 − ε(T)

      ε(T)  =  λ·A·T·AVF          particle strikes         (P2)
            +  N_sync·P_meta(T)   unresolved synchronisers (P1)
            +  P_droop            supply excursions        (P6)

(Symbols: λ is the particle flux and A the die area; AVF, the architectural vulnerability factor, is the fraction of raw bit-flips that matter architecturally; N_sync counts the synchroniser boundaries where the design meets unclocked inputs. All three ε-terms are derived, not decorative — each has its own chapter.)

Three features of this statement are deliberate and worth defending.

It is probabilistic, and irreducibly so. No amount of proof removes ε. P1 is irreducible by Marino's theorem — no continuous bistable escapes unbounded settling — and P2 is a Poisson process driven by an external flux. What proof can do is derive their coefficients rather than measure them, which is what shrinks P1 and P2 in the axiom register without eliminating them.

Both ends are slots filled by their own layers, and neither is a placeholder for something easy. Envelope is L0's, and is a genuine intersection of five structurally different constraint shapes (L0/04). Sys is L5's, its ISA core is L4's — which for the Rocket core must include the machine-mode privileged subset (CSRs, traps, interrupts, PMP) alongside the base ISA — and parts of the surrounding SoC's behaviour exist only as generated code, device-tree annotations, and de-facto register conventions, so the residual device/CSR semantics must be authored rather than imported (L4, L5).

⊑ is trace refinement up to stuttering, not equality. The implementation takes many cycles per architectural step; L3's obligation is a stuttering simulation with a measure function, not a cycle-accurate correspondence.

The spec tower

The named objects at the seams. Each is the node of some layer — the object that layer is. Every layer README opens with its node (the object) and its edge up (the theorem carrying that object to the next one): a node supplies an object; the edge above it is a theorem connecting two objects.

One identification is used silently everywhere and stated only here: N is a single shared object. The netlist that L1's LVS certifies the geometry against, the netlist L1's STA runs on, and the left-hand side of L2's equivalence are all ⟦ChipTop.mapped.v⟧ — the flow's hardened netlist — under one parse. X1's obligation, one parser, three consumers.

The organising principle

With unbounded proof capacity, the deliverable is the axiom list.

Everything merely hard collapses to time. What survives is what is not a theorem: specification fidelity, empirical models, physical facts, and genuinely probabilistic phenomena. So each layer is organised around what it discharges and what it introduces, and the running register is axioms.md — with the open mathematical questions (M1–M8) kept separate from the axioms, because effort could in principle remove them.

Notation. Lettered identifiers index the appendix registers: S/E/P/X+number are axioms, F+number are findings about the design and its flow (unestablished or false hypotheses), M+number are the open mathematical questions — all in Axioms. Layer-local check families are defined in their owning chapters: W1–W4 (netlist well-formedness, L2/01), G1–G6 (geometric checks, L1/12), V1–V8 (the operating envelope, L0/04), C1–C7 (spec choices, L4/02), B1–B3 (claim boundaries, L5/01). The spec-tower objects are introduced just below; the standalone value X — the untracked third logic value — is in the glossary. Reading top-down, these appear before their definitions; every mention is a link.

Backgrounds. No single reader arrives knowing all of the fields this book crosses — the required intersection (computer architecture ∩ EDA ∩ analog design ∩ device physics ∩ PDE theory ∩ formal methods) is empty. So every chapter after the introduction (which is background throughout) opens with a Background section written for a reader from outside its field: the concepts, mechanisms, and proof techniques the chapter is about to use, explained from scratch (the layer chapters' are brief orientations; the sub-chapters' do the real teaching). Experts in a chapter's home field should skip its Background; everyone else should not. The glossary is the quick-lookup complement; the reading list is the textbook-depth one.

The dispatch

Each layer's named obligations. This is the proof skeleton; the layer documents are the expansions.

Every layer is a node — an object at one abstraction altitude — and the theorem connecting it to the layer above is one subsection of it, its "edge up." Definitions live in nodes; theorems live between them, on the edges. The tower has six nodes (L0–L5) and five edges. Two of those edges are decisive crossings: the ε-crossing (L0→L1), where physics establishes the deterministic EE abstraction, and the digital crossing (L1→L2), where timing closure, the geometry/interference checks, and gain-driven restoration turn analog transfer functions into a Boolean machine. Below the ε-crossing the world is analog and probabilistic; between the two crossings it is deterministic-analog; above the digital crossing it is Boolean and architectural.

Nodes and edges fail differently, and the asymmetry is why they are marked. A wrong edge (theorem) will not prove — the kernel guards it. A wrong node (definition) yields a true theorem about the wrong object — only adequacy guards it, which is why the definition nodes (L4, L5, and the L3 node) carry adequacy machinery instead of proofs. Most crossing-constraints are discharged — established at the edge and then gone (timing, restoration, the interference budgets). One survives as a standing hypothesis of the node above: well-formedness (acyclic combinational logic, no shorts, no runaway) cannot be spent at the digital crossing, because L2's Boolean machine is only well-defined under it (W1–W4). (The table runs bottom-up, L0→L5, following the composition; the book's chapters run top-down, L5→L0 — start wherever suits.)

The effort accounting. Figures are for one competent person and are the sums of the subcomponent estimates — the two merged nodes (L1 = geometry + timing, L3 = RTL semantics + the refinement) show their two summands. The original per-layer figures — seeded before the decomposition at "a few years each" — ran roughly 2× higher; scoping the pieces is precisely what revised them, and the sums reflect the better understanding, so they replaced the anchors. One cross-cutting cost is priced separately because no layer owns it: shared infrastructure — the hybrid proof framework itself, bitvector automation, symbolic simulation, and the LRAT/PAC checker integrations — 1–2 person-years, consumed by every theorem edge. Naive sequential total: 8–15 person-years, before the FPGA alternative (which deletes L1's geometry half, 2–4 of them).

Note one deliberate inversion: L2's CEC edge consumes L3's object ⟦RTL⟧, so proof order is not tower order. The numbering is by artifact altitude — netlist below RTL — not by logical dependency.

How they compose

Each ≔ line is a node (an object supplied); each ⊨ line is that node's edge up (a theorem to the next object). ≔/⊨ alternate all the way up.

device d ∈ Envelope
  ≔ L0    Field(d), device models, ε                 [the physics node; E1, Poisson error model]
  ⊨ L0→L1 Field(d) ⊑ Contracts(N)                    [electrical abstraction; M3, M7; modulo E1]  † ε-crossing
  ≔ L1    N and RC well-defined ∀A in the E7 family  [the EE-circuit node; (H1)(H2) checked, E7 ⊨ (H3); M2]
  ⊨ L1→L2 Contracts(N) ⊑ Mealy(N)                    [digital crossing = timing+geometry+restoration; M5; F-series] †
  ≔ L2    Mealy(N)                                   [the synchronous machine; W1–W4 standing]
  ⊨ L2→L3 Mealy(N) ≈ρ ⟦RTL⟧                          [the CEC — horizontal equivalence; ρ = F5]
  ≔ L3    ⟦RTL⟧ = the microarchitecture              [measured census]
  ⊨ L3→L4 ⟦RTL⟧ ⊑ ISA                                [the invariant — the genuine abstraction step]
  ≔ L4    ISA  = Sail-RV32 ⊕ machine-mode subset      [S2, S3, S4]
  ≔ L5    Sys(F) = ISA ⊕ memory map ⊕ devices        [X4, bus contract — the ISA⊕devices composition]
  ────────────────────────────────────────────────────────
       obs(d,F,E) ⊑ Sys(F)   with probability ≥ 1 − ε(T)

† is where ε enters. The two marked lines hold on the event "no particle strike (P2) and no unresolved synchroniser read (P1) during [0,T]"; every line above them is deterministic conditional on that event, and ε(T) is exactly the probability of its complement (plus P6's droop term). The probability in the conclusion is not smeared across the chain — it is the measure of the conditioning event for two specific lines.

Interfaces

Each node exports a thin object, and each edge is one arrow up. The functional chain (L2→L5) and the physical chain (L0→L2, the two crossings) are nearly independent and meet only at the netlist:

                    L5  Sys(F): pad traces (memory map, serial TL, UART, obs)   ← top node
                     ↑  ISA ⊕ devices ⟹ Sys — composition at the chosen boundary
                    L4  ISA (Sail + the Rocket-specific parts authored)          ← definition node
                     ↑  the invariant — stuttering refinement, word-level        ← THE WORK
                    L3  ⟦RTL⟧ = the microarchitecture (buses, arithmetic intact) ← definition node
                     ↑  the CEC — horizontal equivalence, certificates
                    L2  the synchronous machine / gate netlist  ←── meeting point ───┐
                     ↑  DIGITAL CROSSING: timing + geometry checks + restoration     │ annotations
                    L1  the EE circuit: extraction ⟹ N + RC, timed contracts, SDC    │ (delay, RC)
                     ↑  ε-CROSSING: field sim ⟹ deterministic transfer functions     │
                    L0  devices/field: cells ⟹ Boolean functions, ε ────────────────┘

The refinement proof never touches RC. Electrical data exists solely to discharge the digital crossing's hypotheses. That is the cleanest seam in the stack and should be preserved deliberately — see L1 on keeping crosstalk out of the interface, and treating any net that would need a functional coupling constraint as a layout bug.

Note that geometry is not a layer — it splits by character. The continuous, field geometry (transistor and wire shapes, RC) lives in L0's edge up, the ε-crossing, where the field simulation runs on it to establish the transfer functions; it is analog. The combinatorial, relational geometry (tap density, min spacing, "≥ N apart" checks) lives in L1's edge up, the digital crossing, where each check discharges a budget L0 set — L0 states an analog budget ("interference < X ⟹ ε bounded"), and the layout check is the finite combinatorial proof the budget holds. So a safety condition is stated in one layer and discharged in another: L0/06 carries the dispatch table, and L0 owns the statement of every envelope condition but the check for only one.

The composition, machine-checked — and its seam ledger

The chain above is not only prose: it is a Lean theorem, chip_realises_isa (dieBeh = isaBeh), which says the physical die and the ISA reference produce the same pad-trace on every program, and it type-checks — the layer boundaries genuinely line up. Its content is entirely in what it assumes, and #print axioms reads that back exactly. One boundary is a real, sorry-free proof: the netlist ↔ RTL middle (trace_refines, composing the proved one-step l2_commutes across cycles). Every other arrow in the diagram is a named interface axiom, because the layers that would discharge it are still proof-phase.

Those interface axioms are the honest measure of "the layers connect formally": each is a seam the thesis claims but has not yet proved. They are the arrows of the diagram, and — this is the gap the Lean attempt surfaced — the per-layer scoreboards scored the layers' internal obligations but never scored the seams. So the seams are now a first-class section of the scoreboard (IF/*, generated by tools/check-interfaces.py), one row per arrow, and are described in full in the seams appendix: the M5 timing bridge (iface_L1_timing), extraction+grounding (iface_L1_L0, which composes the celltopo/routecheck/LVS islands nothing else joins), the RTL front-end (frontEndCommutes), matched reset (reset_corr), the L3 refinement invariant (iface_L3), and the ISA/system boundary (iface_L4_L5) — plus the one dischargeable trust anchor the equivalence certificates rest on (miterCNF_sound). Closing the tower is discharging those seven rows; until then, the end-to-end theorem is real but conditional, and says precisely on what.

Three structural facts that recur at every layer

These are why the edifice is possible, and they shape every proof in it.

1. Nothing accumulates. Every layer has a mechanism that resets the error budget: gate restoration kills noise accumulation across logic depth; the clock edge kills timing-error accumulation across cycles; local variation adds in quadrature (√n) rather than linearly along a path; ECC plus scrubbing converts a linear-in-time failure rate into a quadratic one. Consequently every proof here is inductive with a fixed invariant, never one tracking a growing quantity.

2. Continuous perturbations get discharged; discrete events get carried. The continuous mechanisms are suppressed by hundreds of orders of magnitude — thermal escape faces a ~7,500 kT barrier, giving ~10⁻³²⁸⁵ — and should be bounded away and deleted, not carried as epsilons. The discrete ones (particle strikes, manufacturing defects) are Poisson, do not shrink with margin, and are handled by redundancy or by test, never by better analysis. Confusing the two is the most common modelling error in this area, and the trap is that coupling capacitance looks like the first kind and behaves like the second: it is additive, so its far-field sum needs a genuine convergence argument (M2) rather than a smallness claim.

3. Amortisation is the whole game. The ~400 standard cells of the library, verified once, cover every design on the process — this design's hardened netlist draws its 51,359 instances from just 96 cell types. One SRAM macro proof covers every instance of that macro (the 2 KiB data array appears twice; the memory obligation is parametric in depth, so size costs area, never proof). And because the design is generated, its entropy is the configuration: a few dozen lines of Scala elaborate to 228 modules and 9.4 MB of SystemVerilog. The per-design content is far smaller than the artifact size suggests.

A pattern worth naming

Recurring often enough to be a heuristic rather than a coincidence:

A real physical instability, prevented by a design rule, which is therefore secretly a hypothesis of a well-posedness or boundedness claim rather than a manufacturing constraint.

Instances so far: min-width and min-spacing are the hypotheses of L1's topology-preservation theorem; tap coverage is what destroys latch-up's second PDE solution branch (M1), i.e. what makes "the transistor's I-V characteristic" well-defined; the voltage rating keeps impact-ionisation terms out of the model and hence keeps global existence available; tied metal fill is a precondition of M2's cascade, since floating conductors relay rather than screen.

Several DRC rules are the side conditions of theorems nobody has written, and recovering those theorems may be the cleanest way to say what a rule deck actually means.

The certificate archetypes

Every PASS obligation on the scoreboard is discharged the same way — a tool emits a witness an independent checker re-verifies — but the checkers are not equally trustworthy, and the ladder is worth naming. Ordered by distance to a self-checking proof:

1. Functional, re-checkable. The tool's output is verified over the full input space by a second, simpler program. celltopo derives a cell's switch-level Boolean function from its transistors and checks it equals the Liberty function over the whole truth table; the CEC trail (L2/04) dumps each synthesis pass's miter and a SAT refutation an independent solver replays. The anchor is a single checker-soundness line (the truth-table comparator; the DRAT checker) — nothing else is trusted.

2. Independent witness. A structural property re-derived from scratch, independent of the tool that made the artifact. routecheck re-verifies the router's no-opens/no-shorts from the routed DEF by union-find and a sweep-line — trusting the witness algorithm, not the router.

3. Conservative bound over a trusted model. A monotone or interval argument that a specification number bounds a physical measurement. spicecheck screens each Liberty delay against an ngspice/BSIM4 simulation; the power-grid droop check reduces to a box-corner evaluation because the grid Laplacian is an M-matrix (monotone). Here a physical model (BSIM4, the Laplacian) enters the trust base, discharged only up to the model's fidelity.

4. Oracle against a golden model. An execution checked instruction-by-instruction against a reference. cosim runs the hardened RTL against spike and confirms every committed instruction's PC, writeback, and CSR. The golden model is trusted; this is the executable precursor to the L3 refinement proof, not a substitute for it.

5. Structural census. A finite decidable predicate re-run over the artifact — W1–W4 on the netlist, the memory-map / boundary / interrupt checks against the device tree, the RTL construct census. The predicate itself is small and auditable; that is the whole trust.

The ladder is exactly where the remaining trust concentrates: (1)–(2) hand back something independently verifiable, while (3) rests on a physics model and (4) on a reference implementation — which is why the analog models and the ISA oracle sit next to the axiom register's EXTERN entries. The taxonomy is made precise in the project's Lean skeleton (lean/, Prelude/Certificates), where each archetype is a typed certificate whose soundness axiom is exactly its anchor, and every layer L0–L5 carries at least one certificate-backed, sorry-free leaf.

Status

Open mathematics (M1–M8 in axioms.md): M2 (the screening exponent) and M5 (the bridge theorem) are the two the project's structure most depends on; M1 (uniqueness for stationary drift–diffusion) is the only one that is open mathematics rather than open formalisation.

Established for this design — the parts that are not speculative:

• The full generation chain reproduces from pinned sources: Chisel elaboration through FIRRTL and CIRCT to SystemVerilog, synthesis to a netlist with zero unmapped cells, all memories resolved to three SRAM macro kinds. The artifacts the layers name exist and were produced here.
• Independent signoff engines are not interchangeable, and the register carries the measurement: on the same layout, one DRC engine reports clean while another reports violations — so a single engine's verdict is treated as one witness, and the geometric checks (G1–G6) are stated engine-independently.

Unestablished for this design (the F-series in axioms.md): the physical signoff — multi-corner timing, DRC, LVS on the final layout — is not yet closed by the flow, and until it is, the hypotheses of the bridge theorem are not established; the SDC exception set is unverified; register correspondence through synthesis is unknown. The checker suite that pins these rows is being re-anchored to the flow's artifacts, and the scoreboard tracks exactly which obligations have a running check.

See findings.md for the measured data behind all of it — and the scoreboard for the live checker verdicts of the commit this book was built from: every obligation as PASS, FINDING, TODO (with its blocker named), or EXTERN.

The chapters descend the tower from here: L5 first — the claim — down to L0, where it runs out of turtles.