The axiom register
The primary deliverable. With unbounded proof capacity everything else is time; this list is what the result would actually be.
Each entry: what is assumed, which layer introduces it, whether it is testable, and what it would take to push it further down.
Reassessment pass (2026-07). Test applied to every entry: is this a fact about the world outside the mathematics — fabrication, environment, intent — or merely an unproven theorem? Entries failing the test are marked T→theorem with a named discharge route (they remain assumptions only until that route is executed), retired (R), or moved to the Discharged section. The result is summarised in The irreducible core.
Update (2026-09). E1 — "the compact model contains the true device" — is discharged. The device enclosure is not assumed; it is derived from the measurement data (the data register, now the tower's actual physical input) by a drift–diffusion solve plus Bayesian inversion (L0/02), leaving only a thin model-class-adequacy residue and a declared prior. The name "E1" now denotes that derived enclosure, so "modulo E1" throughout reads as modulo the derived device model. The physical content of the bottom layer has moved from an axiom ("trust the fit") to an input (the data) — which is where a category of measured data belongs.
Status key —
- A unfalsifiable in principle (specification fidelity)
- E empirical, testable
- P physical/probabilistic, no deterministic statement exists
- T→theorem removable, discharge route named
- R retired — not needed for the per-die validation claim.
Specification-side (errors here are silent)
| # | axiom | layer | status | notes |
|---|---|---|---|---|
| S2 | The Sail RISC-V model faithfully captures the standard | L4 | A (small) | Smaller than it looks: sail-riscv is the standard's official golden model — adopted by RISC-V International, and new extensions must extend it for ratification. Residue: the model's fidelity to the ratified manuals, plus the Sail→prover translation's trust status (L4 open problem 4). Mitigate by running the official compliance suite against the imported model. |
| S3 | The residual authored semantics are what was intended | L4 | A (small) | The core uses the standard machine-mode CSR/trap/interrupt machinery and the standard debug architecture, so the bulk of what a custom design would force into S3 dissolves into S2's import (the Sail privileged subset) and the debug spec. What remains authored: the xrocket custom-CSR fragment, the performance-counter event table, and the platform devices' register conventions (CLINT's de-facto document, the PLIC instance) — small, but the same unfalsifiable character; the generator-source-first-then-diff discipline applies. |
| S4 | Where RISC-V is underspecified, our chosen refinement is acceptable | L4 | A | Interrupt timing ("eventually"), WARL field choices, some PMA behaviour. Conformance to an underspecified spec is not a statement. |
Empirical models (testable, calibrated, never derived)
The row that once headed this section — E1, "the compact device model contains the true device" — is discharged (see the Discharged table): the device enclosure is now derived from measurement data by Bayesian inversion, not assumed, so the physical content of the bottom layer moved to the data register — the actual input — and only a thin model-class-adequacy residue remains. What survives in this table are the geometry and process claims.
| # | axiom | layer | status | notes |
|---|---|---|---|---|
| E4 | Corner models bound the actual PVT distribution | L1 | merged | No independent content: the empirical half ("actual dies lie within the corner parameter ranges") is P4; the mathematical half ("box extremes are attained at corners") is M4 — an obligation, not an axiom. |
| E6 | DRC rules imply manufacturability | L1 | R | Retired: a yield claim, not a correctness claim. For validating an existing, fabricated, tested die, manufacturability is moot. What the proof needs — as-fabricated geometry within tolerance — is E7's restated content; per-die escapes are P5's. |
| E7 | The as-fabricated geometry lies within the stated tolerance family of the drawn layout | L1 | E | Restated (absorbing what E6 actually contributed): litho + etch + CMP + overlay keep this die's geometry inside the family over which L1's enclosures and sandwich theorem are quantified. Sits between LVS and the fab — the mask is deliberately not the drawn layout (OPC), so LVS-verified geometry is not what prints. Scales worst as features shrink relative to wavelength. Irreducible: it is a claim about a physical object, checked only statistically (process control) and indirectly (test). Data: D3 — the partially unpublished class; provenance via the DRC-deck inversion (see the register). Now carries L1/01's hypothesis (H3) — no spurious material: the sandwich alone permits the fabricated set to contain an island that meets no eroded net, i.e. a net absent from the drawn layout, and the topology-preservation theorem is false without it. Not checkable (it quantifies over A); the physical reason it holds is that etch and litho displace edges rather than nucleate islands, so an edge-displacement process model would imply it. |
Physical / probabilistic (no deterministic theorem exists)
| # | axiom | layer | status | notes |
|---|---|---|---|---|
| P1 | Synchronisers resolve | L1 | P (shrunk) | Irreducible in principle — Marino's theorem (L1/06): no continuous bistable escapes unbounded settling. But the rate becomes a theorem: τ is the unstable eigenvalue at the metastable saddle, derivable as an enclosure from E1's interval model (M8), and the settling-time distribution follows. Surviving axiom content: the asynchronous-input arrival process is bounded (environmental — P6-class). |
| P2 | No single-event upsets outside the ECC budget | L0 | P (shrunk) | Poisson, linear in area×time, does not shrink with margin. But most of its parameters are derivable modulo E1: Q_crit and collection cross-section from device physics, masking/AVF from netlist + timing (L0/03), interleaving from layout (X2's route). Irreducible core: the flux (JEDEC JESD89A) and the measured multi-cell upset radius — environmental and empirical facts. Data: D5 (flux); the upset radius is a D3/D4-class measurement. |
| P4 | Process variation stays within corners | L1 | P | Absorbs E4's empirical half: as-fabricated device and interconnect parameters of produced dies lie within the corner ranges. Becomes yield, caught by test, not a runtime failure. Fluctuation granularity (discrete dopants, RTN — L0/05) enters here as part of the corner spread. Data: D3 + D4 (corner ranges). |
| P5 | The fabricated die is defect-free on the tested faults | L1 | P | Per-die assurance is statistical: ATPG coverage (~99% stuck-at), not proof. A far larger hole than anything in the proof. Irreducible for existing silicon; the only shrink available is better coverage accounting, which is computable. Data: D3 (defect density D₀) + the measured coverage of the actual test set. |
| P6 | Environment within spec | L1 | P | The collector for every bound the world must supply: supply voltage and droop, temperature, clock-reference accuracy, asynchronous-input arrival rates (P1's residue), radiation flux (P2's residue), jitter budget (X5's residue). Irreducible by nature — no theorem constrains the environment. Data: D5. |
Structural / interface
| # | axiom | layer | status | notes |
|---|---|---|---|---|
| X3 | Coupling beyond the extraction window is bounded in aggregate | L1 | T→theorem (on M2) | The assumption standing in for the screening theorem. Removable the day M2 is proved; not justified by per-pair smallness — the naive far-field sum over ~61k nets diverges without screening. |
| X4 | The off-die parts meet their datasheets — the board oscillator, the serial-link far end, the UART peer, the pad-ring IO cells, the POR/supervisor arrangement | L5 | A/E | A scoping dial, not a monolith: L5's boundary decision (B1 core / B2 SoC / B3 device) determines exactly which batch of it each theorem is conditional on — B1 needs none, B2 adds the SRAM macro contracts (with open collateral behind them — checkable by effort), B3 the rest. Required in full only for the claim about the device you can hold. |
| X5 | (retired for this design) The on-die clock generator meets its frequency contract | L1 | R | This design has no on-die oscillator: the clock arrives at a pad from the board, so the generation contract relocates wholesale to the environment (P6's period/jitter bounds) with the board oscillator's datasheet as X4-class evidence — and the excision-and-contract machinery this row once carried is not needed. The mathematics stays available (M8's Floquet/Poincaré programme) for any future configuration that adds a PLL; the netlist-side expectation becomes zero combinational cycles, enforced by W3 as a defect check rather than a boundary delimiter. |
Empirical inputs (the data register)
With E1 discharged (above), this register is the tower's primary physical input. The device I–V is no longer trusted as a fitted formula; it is inferred from these measurements by Bayesian inversion (L0/02), so the device and material data (D4, D2) are the input to that inference — the actual physical content of the bottom layer — not the calibration of an assumed model. The remaining axiom tables above are residual model-adequacy claims; this table is the measured data they and the inference consume. Discipline: every number enters a proof as an interval with stated provenance, never a point value. Per number the axiom is "the true value lies in the stated interval"; the proof determines the required width (from the margin budget), metrology determines the available width, and the health metric is the ratio.
| # | class | examples | required vs available | consumed by |
|---|---|---|---|---|
| D1 | fundamental constants | k_B, e, h — exact since the 2019 SI redefinition; ε₀, α at ~10⁻¹⁰ relative | ~2 digits vs exact — free | P3's discharge (kT), charge counting (e, Q_crit), capacitance (ε₀) — these enter L0's own arguments directly, independent of E1 |
| D2 | bulk material data (Si, SiO₂, metals) | ε_r(SiO₂) ≈ 3.9, ε_r(Si) ≈ 11.7, E_g = 1.12 eV, n_i(300 K) ≈ 10¹⁰ cm⁻³; mobility and ionisation vs dopant concentration (Caughey–Thomas, Masetti fits); v_sat; Chynoweth coefficients; metal resistivities; thermal conductivities | ~10% needed vs ~1% available | L1's enclosures consume ε_r and ρ directly, not via E1; L0/04's avalanche and thermal criteria; the rest via E1's fit |
| D3 | process / facility metrology | layer thicknesses, t_ox, sheet resistances ± corners (published in the PDK); overlay σ, CD-control σ, LER amplitude and correlation length, etch bias vs density, defect density D₀ (not published) | the binding class — required ≈ available | E7's tolerance family — these are literally the r_m = bias + k·σ + overlay of L1's sandwich theorem; P4's corner ranges; P5's defect statistics |
| D4 | device calibration | the SKY130 BSIM4 model-card parameters per device flavour, with corner spreads (published); the doping profiles behind them (not published) | interval width set by the noise margin — L0/02 argues coarse suffices | E1 — this is E1's data |
| D5 | environmental reference | JEDEC JESD89A flux spectrum; ambient temperature range; supply tolerance; reference-oscillator accuracy; the mechanical qualification limits (JEDEC JESD22 shock / vibration / thermal-cycling) and EM immunity levels (IEC 61000-4, the IC-level IEC 62132 DPI) — the field→pin scaling that turns these into pin-referred disturbances is board-dependent (X4-class) (datasheet / qual-level) | datasheet-level | P2's λ; P6's bounds; X4; L0/04's V9/V10 |
Three notes:
- The unpublished half of D3 has an observable shadow: the DRC deck. Spacing and enclosure values encode the foundry's own margin arithmetic (
rule ≈ f(overlay, CD σ, …)), so the tolerance family can be inferred from rules the foundry publishes and stakes its yield on, rather than assumed. This inversion should be performed explicitly and recorded as the provenance of E7's intervals — it is the same move as reading DRC rules as theorem hypotheses, applied to data. - Why the data floor is D2, not the standard model. The most optimistic anchor — fundamental constants only — is blocked by L0/05's chain gaps: ab initio methods reach percent accuracy at best on the quantities that matter (the DFT bandgap problem), no better than measurement. D1 still enters directly where L0 uses it, but everything material is measured, and would remain measured even with the reduction chain proved.
- Liberty tables and extraction decks are deliberately absent from this register: after E2's and E3's discharge routes they are derived objects, not inputs. D4's unpublished doping profiles are why Route A (solving the device PDE) is blocked by data availability as well as by mathematics.
Discharged and retired
Kept for the record; identifiers remain valid where other documents cite them.
| # | was | verdict |
|---|---|---|
| E1 | The compact device model (BSIM) contains the true device | Discharged (reforged) — removed from the trusted-axiom list. The device I–V enclosure is derived, not assumed: the measurement data (the data register — now the actual physical input) + a validated drift–diffusion forward solve + Bayesian inversion (L0/02) produce a credible enclosure. "The fit contains the truth" is gone; what stays in the trusted base is (i) the measurement data itself, (ii) a thin model-class-adequacy residue — the DD/semiclassical description is valid in this regime with a bounded discrepancy term (L0/05, cheap at 130 nm) — and (iii) a declared prior. The name E1 now denotes this derived enclosure and its residual base, so "modulo E1" throughout the book reads as modulo the derived device model — coherent, since an enclosure is exactly what a proof is conditional on. What was once "the tower's one physical axiom" is now an input (data) plus a much thinner adequacy claim, contributing a data-shrinkable epistemic term to ε(T) (L0/03). The mechanical-stress (V9) and EM-forcing (V10) coordinates and their system-dependent field→pin residue ride along on the enclosure as before. |
| S1 | The netlist semantics is the right semantics | Discharged — In this project the netlist's Mealy semantics is derived, not posited — per-cell Boolean functions (L1/06's (A)) + the bridge theorem (M5) + LVS (L1) yield it as the conclusion of the physical stack. |
| P3 | Thermal noise does not cross the noise margin | Discharged — a theorem modulo E1: barrier ≈ 7,500 kT ⟹ ~10⁻³²⁵⁷ (L0/03); the quantum-tunnelling analogue is smaller still (L0/05). One caveat is load-bearing: the discharge requires restoration, and fails on the oscillator's phase mode — that residue is X5/P6's jitter, not a level-noise failure. |
| X1 | The netlist printer / file parser is faithful | Obligation, not axiom — a verified parser/printer for a ~20-production format is standard work (CompCert-style validated front-ends). Route known, no empirical content; it was never a claim about the world. |
| E2 | Standard-cell Liberty tables match SPICE match silicon | Discharged — Route: L0/07 derives interval-valued tables (with inter-sample derivative bounds) from E1's interval device model by verified DAE enclosure. The PDK .lib then exits the trusted base and is demoted to an oracle for cross-checking. |
| E3 | The extraction rule deck (pattern library) is accurate | Discharged — Route: L1's variational enclosures — Dirichlet/Thomson two-sided bounds, Nakao–Plum–Watanabe machinery. Accuracy target ~5% against 10–20% carried margin, so rigorous-but-loose suffices. The far-field part additionally needs M2. |
| E5 | The delay model (cell + interconnect) matches physical behaviour | Discharged — Subsumed: cell part by E2's route (L0/07), interconnect part by E3's route (L1), composition by M3/M5. Not a separate assumption once those land. |
| E6 | DRC rules imply manufacturability | Retired — yield economics, not per-die correctness. Needed content restated into E7. |
| X2 | Errors within an ECC word are independent | Route: "cells of one word are pairwise ≥ r apart" is a decidable layout check (L1 machinery); the empirical content — the upset radius r, growing with scaling (Ibe et al.) — moves into P2's parameter set. Still the clearest cross-layer obligation in the project: the check lives in the GDS, invisible to both the code's algebra and the netlist. |
Unestablished or false for this design (the F-series)
Not axioms — open defects in the assumption set, discovered during scoping and measurement. Rows close by flow work, checker work, or design modification; each carries its current evidence.
| # | claim | layer | status |
|---|---|---|---|
| F2 | All loads/slews lie within the Liberty characterisation range | L1 | AT RISK, measured — the independent hardening run reported thousands of max-slew and hundreds of max-cap violations on stretched nets; outside the table the tool extrapolates, so affected timing numbers are vacuous rather than merely wrong. The primary flow's verdict is pending; the row closes only with a clean domain check. |
| F3 | The constraint set is complete and its exceptions justified | L1 | FAILS as generated, sharply — the emitted SDC declares one clock; the JTAG and serial-link clock domains are absent, so their paths and crossings are unanalysed, not excepted (L1/04). No false-path or case-analysis assertions exist to audit — the whole risk is the gap. Closure: complete the set, re-run signoff, discharge the crossings against the synchroniser inventory. |
| F5 | Register correspondence ρ survives synthesis | L2 | ρ RECOVERABLE FROM THE NETLIST, measured — the flop instance names are anonymised (_NNNNN_), but the register's identity lives in its Q-net name, and 10,873 of 10,915 (99.6%) carry the RTL hierarchical name of the register they implement. So ρ is a checkable hypothesis readable from the existing artifact — no synthesis instrumentation or tool patch needed (an earlier reading of the instance names wrongly concluded 100% anonymised). The 36 anonymous Q-nets plus any constant-folded/merged registers are the residue (the opt_dff/opt_merge deviations L2/03 names), settled by the CEC that verifies the whole ρ. Open only in that the verifying CEC has not yet run. |
| F8 | Independent signoff engines agree | L1 | FALSE, measured — on the same layout, Magic DRC reported 0 violations while KLayout reported 4 (met4 width/spacing); LVS meanwhile caught a real power short the geometric engines disagreed about (findings). Consequence: no single engine's verdict is treated as the verdict — G-checks are stated engine-independently, and agreement is a claim to measure per layout. |
(F1 — timing closure — dissolved: the nine-corner run is a passing check (L1/nine-corner) at the conservative clock, and a passed check is not a finding. Its only caveat — that out-of-domain lookups are vacuous — is F2, and a claim "holds conditional on another finding" carries no independent open content, so it collapses into F2. F4 — mode coverage — merged into F3: the generated constraints declare no modes, so completeness is the whole question. F6 — reachable clock configurations respect closure — retired: no software-reachable clock knob exists on this design; the clock-frequency condition is the board's obligation, filed under P6/X4. F7 — one design across the artifact chain — dissolved: it holds by construction on this target, since every artifact descends from one pinned elaboration, and a property that holds is not a defect; its standing check is the re-elaboration diff, tracked as L3/re-elaboration.)
Open mathematical questions
Not axioms — things that might be theorems, that the project needs, and that nobody has. Distinguished from the tables above because effort could in principle remove them. Note the T→theorem routes above land here: executing them is what shrinks the register.
| # | question | layer | notes |
|---|---|---|---|
| M1 | Uniqueness for stationary drift–diffusion under operating bias | L0/02 | Existence is established; uniqueness is known only near equilibrium and genuinely fails where latch-up or snapback occur — a parasitic thyristor is a real bistable device. So "the transistor's I-V characteristic" is not well-defined from first principles. Industry dodges this by not solving the PDE (→ E1). Tap-coverage rules are secretly the side condition that kills the second branch. May be bypassable: state all enclosures universally over weak solutions of the transient problem; what is then needed is unreachability of the second basin from the unpowered state under tap coverage, and the method fails safe if that cannot be shown (L0/00). |
| M2 | The screening exponent α | L1 | Convergence of the far-field coupling sum is empirically certain — silicon works, and industrial extraction truncates at a fixed window and matches it — but its a-priori proof is open: net counts grow polynomially in distance while unscreened coupling decays only logarithmically, so convergence rests on the cascaded mesh apertures giving C_far(d) ≲ C_adj·α^(d/p). M2 is not a missing certificate (the calibrated deck, E3, is the certificate industry uses); it is the sub-lemma that discharges E3's far-field part — deriving α from a harmonic-measure estimate is what turns cheap local extraction from empirically-calibrated into proved, and X3 retires when it lands. |
| M3 | The lumping/composition theorem | L0/08 | "The lumped circuit model is sound with respect to the field problem, with this error bound." Universally assumed, never stated in a form usable as a verification hypothesis. The right formal frame is ISS small-gain / contraction (L0/08). |
| M4 | Where monotonicity holds | L0/08, L1 | Corner-based methodology is sound iff the response is monotone in the corner parameters — otherwise the extremes are not at the corners. Assumed industry-wide. Production data violates it: cell_fall is non-monotone in input slew at two grid points of inv_1. Absorbs E4's mathematical half. Diagnosed (L1/09): the violation is an artifact of the (t₅₀, slew) quotient — the 50% anchor vs. conduction from V_th — while the waveform-level map is monotone by ODE comparison (given E1 states I increasing in V_in). So M4 splits: the timing half dissolves under waveform-envelope propagation; the genuinely open residue is monotonicity in the P/V/T parameters proper. |
| M5 | The bridge theorem | L1 | Timing closure ⟹ the discrete Mealy semantics is sound. Everything above L1 presupposes it, and S1's discharge route runs through it. Tractable — a paper, not a decade. |
| M6 | An explicit constant in the quasi-static error bound | L0/01 | ‖φ_Maxwell − φ_EQS‖ ≤ C·(L/λ)²·‖source‖ with C geometry-dependent. The theorem shape exists (Ammari–Buffa–Nédélec); the explicit constant over realistic geometry does not. Without it the reduction is qualitative. |
| M7 | The regime decomposition: robust invariance + progress | L1/06 | The honest form of "the digital abstraction". Not a static noise-margin claim but (I) you never leave the union of valid regimes under bounded disturbances, (P) transitions complete in bounded time, (A) the induced discrete map is the Boolean function. Needs barrier certificates for (I) and a Lyapunov functional for (P). The van Roosbroeck free energy is the natural candidate, but it decreases toward equilibrium — adapting it to a boundary-driven steady state is the open piece. Metastability is precisely the failure of (P). |
| M8 | The metastable-saddle eigenvalue (τ) | L1/06 | For this design M8 is one problem, not two: the synchroniser's settling rate τ — the unstable eigenvalue at the metastable saddle — an eigenvalue-enclosure over the interval device model, the same machinery as L0/07. Discharging it converts P1's rate bound into a theorem modulo E1. Prior art: interval Poincaré maps (Zgliczyński, Galias). (The oscillator-phase mode — the frequency and phase-diffusion coefficient of an on-die limit cycle, Demir–Mehrotra–Roychowdhury — is generality-only here: the clock is board-supplied, so there is no on-die oscillator to analyse, the same reason X5 retired.) |
M2, M3, M5 and M7 are the four where the project's structure genuinely depends on the answer. M1 is the only one that is open mathematics rather than open formalisation — and the enclosure formulation may sidestep it. M8 is the ledger-shrinker: it exists purely to convert axioms into theorems.
Note M7 subsumes what a static "noise margin" argument was doing: the margin is the robustness radius of the invariant set, and restoration is the contraction that makes the set attracting — not separate phenomena.
The irreducible core
If every T→theorem route is executed and every M is proved, the register collapses to:
| cluster | entries | why no proof reaches it |
|---|---|---|
| specification fidelity | S3, S4, S2's residue | intent is not a mathematical object |
| the physical model | the device measurements (D-register) + model-class adequacy + a declared prior | the device enclosure is inferred from data (E1 discharged into these); no proof reaches the measurements themselves, the adequacy of the DD model class (L0/05), or the prior |
| this particular die | E7, P4, P5 | fabrication is sampling and test is statistical; no theorem reaches the object itself |
| the environment | P6 (absorbing P1's arrival bound, P2's flux, and the board clock's period/jitter contract) | no theorem constrains the world |
| surviving randomness | P1, P2 residues | Marino's theorem; Poisson arrivals — irreducible in principle, quantified by theorems |
| scope | X4 | a choice, not a claim |
Twenty-two entries reduce to roughly eleven, and every survivor is a statement about the world — fabrication, environment, intent — rather than about mathematics. Each survivor's numerical content is an interval-containment claim over the data register (D1–D5) above — so the fully reduced trusted base is: the intent claims, the D-intervals with their provenance, and the Poisson/Marino residues. The middle of the stack becomes theorem all the way through: the only assumptions below the netlist are the device measurements and a thin model-class-adequacy residue (E1 the axiom discharged into them), plus the die/environment cluster; and the only assumptions above it are the three specification-fidelity claims at the very top. That shape — empirical floor, unfalsifiable ceiling, theorems in between — is the honest form of "the chip is verified."