L3 — RTL semantics = the microarchitecture

Node — RTL semantics, which is the microarchitecture: ⟦RTL⟧, the word-level transition system of the source text, defined for the synthesisable subset this design actually uses (00–04) and toured as the generated Rocket core it elaborates to (05–07). Used on both sides of the tower: L2's CEC compares against it, and this layer's own edge refines from it. Edge up — the ISA refinement (the genuine abstraction step): ⟦RTL⟧ ⊑ ISA, a stuttering simulation (I, α, m) — carried by the refinement statement (08), the invariant (09), and the per-instruction obligations (10). The node is a definition (its risk is inverted: a wrong definition yields a true theorem about the wrong object, so its obligations are well-definedness and adequacy, not proof); the edge up is the tower's one irreducible theorem — the ← THE WORK arrow no tool produces and no measurement substitutes for.

This layer is the merge of two: defining what the RTL means, and proving that what it means implements the ISA. They are the same object at two depths of description — a clean synchronous transition system, which when you look at what it computes is a five-stage pipeline. The node fixes the object; the edge up is the refinement.

Background

Before anything can be proved about the RTL, the RTL must mean something. Verilog's official semantics is an event-driven simulator with deliberately loose scheduling — unusable as a proof object — so the node defines the design's meaning directly, as a clean synchronous transition system, for exactly the subset of the language this design occupies, with membership mechanically checked rather than assumed (00, 01). The two conditions that make combinational logic actually combinational are checked in 02; the treatment of unknown values and reset in 03; and the question no proof can answer — whether the definition captures what the artifact really means — is made detectable, since it cannot be made provable, in 04.

That same transition system, read for its structure rather than its semantics, is the layer a computer-architecture course would recognise: a processor implementing its instruction set. The edge up proves exactly that, and it is the tower's irreducible theorem — the one piece no tool produces. The proof technique is the simulation: an abstraction function reads architectural state out of the hardware at commit points, an invariant describes the machine's in-flight state well enough to survive induction, and a measure bounds how long any instruction can take — all introduced from scratch in 08's Background, with the machine's anatomy toured in 05. The invariant (09) is where the thinking concentrates; the rest is wide, shallow, and largely mechanisable (10, 06–07).

The node: RTL semantics

A semantics for the synthesisable subset this design actually uses — not for Verilog: the simple synchronous semantics (two-phase non-blocking commit over an acyclic combinational pass), with the relationship to the LRM's event scheduler isolated as the scheduler-independence claim — probed by adequacy checks, stateable as a theorem. The subset is measured over the emitted design: one level-sensitive block (the clock-gate primitive), one X-idiom (23 memory-read don't-care sites), one initializer idiom, and the worst of the language's categories absent by construction.

Read structurally, that object is the generated Rocket core: a five-stage in-order pipeline with a 4 KiB instruction cache, a full bypass network, three ratified extensions (M, A, C), and standard machine-mode trap machinery, with its buses and debug port as assume-guarantee interfaces (05–07). Defining the object and touring the microarchitecture are the same act at two granularities — which is exactly why the old "RTL semantics" and "microarchitecture" layers are one node here.

The edge up: the ISA refinement

⟦RTL⟧ ⊑ ISA: a stuttering simulation (I, α, m) — invariant, abstraction read at retirement, measure — conditional on the bus contract (L5) and stated over the configuration record. Displayed in full in 08; inventing the invariant I is the one thing in the entire project no tool produces (09). ⊑ is trace refinement up to stuttering, not equality: the implementation takes many cycles per architectural step, so the obligation is a stuttering simulation with a measure function, not a cycle-accurate correspondence. This is the genuine abstraction step of the tower — unlike the horizontal CEC below it, which is an equivalence between two descriptions of the same machine.

Subcomponents

Interfaces

