@[implicit_reducible]

instance Sparkle.IR.Optimize.instInhabitedExpr : Inhabited AST.Expr

Equations

• Sparkle.IR.Optimize.instInhabitedExpr = { default := Sparkle.IR.AST.Expr.const 0 0 }

@[reducible, inline]

abbrev Sparkle.IR.Optimize.DefMap : Type

O(1) lookup maps built from module data

Equations

• Sparkle.IR.Optimize.DefMap = Std.HashMap String Sparkle.IR.AST.Expr

@[reducible, inline]

abbrev Sparkle.IR.Optimize.WidthMap : Type

Equations

• Sparkle.IR.Optimize.WidthMap = Std.HashMap String Nat

def Sparkle.IR.Optimize.buildDefMap (stmts : List AST.Stmt) : DefMap

Build a name → defining-expression map from assign statements

Equations

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

def Sparkle.IR.Optimize.buildWidthMap (m : AST.Module) : WidthMap

Build name → bit-width map from module ports and wires

Equations

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

partial def Sparkle.IR.Optimize.inferWidth (wm : WidthMap) : AST.Expr → Nat

Infer the bit-width of an expression

partial def Sparkle.IR.Optimize.resolveSliceOfConcatAux (remaining : List (AST.Expr × Nat)) (hiEdge sliceHi sliceLo : Nat) : Option AST.Expr

Try to resolve a slice of a concat to a direct reference or narrower slice.

For concat [a(wa), b(wb), c(wc), ...] with total width T:

• a occupies [T-1 : T-wa]
• b occupies [T-wa-1 : T-wa-wb]
• etc. (MSB-first layout, same as Verilog {a, b, c, ...})

Returns the replacement if the slice maps entirely within one arg.

def Sparkle.IR.Optimize.resolveSliceOfConcat (args : List AST.Expr) (widths : List Nat) (sliceHi sliceLo : Nat) : Option AST.Expr

Equations

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

partial def Sparkle.IR.Optimize.resolveSlice (dm : DefMap) (wm : WidthMap) (name : String) (hi lo fuel : Nat) : AST.Expr

Resolve a slice of a named wire through the defMap, recursively following:

1. Ref aliases: X = Y → slice(Y, hi, lo)
2. Slice chains: X = Y[h:l] → slice(Y, l+hi, l+lo)
3. Concat args: X = {a, b} → a (if slice matches exactly) Depth-limited to prevent infinite recursion on malformed IR.

def Sparkle.IR.Optimize.foldConstants : AST.Expr → AST.Expr

Fold constant expressions

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.IR.Optimize.foldConstants (Sparkle.IR.AST.Expr.op Sparkle.IR.AST.Operator.mux [Sparkle.IR.AST.Expr.const 1 1, t, head]) = t
• Sparkle.IR.Optimize.foldConstants (Sparkle.IR.AST.Expr.op Sparkle.IR.AST.Operator.mux [Sparkle.IR.AST.Expr.const 0 1, head, e]) = e
• Sparkle.IR.Optimize.foldConstants (Sparkle.IR.AST.Expr.op Sparkle.IR.AST.Operator.add [Sparkle.IR.AST.Expr.const 0 width, e]) = e
• Sparkle.IR.Optimize.foldConstants (Sparkle.IR.AST.Expr.op Sparkle.IR.AST.Operator.add [e, Sparkle.IR.AST.Expr.const 0 width]) = e
• Sparkle.IR.Optimize.foldConstants (Sparkle.IR.AST.Expr.op Sparkle.IR.AST.Operator.or [Sparkle.IR.AST.Expr.const 0 width, e]) = e
• Sparkle.IR.Optimize.foldConstants (Sparkle.IR.AST.Expr.op Sparkle.IR.AST.Operator.or [e, Sparkle.IR.AST.Expr.const 0 width]) = e
• Sparkle.IR.Optimize.foldConstants (Sparkle.IR.AST.Expr.op Sparkle.IR.AST.Operator.and [Sparkle.IR.AST.Expr.const 0 w, head]) = Sparkle.IR.AST.Expr.const 0 w
• Sparkle.IR.Optimize.foldConstants (Sparkle.IR.AST.Expr.op Sparkle.IR.AST.Operator.and [head, Sparkle.IR.AST.Expr.const 0 w]) = Sparkle.IR.AST.Expr.const 0 w
• Sparkle.IR.Optimize.foldConstants (Sparkle.IR.AST.Expr.op Sparkle.IR.AST.Operator.mux [Sparkle.IR.AST.Expr.const 0 width, head, e]) = e
• Sparkle.IR.Optimize.foldConstants (Sparkle.IR.AST.Expr.op Sparkle.IR.AST.Operator.mux [cond, Sparkle.IR.AST.Expr.const 1 1, Sparkle.IR.AST.Expr.const 0 1]) = cond
• Sparkle.IR.Optimize.foldConstants (Sparkle.IR.AST.Expr.op Sparkle.IR.AST.Operator.not [Sparkle.IR.AST.Expr.op Sparkle.IR.AST.Operator.not [x_1]]) = x_1
• Sparkle.IR.Optimize.foldConstants x✝ = x✝

