3. RTL Contract🔗

The first RTL target is a single Janus cell. It is intentionally small: one 64-bit program counter, one 64-bit accumulator, eight 64-bit scalar registers, four 256-entry local memories, 32-bit resident weights, 32-bit streamed operands, and debug counters. The host loads memories through 16-bit local indexes while the cell is halted, pulses start, and then observes halted, pc, acc, cycles, and retired. Instruction, data, resident-weight, stream, and debug-data accesses use the low eight bits of the presented local address or program counter.

The four hot memories no longer live as bare inferred arrays inside the cell. They sit behind a janus_sram adapter submodule boundary: a synchronous-write, combinational-read model with a single write port and one read port for the program, weight, and stream memories, and two read ports for the scalar data memory (concurrent load and debug read). The adapter is exactly the interface a technology SRAM macro is bound onto during synthesis. The abstract read timing is still combinational, so the simulation and golden behavior are unchanged from the inferred-array cell.

This chapter fixes the external boundary used by the generated SystemVerilog. The cell is generated from a Lean RTL DSL value, not a raw SystemVerilog template. The execute path of that DSL value is proved to refine step; the plain-text SystemVerilog file is the renderer output checked by CI.

namespace Janus

inductive RtlDir where
  | input
  | output
deriving Repr, DecidableEq

structure RtlPort where
  name : String
  dir : RtlDir
  width : Nat
deriving Repr, DecidableEq

def janusCellPorts : List RtlPort :=
  [ { name := "clk", dir := .input, width := 1 },
    { name := "rst_n", dir := .input, width := 1 },
    { name := "start", dir := .input, width := 1 },
    { name := "instr_we", dir := .input, width := 1 },
    { name := "instr_addr", dir := .input, width := 16 },
    { name := "instr_wdata", dir := .input, width := 32 },
    { name := "data_we", dir := .input, width := 1 },
    { name := "data_addr", dir := .input, width := 16 },
    { name := "data_wdata", dir := .input, width := 64 },
    { name := "weight_we", dir := .input, width := 1 },
    { name := "weight_addr", dir := .input, width := 16 },
    { name := "weight_wdata", dir := .input, width := 32 },
    { name := "stream_we", dir := .input, width := 1 },
    { name := "stream_addr", dir := .input, width := 16 },
    { name := "stream_wdata", dir := .input, width := 32 },
    { name := "dbg_reg_sel", dir := .input, width := 3 },
    { name := "dbg_data_addr", dir := .input, width := 16 },
    { name := "halted", dir := .output, width := 1 },
    { name := "busy", dir := .output, width := 1 },
    { name := "pc", dir := .output, width := 64 },
    { name := "acc", dir := .output, width := 64 },
    { name := "wptr", dir := .output, width := 16 },
    { name := "sptr", dir := .output, width := 16 },
    { name := "cycles", dir := .output, width := 64 },
    { name := "retired", dir := .output, width := 64 },
    { name := "dbg_reg_value", dir := .output, width := 64 },
    { name := "dbg_data_value", dir := .output, width := 64 } ]

def rtlXlen : Nat := 64
def rtlElemBits : Nat := 32
def rtlAccBits : Nat := 64
def rtlAddrBits : Nat := 64
def rtlLocalAddrBits : Nat := 16
def rtlMemIndexBits : Nat := 8
def rtlMemDepth : Nat := 256
def rtlRegCount : Nat := 8
def rtlInstrBits : Nat := 32
def rtlOpcodeBits : Nat := 4
def rtlImmBits : Nat := 16

theorem rtlConfigMatchesDefault :
    rtlXlen = defaultConfig.xlen
      /\ rtlElemBits = defaultConfig.elemBits
      /\ rtlAccBits = defaultConfig.accBits
      /\ rtlAddrBits = defaultConfig.addrBits
      /\ rtlLocalAddrBits = defaultConfig.localAddrBits
      /\ rtlMemIndexBits = defaultConfig.memIndexBits
      /\ rtlRegCount = defaultConfig.regCount := by⊢ rtlXlen = defaultConfig.xlen ∧
  rtlElemBits = defaultConfig.elemBits ∧
    rtlAccBits = defaultConfig.accBits ∧
      rtlAddrBits = defaultConfig.addrBits ∧
        rtlLocalAddrBits = defaultConfig.localAddrBits ∧
          rtlMemIndexBits = defaultConfig.memIndexBits ∧ rtlRegCount = defaultConfig.regCount
  native_decideAll goals completed! 🐙

theorem rtl_memory_depth_matches_default :
    rtlMemDepth = memDepth defaultConfig := by⊢ rtlMemDepth = memDepth defaultConfig
  native_decideAll goals completed! 🐙

The instruction word is fixed at thirty-two bits:

bits [31:28]: opcode
bits [27:24]: destination register
bits [23:20]: first source register or branch-test register
bits [19:16]: second source register or store source register
bits [15:0]: signed immediate, branch offset, or pointer address

The branch target follows the architectural contract: when blz is taken, the new PC is pc + off, not pc + 1 + off.

def rtlOpcode {cfg : Config} : Instr cfg -> Nat
  | .mac _ _ => 0
  | .kmac => 1
  | .clracc => 2
  | .movacc _ => 3
  | .li _ _ => 4
  | .ld _ _ => 5
  | .st _ _ => 6
  | .setwptr _ => 7
  | .setsptr _ => 8
  | .blz _ _ => 9
  | .halt => 10

def rtlOpcodeMax : Nat := 10

theorem rtl_opcode_fits : rtlOpcodeMax < 2 ^ rtlOpcodeBits := by⊢ rtlOpcodeMax < 2 ^ rtlOpcodeBits
  native_decideAll goals completed! 🐙

theorem rtl_halt_opcode (cfg : Config) :
    rtlOpcode (cfg := cfg) .halt = 10 := rfl

theorem rtl_kmac_opcode (cfg : Config) :
    rtlOpcode (cfg := cfg) .kmac = 1 := rfl

end Janus

The low-eight-bit physical index is part of this initial standard-cell target, not an accidental truncation. The janus_sram adapter submodules are the macro-adapter contract: larger local memories and a fully technology-mapped macro are later physical integration steps that reuse this same boundary.

A first OpenLane2 sky130 run was made before the adapter existed, against the bare inferred-array cell. It is kept as a recorded warning about that earlier boundary: because the cell memories were inferred arrays, Yosys lowered the program, scalar-data, resident-weight, stream, and register memories into registers and muxes. The run reached Yosys synthesis and DFF legalization with 0 Yosys check problems, 0 remaining memories, 318547 cells, and 40994 mapped sky130 flip-flops. The final ABC mapping did not complete within the bounded run, so the book records no pre-PNR timing number for that inferred-memory target.

That result motivated the adapter. A single generated unit could be simulated and synthesized, but four 256-entry hot memories should not be implemented as flip-flop arrays in a useful physical tile. The janus_sram boundary now lets synthesis bind a technology memory macro in place of those arrays; the abstract cell keeps combinational-read timing, so a bound synchronous macro is a synthesis-shape experiment rather than a cycle-faithful implementation of the proved cell.