Stability Property Registration

A stability property records that a signal maintains a specific value for a known duration.

structure Sparkle.Core.OptimizedSim.StabilityProperty (d : Domain.DomainConfig) : Type

• signalId : String
• startCycle : Nat
• value : Nat
• duration : Nat

def Sparkle.Core.OptimizedSim.StabilityProperty.applies {d : Domain.DomainConfig} (prop : StabilityProperty d) (signalId : String) (currentCycle : Nat) : Bool

Equations

• prop.applies signalId currentCycle = (prop.signalId == signalId && decide (currentCycle ≥ prop.startCycle) && decide (currentCycle < prop.startCycle + prop.duration))

def Sparkle.Core.OptimizedSim.StabilityProperty.remainingCycles {d : Domain.DomainConfig} (prop : StabilityProperty d) (currentCycle : Nat) : Nat

Equations

• prop.remainingCycles currentCycle = prop.startCycle + prop.duration - currentCycle

Temporal Property Registry

Stores proven stability properties that can be used for cycle-skipping.

structure Sparkle.Core.OptimizedSim.PropertyRegistry (d : Domain.DomainConfig) : Type

• properties : List (StabilityProperty d)

def Sparkle.Core.OptimizedSim.PropertyRegistry.empty {d : Domain.DomainConfig} : PropertyRegistry d

Create an empty property registry

Equations

• Sparkle.Core.OptimizedSim.PropertyRegistry.empty = { properties := [] }

def Sparkle.Core.OptimizedSim.PropertyRegistry.addProperty {d : Domain.DomainConfig} (reg : PropertyRegistry d) (prop : StabilityProperty d) : PropertyRegistry d

Add a stability property to the registry

Equations

• reg.addProperty prop = { properties := prop :: reg.properties }

def Sparkle.Core.OptimizedSim.PropertyRegistry.canSkip {d : Domain.DomainConfig} (reg : PropertyRegistry d) (signalId : String) (currentCycle : Nat) : Option (Nat × Nat)

Query if we can skip cycles for a signal at current time

Equations

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

Simulation Statistics

structure Sparkle.Core.OptimizedSim.SimulationStats : Type

• totalCycles : Nat
• evaluatedCycles : Nat
• skippedCycles : Nat
• skipEvents : Nat

instance Sparkle.Core.OptimizedSim.instReprSimulationStats : Repr SimulationStats

Equations

• Sparkle.Core.OptimizedSim.instReprSimulationStats = { reprPrec := Sparkle.Core.OptimizedSim.instReprSimulationStats.repr }

def Sparkle.Core.OptimizedSim.instReprSimulationStats.repr : SimulationStats → Nat → Std.Format

Equations

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

def Sparkle.Core.OptimizedSim.SimulationStats.init : SimulationStats

Equations

• Sparkle.Core.OptimizedSim.SimulationStats.init = { totalCycles := 0, evaluatedCycles := 0, skippedCycles := 0, skipEvents := 0 }

def Sparkle.Core.OptimizedSim.SimulationStats.addEvaluation (stats : SimulationStats) : SimulationStats

Equations

• stats.addEvaluation = { totalCycles := stats.totalCycles, evaluatedCycles := stats.evaluatedCycles + 1, skippedCycles := stats.skippedCycles, skipEvents := stats.skipEvents }

def Sparkle.Core.OptimizedSim.SimulationStats.addSkip (stats : SimulationStats) (n : Nat) : SimulationStats

Equations

• stats.addSkip n = { totalCycles := stats.totalCycles, evaluatedCycles := stats.evaluatedCycles, skippedCycles := stats.skippedCycles + n, skipEvents := stats.skipEvents + 1 }

def Sparkle.Core.OptimizedSim.SimulationStats.speedup (stats : SimulationStats) : Float

Equations

• stats.speedup = if (stats.evaluatedCycles == 0) = true then 1.0 else (stats.evaluatedCycles.toFloat + stats.skippedCycles.toFloat) / stats.evaluatedCycles.toFloat

def Sparkle.Core.OptimizedSim.SimulationStats.toString (stats : SimulationStats) : String

Equations

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

instance Sparkle.Core.OptimizedSim.SimulationStats.instToString : ToString SimulationStats

Equations

• Sparkle.Core.OptimizedSim.SimulationStats.instToString = { toString := Sparkle.Core.OptimizedSim.SimulationStats.toString }

Optimized Simulator

def Sparkle.Core.OptimizedSim.simulateOptimized {d : Domain.DomainConfig} (registry : PropertyRegistry d) (signalId : String) (signal : Signal.Signal d Nat) (maxCycles : Nat) : List Nat × SimulationStats

Simulate with cycle-skipping optimization (Nat signals only for simplicity)

Equations

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

partial def Sparkle.Core.OptimizedSim.simulateOptimized.sim {d : Domain.DomainConfig} (registry : PropertyRegistry d) (signalId : String) (signal : Signal.Signal d Nat) (maxCycles t : Nat) (acc : List Nat) (stats : SimulationStats) : List Nat × SimulationStats

def Sparkle.Core.OptimizedSim.simulateStandard {d : Domain.DomainConfig} (signal : Signal.Signal d Nat) (maxCycles : Nat) : List Nat

Simulate without optimization (for comparison)

Equations

• Sparkle.Core.OptimizedSim.simulateStandard signal maxCycles = List.map signal.atTime (List.range maxCycles)

Helper Functions

def Sparkle.Core.OptimizedSim.mkStabilityProperty {d : Domain.DomainConfig} (signalId : String) (value startCycle duration : Nat) : StabilityProperty d

Equations

• Sparkle.Core.OptimizedSim.mkStabilityProperty signalId value startCycle duration = { signalId := signalId, startCycle := startCycle, value := value, duration := duration }

def Sparkle.Core.OptimizedSim.registryWith {d : Domain.DomainConfig} (prop : StabilityProperty d) : PropertyRegistry d

Equations

• Sparkle.Core.OptimizedSim.registryWith prop = Sparkle.Core.OptimizedSim.PropertyRegistry.empty.addProperty prop

Example Usage

def Sparkle.Core.OptimizedSim.resetCounter : Signal.Signal Domain.defaultDomain Nat

Equations

• Sparkle.Core.OptimizedSim.resetCounter = { val := fun (t : Nat) => if t < 1000 then 0 else t - 1000 }

def Sparkle.Core.OptimizedSim.resetCounterProperty : StabilityProperty Domain.defaultDomain

Equations

• Sparkle.Core.OptimizedSim.resetCounterProperty = Sparkle.Core.OptimizedSim.mkStabilityProperty "resetCounter" 0 0 1000

def Sparkle.Core.OptimizedSim.resetCounterRegistry : PropertyRegistry Domain.defaultDomain

Equations

• Sparkle.Core.OptimizedSim.resetCounterRegistry = Sparkle.Core.OptimizedSim.registryWith Sparkle.Core.OptimizedSim.resetCounterProperty

def Sparkle.Core.OptimizedSim.testResetCounter : IO Unit

Equations

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