Janus

8. Synchronous-Read Cell🔗

The generated cell reads its memories combinationally: it presents an address and uses the returned word in the same cycle. A technology SRAM macro, like the sky130 macro bound in the synthesis chapter, is synchronous-read: the word is registered and valid one cycle after the address. A cell that binds such macros for every memory must therefore stage each read. This chapter gives that fully synchronous cell an abstract model and proves it commits exactly what the combinational cell does.

The model runs each instruction as three non-overlapped phases. A fetch phase presents the program counter and latches the instruction register. A read phase presents the operand addresses and latches the loaded data word, resident weight, and streamed operand. An execute phase applies the latched instruction and operands. Because the phases never overlap, no architectural state changes between reading an operand and using it, so a latched read equals a live read: the load-use argument is a stability argument, not a hazard argument.

namespace Janus inductive SyncPhase where | fetch | read | exec deriving Repr, DecidableEq structure SyncCell where arch : State defaultConfig imem : Nat -> DecodedInstr busy : Bool phase : SyncPhase ir : DecodedInstr ldv : Word defaultConfig wv : Elem defaultConfig sv : Elem defaultConfig

execLatched is the execute-phase transition. It is execDecoded with its three memory reads replaced by latched values: the loaded data word for ld, and the resident weight and streamed operand for kmac. Every other instruction reads only registers and immediates and is unchanged.

