structure Sparkle.Core.SimParallel.SimEndpoint : Type

Everything runSim needs about one loaded JIT domain. Usually built via someModule.Sim.Simulator.toEndpoint.

• handle : JIT.JITHandle
• moduleName : String
• lookupOutput : String → Option UInt32
• lookupInput : String → Option UInt32
• outputNames : List String
• inputNames : List String

@[reducible, inline]

abbrev Sparkle.Core.SimParallel.Connection : Type

(producerOutputPortName, consumerInputPortName) — a single wire connection between two domains routed through the CDC SPSC queue.

Equations

• Sparkle.Core.SimParallel.Connection = (String × String)

structure Sparkle.Core.SimParallel.SimStats : Type

Aggregated statistics returned by runSim. For single-domain runs, messagesSent/messagesReceived/rollbacks are all 0.

• cyclesRun : UInt64
• messagesSent : UInt64
• messagesReceived : UInt64
• rollbacks : UInt64

instance Sparkle.Core.SimParallel.instReprSimStats : Repr SimStats

Equations

• Sparkle.Core.SimParallel.instReprSimStats = { reprPrec := Sparkle.Core.SimParallel.instReprSimStats.repr }

def Sparkle.Core.SimParallel.instReprSimStats.repr : SimStats → Nat → Std.Format

Equations

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

def Sparkle.Core.SimParallel.runSingleSim (ep : SimEndpoint) (cycles : UInt64) : IO SimStats

Single-threaded evalTick loop. Forces the non-parallel backend. Use this directly if you want to bypass runSim's auto-selection.

Equations

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

def Sparkle.Core.SimParallel.runMultiDomainSim (producer consumer : SimEndpoint) (connection : Connection) (producerCycles consumerCycles : UInt64) : IO SimStats

Multi-domain CDC runner backed by JIT.runCDC. Forces the parallel backend. Use this directly if you want to skip runSim dispatch.

Raises IO.userError if the connection names are not valid ports of the producer/consumer endpoints.

Equations

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

def Sparkle.Core.SimParallel.runSim (endpoints : List SimEndpoint) (connections : List Connection := []) (cycles : UInt64 := 0) (endpointCycles : List UInt64 := []) : IO SimStats

High-level dispatcher: automatically picks the fastest runner.

Rules:

• [ep] with no connections → runSingleSim (fastest for 1 domain)
• [prod, cons] with one connection → runMultiDomainSim (CDC queue)
• anything else → IO.userError describing the limitation.

cycles sets a uniform cycle budget that applies to every endpoint. To model a CDC with genuinely different clock frequencies (e.g. a 200 MHz producer talking to a 100 MHz consumer) pass endpointCycles instead: it gives a per-endpoint cycle count and cycles is ignored when it is non-empty. The list must have the same length as endpoints.

Limitations:

• 3+ endpoints are not yet supported (needs multi-queue runCDC).
• Multi-connection between the same pair of endpoints is not yet supported (needs runCDC extension). See KnownIssues Issue 3.

Equations

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