L5 — The system specification
Node — the top of the tower:
Sys(F)andobs, the two objects the overview's top-level statement quantifies over (00–05);Sys(F) = ISA ⊕ memory map ⊕ devices, with theISA ⊕ devices ⟹ Syscomposition — the edge into this node from L4 — carried by 03. No edge up: this is where the tower ends. A definition node — specification authoring, not proof. Consumes:ISA(L4), device datasheet models (X4).
Background
This is the first layer of the book and the top of the tower, and it answers a question that sounds administrative but is foundational: what is the end-to-end theorem about? Not the ISA — an instruction set has no pins, and no statement about it mentions a physical object. The only interface a chip has with the world is its pads, the few dozen metal contacts the package's pins bond to, so the top-level specification must be a set of allowed pad-signal histories, and everything standing between the processor core and the pads becomes spec rather than scenery: the memory map, the boot ROM and the serial TileLink port the program arrives by, the UART the output leaves by, the JTAG debug port, and the power supply's arrivals, sags, and departures.
The chapters build exactly that. 00 defines the two top-level objects; 01 decides which physical object the claim is about (core, SoC, or the device you can hold); 02 writes the promises core and fabric exchange; 03 models the peripherals; 04 handles power, including brown-out; 05 fences off the configurations the theorems don't cover. Each chapter's own Background introduces its protocols and mechanisms from scratch.
Statement
This layer owns the map from architecture to observable behaviour — Sys(F) = ISA ⊕ memory map ⊕ serial TileLink ⊕ UART ⊕ debug/boot machinery, rendered as timed pad traces, and obs as the physical observation (00). The boundary test with L4: move the core to an FPGA and L4 survives byte-for-byte while this layer is replaced wholesale — L5 is this chip.
Subcomponents
| status | ||
|---|---|---|
| 00 | The two definitions; the physical trace alphabet (forced by epoch composition) with byte views derived | weeks; everything plugs in here |
| 01 | B1 core → B2 SoC → B3 device as successive theorems; X4 as a per-level dial | decision + the B3 smoke test |
| 02 | The bus contract: the TileLink assume-clauses and the load-bearing latency bound B(config); discharged at B2 | days to author |
| 03 | Memory map, IRQ map, UART, boot devices — the generator's sources consolidated, diffed against the RTL | months, wide |
| 04 | Epoch composition: V8, POR, X-elimination, boot promise, F-immutability, brown-out + supervisor | composition: weeks |
| 05 | The recommended-operating-conditions clause: register-reachable knobs (clock gating, tile reset, boot select), X-flood semantics of "unspecified" | days; the slot matters |
Interfaces
Consumes: ISA (L4), L3's configuration record, the SoC RTL and its generated device tree (as 03's raw material), X4's models per B-level. Exports: Sys(F) and obs to the overview; the bus contract and B to L3; the configuration objects to the operating-conditions clause; the epoch requirements to the board (supervisor, sequencing).
Axioms introduced
X4 (device datasheet models) — a scoping dial, not a monolith: B1 needs none, B2 the on-die batch, B3 all of it, including whatever agent sits across the serial TileLink port; each theorem conditional on exactly its batch (01).
The layer's shape
Two definitions and four consequences. 00 fixes the objects, with the alphabet choice forced from below (epochs need prefix closure, which only the physical level has). 01 fixes what the claim is about, in three widening rings. The remaining files are the composition's components: the interface half (02), the address-and-device half (03), time's outer structure (04), and the domain clause (05). The recurring find of the layer: the SoC's small control devices keep receiving their formal jobs here — the boot-address register (boot promise), the tile-reset setter (epoch structure), the clock gater (operating-conditions knob), the error device (the bus contract's failure clause) — continuing the pattern that nothing in this design is decorative.
Open problems
- Author the bus contract (02) — gates L3's refinement statement; days.
- The RTL-vs-generated-metadata diffs (03) — drift between RTL, device tree, and register maps is the expected finding.
- The UART framing-error decision and the rest of 00's derivation stack.
- The F-immutability check and the supervisor inequalities (04).
- Whether the pad ring and the serial-TileLink far end get behavioural models (B3) or the claim stops at B2 (01).
First experiments
- Write the B1 bus contract and check it against the tile's TileLink transactions in simulation (02) — unblocks L3.
- Extract the memory map from the RTL, diff against the generated device tree and register maps (03).
- State B3 for one hello-world image — "with F = this image in the boot path, the UART emits 'hello' at the configured baud" — fully formally, even unproven: it exercises every definition in the layer and will surface each one that is missing (01).
Effort
~6 months, definitional. The risk profile matches L4: errors here are invisible to every layer below and produce a true theorem about the wrong system.
Reading
The TileLink specification — the protocol 02's contract restricts. The RISC-V debug specification (the JTAG port is a pad-visible agent with its own protocol). The generated device tree and register maps — 03's provenance table maps them.