@[reducible, inline]

abbrev Sparkle.Backend.CSim.TypeMap : Type

Name→type lookup used by the emitters. Backed by a Std.HashMap so lookupWidth is O(1): emitExpr/inferExprWidth probe it once per expression node. The old linear-scan List made emit O(N·M) over a module's N nodes and M wires — quadratic on large designs like Keccak's ~1600-wire round.

Equations

• Sparkle.Backend.CSim.TypeMap = Std.HashMap String Sparkle.IR.Type.HWType

def Sparkle.Backend.CSim.buildTypeMap (m : IR.AST.Module) : TypeMap

Build a name-to-type map from a module's ports and wires. insertIfNew preserves the first binding on a name clash, matching the old List.find? (inputs, then outputs, then wires) semantics.

Equations

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

def Sparkle.Backend.CSim.lookupWidth (typeMap : TypeMap) (name : String) : Nat

Look up bit-width for a name in the type map

Equations

• Sparkle.Backend.CSim.lookupWidth typeMap name = match Std.HashMap.get? typeMap name with | some ty => ty.bitWidth | none => 32

def Sparkle.Backend.CSim.sanitizeName (name : String) : String

Sanitize a name to be a valid C identifier. Fast path: called per name occurrence during emission (millions of times on XiangShan-scale modules); almost every name is clean.

Equations

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

def Sparkle.Backend.CSim.emitScalarBase : IR.Type.HWType → String

Convert HWType to a C scalar type string. For wide integers (> 64 bits) and arrays we return a base scalar type; the surrounding declaration adds the array dimensions (see emitFieldDecl).

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.Backend.CSim.emitScalarBase Sparkle.IR.Type.HWType.bit = "uint8_t"
• Sparkle.Backend.CSim.emitScalarBase (Sparkle.IR.Type.HWType.array size elemType) = Sparkle.Backend.CSim.emitScalarBase elemType
• Sparkle.Backend.CSim.emitScalarBase (Sparkle.IR.Type.HWType.bitVectorDim width) = "SPARKLE_UNSUPPORTED_SYMBOLIC_WIDTH"

partial def Sparkle.Backend.CSim.emitArraySuffix : IR.Type.HWType → String

Total array length suffix for a HWType, e.g. [3] for a 96-bit wide type, [8][3] for array 8 (bitVector 96), or empty for a single ≤ 64-bit scalar.

def Sparkle.Backend.CSim.emitFieldDecl (ty : IR.Type.HWType) (name : String) : String

Emit a C field/local declaration like uint32_t foo[3] — the type goes on the left, the array dimensions on the right of the name (C array syntax).

Equations

• Sparkle.Backend.CSim.emitFieldDecl ty name = toString (Sparkle.Backend.CSim.emitScalarBase ty) ++ toString " " ++ toString name ++ toString (Sparkle.Backend.CSim.emitArraySuffix ty)

def Sparkle.Backend.CSim.emitTypeName (ty : IR.Type.HWType) : String

For situations where a parameter or declaration needs just the type and dimensions but no identifier, used by casts.

Equations

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

def Sparkle.Backend.CSim.needsMask (w : Nat) : Bool

True for widths that are not native C integer widths.

Equations

• Sparkle.Backend.CSim.needsMask w = (w != 8 && w != 16 && w != 32 && w != 64)

def Sparkle.Backend.CSim.emitMask (w : Nat) : String

Emit a bit mask expression for the given width

Equations

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

def Sparkle.Backend.CSim.applyMask (expr : String) (w : Nat) : String

Wrap an expression with a mask if the width requires it

Equations

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

partial def Sparkle.Backend.CSim.exprIsMasked (w : Nat) : IR.AST.Expr → Bool

Check if an IR expression produces a result that is already correctly masked. Invariant: every assignment applies a mask, so .ref reads yield masked values.

def Sparkle.Backend.CSim.emitCOperator (op : IR.AST.Operator) : String

Convert Operator to C operator symbol

Equations

• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.and = "&"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.or = "|"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.xor = "^"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.not = "~"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.add = "+"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.sub = "-"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.mul = "*"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.eq = "=="
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.lt_u = "<"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.lt_s = "<"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.le_u = "<="
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.le_s = "<="
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.gt_u = ">"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.gt_s = ">"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.ge_u = ">="
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.ge_s = ">="
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.shl = "<<"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.shr = ">>"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.asr = ">>"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.neg = "-"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.mux = "?"

def Sparkle.Backend.CSim.signedCastType (w : Nat) : String

Get signed cast type for a given width

Equations

• Sparkle.Backend.CSim.signedCastType w = if w ≤ 8 then "int8_t" else if w ≤ 16 then "int16_t" else if w ≤ 32 then "int32_t" else "int64_t"

partial def Sparkle.Backend.CSim.inferExprWidth (typeMap : TypeMap) : IR.AST.Expr → Nat

Best-effort width inference for an expression

partial def Sparkle.Backend.CSim.emitExpr (typeMap : TypeMap) (e : IR.AST.Expr) : String

