structure Sparkle.IR.Builder.CircuitState : Type

State for circuit building

• counter : Nat
• module : AST.Module
• design : AST.Design
• usedNames : List String

instance Sparkle.IR.Builder.instReprCircuitState : Repr CircuitState

Equations

• Sparkle.IR.Builder.instReprCircuitState = { reprPrec := Sparkle.IR.Builder.instReprCircuitState.repr }

def Sparkle.IR.Builder.instReprCircuitState.repr : CircuitState → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Sparkle.IR.Builder.CircuitM (α : Type) : Type

Circuit builder monad

Equations

• Sparkle.IR.Builder.CircuitM = StateM Sparkle.IR.Builder.CircuitState

def Sparkle.IR.Builder.CircuitM.init (topModuleName : String) : CircuitState

Create initial circuit state

Equations

• Sparkle.IR.Builder.CircuitM.init topModuleName = { counter := 0, module := Sparkle.IR.AST.Module.empty topModuleName, design := Sparkle.IR.AST.Design.empty topModuleName, usedNames := [] }

def Sparkle.IR.Builder.CircuitM.getModule : CircuitM AST.Module

Get the current module

Equations

• Sparkle.IR.Builder.CircuitM.getModule = do let s ← get pure s.module

def Sparkle.IR.Builder.CircuitM.setModule (m : AST.Module) : CircuitM Unit

Set the module

Equations

• Sparkle.IR.Builder.CircuitM.setModule m = modify fun (s : Sparkle.IR.Builder.CircuitState) => { counter := s.counter, module := m, design := s.design, usedNames := s.usedNames }

def Sparkle.IR.Builder.CircuitM.getDesign : CircuitM AST.Design

Get the current design

Equations

• Sparkle.IR.Builder.CircuitM.getDesign = do let s ← get pure s.design

def Sparkle.IR.Builder.CircuitM.addModuleToDesign (m : AST.Module) : CircuitM Unit

Add a completed module to the design

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.IR.Builder.CircuitM.freshName (hint : String) (named : Bool := false) : CircuitM String

Generate a fresh wire name. When named=true (user let-bindings), produces _gen_{hint} — stable across recompilations. When named=false (compiler intermediates), produces _tmp_{hint}_{counter} — numbered.

The hint is stripped of any Lean macro-hygiene suffix (...__@_...__hygCtx__hyg_N) so the resulting wire name is a valid Verilog identifier.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.IR.Builder.CircuitM.sanitizeName (name : String) : String

Sanitize a name to be a valid Verilog identifier

Equations

• Sparkle.IR.Builder.CircuitM.sanitizeName name = (((name.replace "." "_").replace "-" "_").replace " " "_").replace "'" "_prime"

def Sparkle.IR.Builder.CircuitM.isNameUsed (name : String) : CircuitM Bool

Check if a name is already used

Equations

• Sparkle.IR.Builder.CircuitM.isNameUsed name = do let s ← get pure (s.usedNames.contains name)

def Sparkle.IR.Builder.CircuitM.reserveName (name : String) : CircuitM Unit

Reserve a specific name (for input/output ports)

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.IR.Builder.CircuitM.makeWire (hint : String) (ty : «Type».HWType) (named : Bool := false) : CircuitM String

Create a new wire with the given type. Returns the unique name of the wire.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.IR.Builder.CircuitM.emitAssign (lhs : String) (rhs : AST.Expr) : CircuitM Unit

Emit a continuous assignment statement. lhs := rhs

Note: Mux validation is performed at Verilog generation time. Always use: .op .mux [cond, thenVal, elseVal] (exactly 3 arguments)

Equations

• Sparkle.IR.Builder.CircuitM.emitAssign lhs rhs = do let m ← Sparkle.IR.Builder.CircuitM.getModule Sparkle.IR.Builder.CircuitM.setModule (m.addStmt (Sparkle.IR.AST.Stmt.assign lhs rhs))

def Sparkle.IR.Builder.CircuitM.emitRegister (hint clock reset : String) (input : AST.Expr) (initValue : Int) (ty : «Type».HWType) (named : Bool := false) (resetKind : «Type».ResetKind := «Type».ResetKind.asynchronous) : CircuitM String

