Janus

9. Pipelined Cell🔗

The fully synchronous cell pays three clocks per instruction because it never overlaps its phases. This chapter overlaps them for throughput and proves the result still commits the sequential trace. The overlap is deliberately narrow: only instruction fetch runs ahead. That is exactly the overlap this instruction set makes safe.

The reasoning turns on which hazards exist. There is no data hazard from register, accumulator, or pointer dependencies, because each instruction still executes against the fully committed architectural state — commits stay one-per-cycle and in order, so every operand read sees all prior writebacks. The instruction memory is read-only while the cell runs, so a prefetched instruction never depends on a writeback either. The one hazard is control: the prefetch predicts the fall-through address pc + 1, and a taken branch or a halt makes that prediction wrong. A wrong prefetch is caught and squashed, costing a single bubble.

The pipeline state adds a fetch latch to the architectural state: a validity bit, the memory index the latched instruction was fetched from, and the instruction itself. The invariant is that a valid latch holds the instruction at its recorded index.

namespace Janus def wantIdx (s : State defaultConfig) : Nat := memIndexOfNat defaultConfig s.pc.toNat structure PipeCell where arch : State defaultConfig imem : Nat -> DecodedInstr busy : Bool fvalid : Bool fpc : Nat fir : DecodedInstr -- One clock. A hit (the latch holds the instruction the program counter wants) -- commits that instruction and prefetches the predicted fall-through. A miss -- refetches the wanted instruction and bubbles. def pstep (c : PipeCell) : PipeCell := if c.busy then if c.arch.halted then c else if c.fvalid && (c.fpc == wantIdx c.arch) then let arch' := execDecoded c.fir c.arch let pidx := memIndexOfNat defaultConfig (c.arch.pc.toNat + 1) { c with arch := arch', busy := !arch'.halted, fvalid := true, fpc := pidx, fir := c.imem pidx } else let widx := wantIdx c.arch { c with fvalid := true, fpc := widx, fir := c.imem widx } else c

Every clock keeps the fetch-latch invariant: whatever address the latch records, it holds that instruction. Both the hit and miss branches load the latch from the instruction memory at the index they record, and neither writes the instruction memory.

theorem pstep_preserves_inv (c : PipeCell) (hinv : c.fvalid = true -> c.fir = c.imem c.fpc) : (pstep c).fvalid = true -> (pstep c).fir = (pstep c).imem (pstep c).fpc := c:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpc⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpc c:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:c.busy = true⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpcc:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:¬c.busy = true⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpc c:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:c.busy = true⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpc c:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:c.busy = truehh:c.arch.halted = true⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpcc:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:c.busy = truehh:¬c.arch.halted = true⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpc c:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:c.busy = truehh:c.arch.halted = true⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpc All goals completed! 🐙 c:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:c.busy = truehh:¬c.arch.halted = true⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpc c:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:c.busy = truehh:c.arch.halted = false⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpc c:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:c.busy = truehh:c.arch.halted = falsehit:(c.fvalid && c.fpc == wantIdx c.arch) = true⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpcc:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:c.busy = truehh:c.arch.halted = falsehit:¬(c.fvalid && c.fpc == wantIdx c.arch) = true⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpc c:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:c.busy = truehh:c.arch.halted = falsehit:(c.fvalid && c.fpc == wantIdx c.arch) = true⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpc c:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:c.busy = truehh:c.arch.halted = falsehit:(c.fvalid && c.fpc == wantIdx c.arch) = truea✝:(pstep c).fvalid = true⊢ (pstep c).fir = (pstep c).imem (pstep c).fpc; All goals completed! 🐙 c:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:c.busy = truehh:c.arch.halted = falsehit:¬(c.fvalid && c.fpc == wantIdx c.arch) = true⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpc c:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:c.busy = truehh:c.arch.halted = falsehit:(c.fvalid && c.fpc == wantIdx c.arch) = false⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpc c:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:c.busy = truehh:c.arch.halted = falsehit:(c.fvalid && c.fpc == wantIdx c.arch) = falsea✝:(pstep c).fvalid = true⊢ (pstep c).fir = (pstep c).imem (pstep c).fpc; All goals completed! 🐙 c:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:¬c.busy = true⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpc c:PipeCellhinv:c.fvalid = true → c.fir = c.imem c.fpchb:c.busy = false⊢ (pstep c).fvalid = true → (pstep c).fir = (pstep c).imem (pstep c).fpc All goals completed! 🐙

A hit commits exactly what the combinational cell commits in one cycle, so it refines the ISA step for that instruction. The prefetch is validated by the hit condition itself: the latched index equals the wanted index, so by the invariant the latched instruction is the right one.