Convert IR expression to C expression.

Wide (> 64 bit) values are represented as uint32_t[N] arrays in declarations. In expression contexts an "rvalue array" doesn't really exist in C, so the only ways we produce wide expressions are:

• .ref to a wide variable — emits the bare identifier, which C decays to a pointer in most contexts; the wide-assign code below indexes it slot-by-slot rather than copying.
• .const with width > 64 — emits a C99 compound literal (uint32_t[N]){w0, w1, …}, which is a valid rvalue only at statement scope.
• .concat over wide totals — same compound-literal shape.

All wide assignments (see emitStmt) must therefore either: (a) be element-wise slot writes (lhs[j] = …), or (b) wrap the RHS in memcpy(lhs, RHS, sizeof(lhs)) when RHS is a compound literal — lhs = RHS on a C array is rejected by the compiler.

structure Sparkle.Backend.CSim.StmtParts : Type

Parts of a C struct + helper-set generated from a single statement

• declarations : List String
• evalBody : List String
• tickBody : List String
• resetBody : List String
• evalTickLocals : List String

@[implicit_reducible]

instance Sparkle.Backend.CSim.instInhabitedStmtParts : Inhabited StmtParts

Equations

• Sparkle.Backend.CSim.instInhabitedStmtParts = { default := Sparkle.Backend.CSim.instInhabitedStmtParts.default }

@[implicit_reducible]

instance Sparkle.Backend.CSim.instAppendStmtParts : Append StmtParts

Equations

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

def Sparkle.Backend.CSim.StmtParts.empty : StmtParts

Equations

• Sparkle.Backend.CSim.StmtParts.empty = { declarations := [], evalBody := [], tickBody := [], resetBody := [], evalTickLocals := [] }

def Sparkle.Backend.CSim.emitInitScalar (initValue : Int) (width : Nat) : String

Emit a C reset value for a register init.

For ≤ 64-bit widths returns a scalar cast.

For wide (> 64-bit) widths returns a list of slot assignments like lhs[0] = 0x…u; lhs[1] = 0x…u; since C does not let you assign a compound literal to an array-typed lvalue. The caller (register reset path) threads these through resetBody.

Equations

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

def Sparkle.Backend.CSim.emitInitWideLines (name : String) (initValue : Int) (width : Nat) : List String

Per-slot reset lines for a wide register name.

Equations

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

def Sparkle.Backend.CSim.emitMuxAsIfElse (typeMap : TypeMap) (lhsName : String) (width : Nat) (rhs : IR.AST.Expr) (minArms : Nat := 4) : List String

Emit a MUX chain as if-else block for better branch prediction.

Equations

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

partial def Sparkle.Backend.CSim.emitStmt (stmt : IR.AST.Stmt) (typeMap : TypeMap) (design : Option IR.AST.Design := none) : StmtParts

Split a statement into declaration/eval/tick/reset parts

partial def Sparkle.Backend.CSim.emitStmt.matWide (typeMap : TypeMap) (sn : String) (nWords : Nat) (shlSlot : String → Nat → Nat → String) (shrSlot : String → Nat → Nat → Nat → String) (label : String) (e : IR.AST.Expr) : List String × String

partial def Sparkle.Backend.CSim.collectExprRefsAux (acc : List String) : IR.AST.Expr → List String

Collect all wire name references from an IR expression

def Sparkle.Backend.CSim.collectExprRefs (e : IR.AST.Expr) : List String

Equations

• Sparkle.Backend.CSim.collectExprRefs e = Sparkle.Backend.CSim.collectExprRefsAux [] e

def Sparkle.Backend.CSim.collectTickRefWires (body : List IR.AST.Stmt) : List String

Collect all wire names referenced in tick() bodies.

Equations

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

def Sparkle.Backend.CSim.scheduleEvalBody (design : Option IR.AST.Design) (m : IR.AST.Module) (body : List IR.AST.Stmt) : List IR.AST.Stmt × Bool

