L3/11 — The bus and debug obligations

Edge: this file is the theorem the node carries — the request-discipline guarantees the core proves, entering 09's invariant as clauses, the interface half of the L3→L4 refinement edge. The ports and debug module as structure are the node, 06.

The core's half of the port bargains, as the clauses it guarantees. What the ports are — the instruction and data masters, the debug side door, and what their absences buy — is the node, 06; here are the promises those masters prove.

The instruction-port guarantees

The I-cache's refill master. Guarantees, provable as invariant clauses (09 clause 7):

Gi1  refills are well-formed: line-aligned base, legal size, a single
     source ID per outstanding refill, beats accepted per the handshake
Gi2  a refill, once started, is not abandoned (except by reset)
Gi3  fetch addresses are execute-region addresses (no device-region fetches)

The data-port guarantees

The data-side master:

Gd1  requests are legal TileLink: aligned to their size, permitted opcodes,
     source IDs within the negotiated set, stable until accepted
Gd2  byte masks well-formed and consistent with the retiring access width
Gd3  no speculative writes: a store's request issues only for a retiring store
Gd4  atomic requests carry the correct AMO opcode and operand; an SC issues
     only against its own valid reservation

Gd3 is where the pipeline meets the memory: flushed instructions must not have touched the bus.

The debug non-interference lemma

The hardware-side obligation for the debug module is only that inactive means invisible — a non-interference lemma of the same shape as 07's masked-interrupt one. It discharges the debug-inactive hypothesis (no halt request in flight, no abstract command executing) that the node (06) threads once through 08's statement.

Obligations

  1. Gi1–Gi3 and Gd1–Gd4 as invariant clauses, with the simulation oracle re-run against this core first (execute a real image with the clauses asserted continuously; a clause that survives a real run is worth stating, and one that does not is found here rather than in a proof attempt).
  2. The debug non-interference lemma, and the debug-inactive hypothesis threaded through the statement.
  3. The burst-length/line-size agreement between the cache and the refill master (one constant, two readers — pin it in the configuration record).

Effort

Weeks; the protocol clauses are IC3-shaped. The value is in the statement discipline — every later surprise about "what does the bus promise" lands here or in L5, never diffusely.