Consumes: the emitted SystemVerilog design cone (~230 modules) and its FIRRTL ancestor; the elaborated configuration record; the licence to reason discretely (L1); the bus contract and its latency bound B (L5); the Sail import including the machine-mode subset (L4). Exports: ⟦RTL⟧ to L2 (the CEC's right-hand side) and back to this layer's own edge; the configuration record to L4 (ISA subset) and L5; the reset/X story to L5's epoch model; and the refinement theorem — the tower's ← THE WORK arrow — plus the retirement-gap bounds (the measure read quantitatively, 08), consumed by L5/04's epilogue sizing.

Axioms introduced

None. The node is a definition (it once mirrored the netlist-semantics axiom S1, but S1 is now derived by the stack below; ⟦RTL⟧ has no such derivation, which is exactly why 04's checks matter — the failure mode is detected by the CEC cross-check and differential simulation rather than silent). The edge up introduces none of its own either; it is where the others are cashed in, its conditionality explicit: on B (L5), on S2/S3's spec fidelity (L4's ledger), on the configuration record, and on debug-inactive (05, 06).

The layer's shape

The node is the admissible-subset move plus its receipts. 01 fixes the boundary and proves the awful constructs absent; 00 gives the clean semantics that is correct for that subset — with scheduler independence as the honest statement of why the LRM can be ignored; 02 checks the two conditions without which the semantics is undefined; 03 reconciles the two-valued idealisation with physical power-up; 04 makes definitional error detectable. The node stays small because the subset is small — the target-selection decision, and the census is its receipt.

The edge up then rides on the machine's own structure. 05 fixes what is being verified; the pipeline's stage structure organises everything: retirement at WriteBack defines the commit points (08), the inter-stage register banks organise the invariant per stage (09), and the bypass/interlock discipline is precisely what restores the cross-instruction independence the per-instruction obligations need (10). The ports where the world enters are assume-guarantee pairs, the debug port quarantined behind a conditionality (06); the interrupt machinery is checked against the imported standard spec, with the small custom residue isolated (07).

Open problems

1. The invariant (09) — irreducible; the IC3 calibration decides how much of it is tedium vs. thought.
2. Prove scheduler independence for the subset (00) — bounded, genuine, severable from the critical path.
3. The fence.i / I-cache agreement story (05, 09) — small state, real content.
4. The register power-up story against the hardened netlist (03).
5. The residual authored semantics — the custom control CSRs (L4/01) — decide and record before proving.

First experiments

For the node:

• Extract and record the elaborated configuration (gates three other layers' scoping — cheapest high-value item in the layer).
• The completeness and RTL SCC checks (02) — an afternoon each, and both are hard failures the front end should enforce thereafter.
• The differential harness on the design's own testbenches (04).

For the edge up:

• Write the refinement statement and α before any proof (08) — against the core's own trace port (the retirement interface the ecosystem's co-simulation uses), checked on simulation traces as a cheap oracle.
• Extract the stall/flush/bypass structure from the emitted RTL and derive the retirement-gap bounds (05, 08).
• The IC3 calibration on the structural clauses (09) — cheap, and it sizes the layer's real cost.

Effort

3–6 months for the node — the smallest definitional piece in the tower, unusually well-bounded because the scope was measured rather than assumed; the only cost beyond the subcomponent sum is the elaborator front end, shared with X1's parser work. Then 1.5–3 years for the edge up: the pipeline, the bypass network, and three live extensions put this machine several rows up the effort-multiplier table from a multicycle core, but the mitigations are real — no data-cache miss machinery (the data side is a scratchpad), no speculation in this configuration, no virtual memory, no FPU, and a designer-declared trace port as a ready-made α anchor. The irreducible content remains plausibly a few hundred lines of clauses plus glue; the rest is the project-wide infrastructure item (symbolic simulation, bitvector automation, the stuttering framework).

Reading

Lööw's HOL4 Verilog semantics — the existing deep embedding, and the reference point for how much of the language one actually needs. The FIRRTL spec — the IR the design actually descends through, and the node's long-term anchor (04). The rocket-chip repository — the generator source is the design intent. Burch & Dill on flushing, and Manolios on WEB refinement — the two standard α constructions for pipelined machines. Sawada & Hunt on intermediate abstractions. Fox's ARM6 verification — a pipelined commercial ISA against a real microarchitecture, the closest existing analogue. riscv-formal's RVFI discipline — the retirement-interface prior art α should stay comparable with.