partial def Sparkle.IR.Optimize.optimizeExpr (dm : DefMap) (wm : WidthMap) : AST.Expr → AST.Expr

Optimize a single expression by resolving slice chains, folding constants, and propagating constant-assigned wires.

partial def Sparkle.IR.Optimize.collectExprRefs : AST.Expr → List String

Collect all reference names from an expression.

partial def Sparkle.IR.Optimize.countExprUses (e : AST.Expr) (counts : Std.HashMap String Nat) : Std.HashMap String Nat

def Sparkle.IR.Optimize.countAllUses (stmts : List AST.Stmt) : Std.HashMap String Nat

Count uses of each wire across all statements

Equations

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

def Sparkle.IR.Optimize.optimizeStmt (dm : DefMap) (wm : WidthMap) : AST.Stmt → AST.Stmt

Optimize a single statement's expressions

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.IR.Optimize.optimizeStmt dm wm (Sparkle.IR.AST.Stmt.assign lhs rhs) = Sparkle.IR.AST.Stmt.assign lhs (Sparkle.IR.Optimize.optimizeExpr dm wm rhs)

partial def Sparkle.IR.Optimize.substituteExpr (dm : DefMap) (inlinable : Std.HashMap String Bool) (widthOfWire : String → Nat) (fuel : Nat) : AST.Expr → AST.Expr

Recursively substitute inlinable references with their defining expressions.

widthOfWire is the substituted wire's DECLARED width, and it is load- bearing: CSim emits expressions unmasked and re-masks only at named-wire assignment boundaries (self->w = (expr) & 0x7ULL). A wire is therefore a masking point, and inlining one deletes its mask. When the declared width differs from the width C arithmetic naturally wraps at (32 for promoted narrow operands, 64 for wide storage), the value changes: CAVLC's 3-bit slDec = suffixLen - 1 reads 7 as a wire but −1 → 2³²−1 inlined, and 3 << slDec went from 384 to garbage — every emitted bitstream block was wrong. So any inlined definition whose declared width is not exactly 32 or 64 is re-wrapped in an explicit & (2^w − 1), which every backend renders inline and constant-folds.

def Sparkle.IR.Optimize.inlineSingleUseWires (m : AST.Module) (body : List AST.Stmt) (observableWires : Option (List String) := none) (protectedWires : Std.HashMap String Bool := ∅) : List AST.Stmt × List AST.Port

Inline single-use wires: replace references with their defining expressions and remove the now-dead assign statements.

Equations

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

def Sparkle.IR.Optimize.inlineSingleUseWires.grow (assignDefs : Std.HashMap String AST.Expr) (work : List String) (seen : Std.HashMap String Bool) (fuel : Nat) : Std.HashMap String Bool

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.IR.Optimize.inlineSingleUseWires.grow assignDefs work seen 0 = seen
• Sparkle.IR.Optimize.inlineSingleUseWires.grow assignDefs [] seen fuel = seen

def Sparkle.IR.Optimize.propagateConstants (body : List AST.Stmt) (dm : DefMap) : List AST.Stmt × DefMap

Propagate constant and simple-ref assignments into all uses. x = const → replace all refs to x with const x = y → replace all refs to x with y (alias elimination) This runs even for gen (JIT-observable) wires since they're just aliases.

Equations

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

@[irreducible]

def Sparkle.IR.Optimize.propagateConstants.substExpr (constMap : Std.HashMap String AST.Expr) : AST.Expr → AST.Expr

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.IR.Optimize.propagateConstants.substExpr constMap (Sparkle.IR.AST.Expr.ref name) = match constMap.get? name with | some replacement => replacement | none => Sparkle.IR.AST.Expr.ref name
• Sparkle.IR.Optimize.propagateConstants.substExpr constMap (Sparkle.IR.AST.Expr.const value width) = Sparkle.IR.AST.Expr.const value width
• Sparkle.IR.Optimize.propagateConstants.substExpr constMap (inner.slice hi lo) = (Sparkle.IR.Optimize.propagateConstants.substExpr constMap inner).slice hi lo
• Sparkle.IR.Optimize.propagateConstants.substExpr constMap (inner.sliceDim hi lo) = (Sparkle.IR.Optimize.propagateConstants.substExpr constMap inner).sliceDim hi lo
• Sparkle.IR.Optimize.propagateConstants.substExpr constMap (Sparkle.IR.AST.Expr.concat args) = Sparkle.IR.AST.Expr.concat (List.map (Sparkle.IR.Optimize.propagateConstants.substExpr constMap) args)

partial def Sparkle.IR.Optimize.eliminateZeroBitInExpr (wm : WidthMap) : AST.Expr → AST.Expr

Filter zero-bit elements out of an Expr tree.

