Skip to content

SignalDSL_Syntax.md

Latest commit

 

History

History
285 lines (222 loc) · 8.25 KB

SignalDSL_Syntax.md

File metadata and controls

285 lines (222 loc) · 8.25 KB

Signal DSL Syntax Reference for RV32 Rewrite

This document provides a side-by-side comparison of CircuitM (manual IR builder) and Signal DSL (recommended) patterns, specifically for the RV32I core rewrite.

Rule: Use Signal DSL for everything. Only fall back to CircuitM for vendor blackbox instantiation.

Wire / Constant

-- CircuitM (manual)
let w ← makeWire "result" (.bitVector 32)
emitAssign w (.const 42 32)

-- Signal DSL (recommended)
let w : Signal dom (BitVec 32) := Signal.pure 42#32

Arithmetic

-- CircuitM
let sum ← makeWire "sum" (.bitVector 32)
emitAssign sum (.op .add [.ref "a", .ref "b"])

-- Signal DSL
let sum := (· + ·) <$> a <*> b

Multiplexer

-- CircuitM
let result ← makeWire "result" (.bitVector 32)
emitAssign result (.op .mux [.ref "sel", .ref "thenVal", .ref "elseVal"])

-- Signal DSL
let result := Signal.mux sel thenVal elseVal

Register (D Flip-Flop)

-- CircuitM
let nextVal ← makeWire "next_val" (.bitVector 32)
emitAssign nextVal (.op .add [.ref regOut, .const 1 32])
let regOut ← emitRegister "counter" "clk" "rst" (.ref nextVal) 0 (.bitVector 32)

-- Signal DSL
let rec counter := Signal.register 0#32 (counter.map (· + 1))

Memory (BRAM)

-- CircuitM
let rdata ← emitMemory "dmem" 14 32 "clk"
  (.ref writeAddr) (.ref writeData) (.ref writeEn) (.ref readAddr)

-- Signal DSL
let rdata := Signal.memory writeAddr writeData writeEn readAddr

Bit Slice (extract field)

-- CircuitM
let opcode ← makeWire "opcode" (.bitVector 7)
emitAssign opcode (.slice (.ref "inst") 6 0)