def execLatched (d : DecodedInstr) (ldw : Word defaultConfig) (wv sv : Elem defaultConfig) (s : State defaultConfig) : State defaultConfig := match d.op with | .mac => let x := elemOfWord defaultConfig (readReg s d.ra) let y := elemOfWord defaultConfig (readReg s d.rb) retire (setAcc s (accAddProduct defaultConfig s.acc x y)) (nextPC defaultConfig s.pc) | .kmac => let s1 := setAcc s (accAddProduct defaultConfig s.acc wv sv) retire (setPtrs s1 (nextLocal defaultConfig s.wptr) (nextLocal defaultConfig s.sptr)) (nextPC defaultConfig s.pc) | .clracc => retire (setAcc s 0) (nextPC defaultConfig s.pc) | .movacc => let v := wordOfInt defaultConfig s.acc.toInt retire (setRegs s (updReg s.regs d.rd v)) (nextPC defaultConfig s.pc) | .li => let v := wordOfInt defaultConfig d.imm retire (setRegs s (updReg s.regs d.rd v)) (nextPC defaultConfig s.pc) | .ld => retire (setRegs s (updReg s.regs d.rd ldw)) (nextPC defaultConfig s.pc) | .st => let addr := memIndexOfWord defaultConfig (readReg s d.ra) let value := readReg s d.rb retire (setData s (updMem s.data addr value)) (nextPC defaultConfig s.pc) | .setwptr => retire (setPtrs s (localAddrOfNat defaultConfig d.addr) s.sptr) (nextPC defaultConfig s.pc) | .setsptr => retire (setPtrs s s.wptr (localAddrOfNat defaultConfig d.addr)) (nextPC defaultConfig s.pc) | .blz => let pc' := if (readReg s d.ra).toInt <= 0 then branchPC defaultConfig s.pc d.imm else nextPC defaultConfig s.pc retire s pc' | .halt => retireHalt s -- Latching the operands from a state and then executing equals executing that -- state directly: the latched reads are exactly the reads `execDecoded` makes. theorem execLatched_eq (d : DecodedInstr) (s : State defaultConfig) : execLatched d (readData s (memIndexOfWord defaultConfig (readReg s d.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded d s := d:DecodedInstrs:State defaultConfigexecLatched d (readData s (memIndexOfWord defaultConfig (readReg s d.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded d s s:State defaultConfigop:CellOprd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s s:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s s:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } ss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:NatexecLatched { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } (readData s (memIndexOfWord defaultConfig (readReg s { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra))) (readWeight s (memIndexOfLocal defaultConfig s.wptr)) (readStream s (memIndexOfLocal defaultConfig s.sptr)) s = execDecoded { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s All goals completed! 🐙

One clock advances one phase. Fetch and read leave the architectural state untouched; only execute changes it.

def syncStep (c : SyncCell) : SyncCell := if c.busy then if c.arch.halted then c else match c.phase with | .fetch => { c with ir := c.imem (memIndexOfNat defaultConfig c.arch.pc.toNat), phase := .read } | .read => { c with ldv := readData c.arch (memIndexOfWord defaultConfig (readReg c.arch c.ir.ra)), wv := readWeight c.arch (memIndexOfLocal defaultConfig c.arch.wptr), sv := readStream c.arch (memIndexOfLocal defaultConfig c.arch.sptr), phase := .exec } | .exec => let arch' := execLatched c.ir c.ldv c.wv c.sv c.arch { c with arch := arch', phase := .fetch, busy := !arch'.halted } else c

A fetch, a read, and an execute together advance the architectural state by exactly one decoded instruction, the same value the combinational cell produces in one cycle. The synchronous reads change when each result is committed, not what it is.

theorem syncCell_three_cycles (c : SyncCell) (hbusy : c.busy = true) (hhalt : c.arch.halted = false) (hphase : c.phase = .fetch) : (syncStep (syncStep (syncStep c))).arch = execDecoded (c.imem (memIndexOfNat defaultConfig c.arch.pc.toNat)) c.arch := c:SyncCellhbusy:c.busy = truehhalt:c.arch.halted = falsehphase:c.phase = SyncPhase.fetch(syncStep (syncStep (syncStep c))).arch = execDecoded (c.imem (memIndexOfNat defaultConfig (BitVec.toNat c.arch.pc))) c.arch c:SyncCellhbusy:c.busy = truehhalt:c.arch.halted = falsehphase:c.phase = SyncPhase.fetchexecLatched (c.imem (memIndexOfNat defaultConfig (BitVec.toNat c.arch.pc))) (readData c.arch (memIndexOfWord defaultConfig (readReg c.arch (c.imem (memIndexOfNat defaultConfig (BitVec.toNat c.arch.pc))).ra))) (readWeight c.arch (memIndexOfLocal defaultConfig c.arch.wptr)) (readStream c.arch (memIndexOfLocal defaultConfig c.arch.sptr)) c.arch = execDecoded (c.imem (memIndexOfNat defaultConfig (BitVec.toNat c.arch.pc))) c.arch All goals completed! 🐙 theorem syncCell_returns_to_fetch (c : SyncCell) (hbusy : c.busy = true) (hhalt : c.arch.halted = false) (hphase : c.phase = .fetch) : (syncStep (syncStep (syncStep c))).phase = .fetch := c:SyncCellhbusy:c.busy = truehhalt:c.arch.halted = falsehphase:c.phase = SyncPhase.fetch(syncStep (syncStep (syncStep c))).phase = SyncPhase.fetch All goals completed! 🐙

The synchronous cell commits the same architectural state as the combinational cellExecCycle, and by the execute-path refinement it refines the ISA step function across its three cycles.

theorem syncCell_matches_combinational (c : SyncCell) (hbusy : c.busy = true) (hhalt : c.arch.halted = false) (hphase : c.phase = .fetch) : (syncStep (syncStep (syncStep c))).arch = (cellExecCycle { arch := c.arch, imem := c.imem, busy := c.busy }).arch := c:SyncCellhbusy:c.busy = truehhalt:c.arch.halted = falsehphase:c.phase = SyncPhase.fetch(syncStep (syncStep (syncStep c))).arch = (cellExecCycle { arch := c.arch, imem := c.imem, busy := c.busy }).arch c:SyncCellhbusy:c.busy = truehhalt:c.arch.halted = falsehphase:c.phase = SyncPhase.fetchexecDecoded (c.imem (memIndexOfNat defaultConfig (BitVec.toNat c.arch.pc))) c.arch = (cellExecCycle { arch := c.arch, imem := c.imem, busy := c.busy }).arch All goals completed! 🐙 theorem syncCell_refines_isa (c : SyncCell) (hbusy : c.busy = true) (hhalt : c.arch.halted = false) (hphase : c.phase = .fetch) : step defaultConfig (programOf c.imem) c.arch = some (syncStep (syncStep (syncStep c))).arch := c:SyncCellhbusy:c.busy = truehhalt:c.arch.halted = falsehphase:c.phase = SyncPhase.fetchstep defaultConfig (programOf c.imem) c.arch = some (syncStep (syncStep (syncStep c))).arch c:SyncCellhbusy:c.busy = truehhalt:c.arch.halted = falsehphase:c.phase = SyncPhase.fetchstep defaultConfig (programOf c.imem) c.arch = some (execDecoded (c.imem (memIndexOfNat defaultConfig (BitVec.toNat c.arch.pc))) c.arch) All goals completed! 🐙

Running the cell is iterating the clock; an n-instruction program retires in 3 * n cycles because each instruction is a fetch/read/execute triple, and after each triple the cell is back in its fetch phase.

def syncRun : Nat -> SyncCell -> SyncCell | 0, c => c | k + 1, c => syncRun k (syncStep c) def syncCellCycles (n : Nat) : Nat := 3 * n theorem syncCellCycles_three_per_instr (n : Nat) : syncCellCycles (n + 1) = syncCellCycles n + 3 := n:NatsyncCellCycles (n + 1) = syncCellCycles n + 3 n:Nat3 * (n + 1) = 3 * n + 3; All goals completed! 🐙 end Janus

This model is emitted as generated SystemVerilog. Alongside the combinational janus_cell, the renderer produces rtl/janus_cell_sync.sv: a second cell whose program, resident-weight, and stream memories are registered-read janus_sram_sync_32 adapters and whose scalar-data load port is the registered port of a janus_sram_sync_64 adapter. The SRAM output registers are the cell's instruction and operand latches, so synchronous SRAM macros bind directly with no extra logic. A separate combinational debug port keeps host inspection async. The generated cell follows the same three-phase sequence proved above and passes the same golden program suite as the combinational cell, retiring identical architectural results over three times as many clocks.

This closes the cycle-faithfulness gap left by the macro-adapter synthesis: every architectural read in the cell is now a registered-read stage with a proved refinement and a generated RTL cell, matching synchronous SRAM macros instead of combinational arrays. The kernel operand path also has its throughput counterpart in the scheduling chapter, whose conservation law accounts for overlapping the MAC reads at any latency. Overlapping the phases for throughput, and timing the synchronous cell through place-and-route, are the remaining steps toward a fully macro-timed physical tile.