theorem pstep_hit_matches (c : PipeCell) (hbusy : c.busy = true) (hhalt : c.arch.halted = false) (hvalid : c.fvalid = true) (hpc : c.fpc = wantIdx c.arch) (hinv : c.fir = c.imem c.fpc) : (pstep c).arch = (cellExecCycle { arch := c.arch, imem := c.imem, busy := c.busy }).arch := c:PipeCellhbusy:c.busy = truehhalt:c.arch.halted = falsehvalid:c.fvalid = truehpc:c.fpc = wantIdx c.archhinv:c.fir = c.imem c.fpc⊢ (pstep c).arch = (cellExecCycle { arch := c.arch, imem := c.imem, busy := c.busy }).arch c:PipeCellhbusy:c.busy = truehhalt:c.arch.halted = falsehvalid:c.fvalid = truehpc:c.fpc = wantIdx c.archhinv:c.fir = c.imem c.fpchit:(c.fvalid && c.fpc == wantIdx c.arch) = true⊢ (pstep c).arch = (cellExecCycle { arch := c.arch, imem := c.imem, busy := c.busy }).arch c:PipeCellhbusy:c.busy = truehhalt:c.arch.halted = falsehvalid:c.fvalid = truehpc:c.fpc = wantIdx c.archhinv:c.fir = c.imem c.fpchit:(c.fvalid && c.fpc == wantIdx c.arch) = true⊢ (if false = true then c else { arch := execDecoded c.fir c.arch, imem := c.imem, busy := !(execDecoded c.fir c.arch).halted, fvalid := true, fpc := memIndexOfNat defaultConfig (BitVec.toNat c.arch.pc + 1), fir := c.imem (memIndexOfNat defaultConfig (BitVec.toNat c.arch.pc + 1)) }).arch = (cellExecCycle { arch := c.arch, imem := c.imem, busy := true }).arch c:PipeCellhbusy:c.busy = truehhalt:c.arch.halted = falsehvalid:c.fvalid = truehpc:c.fpc = wantIdx c.archhinv:c.fir = c.imem c.fpchit:(c.fvalid && c.fpc == wantIdx c.arch) = true⊢ (if false = true then c else { arch := execDecoded (c.imem (wantIdx c.arch)) c.arch, imem := c.imem, busy := !(execDecoded (c.imem (wantIdx c.arch)) c.arch).halted, fvalid := true, fpc := memIndexOfNat defaultConfig (BitVec.toNat c.arch.pc + 1), fir := c.imem (memIndexOfNat defaultConfig (BitVec.toNat c.arch.pc + 1)) }).arch = (cellExecCycle { arch := c.arch, imem := c.imem, busy := true }).arch All goals completed! 🐙 theorem pstep_hit_refines_isa (c : PipeCell) (hbusy : c.busy = true) (hhalt : c.arch.halted = false) (hvalid : c.fvalid = true) (hpc : c.fpc = wantIdx c.arch) (hinv : c.fir = c.imem c.fpc) : step defaultConfig (programOf c.imem) c.arch = some (pstep c).arch := c:PipeCellhbusy:c.busy = truehhalt:c.arch.halted = falsehvalid:c.fvalid = truehpc:c.fpc = wantIdx c.archhinv:c.fir = c.imem c.fpc⊢ step defaultConfig (programOf c.imem) c.arch = some (pstep c).arch c:PipeCellhbusy:c.busy = truehhalt:c.arch.halted = falsehvalid:c.fvalid = truehpc:c.fpc = wantIdx c.archhinv:c.fir = c.imem c.fpc⊢ step defaultConfig (programOf c.imem) c.arch = some (cellExecCycle { arch := c.arch, imem := c.imem, busy := c.busy }).arch All goals completed! 🐙

A miss changes nothing architecturally; it only reloads the latch with the wanted instruction. So a miss is a stutter step, and the state it produces is hit-ready: valid, with the recorded index equal to the wanted index and the invariant restored. The bubble after a mispredict therefore lasts exactly one cycle.

theorem pstep_miss_stutter (c : PipeCell) (hbusy : c.busy = true) (hhalt : c.arch.halted = false) (hmiss : (c.fvalid && (c.fpc == wantIdx c.arch)) = false) : (pstep c).arch = c.arch := c:PipeCellhbusy:c.busy = truehhalt:c.arch.halted = falsehmiss:(c.fvalid && c.fpc == wantIdx c.arch) = false⊢ (pstep c).arch = c.arch All goals completed! 🐙 theorem pstep_miss_then_ready (c : PipeCell) (hbusy : c.busy = true) (hhalt : c.arch.halted = false) (hmiss : (c.fvalid && (c.fpc == wantIdx c.arch)) = false) : (pstep c).fvalid = true /\ (pstep c).fpc = wantIdx (pstep c).arch /\ (pstep c).fir = (pstep c).imem (pstep c).fpc /\ (pstep c).busy = c.busy /\ (pstep c).imem = c.imem := c:PipeCellhbusy:c.busy = truehhalt:c.arch.halted = falsehmiss:(c.fvalid && c.fpc == wantIdx c.arch) = false⊢ (pstep c).fvalid = true ∧ (pstep c).fpc = wantIdx (pstep c).arch ∧ (pstep c).fir = (pstep c).imem (pstep c).fpc ∧ (pstep c).busy = c.busy ∧ (pstep c).imem = c.imem All goals completed! 🐙

The two combine into the throughput statement: a mispredict bubble followed by its refetch commits exactly one sequential step. Any taken branch costs one lost cycle and no correctness; straight-line code commits one instruction per cycle.