lowerExpr / runCircuitH-style elaborators can produce IR nodes that thread a bitVector 0 "empty payload" through .concat and .slice chains — for instance bundle2 X (Signal.pure ()) lowers to .concat [X, <0-bit ref>], and the matching Signal.map Prod.fst lowers to a slice that discards the 0-bit tail.

Emitting these into SystemVerilog produces invalid constructs like assign x = 0'd0; (a zero-width literal is not legal SV). This pass rewrites the IR so that:

• .const v 0 is dropped from .concat arg lists;
• .concat [x] (after dropping zero-bit args) collapses to the single remaining arg;
• .concat [] collapses to a 1-bit zero placeholder (should be unreachable in practice — pruned later by DCE);
• .slice e hi lo where hi - lo + 1 == 0 is rewritten to a 0-bit constant (later dropped at the use site).

Sub-expressions are rewritten recursively.

def Sparkle.IR.Optimize.eliminateZeroBitStmt (wm : WidthMap) : AST.Stmt → Option AST.Stmt

Drop Stmt.assign whose LHS has zero width — these only exist as leftover bookkeeping from 0-bit IR construction (see eliminateZeroBitInExpr). Other Stmt kinds are kept as is.

Equations

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

def Sparkle.IR.Optimize.eliminateZeroBits (m : AST.Module) : AST.Module

Run the 0-bit elimination pass over a module's body and wire list.

Equations

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

partial def Sparkle.IR.Optimize.resolveSubst (subst : Std.HashMap String String) (w : String) : String

Resolve a wire name through the CSE substitution map, following chains (w2 → w1 → w0). Chains are acyclic by construction — a wire only enters the map when its defining statement is dropped, and the representative's statement is always kept — so plain recursion terminates.

partial def Sparkle.IR.Optimize.renameRefs (subst : Std.HashMap String String) : AST.Expr → AST.Expr

Rewrite every wire reference through the CSE substitution map.

def Sparkle.IR.Optimize.mapStmtExprs (f : AST.Expr → AST.Expr) : AST.Stmt → AST.Stmt

Apply f to every expression embedded in a statement.

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.IR.Optimize.mapStmtExprs f (Sparkle.IR.AST.Stmt.assign lhs rhs) = Sparkle.IR.AST.Stmt.assign lhs (f rhs)
• Sparkle.IR.Optimize.mapStmtExprs f (Sparkle.IR.AST.Stmt.register output clock reset input initValue) = Sparkle.IR.AST.Stmt.register output clock reset (f input) initValue

def Sparkle.IR.Optimize.cseAndMergeInstances (m : AST.Module) (body0 : List AST.Stmt) (protectedWire : String → Bool) : List AST.Stmt

Phase 0.6: cross-wire common-subexpression elimination + duplicate sub-module instance merging (Issue #107).

The synth elaborator re-walks the circuit body once per register next-state leaf; wires derived from let/loop-bound state come out under fresh names per walk (_gen_x, _gen_x_1, …) even though they compute identical expressions over identical base wires, and each walk re-emits the sub-module instances fed by those wires — E = I·(D+1) instances instead of I. The Lean-side caches can't see through the fresh fvars, but at the IR level everything is canonical: the clones are literally assign x_1 = <same rhs> and inst … (<same input connections>).

Value-number assigns by their (substitution-rewritten) rhs; when a later assign duplicates an earlier one, drop it and alias its lhs to the representative. Merge instances of the same module whose input connections are identical, aliasing their output wires. A connection .ref w where w is not driven by any non-instance statement (and is not a module input) is an output of that instance — no cross-module port-direction table needed.

Merging stateful instances is sound: same module + same inputs + same clock/reset ⇒ same state trajectory ⇒ same outputs, which is exactly the denotation Sparkle's pure semantics assigns to structurally identical calls. (This is the fold yosys's opt_merge refuses to do because it would need sequential equivalence checking; here it is correct by construction.)

protectedWire (module outputs + observable waveform taps) never gets aliased away. Iterates to a fixpoint because folding one layer of duplicates makes the next layer's keys equal.

Equations

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

def Sparkle.IR.Optimize.optimizeModule (m : AST.Module) (observableWires : Option (List String) := none) : AST.Module

Optimize a module: strip zero-bit shapes, eliminate concat/slice chains, then remove dead code.

Equations

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

def Sparkle.IR.Optimize.optimizeModule.grow (assignDefs regInputs : Std.HashMap String AST.Expr) (worklist : List String) (live : Std.HashMap String Bool) (fuel : Nat) : Std.HashMap String Bool

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.IR.Optimize.optimizeModule.grow assignDefs regInputs worklist live 0 = live
• Sparkle.IR.Optimize.optimizeModule.grow assignDefs regInputs [] live fuel = live

def Sparkle.IR.Optimize.optimizeDesign (d : AST.Design) (observableWires : Option (List String) := none) : AST.Design

Optimize all modules in a design

Equations

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