Order the eval-relevant statements (assigns, instances, combo-read memories) topologically by def-use. The lowering's topoSortBody sorts ASSIGNS only and appends instances last, so a parent's combinational logic that CONSUMES a child instance's outputs was emitted before the child's eval call and read stale values — a Mealy path through a sub-module (XiangShan CVT64: parent mantissa logic reads the Lzc child's leadZeros output). Registers and non-combo memories contribute nothing to eval (they latch in tick), so they keep their original relative order at the end; on a combinational cycle the remaining statements fall back to source order (single-pass semantics, as before).

Equations

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

def Sparkle.Backend.CSim.wideShrHelper (funcQual : String) : String

Runtime helper for a DYNAMIC shift of a >64-bit value consumed in a ≤64-bit context (firtool's flattened packed-array dynamic select: (_GEN >> (addr * 8)) & 0xff with a multi-word _GEN): returns the 64-bit window starting at bit amt. Emitted (once, guarded) ahead of every module so nested wide shifts have a valid C rendering — the raw form array >> amt is not C at all.

Equations

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

partial def Sparkle.Backend.CSim.exprHasSymbolicWidth : IR.AST.Expr → Bool

Reject unspecialized parameterized IR at CSim module boundaries before concrete-width helpers can observe it. Use the explicit specialization entry points below to emit one fixed-ABI C model for a chosen parameter configuration.

def Sparkle.Backend.CSim.moduleHasSymbolicWidth (m : IR.AST.Module) : Bool

Equations

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

def Sparkle.Backend.CSim.unsupportedSymbolicWidthError : String

Equations

• Sparkle.Backend.CSim.unsupportedSymbolicWidthError = "#error \"Sparkle CSim requires concrete widths; specialize retained parameters before emission\"\n"

def Sparkle.Backend.CSim.emitModule (m : IR.AST.Module) (design : Option IR.AST.Design := none) (observableWires : Option (List String) := none) (funcQual : String := "") : String

Emit a complete C struct + static helpers for a module. Returns the full C source fragment (no includes; callers add those at design level).

Equations

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

def Sparkle.Backend.CSim.hoistWideForC (m : IR.AST.Module) : IR.AST.Module

Backend-local pre-pass: hoist wide (>64-bit) compound expressions out of positions the C emitter cannot render inline, into their own wires. C has no expression form for a multi-word value, so a wide compound is only renderable where the emitter MATERIALISES it (matWide under an assign/register, wideConnLines for slice connections). Everywhere else — an instance connection built from a mux-of-concats (DivUnit's csa_sel operands), a wide operand of a comparison (ShiftRightJam's |(io_in & sticky_mask)), a wide arm of a mux whose RESULT is ≤64 bits (SBToTL's cond ? 64'h0 : {…}) — emitExpr used to render a compound literal into scalar arithmetic and the C did not compile. Hoisting each such subexpression into a wire routes it through the well-tested wide-assign machinery; scalar consumers then read the wire, which every arm already handles. Semantically neutral: the hoisted cones are combinational and effect-free.

Equations

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

@[irreducible]

def Sparkle.Backend.CSim.hoistWideForC.fix (tm : TypeMap) (hoist : IR.AST.Expr → Nat → Nat → IR.AST.Expr × IR.AST.Stmt × IR.AST.Port) (isCompound : IR.AST.Expr → Bool) (top : Bool) (e : IR.AST.Expr) : StateM (Nat × List IR.AST.Stmt × List IR.AST.Port) IR.AST.Expr

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.Backend.CSim.hoistWideForC.fix tm hoist isCompound top (a.sliceDim hi lo) = do let a' ← Sparkle.Backend.CSim.hoistWideForC.fix tm hoist isCompound false a pure (a'.sliceDim hi lo)
• Sparkle.Backend.CSim.hoistWideForC.fix tm hoist isCompound top e = pure e

def Sparkle.Backend.CSim.toCDesign (d : IR.AST.Design) (observableWires : Option (List String) := none) (funcQual : String := "") : String

Convert a full design to C simulation code (no JIT wrapper)

Equations

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

def Sparkle.Backend.CSim.toCDesignWithParameters (d : IR.AST.Design) (bindings : IR.Specialize.Bindings) (observableWires : Option (List String) := none) (funcQual : String := "") : Except String String

Specialize retained dimensions for one explicit configuration, then emit a fixed-ABI C model for the whole design.

Equations

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

def Sparkle.Backend.CSim.toC (m : IR.AST.Module) : String

Convert a single module to C simulation code with includes

Equations

• Sparkle.Backend.CSim.toC m = "#include <stdint.h>\n" ++ "#include <stdlib.h>\n" ++ "#include <string.h>\n\n" ++ Sparkle.Backend.CSim.emitModule m

def Sparkle.Backend.CSim.toCWithParameters (m : IR.AST.Module) (bindings : IR.Specialize.Bindings) : Except String String

Specialize retained dimensions for one explicit configuration, then emit a fixed-ABI C model for a single module.

Equations

• Sparkle.Backend.CSim.toCWithParameters m bindings = do let concrete ← Sparkle.IR.Specialize.specializeModule m bindings pure (Sparkle.Backend.CSim.toC concrete)

JIT FFI wrapper

Each .so exports exactly ONE symbol — jit_vtable — which returns a pointer to a JitVTable containing function pointers for every operation. Everything else is static, so dlsym cannot reach it. This sidesteps the collision-on- shared-symbol problem from Issue #70: two .so files with the same internal jit_eval cannot conflict because neither publishes that name.

def Sparkle.Backend.CSim.toCJIT (d : IR.AST.Design) (observableWires : Option (List String) := none) : String

Equations

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

def Sparkle.Backend.CSim.toCJITWithParameters (d : IR.AST.Design) (bindings : IR.Specialize.Bindings) (observableWires : Option (List String) := none) : Except String String

Specialize retained dimensions for one explicit configuration, then emit the fixed-ABI C JIT wrapper.

Equations

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