class Sparkle.Core.Sim.Sim (S : Type) (I O : outParam Type) : Type

The unified simulation interface.

S is the per-design simulator state (e.g. Foo.Sim.Simulator). I is the typed input record, O the output record. Both are outParams so writing sim.step inp lets Lean infer them.

All four methods are IO-monadic; backends that don't need to run effects (pure-Lean) still wrap their work in IO so the call-site signature is identical across backends.

• reset : S → IO Unit

  Restore the simulator to its initial state (cycle 0, registers at their declared init values).

• step : S → I → IO Unit

  Drive the inputs and advance one clock cycle.

• read : S → IO O

  Read the current outputs.

• destroy : S → IO Unit

  Release any resources (close the dlopen handle, free Verilator obj_dir, ...). Implementations should be idempotent.

def Sparkle.Core.Sim.Sim.trace {S I O : Type} [Sim S I O] (sim : S) (inputs : List I) : IO (List O)

Run n cycles, returning the per-cycle output trace. Convenience wrapper over step + read; useful for chapter-scale demos where you don't want to hand-roll a for loop.

Equations

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

def Sparkle.Core.Sim.Sim.run {S I O : Type} [Sim S I O] (sim : S) (n : Nat) (i : I) : IO (List O)

Run n cycles with a constant input. Handy when the input is "no inputs" (a SimInput with no fields), since callers can write sim.run 100 {}.

Equations

• Sparkle.Core.Sim.Sim.run sim n i = Sparkle.Core.Sim.Sim.trace sim (List.replicate n i)