L5/06 — The device models

Edge: this file is the theorem the node carries — the device models (UART, IRQ/CLINT/PLIC, boot, serial-TileLink) that compose with the ISA into Sys (ISA ⊕ devices ⟹ Sys), the composition edge. The memory-map object they attach to is the node, 03.

The models to write

Memory map: an address-decode function addr → (region, device, offset) — extracted from the RTL's decode logic and diffed three ways against the device tree and the register maps; then cast as the formal decode component, including the error-device routing on holes, exported to 02's A5 and to L3's load/store lemmas. The extracted table itself and its RTL-vs-metadata diff are the node's, 03; here it enters the composition.

The IRQ map: which physical event drives which line of L4/01's interrupt array — the system half of interrupts, deliberately not in the portable spec. The shape is standard RISC-V: CLINT compare drives mtip, CLINT software-interrupt register drives msip, and the PLIC drives meip, with the UART as PLIC source 1. Where an interrupt persists is the PLIC's gateway-and-pending machinery (level-triggered gateways, claim/complete, priority threshold) — L4/01's pending CSR is a live view — so the PLIC model is a required component of Sys, carrying the no-lost-interrupts half of L3/07's delivery obligation.

UART: the observable channel — divisor register semantics, bit-cell generation against the bus clock, transmit/receive FIFOs and watermark interrupts, the TX trace feeding 00's derivation stack; RX's synchroniser is L1/11's business, its byte semantics here.

Boot machinery: the ROM's contents as data, the boot-address register, and the custom_boot pin — together they determine the first fetch address and hence what "with image F" means in every end-to-end statement; the load paths (resident ROM, debug-module writes, serial-link writes) are each a spec-level way for F to arrive.

Serial TileLink bridge: phit serialisation and clock crossing on the chip side — the piece that turns 02's B(config) into a function of the link clock ratio; the far side is X4.

Obligations

1. The five models above as components of Sys's composition (00 obligation 3) — for the map, that is the extracted table plus the error-device semantics on holes, as a formal decode function. The extraction and diff of that table are the node's, 03.

Effort

Months, wide and mechanical; the models are small individually and the composition into Sys is the deliverable. The memory-map object and its diff live in the node, 03.