Sparkle.Compiler.Elab

def Sparkle.Compiler.Elab.CompilerM.emitMemory (hint : String) (addrWidth dataWidth : Nat) (clk : String) (writeAddr writeData writeEnable readAddr : IR.AST.Expr) (named : Bool := false) :

CompilerM String

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.CompilerM.emitMemoryComboRead (hint : String) (addrWidth dataWidth : Nat) (clk : String) (writeAddr writeData writeEnable readAddr : IR.AST.Expr) (named : Bool := false) :

CompilerM String

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.CompilerM.emitInstance (moduleName instName : String) (connections : List (String × IR.AST.Expr)) :

CompilerM Unit

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.CompilerM.addModuleToDesign (m : IR.AST.Module) :

CompilerM Unit

Equations

Sparkle.Compiler.Elab.CompilerM.addModuleToDesign m = do let cs ← get match Sparkle.IR.Builder.CircuitM.addModuleToDesign m cs with | (PUnit.unit , cs') => set cs'

Instances For

source

def Sparkle.Compiler.Elab.CompilerM.addParameter (name : String) (defaultValue : Nat) :

CompilerM Unit

Add a retained parameter, rejecting duplicate module declarations.

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.primitiveRegistry :

List (Lean.Name × IR.AST.Operator)

Primitive Registry: Maps Lean function names to IR operators

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.isPrimitive (name : Lean.Name) :

Bool

Equations

Sparkle.Compiler.Elab.isPrimitive name = Sparkle.Compiler.Elab.primitiveRegistry.any fun (x : Lean.Name × Sparkle.IR.AST.Operator) => match x with | (n, snd) => n == name

Instances For

source

def Sparkle.Compiler.Elab.getOperator (name : Lean.Name) :

Option IR.AST.Operator

Equations

Sparkle.Compiler.Elab.getOperator name = List.lookup name Sparkle.Compiler.Elab.primitiveRegistry

Instances For

source

partial def Sparkle.Compiler.Elab.inferHWType (type : Lean.Expr) :

Lean.MetaM (Option IR.Type.HWType)

source

partial def Sparkle.Compiler.Elab.inferHWType.extractWidth (e : Lean.Expr) :

Lean.MetaM Nat

source

partial def Sparkle.Compiler.Elab.extractDimExpr (expr : Lean.Expr) :

CompilerM IR.Type.DimExpr

Preserve a retained top-level Nat binder as a closed symbolic dimension.

source

partial def Sparkle.Compiler.Elab.inferHWTypeWithDimensions (type : Lean.Expr) :

CompilerM (Option IR.Type.HWType)

Infer hardware types with retained dimensions when parameter synthesis is active. The established concrete inference path remains untouched for ordinary APIs.

source

def Sparkle.Compiler.Elab.inferResetKindFromSignal (signalType : Lean.Expr) :

CompilerM IR.Type.ResetKind

Extract ResetKind from a Signal dom α expression.

We whnf-reduce the dom argument and then use Lean's evalExpr to evaluate it as a DomainConfig, reading the resetKind field directly. Falls back to .asynchronous (the historical default) if the expression doesn't reduce to a literal DomainConfig.

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.inferHWTypeFromSignal (signalType : Lean.Expr) :

CompilerM IR.Type.HWType

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.isSignalBinderType (type : Lean.Expr) :

CompilerM Bool

Syntactically identify Signal binders so symbolic-width diagnostics are not swallowed by the fallback path for erased configuration arguments.

Equations

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

Instances For

source

partial def Sparkle.Compiler.Elab.extractNat (e : Lean.Expr) :

CompilerM Nat

Helper to extract a Nat literal or OfNat.ofNat wrap.

source

def Sparkle.Compiler.Elab.makeSliceExpr (source : IR.AST.Expr) (hi lo : IR.Type.DimExpr) :

IR.AST.Expr

Build a concrete or symbolic IR slice without freezing either bound.

Equations

Sparkle.Compiler.Elab.makeSliceExpr source hi lo = match hi.toNat?, lo.toNat? with | some hiValue, some loValue => source.slice hiValue loValue | x, x_1 => source.sliceDim hi lo

Instances For

source

def Sparkle.Compiler.Elab.makeSliceFromStartLength (source : IR.AST.Expr) (start length : IR.Type.DimExpr) :

IR.AST.Expr

Equations

Sparkle.Compiler.Elab.makeSliceFromStartLength source start length = Sparkle.Compiler.Elab.makeSliceExpr source ((start.mkAdd length).mkSub (Sparkle.IR.Type.DimExpr.literal 1)) start

Instances For

source

def Sparkle.Compiler.Elab.lowerZeroExtendWire (hint sourceWire : String) (targetWidth : IR.Type.DimExpr) (isNamed : Bool := false) :

CompilerM String

Lower unsigned extension/truncation while retaining parameter expressions. SystemVerilog assignment performs both operations correctly for symbolic vector widths; the established concat/slice lowering remains for concrete IR.

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.extractBitVecLiteral (expr : Lean.Expr) :

CompilerM (Nat × Nat)

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.extractNatLiteral (expr : Lean.Expr) :

CompilerM (Nat × Unit)

Extract a Nat literal from an expression

Equations

Sparkle.Compiler.Elab.extractNatLiteral expr = do let n ← Sparkle.Compiler.Elab.extractNat expr pure (n, ())

Instances For

source

partial def Sparkle.Compiler.Elab.extractBitVecList (expr : Lean.Expr) :

CompilerM (Array (Nat × Nat))

Extract values from a List (BitVec n) expression into an array of (value, width) pairs

source

def Sparkle.Compiler.Elab.extractBitVecArray (expr : Lean.Expr) :

CompilerM (Array (Nat × Nat))

Extract values from an Array (BitVec n) expression

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.countedWhnf (e : Lean.Expr) :

CompilerM Lean.Expr

Wrap a MetaM whnf with counters.

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.countedUnfoldDefinition? (e : Lean.Expr) :

CompilerM (Option Lean.Expr)

Wrap Lean.Meta.unfoldDefinition? with counters.

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.cachedInferType (e : Lean.Expr) :

CompilerM Lean.Expr

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.canonHardwareKey (value : Lean.Expr) :

CompilerM String

Canonical, pass-stable key for a hardware-denoting expression: abstract every free variable to a constant named after the WIRE it denotes (wire names are stable within a module synth — they are what the emitted Verilog/C refers to), then hash the abstracted expression.

Hashing the expression directly does not work: fvars are fresh per traversal, so two occurrences denoting the same hardware hash differently (measured 2079038327 vs 1490760256 for two let num occurrences whose fvars both mapped to _gen_pS, _gen_y). After abstraction the key is equal exactly when the denoted hardware is the same — which also makes it the correct INSTANCE identity for multi-output sub-modules: calls with different argument wires get different keys (issue #120), while repeated projections of one let engine := … binder share one key (issue #71).

Equations

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

Instances For

source

partial def Sparkle.Compiler.Elab.translateExprToWire (e : Lean.Expr) (hint : String := "wire") (isTopLevel isNamed : Bool := false) :

CompilerM String

Caching shim around translateExprToWireImpl. All early- intercept handlers (Signal HAdd/HSub/etc., OfNat literals, ...) currently return straight from the inner impl, which means they never write back to the cache. Wrapping here means every successful translate caches its result — so subsequent identical sub-trees become a HashMap lookup instead of a full re-walk through ~10 handlers + Meta.

source

partial def Sparkle.Compiler.Elab.translateExprToWireImpl (e : Lean.Expr) (hint : String := "wire") (isTopLevel isNamed : Bool := false) :

CompilerM String

source

partial def Sparkle.Compiler.Elab.translateExprToWireImpl.toIR (wireS : String) (fvarId : Lean.FVarId) (e : Lean.Expr) :

CompilerM (Option IR.AST.Expr)

source

def Sparkle.Compiler.Elab.handleErrorPatterns (_e : Lean.Expr) (name : Lean.Name) (_args : Array Lean.Expr) (_hint : String) (_isNamed : Bool) :

CompilerM Unit

Detect unsynthesizable patterns (if-then-else, Decidable) and throw errors

Equations

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

Instances For

source

partial def Sparkle.Compiler.Elab.handleTupleProjections (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) :

CompilerM (Option String)

Handle Signal.fst, Signal.snd, Signal.map Prod.fst/Prod.snd

source

partial def Sparkle.Compiler.Elab.handleApplicative (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) :

CompilerM (Option String)

Handle Signal.ap — binary op lifting, concat/sshiftRight special cases.

Also handles N-ary applicative chains f <$> a₁ <*> a₂ <*> ... <*> aₙ (n ≥ 2). These desugar to nested Signal.ap calls — the outermost is Signal.ap (Signal.ap (... (Signal.map f a₁) ...) aₙ₋₁) aₙ. We strip the chain into the inner Signal.map f a₁ plus the trailing argument signals [a₂, ..., aₙ], then apply f to the wires sequentially. For chains whose f is a pure op (or / and / xor / add / etc.) operating pairwise on a left-fold, this resolves into a chain of binary IR ops.

source

partial def Sparkle.Compiler.Elab.handleApplicative.collectAp (acc : Array Lean.Expr) (cur : Lean.Expr) :

Option (Lean.Expr × Array Lean.Expr)

source

partial def Sparkle.Compiler.Elab.handleBitVecOps (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) :

CompilerM (Option String)

Handle BitVec.extractLsb', shifts, concat, isPrimitive dispatch

source

partial def Sparkle.Compiler.Elab.handleRegister (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) :

CompilerM (Option String)

Handle Signal.register, Signal.registerWithEnable

source

partial def Sparkle.Compiler.Elab.handleMux (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) :

CompilerM (Option String)

Handle Signal.mux, lutMuxTree

source

partial def Sparkle.Compiler.Elab.handleMemory (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) :

CompilerM (Option String)

Handle Signal.memory, Signal.memoryComboRead

source

partial def Sparkle.Compiler.Elab.handleLoop (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) :

CompilerM (Option String)

Handle Signal.loop, HWVector.get

source

partial def Sparkle.Compiler.Elab.handleLoop.peelMemoize :

Lean.Expr → Lean.Expr

source

partial def Sparkle.Compiler.Elab.handleCircuitMonad (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) :

CompilerM (Option String)

Handle Bind.bind / Pure.pure specialised to the Sparkle Circuit monad.

Lean's do-notation desugars to Bind.bind m k / Pure.pure v where Bind/Pure are typeclass projections. unfoldDefinition? (the default tryInline path) cannot reduce typeclass projections — it stops at the symbol with the instance still opaque, and the elaborator gives up.

For Sparkle's Circuit monad the bind/pure unfold to pure value-level Prod manipulation that the existing Prod / Signal-map rules already lower. We force a .all transparency reduce on the whole expression and recurse, mirroring how Prod.rec / Prod.casesOn are handled.

source

partial def Sparkle.Compiler.Elab.handleCircuitMonad.peelLambdas :

Lean.Expr → Lean.Expr

source

partial def Sparkle.Compiler.Elab.handleDefinitionUnfold (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) :

CompilerM (Option String)

Handle a Lean function call by either inlining the body (the default) or emitting a sub-module instance (only when the declaration is tagged @[hardware_module]).

Default = inline keeps the generated Verilog flat, which is what most users want for alias-style helpers and small combinational functions: writing def passthrough x := x shouldn't multiply the module count of every caller.

Opt INTO sub-module emission with @[hardware_module] for designs you want to see as their own Verilog module foo block — a CPU, an ALU you intend to re-use, an arbiter, etc. Downstream tools (P&R, OOC synth, hierarchical timing) can then treat the boundary as a real compile unit.

@[inline_hardware] is accepted as a self-documenting synonym for "always inline". Today it has no effect over the default, but it stays binding if a future heuristic ever auto-promotes a definition to a module.

source

partial def Sparkle.Compiler.Elab.translateExprToWireApp (e : Lean.Expr) (hint : String) (isNamed : Bool := false) :

CompilerM String

source

partial def Sparkle.Compiler.Elab.translateExprToWireApp.normSpine (x : Lean.Expr) (fuel : Nat) :

Lean.MetaM Lean.Expr

source

partial def Sparkle.Compiler.Elab.translateShiftAmount (bvExpr natExpr : Lean.Expr) (hint : String) :

CompilerM String

Translate a Nat shift amount argument to a hardware wire. Unwraps BitVec.toNat / Fin.val if the Nat came from a BitVec signal, otherwise treats it as a constant shift amount.

source

partial def Sparkle.Compiler.Elab.getPrimitiveNameFromLambda (e : Lean.Expr) :

CompilerM Lean.Name

source

partial def Sparkle.Compiler.Elab.splitReturnLeaves (e : Lean.Expr) (prefix? : Option String := none) :

Lean.MetaM (Array (String × Lean.Expr))

Split a return value of type ρ into a list of (suggested-port-name, leaf-Lean-expr) pairs at the Lean-expression level — one entry per Signal dom τ leaf under ρ.

Handled shapes:

Signal dom τ → one anonymous leaf carrying the original expression.
Prod α β → recursively split Prod.fst e / Prod.snd e (positional names out_0, out_1, …).
single-constructor inductive (i.e. user record) → for each field, recurse on e.field and prefix the field name so each leaf gets a human-readable port (dmac, payloadValid, …).

Falls back to [(none, e)] if the type doesn't match any of the above — that keeps non-Signal payloads round- tripping through the legacy single-wire path.

source

def Sparkle.Compiler.Elab.openRecordInputs (body : Lean.Expr) :

Lean.MetaM Lean.Expr

"Open" record-typed parameters at the synth boundary.

For a function body = fun (p₁ : T₁) (rec : MyRec) (p₂) => … where MyRec is a single-constructor inductive whose fields are all Signal …, rewrite to fun (p₁) (f₁ : F₁) (f₂ : F₂) … (p₂) => body p₁ { f₁, f₂, … } p₂ so the IR elaborator sees per-field Signal inputs instead of an unsplittable record argument.

Records with no Signal fields (or with non-Signal mixed in) are left untouched. Recursion is one-level — a record whose fields are themselves records is partially opened (the outer record is unwrapped; inner records pass through). Good enough for the common HFT-NIC case where each layer's RxIn is a flat record of Signals.

Implementation: walk params with a worker that recurses inside successive forallTelescopeReducing callbacks so every fvar stays in scope when mkLambdaFVars runs at the deepest layer. No IO.Ref shenanigans — the worker threads state purely.

Equations

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

Instances For

source

partial def Sparkle.Compiler.Elab.openRecordInputs.walk (body : Lean.Expr) (params : Array Lean.Expr) (inner : Lean.Expr) (idx : Nat) (binders : Array Lean.Expr) (subst : Array (Lean.FVarId × Lean.Expr)) (opened : Bool) :

Lean.MetaM Lean.Expr

source

partial def Sparkle.Compiler.Elab.stripMemoizeWrappers (e : Lean.Expr) :

Lean.Expr

Deep-strip every Signal.memoize x sub-expression to x in a Lean expression tree. Signal.memoize is a sim-only identity wrapper used by Compiler C2 to cache per-cycle register reads; for synthesis it serves no purpose and causes infinite-loop hangs in FSM-shaped circuits where register-read → register-write → memoize chain re-enters via Signal.loop body inlining. Stripping them once at the synth entry point breaks the cycle definitively.

Implementation: post-order traversal — strip children first, then check if THIS node is Signal.memoize and unwrap if so. Does not recurse under binders (lambdas) because BVars under a binder have no fvar-binding yet and the memoize wrap there will be handled by Signal.loop's handler when it instantiates the binder.

source

partial def Sparkle.Compiler.Elab.synthesizeCombinationalCore (declName : Lean.Name) (parameters : List (String × Nat)) (symbolicMode : Bool) :

Lean.MetaM (IR.AST.Module × IR.AST.Design)

source

partial def Sparkle.Compiler.Elab.synthesizeCombinationalCore.buildEnv (parameters : List (String × Nat)) (symbolicMode : Bool) (xs : Array Lean.Expr) (i : Nat) (k : CompilerM String) :

CompilerM String

source

partial def Sparkle.Compiler.Elab.synthesizeCombinational (declName : Lean.Name) :

Lean.MetaM (IR.AST.Module × IR.AST.Design)

source

def Sparkle.Compiler.Elab.synthesizeCombinationalWithParameters (declName : Lean.Name) (parameters : List (String × Nat)) :

Lean.MetaM (IR.AST.Module × IR.AST.Design)

Equations

Sparkle.Compiler.Elab.synthesizeCombinationalWithParameters declName parameters = Sparkle.Compiler.Elab.synthesizeCombinationalCore declName parameters true

Instances For

source

def Sparkle.Compiler.Elab.printModule (m : IR.AST.Module) :

Lean.MetaM Unit

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.«command#synthesize_» :

Lean.ParserDescr

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.runDesignDRC (design : IR.AST.Design) :

Lean.MetaM Unit

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.«command#synthesizeVerilog_» :

Lean.ParserDescr

Plain-text Verilog elaborator.

#synthesizeVerilog id synthesises id and prints the resulting SystemVerilog to stdout. Output is plain text — no MIME wrapper, no highlighting — so it works identically under lake build, lake env lean, CI, and any Jupyter kernel.

For a syntax-highlighted view inside JupyterLab use #showVerilog instead; for writing to a file use #writeVerilogDesign id "path".

Equations

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

Instances For

source

def Sparkle.Compiler.Elab.sparkleParameterBinding.quot :

Lean.ParserDescr

Equations

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

Instances For

source

def Lean.Parser.Category.sparkleParameterBinding :