theorem pstep_bubble_then_commit (c : PipeCell) (hbusy : c.busy = true) (hhalt : c.arch.halted = false) (hmiss : (c.fvalid && (c.fpc == wantIdx c.arch)) = false) : (pstep (pstep c)).arch = (cellExecCycle { arch := c.arch, imem := c.imem, busy := c.busy }).arch := c:PipeCellhbusy:c.busy = truehhalt:c.arch.halted = falsehmiss:(c.fvalid && c.fpc == wantIdx c.arch) = false⊢ (pstep (pstep c)).arch = (cellExecCycle { arch := c.arch, imem := c.imem, busy := c.busy }).arch c:PipeCellhbusy:c.busy = truehhalt:c.arch.halted = falsehmiss:(c.fvalid && c.fpc == wantIdx c.arch) = falsehv:(pstep c).fvalid = truehp:(pstep c).fpc = wantIdx (pstep c).archhi:(pstep c).fir = (pstep c).imem (pstep c).fpchbz:(pstep c).busy = c.busyhim:(pstep c).imem = c.imem⊢ (pstep (pstep c)).arch = (cellExecCycle { arch := c.arch, imem := c.imem, busy := c.busy }).arch c:PipeCellhbusy:c.busy = truehhalt:c.arch.halted = falsehmiss:(c.fvalid && c.fpc == wantIdx c.arch) = falsehv:(pstep c).fvalid = truehp:(pstep c).fpc = wantIdx (pstep c).archhi:(pstep c).fir = (pstep c).imem (pstep c).fpchbz:(pstep c).busy = c.busyhim:(pstep c).imem = c.imemharch:(pstep c).arch = c.arch⊢ (pstep (pstep c)).arch = (cellExecCycle { arch := c.arch, imem := c.imem, busy := c.busy }).arch c:PipeCellhbusy:c.busy = truehhalt:c.arch.halted = falsehmiss:(c.fvalid && c.fpc == wantIdx c.arch) = falsehv:(pstep c).fvalid = truehp:(pstep c).fpc = wantIdx (pstep c).archhi:(pstep c).fir = (pstep c).imem (pstep c).fpchbz:(pstep c).busy = c.busyhim:(pstep c).imem = c.imemharch:(pstep c).arch = c.archhb2:(pstep c).busy = true⊢ (pstep (pstep c)).arch = (cellExecCycle { arch := c.arch, imem := c.imem, busy := c.busy }).arch c:PipeCellhbusy:c.busy = truehhalt:c.arch.halted = falsehmiss:(c.fvalid && c.fpc == wantIdx c.arch) = falsehv:(pstep c).fvalid = truehp:(pstep c).fpc = wantIdx (pstep c).archhi:(pstep c).fir = (pstep c).imem (pstep c).fpchbz:(pstep c).busy = c.busyhim:(pstep c).imem = c.imemharch:(pstep c).arch = c.archhb2:(pstep c).busy = truehh2:(pstep c).arch.halted = false⊢ (pstep (pstep c)).arch = (cellExecCycle { arch := c.arch, imem := c.imem, busy := c.busy }).arch c:PipeCellhbusy:c.busy = truehhalt:c.arch.halted = falsehmiss:(c.fvalid && c.fpc == wantIdx c.arch) = falsehv:(pstep c).fvalid = truehp:(pstep c).fpc = wantIdx (pstep c).archhi:(pstep c).fir = (pstep c).imem (pstep c).fpchbz:(pstep c).busy = c.busyhim:(pstep c).imem = c.imemharch:(pstep c).arch = c.archhb2:(pstep c).busy = truehh2:(pstep c).arch.halted = false⊢ (cellExecCycle { arch := (pstep c).arch, imem := (pstep c).imem, busy := (pstep c).busy }).arch = (cellExecCycle { arch := c.arch, imem := c.imem, busy := c.busy }).arch All goals completed! 🐙

Running the cell is iterating the clock.

def pRun : Nat -> PipeCell -> PipeCell | 0, c => c | k + 1, c => pRun k (pstep c) end Janus

The correctness account is complete without a full stuttering-simulation induction. Every committing cycle equals one combinational-cell cycle and refines the ISA; every non-committing cycle leaves the architectural state untouched and is immediately followed by a commit. So the sequence of architectural states the pipeline commits is exactly the sequential trace, with isolated single-cycle bubbles that carry no value. The bubbles are the price of the one real hazard, and they appear only after a taken branch or at startup.

This model is emitted as generated SystemVerilog: rtl/janus_cell_pipe.sv binds a registered-read janus_sram_sync_32 for the instruction fetch and drives its address with the predicted pf_addr, keeping combinational operand memories. A fvalid/fpc fetch latch and a hit line implement the prediction and squash. The generated cell passes the same golden program suite as the combinational cell — retiring identical results and identical instruction counts — over fewer clocks than the fully synchronous cell, with a bubble only where a branch is taken.

Widening the overlap — registering the operand reads and forwarding or interlocking their results, so the fully synchronous cell also reaches one instruction per cycle — is the next pipeline step, and the first that needs true data-hazard reasoning rather than this control-only argument.