L3/06 — The buses and the debug module

Node: this file is the object — the tile's TileLink ports and the debug module as structure. The request-discipline guarantees the core proves (the interface half of the refinement edge) are the edge, 11.

Background

This chapter proves the core's half of the bargains struck at its external ports. The general story — what a bus is, why memory latency varies, and how assume-guarantee reasoning splits an interface proof into promises proved by each side separately — is introduced in L5/02's background, worth reading first; L5 authors the fabric's promises to the core, and here the core proves its own request discipline in return.

The protocol at the tile's ports is TileLink: requests on the A channel (opcode, address, size, source ID), responses on the D channel tagged with the matching source ID, valid/ready handshakes per beat, multi-beat bursts for transfers wider than the bus. The fetch side issues cache-line refill bursts — a line-aligned read streamed over consecutive beats; the data side issues the accesses the DTIM and the memory map serve, including the A extension's atomic operations, which TileLink carries as first-class opcodes rather than as read-modify-write sequences improvised by the master.

One more port exists that most tours omit: the debug module, through which an external agent over JTAG can halt the core, single-step it, and run abstract commands — reaching architectural state without going through the program. For refinement purposes it is a side door, and the standard treatment is the one L2/05 gives scan chains: state the theorem conditional on the door staying shut, and spec the door separately via the RISC-V debug specification's own register model when it is used.

Statement

The tile's TileLink masters and the debug module, as contracts: what the core guarantees about its requests (proved here), what it assumes about responses (L5's contract, with its latency bound B), and the debug-inactive conditionality stated once.

The instruction port

The I-cache's refill master. Its request-discipline guarantees — Gi1–Gi3, provable as invariant clauses (09 clause 7) — are stated with the other obligations in 11. Assumed in return: the D-beat within B per beat, data valid at the beat, boot-region reads return F's contents (L5's A4, with the split between bridge-proved and far-agent-assumed marked there).

The data port

The data-side master; its guarantees Gd1–Gd4 are stated in 11, and the assumed half mirrors the instruction port's.

The debug module

The standard debug architecture: a debug module on the peripheral bus, driven by a debug transport module that terminates the JTAG pins, with halt-request/resume/abstract-command machinery reaching the core. Two facts shape the treatment. First, the module's register model is imported — the RISC-V debug specification defines dmcontrol, abstractcs, and friends — so unlike a bespoke debug unit there is a document to be faithful to rather than semantics to author. Second, the module is also a bus master: system-bus access lets the external agent read and write memory directly, which is one of the load paths for F (L5/03). The refinement is stated conditional on debug-inactive (no halt request in flight, no abstract command executing); the conditionality is one hypothesis, threaded once through 08's statement. The hardware-side obligation that discharges it — inactive means invisible — is the non-interference lemma stated in 11.

What the absences buy

No coherence protocol in flight (the tiny configuration's bus topology is incoherent by construction), no store buffer, no miss queues beyond the single refill: the memory system is a small set of masters with static discipline, and the whole arch-class topic "memory hierarchy" reduces to the contracts above plus one latency bound. The counterfactual — caches with miss queues, store buffers with forwarding, a coherence protocol — is priced in 05's table; this file is the demonstration that the generated machine stays on the cheap side of it.

Effort

Days; the structural description is small — the two masters and the debug side door as objects, plus what their absences buy. The proof weight is in the guarantee clauses and the non-interference lemma, which are the edge, 11.