Sparkle.IR.AST

assign (lhs : String) (rhs : Expr) : Stmt
register (output clock : String) (reset : String × «Type».ResetKind) (input : Expr) (initValue : Int) : Stmt
memory (name : String) (addrWidth dataWidth : Nat) (clock : String) (writeAddr writeData writeEnable readAddr : Expr) (readData : String) (comboRead : Bool := false) : Stmt
inst (moduleName instName : String) (connections : List (String × Expr)) : Stmt

Instances For

source

instance Sparkle.IR.AST.instReprStmt :

Repr Stmt

Equations

Sparkle.IR.AST.instReprStmt = { reprPrec := Sparkle.IR.AST.instReprStmt.repr }

source

def Sparkle.IR.AST.instReprStmt.repr :

Stmt → Nat → Std.Format

Equations

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

Instances For

source

def Sparkle.IR.AST.instBEqStmt.beq :

Stmt → Stmt → Bool

Equations

One or more equations did not get rendered due to their size.
Sparkle.IR.AST.instBEqStmt.beq (Sparkle.IR.AST.Stmt.assign a a_1) (Sparkle.IR.AST.Stmt.assign b b_1) = (a == b && a_1 == b_1)
Sparkle.IR.AST.instBEqStmt.beq (Sparkle.IR.AST.Stmt.inst a a_1 a_2) (Sparkle.IR.AST.Stmt.inst b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
Sparkle.IR.AST.instBEqStmt.beq x✝¹ x✝ = false

Instances For

source

instance Sparkle.IR.AST.instBEqStmt :

BEq Stmt

Equations

Sparkle.IR.AST.instBEqStmt = { beq := Sparkle.IR.AST.instBEqStmt.beq }

source

def Sparkle.IR.AST.Stmt.toString :

Stmt → String

Convert statement to string (for debugging)

Equations

One or more equations did not get rendered due to their size.
(Sparkle.IR.AST.Stmt.assign a a_1).toString = toString a ++ toString " := " ++ toString a_1

Instances For

source

instance Sparkle.IR.AST.Stmt.instToString :

ToString Stmt

Equations

Sparkle.IR.AST.Stmt.instToString = { toString := Sparkle.IR.AST.Stmt.toString }

source

structure Sparkle.IR.AST.Module :

Type

Module: A hardware module with inputs, outputs, internal wires, and logic

This represents a synthesizable hardware component.

If isPrimitive is true, this is a blackbox module (e.g., vendor SRAM, clock gate) that should be instantiated but not defined. The body is ignored for primitives.

name : String
inputs : List Port
outputs : List Port
wires : List Port
body : List Stmt
assertions : List (String × Expr)
isPrimitive : Bool

Instances For

source

def Sparkle.IR.AST.instReprModule.repr :

Module → Nat → Std.Format

Equations

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

Instances For

source

instance Sparkle.IR.AST.instReprModule :

Repr Module

Equations

Sparkle.IR.AST.instReprModule = { reprPrec := Sparkle.IR.AST.instReprModule.repr }

source

instance Sparkle.IR.AST.instBEqModule :

BEq Module

Equations

Sparkle.IR.AST.instBEqModule = { beq := Sparkle.IR.AST.instBEqModule.beq }

source

def Sparkle.IR.AST.instBEqModule.beq :

Module → Module → Bool

Equations

One or more equations did not get rendered due to their size.
Sparkle.IR.AST.instBEqModule.beq x✝¹ x✝ = false

Instances For

source

def Sparkle.IR.AST.Module.empty (name : String) :

Module

Create an empty module

Equations

Sparkle.IR.AST.Module.empty name = { name := name, inputs := [], outputs := [], wires := [], body := [] }

Instances For

source

def Sparkle.IR.AST.Module.primitive (name : String) (inputs outputs : List Port) :

Module

Create a primitive (blackbox) module with specified interface

Equations

Sparkle.IR.AST.Module.primitive name inputs outputs = { name := name, inputs := inputs, outputs := outputs, wires := [], body := [], isPrimitive := true }

Instances For

Append-vs-prepend perf note #

`addInput` / `addOutput` / `addWire` / `addStmt` are called
in the inner loop of every IP synthesis — once per port,
wire, and statement.  The natural definition (`m.body ++ [s]`)
is O(n) per call, which makes the whole module-building
loop O(n²) and dominated runtime for FSM-shape circuits
(memcached server top-level synth went from ~0.5 s for the
first multi-output leaf to 32+ s for the sixth — same Δcalls,
but `module.body` had grown 6× and every `++ [s]` paid
for that).

Fix: build the lists in REVERSE order via head-prepend
(O(1)), then reverse them once at the end of synthesis
in `Module.finalize`.  External callers that read
`m.body` / `m.wires` after `finalize` see the same forward
order they always did.

source

def Sparkle.IR.AST.Module.addInput (m : Module) (p : Port) :

Module

Add an input port (O(1); reversed by finalize).

Equations

m.addInput p = { name := m.name, inputs := p :: m.inputs, outputs := m.outputs, wires := m.wires, body := m.body, assertions := m.assertions, isPrimitive := m.isPrimitive }

Instances For

source

def Sparkle.IR.AST.Module.addOutput (m : Module) (p : Port) :

Module

Add an output port (O(1); reversed by finalize).

Equations

m.addOutput p = { name := m.name, inputs := m.inputs, outputs := p :: m.outputs, wires := m.wires, body := m.body, assertions := m.assertions, isPrimitive := m.isPrimitive }

Instances For

source

def Sparkle.IR.AST.Module.addWire (m : Module) (p : Port) :

Module

Add an internal wire (O(1); reversed by finalize).

Equations

m.addWire p = { name := m.name, inputs := m.inputs, outputs := m.outputs, wires := p :: m.wires, body := m.body, assertions := m.assertions, isPrimitive := m.isPrimitive }

Instances For

source

def Sparkle.IR.AST.Module.addStmt (m : Module) (s : Stmt) :

Module

Add a statement to the body (O(1); reversed by finalize).

Equations

m.addStmt s = { name := m.name, inputs := m.inputs, outputs := m.outputs, wires := m.wires, body := s :: m.body, assertions := m.assertions, isPrimitive := m.isPrimitive }

Instances For

source

def Sparkle.IR.AST.Module.finalize (m : Module) :

Module

Reverse the four append-in-reverse lists to forward order. Must be called exactly once after all incremental additions are done and before any consumer reads m.inputs / outputs / wires / body.

Equations