IF — the seams between layers — what one end-to-end theorem must compose
| obligation | detail | |
|---|---|---|
| TODO | IF/l2-timing — the timed silicon reduces to a discrete Mealy machine (dieBeh = timedBeh) | lean: EndToEnd.iface_L1_timing. The M5 bridge theorem — setup/hold met on every path (L1 STA, nine-corner PASS) licenses the two-phase synchronous model as EXACT. Precursor: the whole L1 board bounds the analog margins; [blocked on: M5 (open mathematics) — turning the metric-timing margins into a behaviour-preservation statement about the discrete abstraction] |
| TODO | IF/l1-l0-extraction — the discrete machine IS denote(theNetlist): extraction + cell grounding (timedBeh = netBeh) | lean: EndToEnd.iface_L1_L0. Composes THREE island certificates that no row currently joins: celltopo (L0/ccc PASS — cells compute their Liberty function), routecheck (L1 — the layout's connectivity), and LVS device-match. The pieces pass; nothing scores their composition into 'the extracted layout denotes netM'. [blocked on: an LVS device+connectivity match against theNetlist, then the lemma 'extracted = theNetlist ∧ celltopo ⇒ dieBeh_comb = netBeh'] |
| TODO | IF/frontend-commute — the RTL front-end preserves cone functions: ⟦RTL⟧ commutes with ρ at the trail head (s0) | lean: L3.frontEndCommutes — the single still-open factor of the proved l2_commutes. The ABC trail (s0→s7, seven PassCerts) is checked; the yosys front-end proc/techmap/flatten that PRODUCES s0 from ⟦RTL⟧ is trusted, not CEC'd. This is the L3↔L2 seam, currently assumed inside the L2 goal. [blocked on: a CEC of ⟦RTL⟧ (the naive-netlist oracle, L3/comb-checks PASS) against ⟦s0⟧] |
| TODO | IF/reset-corr — matched reset: the RTL reset state is ρ's image of the netlist reset (the L5 induction base) | lean: L3.reset_corr — the sorryAx in #print axioms chip_realises_isa, and the one open leaf of L3's trace_refines. L3/x-idiom + L3/init-idiom (PASS — no flop carries a power-up value) is the precursor, but the ρ-image equality of the two reset states is not itself scored. The IBuf residual shows an unreset flop breaks it. [blocked on: reset-state extraction from both sides + the ρ-image check] |
| TODO | IF/l5-refine — ⟦RTL⟧ refines the microarchitecture→ISA abstraction (rtlBeh = archBeh) | lean: EndToEnd.iface_L3. The inductive invariant — L3's irreducible content. Precursor: L3/cosim PASS (1631 instructions vs spike, zero mismatches) is the executable oracle; the interface THEOREM (α, the invariant) is proof-phase. [blocked on: proof-phase start (L3/invariant, L3/invariant-alpha)] |
| TODO | IF/l6-l7-isa — the microarchitectural behaviour equals the ISA reference at the observable boundary (archBeh = isaBeh) | lean: EndToEnd.iface_L4_L5. Bundles the sail-riscv model (L4), the memory map (L5/memmap PASS), and the boot/observation contract (L5/boundary PASS, L5/b3-smoke PASS). The observables are scored; their equality to the sail reference at the pad boundary is not. [blocked on: L4/sail-pin (import the model) + L5-refine + the L5 device models (L5/sys-models)] |
| EXTERN | IF/miter-faithful — the miter construction faithfully encodes cone-inequivalence (the CEC/trail anchor) | lean: miterCNF_sound. Every PassCert's equiv rests on it, as does l2_commutes. Currently trusted (polarity was falsification-tested in trail-cec, not proved). UNLIKE E1/M-series it is dischargeable: a real Tseitin encoding would make it a theorem, not an axiom — the clearest 'promote an assumption to a proof' target. |
7 obligations — EXTERN:1 TODO:6
L5 — the system
| obligation | detail | |
|---|---|---|
| FINDING | L5/memmap — the memory map: device tree vs per-device register maps | device tree absent (regenerate: tools/build-rocket.sh): /project/thinking-sand-tools/chipyard/vlsi/generated-src/chipyard.harness.TestHarness.TinyRocketConfig/chipyard.harness.TestHarness.TinyRocketConfig.dts (0.0s) |
| FINDING | L5/boundary — the ChipTop port list is the book's 18-signal boundary | ChipTop.sv absent (regenerate: tools/build-rocket.sh) (0.0s) |
| FINDING | L5/irq-map — the interrupt wiring from the device tree | device tree absent (0.0s) |
| FINDING | L5/b3-smoke — the B3 instance: an image executes and the UART emits its message | simulator or image absent (tools/run-sim.sh build; tools/run-sim.sh hello) (0.0s) |
| TODO | L5/rtl-decode-diff — the RTL's actual address decode diffed against the dts | [blocked on: a decode extractor over the TL fabric modules (the third leg of the diff)] |
| TODO | L5/pad-defaults — the reset drive state of every output pad | [blocked on: reset-state extraction from the IOCell/serializer RTL] |
| TODO | L5/b-config — the latency bound B per configuration | [blocked on: the serializer FSM analysis + link-clock ratio] |
| TODO | L5/sys-models — the device models (UART, CLINT, PLIC, boot, serial-TL) as Sys components | [blocked on: spec-phase authoring] |
| EXTERN | L5/X4 — external devices meet their datasheets (per B-level batch) | the board oscillator, the serial-link far end, the pad-ring cells, the POR arrangement — modelled from datasheets, never checked from artifacts |
9 obligations — EXTERN:1 FINDING:4 TODO:4
L4 — the ISA
| obligation | detail | |
|---|---|---|
| FINDING | L4/isa-scope — the elaboration's ISA string fixes the partition scope | device tree absent (regenerate: tools/build-rocket.sh) (0.0s) |
| FINDING | L4/xrocket-surface — the custom fragment's structural surface in the emitted core | RTL cone absent (regenerate: tools/build-rocket.sh) (0.0s) |
| TODO | L4/sail-pin — import sail-riscv at a pinned commit; record the translation/trust line (S2's ledger) | [blocked on: adding sail-riscv to the fetch script with a pinned SHA (cheap)] |
| TODO | L4/compliance — run the architectural compliance suite against the imported model | [blocked on: sail-pin + the riscv-arch-test harness] |
| TODO | L4/spec-pin — the spec patterns from riscv-opcodes at a pinned commit, both widths | [blocked on: regenerating the pattern tables for the full extension set (I/M/A/C + Zicsr/Zifencei)] |
| TODO | L4/partition — the encoding partition vs the generated decoder's legal set | [blocked on: decoder legality-cube extraction from the emitted Rocket decode (yosys-based)] |
| TODO | L4/c-register — the measurable choice-register rows extracted from the core | [blocked on: the C2–C8 extractions (trap behaviour needs simulation or careful RTL reading)] |
| TODO | L4/ub-free-image — a real boot image contains no spec-UB instruction word | [blocked on: partition; then per-image, mechanical] |
| EXTERN | L4/S3-fidelity — the authored residue is what was intended | unfalsifiable; anchored by generator source and ecosystem software — never checked |
| EXTERN | L4/S4-choices — the recorded choices are acceptable readings of the standard | legislative by nature; what IS checkable (RTL agrees with each pick) lands in L3's lemmas |
10 obligations — EXTERN:2 FINDING:2 TODO:6
L3 — RTL and microarchitecture
| obligation | detail | |
|---|---|---|
| FINDING | L3/census — the construct census of the emitted design cone | RTL cone absent (regenerate: tools/build-rocket.sh): /home/runner/work/thinking-sand/thinking-sand/flow/rocket-sram22/src (0.0s) |
| FINDING | L3/x-idiom — every 'bx literal is the memory disabled-read idiom | RTL cone absent (regenerate: tools/build-rocket.sh) (0.0s) |
| FINDING | L3/init-idiom — every initial block is simulation-only (empty-or-absent under synthesis) | RTL cone absent (regenerate: tools/build-rocket.sh) (0.0s) |
| FINDING | L3/comb-checks — no unintended latch + RTL-level SCC over the cone | RTL cone absent (regenerate: tools/build-rocket.sh) (0.0s) |
| TODO | L3/re-elaboration — regenerate FIRRTL+SV from the pinned generator; diff against the cone | [blocked on: wiring build-rocket.sh output into a byte-diff (the chain-consistency check; F7 dissolved into this)] |
| TODO | L3/diff-sim — differential simulation with the emitted assertions enabled | [blocked on: the semantics side existing; Verilator harness] |
| TODO | L3/semantics — the two-phase synchronous semantics for the measured subset | [blocked on: proof-phase start] |
| EXTERN | L3/scheduler-independence — every LRM-conformant scheduling computes the simple semantics | stateable as a theorem for the subset; deferred, not assumed — the adequacy checks probe it empirically |
| FINDING | L3/config-declared — the elaboration-declared configuration record | device tree absent (regenerate: tools/build-rocket.sh) (0.0s) |
| FINDING | L3/config-confirmed — the declared record confirmed structurally from the emitted RTL | RTL cone absent (regenerate: tools/build-rocket.sh) (0.0s) |
| FINDING | L3/cosim — the trace-oracle: committed instructions match the golden ISA model | cosim simulator absent (tools/run-sim.sh cosim-build — needs the RV32 cospike patch) (0.0s) |
| TODO | L3/stage-graph — the pipeline stall/flush/bypass structure and occupancy bounds | [blocked on: a SystemVerilog front end over Rocket.sv (shared with L4)] |
| TODO | L3/wcet-table — the retirement-gap bounds (the measure read quantitatively) | [blocked on: stage-graph] |
| TODO | L3/bus-guarantees — Gi/Gd clauses asserted over a real execution (simulation oracle) | [blocked on: wiring the TileLink monitor assertions into the now-working harness (tools/run-sim.sh)] |
| TODO | L3/invariant-alpha — α as the formal abstraction (beyond the cosim oracle), toward the refinement proof | [blocked on: proof-phase start; the cosim oracle is the executable precursor] |
| TODO | L3/invariant — the inductive invariant (the project's irreducible content) | [blocked on: proof-phase start] |
16 obligations — EXTERN:1 FINDING:7 TODO:8
L2 — logic
| obligation | detail | |
|---|---|---|
| FINDING | L2/W-syn — W1–W4 on the synthesis netlist | synthesis netlist absent (rerun the flow): /home/runner/work/thinking-sand/thinking-sand/flow/rocket-sram22/runs/gds3/06-yosys-synthesis/ChipTop.nl.v (0.0s) |
| FINDING | L2/W-routed — W1–W4 on the post-route netlist | post-route netlist absent (rerun the flow): /home/runner/work/thinking-sand/thinking-sand/flow/rocket-sram22/runs/gds3/43-openroad-detailedrouting/ChipTop.nl.v (0.0s) |
| FINDING | L2/macros — the SRAM macro census: five instances of three kinds | synthesis netlist absent (rerun the flow) (0.0s) |
| FINDING | L2/deletion-classes — the physical/clock/logic deletion fractions of the routed netlist | post-route netlist absent (rerun the flow) (0.0s) |
| FINDING | L2/rho-recoverable — is the register correspondence ρ recoverable post-hoc from the netlist? (F5) | synthesis netlist absent (rerun the flow) (0.0s) |
| FINDING | L2/scoped-cec — RTL ≡ netlist on a real cone, by name-matching (the L3 pipeline, run) | CEC ran but did not report a clean prove: — ### synthesising AMOALU standalone -> /home/runner/work/thinking-sand/thinking-sand/flow/rocket-sram22/cec/work/AMOALU/AMOALU.nl.v (0.0s) |
| TODO | L2/macro-contracts — the three SRAM contracts stated; tie-offs verified structurally | [blocked on: authoring the contract format; the macro Verilog is the draft source] |
| TODO | L2/cec-fullchip — the whole-ChipTop verdict (the scoped pipeline already closes — see scoped-cec) | [blocked on: compute. Two routes, both matching by name (ρ) with no hint file. (a) eqy partitions per flop and re-flattens the whole design per partition — ~10,900 partitions, serial combine ran ~95% (21,329 flatten passes) before a 2h cap, ahead of the parallel SAT sweep. (b) cec/fullchip-equiv.sh: ONE miter via yosys-native equiv_make/equiv_simple/equiv_induct (async2sync is load-bearing — the netlist has async-reset flops equiv's SAT can't model; SRAM macros boxed). equiv_simple's coverage (how many cone functions are proven identical) is the meaningful L3 number; equiv_induct's base case cannot close from ARBITRARY state because of unreset data registers (see CEC-NOTES.md / IBuf). RAN (route b): equiv_make matched 642 cones by name at full scale (ρ confirmed), but equiv_simple proved only 6/642 — the free-register-init wall dominates even the combinational check at 61k cells, and equiv_induct exploded past 10GB without closing (killed to protect the sandbox). So the native single-miter route does NOT yield a clean full-chip verdict; the eqy per-partition route (which cuts combinationally at register boundaries) or reset-sequence modelling is needed. The scoped-cec AMOALU pass remains the proof the pipeline itself is sound] |
| TODO | L2/cec-sequential-clean — a CLEAN sequential-cone pass (IBuf: register match by Q-net, all cones) | [blocked on: equiv_induct + don't-care pruning. run-cec.sh IBuf IBuf.sv RVCExpander.sv reproduces the ρ signature (53 flops, buf_pc/buf_data/nBufValid preserved on Q-nets) and proves 198/212 cones first pass; the residual is the cost of carving a module out of its parent (unreset-flop init freedom + boundary observability don't-cares, e.g. equiv_make matching a gold bit against literal 1'x), not a logic bug — the AMOALU clean pass confirms the flow. Closing it cleanly needs the in-context full-chip run or don't-care handling] |
9 obligations — FINDING:6 TODO:3
L1 — the electrical layer
| obligation | detail | |
|---|---|---|
| FINDING | L1/drc-triage — BEOL DRC verdict, macro-internal hits separated by coordinate clustering | DRC database absent (rerun the tiled deck): /home/runner/work/thinking-sand/thinking-sand/flow/rocket-sram22/runs/gds3/58-klayout-drc/reports/drc.klayout.beol2.lyrdb (0.0s) |
| FINDING | L1/routing-witness — the router's own no-opens/no-shorts witness, re-verified from the routed DEF | routed DEF absent (rerun the flow): /home/runner/work/thinking-sand/thinking-sand/flow/rocket-sram22/runs/gds3/43-openroad-detailedrouting/ChipTop.def (0.0s) |
| TODO | L1/gds-admissible — the admissible-GDS subset check on the streamed layout (no PATH type 1, no self-intersection, 90-degree SREFs) | record-level scan; gdsdump.py already walks the records — promote it to a verdict. Cheapest L1 item and the front end for everything below. |
| TODO | L1/h1h2-inv1 — (H1)/(H2) — erode-connectivity and colour-aware spacing on inv_1, then a cell row | [blocked on: polygon morphology (erosion/dilation + union-find over scanline geometry)] |
| TODO | L1/lvs-inv1 — extraction + LVS of inv_1 against its schematic; (D1)-(D3) sized on the same cell | [blocked on: magic/netgen in the environment, or a minimal extractor over the flattened colouring. This is the CELL-MASTER half of the L1/02 decomposition — the routing-witness check already covers chip connectivity; extraction is now needed only on the finite library (composes with L0/06 celltopo on the same cells) plus the deterministic streamout validation] |
| TODO | L1/g1-taps — G1: every device within d_max of a well tap (discharges V5/M1's side condition) | [blocked on: parsing placement from caravel_core.def (398,259 COMPONENTS) + the extraction for device sites] |
| FINDING | L1/g3-antenna — G3: antenna ratios after diode repair | no antenna-check step found in the run (0.0s) |
| FINDING | L1/g6-fill-tied — G6: no floating fill — the screen is grounded by construction | routed DEF absent (rerun the flow) (0.0s) |
| TODO | L1/g5-shield — G5: shielding coverage — grid metal actually interposed between coupled nets | [blocked on: the coupling graph (extraction window per net); the design-side half of M2's hypothesis] |
| TODO | L1/density-map — pattern-density map (feeds the CMP thickness correction and local-bias r(x)) | windowed area sums over the GDS — mechanical once the polygon front end exists |
| EXTERN | L1/E7-H3 — as-fabricated geometry within tolerance; no spurious islands (H3) | quantifies over the fabricated set A — no program over shipped data reaches it |
| FINDING | L1/sdc-inventory — the constraint file: declared clocks and (absent) exceptions | SDC absent (rerun the flow): /home/runner/work/thinking-sand/thinking-sand/flow/rocket-sram22/runs/gds3/43-openroad-detailedrouting/ChipTop.sdc (0.0s) |
| FINDING | L1/domain-census — every sequential clock pin traces to a declared clock (F3's table) | netlist/SDC absent (rerun the flow) (0.0s) |
| FINDING | L1/gating-census — the clock-gate cells enumerated (the ICG primitive's instances) | netlist absent (rerun the flow) (0.0s) |
| FINDING | L1/nine-corner — the flow's multi-corner STA closure verdict | STA reports absent (rerun the flow) (0.0s) |
| FINDING | L1/domain-violations — table lookups inside the characterised region (F2's instrument) | STA reports absent (rerun the flow) (0.0s) |
| TODO | L1/verified-sta — re-derive the timing verdict with verified interval rules | [blocked on: proof-phase machinery] |
| TODO | L1/sync-inventory — every crossing lands on a framework synchroniser shape; the P1 ledger | [blocked on: enumerating AsyncQueue/AsyncResetSynchronizer instances against the domain census] |
| EXTERN | L1/P6 — environment within spec — now carrying the board clock's period/jitter contract | no theorem constrains the world; the clock_tap pad makes the contract bench-checkable |
19 obligations — EXTERN:2 FINDING:9 TODO:8
L0 — physics
| obligation | detail | |
|---|---|---|
| FINDING | L0/ccc — every combinational cell's transistors compute its Liberty function (C1–C3) | PDK cell CDL/Liberty absent (persistent PDK root); the check is tools/celltopo.py (0.0s) |
| FINDING | L0/v1a-tristate — the FLOAT set is exactly the closed non-static-CMOS exception list | PDK cell CDL/Liberty absent; the check is tools/celltopo.py (0.0s) |
| FINDING | L0/spice-screen — Liberty delays agree with a BSIM4 SPICE eval at the tt corner (analog screen) | ngspice not built (tools/install-toolchain.sh, or build from the SF git mirror to $TS_SCRATCH/ngspice-inst); the screen is tools/spicecheck.py (0.0s) |
| TODO | L0/inv1-enclosure — the RIGOROUS enclosure: conservative interval BSIM4 evaluation bounding Liberty | [blocked on: an interval DAE integrator wired to an interval BSIM4 evaluation (the layer's central build). The spice-screen check is the empirical precursor — it point-samples agreement; the enclosure must BOUND, replacing the point SPICE with an interval that contains the true device response over the operating box — now including a mechanical-stress coordinate and a bounded exogenous forcing (a disturbance-reachability tube; L0/04 V9/V10)] |
| TODO | L0/envelope-num — numeric envelope margins: operating voltage vs avalanche, F2 slew vs crowbar, mechanical-stress and EM-forcing bounds (V9/V10) | [blocked on: the PDK device ratings, and the package/EM qualification limits (JESD22; IEC 61000-4 / 62132), at pinned SHAs] |
| TODO | L0/noise-exponent — the thermal-discharge arithmetic as a checked computation (barrier / kT per node class) | pure arithmetic over C, V, T once node capacitances are extracted; cheap after L1 extraction exists |
| TODO | L0/quantum-budget — gate leakage + RTN + dopant scatter vs the noise-margin budget (L0/05 open problem 2) | [blocked on: the SKY130 BSIM4 model cards at pinned SHAs] |
| EXTERN | L0/E1 — the compact-model enclosure contains the true device | the tower's one physical axiom; validated by measurement, not checkable from shipped data |
| EXTERN | L0/M1-M8 — the open mathematics (uniqueness, screening, lumping, monotonicity, bridge, constants, regimes, eigenvalue) | proof-phase material by definition; listed so the scoreboard is the complete census |
9 obligations — EXTERN:2 FINDING:3 TODO:4
Scoreboard — checker results
Generated by tools/check-all.py --md from commit 5a24f5e on 2026-09-02 09:26 UTC, against the flow-generated artifacts of data provenance — the same run that built this book. Every obligation the book states appears exactly once; the README documents the suite.
PASS — the check ran and the obligation holds of the generated artifacts. FINDING — the check ran and confirms an adverse fact recorded in Findings (expected). FAIL — the shipped data contradicts the record; a bug in artifact, record, or checker. TODO — not yet checkable; the stub names its blocker. EXTERN — axiom-register material no program over shipped data can reach.