Emit a register statement (D flip-flop). Returns the name of the output wire.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.IR.Builder.CircuitM.emitMemory (hint : String) (addrWidth dataWidth : Nat) (clock : String) (writeAddr writeData writeEnable readAddr : AST.Expr) (named : Bool := false) : CircuitM String

Emit a synchronous memory (RAM/BRAM) primitive. Returns the name of the read data output wire.

Parameters:

• hint: Base name for the memory instance
• addrWidth: Address width (memory size = 2^addrWidth)
• dataWidth: Data width (width of each memory word)
• clock: Clock signal name
• writeAddr: Write address expression
• writeData: Write data expression
• writeEnable: Write enable expression
• readAddr: Read address expression

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.IR.Builder.CircuitM.emitMemoryComboRead (hint : String) (addrWidth dataWidth : Nat) (clock : String) (writeAddr writeData writeEnable readAddr : AST.Expr) (named : Bool := false) : CircuitM String

Emit a memory with combinational (same-cycle) read. Returns the name of the read data output wire.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.IR.Builder.CircuitM.emitInstance (moduleName instName : String) (connections : List (String × AST.Expr)) : CircuitM Unit

Emit a module instantiation.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.IR.Builder.CircuitM.addInput (name : String) (ty : «Type».HWType) : CircuitM Unit

Add an input port to the module.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.IR.Builder.CircuitM.addOutput (name : String) (ty : «Type».HWType) : CircuitM Unit

Add an output port to the module.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.IR.Builder.CircuitM.run {α : Type} (moduleName : String) (builder : CircuitM α) : AST.Module × α

Run the circuit builder and extract the final module.

Equations

• Sparkle.IR.Builder.CircuitM.run moduleName builder = match StateT.run builder (Sparkle.IR.Builder.CircuitM.init moduleName) with | (result, finalState) => (finalState.module, result)

def Sparkle.IR.Builder.CircuitM.runModule (moduleName : String) (builder : CircuitM Unit) : AST.Module

Run the circuit builder and return only the module.

Equations

• Sparkle.IR.Builder.CircuitM.runModule moduleName builder = (Sparkle.IR.Builder.CircuitM.run moduleName builder).fst

def Sparkle.IR.Builder.CircuitM.runDesign (topModuleName : String) (builder : CircuitM Unit) : AST.Design

Run the circuit builder and return the full design.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.IR.Builder.halfAdderExample : AST.Module

Example: Building a simple half adder

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.IR.Builder.mkSRAMPrimitive (name : String) (addrWidth dataWidth : Nat) : AST.Module

Create an SRAM primitive module (single-port synchronous RAM)

Parameters:

• name: Module name (e.g., "SRAM_256x32")
• addrWidth: Address width in bits (depth = 2^addrWidth)
• dataWidth: Data width in bits

Interface:

• Inputs: clk, we (write enable), addr, din (data in)
• Outputs: dout (data out)

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.IR.Builder.mkSRAMDualPortPrimitive (name : String) (addrWidth dataWidth : Nat) : AST.Module

Create a dual-port SRAM primitive module

Parameters:

• name: Module name (e.g., "SRAM_DP_256x32")
• addrWidth: Address width in bits (depth = 2^addrWidth)
• dataWidth: Data width in bits

Interface:

• Inputs: clk, we, raddr (read addr), waddr (write addr), din
• Outputs: dout

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.IR.Builder.mkClockGatePrimitive (name : String) : AST.Module

Create a clock gating cell primitive

Parameters:

• name: Module name (e.g., "CKGT_X2" for a 2x drive strength clock gate)

Interface:

• Inputs: clk (clock in), en (enable)
• Outputs: clk_out (gated clock)

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.IR.Builder.mkROMPrimitive (name : String) (addrWidth dataWidth : Nat) : AST.Module

Create a ROM primitive module

Parameters:

• name: Module name (e.g., "ROM_512x16")
• addrWidth: Address width in bits (depth = 2^addrWidth)
• dataWidth: Data width in bits

Interface:

• Inputs: clk, addr
• Outputs: dout

Equations

• One or more equations did not get rendered due to their size.