-- Signal DSL (requires compiler extension for extractLsb')
let opcode := inst.map (BitVec.extractLsb' 0 7 ·)

Concatenation

-- CircuitM
let sext ← makeWire "sext" (.bitVector 32)
emitAssign sext (.concat [.const 0 20, .ref "imm12"])

-- Signal DSL (requires compiler extension for BitVec.append)
let sext := (BitVec.append · ·) <$> (Signal.pure 0#20) <*> imm12

Comparison

-- CircuitM
let isEq ← makeWire "is_eq" .bit
emitAssign isEq (.op .eq [.ref "a", .ref "b"])

-- Signal DSL
let isEq := (· == ·) <$> a <*> b
-- or: (BEq.beq · ·) <$> a <*> b

Feedback Loop (state machine)

-- CircuitM
let nextState ← makeWire "next_state" (.bitVector 8)
let stateReg ← emitRegister "state" "clk" "rst" (.ref nextState) 0 (.bitVector 8)
emitAssign nextState (.op .mux [.ref "condition",
  .op .add [.ref stateReg, .const 1 8], .ref stateReg])

-- Signal DSL
let state := Signal.loop fun s =>
  let prev := Signal.register 0#8 s
  let next := Signal.mux condition (prev.map (· + 1)) prev
  next

Combinational Logic (pure function + map)

-- CircuitM (must manually create wires for each step)
let isLui ← makeWire "is_lui" .bit
emitAssign isLui (.op .eq [.ref "opcode", .const 0b0110111 7])
let isAuipc ← makeWire "is_auipc" .bit
emitAssign isAuipc (.op .eq [.ref "opcode", .const 0b0010111 7])
let isUtype ← makeWire "is_utype" .bit
emitAssign isUtype (.op .or [.ref isLui, .ref isAuipc])

-- Signal DSL (pure function, auto-synthesized)
def isUtype (opcode : BitVec 7) : Bool :=
  opcode == 0b0110111 || opcode == 0b0010111

let isUtypeSig := inst.map (fun i => isUtype (i.extractLsb' 0 7))

Hierarchical Module Instantiation

-- CircuitM
emitInstance "ALU" "alu_inst" [
  ("alu_op", .ref "op"), ("alu_a", .ref "a"), ("alu_b", .ref "b")]

-- Signal DSL (just function call, auto-hierarchical)
let aluResult := aluSignal op a b

Simulation (why Signal DSL wins)

-- CircuitM: NO Lean-native simulation possible
-- Must generate Verilog → iverilog → vvp (slow, hangs)

-- Signal DSL: Direct Lean evaluation
let value := myCircuit.atTime 100  -- Get output at cycle 100
let trace := List.range 1000 |>.map myCircuit.atTime  -- Full trace
-- Runs in milliseconds, not minutes

When to Use What

Use Case Recommended Why
New RTL design Signal DSL Simulatable, verifiable, synthesizable
Combinational logic Signal DSL (pure function + map) Clean, provable, reusable
Sequential logic Signal DSL (register + loop) Lean-native simulation
Testbenches Signal DSL (Signal.atTime) Fast, no external tools
Vendor primitives CircuitM (via emitInstance) For blackbox instantiation only
Legacy integration CircuitM When wrapping external IP

Compiler Extensions Required for RV32

The following operations need compiler support (Step 1 of the rewrite plan):

Operation Lean Function IR Support Compiler Status
Bit slice BitVec.extractLsb' Expr.slice exists Needs compiler handler
Concatenation BitVec.append Expr.concat exists Needs compiler handler
Shift left BitVec.shiftLeft Operator.shl exists Needs primitive registry entry
Shift right BitVec.ushiftRight Operator.shr exists Needs primitive registry entry
Arith shift right BitVec.sshiftRight Operator.asr exists Needs primitive registry entry
Negation BitVec.neg Operator.neg exists Needs primitive registry entry
Greater than (unsigned) BitVec.ugt Operator.gt_u exists Needs primitive registry entry
Greater or equal (unsigned) BitVec.uge Operator.ge_u exists Needs primitive registry entry
Greater than (signed) BitVec.sgt Operator.gt_s exists Needs primitive registry entry
Greater or equal (signed) BitVec.sge Operator.ge_s exists Needs primitive registry entry
Register with enable Signal.registerWithEnable register + mux Needs compiler handler

RV32 Rewrite Patterns

ALU (combinational → pure function + Signal.map)

-- Pure reference model
def aluCompute (op : ALUOp) (a b : BitVec 32) : BitVec 32 := ...

-- Signal wrapper using nested mux tree
def aluSignal (op : Signal dom (BitVec 4)) (a b : Signal dom (BitVec 32))
    : Signal dom (BitVec 32) :=
  let isAdd := op.map (· == ALUOp.ADD.toBitVec4)
  let addResult := (· + ·) <$> a <*> b
  let isSub := op.map (· == ALUOp.SUB.toBitVec4)
  let subResult := (· - ·) <$> a <*> b
  ...
  Signal.mux isAdd addResult (Signal.mux isSub subResult ...)

Decoder (combinational → pure function)

structure DecoderOutput where
  opcode : BitVec 7
  rd     : BitVec 5
  funct3 : BitVec 3
  rs1    : BitVec 5
  rs2    : BitVec 5
  funct7 : BitVec 7
  imm    : BitVec 32
  aluOp  : BitVec 4

def decode (inst : BitVec 32) : DecoderOutput :=
  let opcode := inst.extractLsb' 0 7
  let rd := inst.extractLsb' 7 5
  ...

Pipeline (sequential → Signal.loop)

def rv32iCore
    (imemRdata : Signal dom (BitVec 32))
    (dmemRdata : Signal dom (BitVec 32))
    : Signal dom CoreOutputs :=
  Signal.loop fun state =>
    let prevState := Signal.register initPipelineState state
    -- IF stage: PC logic
    -- ID stage: decode + register file read
    -- EX stage: ALU + branch evaluation
    -- WB stage: register file write
    -- Compute next state
    ...

Register File (memory)

def regFile
    (rs1Addr rs2Addr : Signal dom (BitVec 5))
    (wrAddr : Signal dom (BitVec 5))
    (wrData : Signal dom (BitVec 32))
    (wrEn : Signal dom Bool)
    : Signal dom (BitVec 32 × BitVec 32) :=
  let rs1Data := Signal.memory wrAddr wrData wrEn rs1Addr
  let rs2Data := Signal.memory wrAddr wrData wrEn rs2Addr
  Signal.bundle2 rs1Data rs2Data

CLINT (sequential → Signal.loop)

def clint (busAddr : Signal dom (BitVec 32))
          (busWdata : Signal dom (BitVec 32))
          (busWe : Signal dom Bool)
    : Signal dom (BitVec 32 × Bool × Bool) :=
  Signal.loop fun state =>
    let prev := Signal.register clintInitState state
    let mtimeLo := prev.map (·.mtimeLo)
    -- auto-increment, write handling, irq comparison...

Lean-Native Testbench

def testSoC : IO Unit := do
  let firmware ← loadHex "firmware/firmware.hex"
  let soc := rv32iSoCWithFirmware firmware
  for cycle in [:100000] do
    let debugPc := soc.debugPc.atTime cycle
    let uartWe := soc.uartWe.atTime cycle
    let uartData := soc.uartData.atTime cycle
    if uartWe then
      IO.println s!"[UART @ cycle {cycle}] 0x{uartData.toHex}"