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 Honeycomb
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 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
s:State defaultConfigop:CellOprd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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:Nat⊢ execLatched { 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.fetch⊢ execLatched (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 := by c:SyncCellhbusy:c.busy = truehhalt:c.arch.halted = falsehphase:c.phase = SyncPhase.fetch⊢ (syncStep (syncStep (syncStep c))).phase = SyncPhase.fetch
simp [syncStep, hbusy, hhalt, hphase] 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 := by 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
rw [syncCell_three_cycles c hbusy hhalt hphase c:SyncCellhbusy:c.busy = truehhalt:c.arch.halted = falsehphase:c.phase = SyncPhase.fetch⊢ execDecoded (c.imem (memIndexOfNat defaultConfig (BitVec.toNat c.arch.pc))) 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⊢ execDecoded (c.imem (memIndexOfNat defaultConfig (BitVec.toNat c.arch.pc))) c.arch =
(cellExecCycle { arch := c.arch, imem := c.imem, busy := c.busy }).arch
simp [cellExecCycle, hbusy, hhalt] 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 := by c:SyncCellhbusy:c.busy = truehhalt:c.arch.halted = falsehphase:c.phase = SyncPhase.fetch⊢ step defaultConfig (programOf c.imem) c.arch = some (syncStep (syncStep (syncStep c))).arch
rw [syncCell_three_cycles c hbusy hhalt hphase c:SyncCellhbusy:c.busy = truehhalt:c.arch.halted = falsehphase:c.phase = SyncPhase.fetch⊢ step defaultConfig (programOf c.imem) c.arch =
some (execDecoded (c.imem (memIndexOfNat defaultConfig (BitVec.toNat c.arch.pc))) c.arch)] c:SyncCellhbusy:c.busy = truehhalt:c.arch.halted = falsehphase:c.phase = SyncPhase.fetch⊢ step defaultConfig (programOf c.imem) c.arch =
some (execDecoded (c.imem (memIndexOfNat defaultConfig (BitVec.toNat c.arch.pc))) c.arch)
exact execDecoded_refines_step c.imem c.arch hhalt 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 := by n:Nat⊢ syncCellCycles (n + 1) = syncCellCycles n + 3
simp [syncCellCycles] n:Nat⊢ 3 * (n + 1) = 3 * n + 3; omega All goals completed! 🐙
end Honeycomb
This model is emitted as generated SystemVerilog. Alongside the combinational
honeycomb_cell, the renderer produces rtl/honeycomb_cell_sync.sv: a second cell whose
program, resident-weight, and stream memories are registered-read
honeycomb_sram_sync_32 adapters and whose scalar-data load port is the registered
port of a honeycomb_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.