Signal Module

This module defines the stream-based signal semantics for Sparkle HDL.

Overview

Signals represent time-varying hardware values using infinite streams. A Signal d α is essentially a function Nat → α where Nat represents discrete time steps (clock cycles).

Key Concepts

• Stream: An infinite sequence Nat → α representing values over time
• Signal: A stream tagged with a clock domain for type safety
• Domain: Type-level clock domain tracking prevents mixing signals from different clocks

Core Primitives

Registers

Use Signal.register init input to create state elements (delays by 1 cycle):

-- Simple register chain (feed-forward)
def registerChain (input : Signal Domain (BitVec 8)) : Signal Domain (BitVec 8) :=
  let d1 := Signal.register 0#8 input
  let d2 := Signal.register 0#8 d1
  d2

-- Counter with feedback (requires let rec)
def counter {dom : DomainConfig} : Signal dom (BitVec 8) :=
  let rec count := Signal.register 0#8 (count.map (· + 1))
  count

Multiplexers

Use Signal.mux for conditional logic (NOT if-then-else):

def conditionalInc (enable : Signal Domain Bool) (input : Signal Domain (BitVec 8))
    : Signal Domain (BitVec 8) :=
  let next := input.map (· + 1)
  Signal.mux enable next input  -- Select between increment or hold

Simulation

Signals can be simulated directly to verify behavior before synthesis:

#eval Signal.simulate myCircuit inputs |>.take 10

See also: Sparkle.Core.Domain for clock domain configuration.

def Sparkle.Core.Signal.Stream (α : Type u) : Type u

Stream is an infinite sequence of values indexed by natural numbers. Time 0 is the initial state, time 1 is after first clock cycle, etc.

Equations

• Sparkle.Core.Signal.Stream α = (Nat → α)

structure Sparkle.Core.Signal.Signal (dom : Domain.DomainConfig) (α : Type u) : Type u

Signal represents a time-varying value in a specific clock domain. It wraps a Stream and carries domain information at the type level.

The domain parameter ensures signals from different clock domains cannot be accidentally mixed.

• val : Stream α

instance Sparkle.Core.Signal.instInhabitedSignal {α : Type u_1} {dom : Domain.DomainConfig} [Inhabited α] : Inhabited (Signal dom α)

Equations

• Sparkle.Core.Signal.instInhabitedSignal = { default := { val := fun (x : Nat) => default } }

@[inline]

def Sparkle.Core.Signal.Signal.atTime {dom : Domain.DomainConfig} {α : Type u} (s : Signal dom α) (t : Nat) : α

Access the value of a signal at a specific time

Equations

• s.atTime t = s.val t

def Sparkle.Core.Signal.Signal.pure {dom : Domain.DomainConfig} {α : Type u} (x : α) : Signal dom α

Create a constant signal (same value at all times)

Equations

• Sparkle.Core.Signal.Signal.pure x = { val := fun (x_1 : Nat) => x }

def Sparkle.Core.Signal.Signal.map {dom : Domain.DomainConfig} {α β : Type u} (f : α → β) (s : Signal dom α) : Signal dom β

Map a function over a signal (combinational logic)

Equations

• Sparkle.Core.Signal.Signal.map f s = { val := fun (t : Nat) => f (s.val t) }

def Sparkle.Core.Signal.Signal.ap {dom : Domain.DomainConfig} {α β : Type u} (sf : Signal dom (α → β)) (s : Signal dom α) : Signal dom β

Apply a signal of functions to a signal of values

Equations

• sf.ap s = { val := fun (t : Nat) => sf.val t (s.val t) }

def Sparkle.Core.Signal.Signal.seq {dom : Domain.DomainConfig} {α β : Type u} (sf : Signal dom (α → β)) (s : Unit → Signal dom α) : Signal dom β

Sequence two signals

Equations

• sf.seq s = sf.ap (s ())

def Sparkle.Core.Signal.Signal.bind {dom : Domain.DomainConfig} {α β : Type u} (s : Signal dom α) (f : α → Signal dom β) : Signal dom β

Monadic bind for signals

Equations

• s.bind f = { val := fun (t : Nat) => (f (s.val t)).val t }

def Sparkle.Core.Signal.Signal.register {dom : Domain.DomainConfig} {α : Type u} (init : α) (input : Signal dom α) : Signal dom α

Register (D Flip-Flop) primitive.

At time 0: outputs the initial value At time t > 0: outputs the input value from time (t-1)

This implements a single-cycle delay, the fundamental building block of sequential logic.

Equations

• Sparkle.Core.Signal.Signal.register init input = { val := fun (t : Nat) => match t with | 0 => init | n.succ => input.val n }

def Sparkle.Core.Signal.Signal.registerWithEnable {dom : Domain.DomainConfig} {α : Type u} (init : α) (en : Signal dom Bool) (input : Signal dom α) : Signal dom α

Register with enable signal.

When enable is true: register updates normally When enable is false: register holds its current value

Equations

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

def Sparkle.Core.Signal.Signal.registerWithEnable.go {dom : Domain.DomainConfig} {α : Type u} (init : α) (en : Signal dom Bool) (input : Signal dom α) (t : Nat) (prev : α) : α

Equations

• Sparkle.Core.Signal.Signal.registerWithEnable.go init en input 0 prev = init
• Sparkle.Core.Signal.Signal.registerWithEnable.go init en input n.succ prev = if en.val n = true then input.val n else prev

def Sparkle.Core.Signal.Signal.fromStream {dom : Domain.DomainConfig} {α : Type u} (s : Stream α) : Signal dom α

Helper to create a signal from a stream

Equations

• Sparkle.Core.Signal.Signal.fromStream s = { val := s }

def Sparkle.Core.Signal.Signal.toStream {dom : Domain.DomainConfig} {α : Type u} (s : Signal dom α) : Stream α

Helper to extract stream from signal

Equations

• s.toStream = s.val

def Sparkle.Core.Signal.Signal.sample {dom : Domain.DomainConfig} {α : Type u} (s : Signal dom α) (n : Nat) : List α

Sample a signal for the first n cycles

Equations

• s.sample n = List.map s.val (List.range n)

instance Sparkle.Core.Signal.instFunctorSignal {dom : Domain.DomainConfig} : Functor (Signal dom)

Equations

• Sparkle.Core.Signal.instFunctorSignal = { map := fun {α β : Type ?u.14} => Sparkle.Core.Signal.Signal.map }

instance Sparkle.Core.Signal.instApplicativeSignal {dom : Domain.DomainConfig} : Applicative (Signal dom)

Equations

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

instance Sparkle.Core.Signal.instMonadSignal {dom : Domain.DomainConfig} : Monad (Signal dom)

Equations

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

instance Sparkle.Core.Signal.instHAddSignalBitVec {dom : Domain.DomainConfig} {n : Nat} : HAdd (Signal dom (BitVec n)) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

• Sparkle.Core.Signal.instHAddSignalBitVec = { hAdd := fun (a b : Sparkle.Core.Signal.Signal dom (BitVec n)) => (fun (x1 x2 : BitVec n) => x1 + x2) <$> a <*> b }

instance Sparkle.Core.Signal.instHSubSignalBitVec {dom : Domain.DomainConfig} {n : Nat} : HSub (Signal dom (BitVec n)) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

• Sparkle.Core.Signal.instHSubSignalBitVec = { hSub := fun (a b : Sparkle.Core.Signal.Signal dom (BitVec n)) => (fun (x1 x2 : BitVec n) => x1 - x2) <$> a <*> b }

instance Sparkle.Core.Signal.instHMulSignalBitVec {dom : Domain.DomainConfig} {n : Nat} : HMul (Signal dom (BitVec n)) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

• Sparkle.Core.Signal.instHMulSignalBitVec = { hMul := fun (a b : Sparkle.Core.Signal.Signal dom (BitVec n)) => (fun (x1 x2 : BitVec n) => x1 * x2) <$> a <*> b }

instance Sparkle.Core.Signal.instHAndSignalBitVec {dom : Domain.DomainConfig} {n : Nat} : HAnd (Signal dom (BitVec n)) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

• Sparkle.Core.Signal.instHAndSignalBitVec = { hAnd := fun (a b : Sparkle.Core.Signal.Signal dom (BitVec n)) => (fun (x1 x2 : BitVec n) => x1 &&& x2) <$> a <*> b }

instance Sparkle.Core.Signal.instHOrSignalBitVec {dom : Domain.DomainConfig} {n : Nat} : HOr (Signal dom (BitVec n)) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

• Sparkle.Core.Signal.instHOrSignalBitVec = { hOr := fun (a b : Sparkle.Core.Signal.Signal dom (BitVec n)) => (fun (x1 x2 : BitVec n) => x1 ||| x2) <$> a <*> b }

instance Sparkle.Core.Signal.instHXorSignalBitVec {dom : Domain.DomainConfig} {n : Nat} : HXor (Signal dom (BitVec n)) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

• Sparkle.Core.Signal.instHXorSignalBitVec = { hXor := fun (a b : Sparkle.Core.Signal.Signal dom (BitVec n)) => (fun (x1 x2 : BitVec n) => x1 ^^^ x2) <$> a <*> b }

instance Sparkle.Core.Signal.instHAppendSignalBitVecHAddNat {dom : Domain.DomainConfig} {m n : Nat} : HAppend (Signal dom (BitVec m)) (Signal dom (BitVec n)) (Signal dom (BitVec (m + n)))

Equations

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

instance Sparkle.Core.Signal.instHAppendSignalBitVecHAddNat_1 {dom : Domain.DomainConfig} {m n : Nat} : HAppend (Signal dom (BitVec m)) (BitVec n) (Signal dom (BitVec (m + n)))

Equations

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

instance Sparkle.Core.Signal.instHAppendBitVecSignalHAddNat {m : Nat} {dom : Domain.DomainConfig} {n : Nat} : HAppend (BitVec m) (Signal dom (BitVec n)) (Signal dom (BitVec (m + n)))

Equations

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

instance Sparkle.Core.Signal.instHAddSignalBitVec_1 {dom : Domain.DomainConfig} {n : Nat} : HAdd (Signal dom (BitVec n)) (BitVec n) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHAddBitVecSignal {n : Nat} {dom : Domain.DomainConfig} : HAdd (BitVec n) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHSubSignalBitVec_1 {dom : Domain.DomainConfig} {n : Nat} : HSub (Signal dom (BitVec n)) (BitVec n) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHSubBitVecSignal {n : Nat} {dom : Domain.DomainConfig} : HSub (BitVec n) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHMulSignalBitVec_1 {dom : Domain.DomainConfig} {n : Nat} : HMul (Signal dom (BitVec n)) (BitVec n) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHMulBitVecSignal {n : Nat} {dom : Domain.DomainConfig} : HMul (BitVec n) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHAndSignalBitVec_1 {dom : Domain.DomainConfig} {n : Nat} : HAnd (Signal dom (BitVec n)) (BitVec n) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHAndBitVecSignal {n : Nat} {dom : Domain.DomainConfig} : HAnd (BitVec n) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHOrSignalBitVec_1 {dom : Domain.DomainConfig} {n : Nat} : HOr (Signal dom (BitVec n)) (BitVec n) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHOrBitVecSignal {n : Nat} {dom : Domain.DomainConfig} : HOr (BitVec n) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHXorSignalBitVec_1 {dom : Domain.DomainConfig} {n : Nat} : HXor (Signal dom (BitVec n)) (BitVec n) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHXorBitVecSignal {n : Nat} {dom : Domain.DomainConfig} : HXor (BitVec n) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHShiftLeftSignalBitVec {dom : Domain.DomainConfig} {n : Nat} : HShiftLeft (Signal dom (BitVec n)) (BitVec n) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHShiftLeftBitVecSignal {n : Nat} {dom : Domain.DomainConfig} : HShiftLeft (BitVec n) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHShiftRightSignalBitVec {dom : Domain.DomainConfig} {n : Nat} : HShiftRight (Signal dom (BitVec n)) (BitVec n) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHShiftRightBitVecSignal {n : Nat} {dom : Domain.DomainConfig} : HShiftRight (BitVec n) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

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

instance Sparkle.Core.Signal.instHAndSignalBool {dom : Domain.DomainConfig} : HAnd (Signal dom Bool) (Signal dom Bool) (Signal dom Bool)

Equations

• Sparkle.Core.Signal.instHAndSignalBool = { hAnd := fun (a b : Sparkle.Core.Signal.Signal dom Bool) => (fun (x1 x2 : Bool) => x1 && x2) <$> a <*> b }

instance Sparkle.Core.Signal.instHOrSignalBool {dom : Domain.DomainConfig} : HOr (Signal dom Bool) (Signal dom Bool) (Signal dom Bool)

Equations

• Sparkle.Core.Signal.instHOrSignalBool = { hOr := fun (a b : Sparkle.Core.Signal.Signal dom Bool) => (fun (x1 x2 : Bool) => x1 || x2) <$> a <*> b }

instance Sparkle.Core.Signal.instHXorSignalBool {dom : Domain.DomainConfig} : HXor (Signal dom Bool) (Signal dom Bool) (Signal dom Bool)

Equations

• Sparkle.Core.Signal.instHXorSignalBool = { hXor := fun (a b : Sparkle.Core.Signal.Signal dom Bool) => (fun (x1 x2 : Bool) => x1 ^^ x2) <$> a <*> b }

instance Sparkle.Core.Signal.instComplementSignalBool {dom : Domain.DomainConfig} : Complement (Signal dom Bool)

Equations

• Sparkle.Core.Signal.instComplementSignalBool = { complement := fun (a : Sparkle.Core.Signal.Signal dom Bool) => (fun (x : Bool) => !x) <$> a }

instance Sparkle.Core.Signal.instComplementSignalBitVec {dom : Domain.DomainConfig} {n : Nat} : Complement (Signal dom (BitVec n))

Equations

• Sparkle.Core.Signal.instComplementSignalBitVec = { complement := fun (a : Sparkle.Core.Signal.Signal dom (BitVec n)) => (fun (x : BitVec n) => ~~~x) <$> a }

instance Sparkle.Core.Signal.instHShiftLeftSignalBitVec_1 {dom : Domain.DomainConfig} {n : Nat} : HShiftLeft (Signal dom (BitVec n)) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

• Sparkle.Core.Signal.instHShiftLeftSignalBitVec_1 = { hShiftLeft := fun (a b : Sparkle.Core.Signal.Signal dom (BitVec n)) => (fun (x1 x2 : BitVec n) => x1 <<< x2) <$> a <*> b }

instance Sparkle.Core.Signal.instHShiftRightSignalBitVec_1 {dom : Domain.DomainConfig} {n : Nat} : HShiftRight (Signal dom (BitVec n)) (Signal dom (BitVec n)) (Signal dom (BitVec n))

Equations

• Sparkle.Core.Signal.instHShiftRightSignalBitVec_1 = { hShiftRight := fun (a b : Sparkle.Core.Signal.Signal dom (BitVec n)) => (fun (x1 x2 : BitVec n) => x1 >>> x2) <$> a <*> b }

def Sparkle.Core.Signal.Signal.lt {α : Type} {dom : Domain.DomainConfig} [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] (a b : Signal dom α) : Signal dom Bool

Unsigned less-than: a <ₛ b on signals.

Equations

• a.lt b = (fun (x y : α) => decide (x < y)) <$> a <*> b

def Sparkle.Core.Signal.Signal.le {α : Type} {dom : Domain.DomainConfig} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (a b : Signal dom α) : Signal dom Bool

Unsigned less-or-equal: a ≤ₛ b on signals.

Equations

• a.le b = (fun (x y : α) => decide (x ≤ y)) <$> a <*> b

def Sparkle.Core.Signal.Signal.slt {dom : Domain.DomainConfig} {n : Nat} (a b : Signal dom (BitVec n)) : Signal dom Bool

Signed less-than on BitVec signals.

Equations

• a.slt b = (fun (x1 x2 : BitVec n) => x1.slt x2) <$> a <*> b

def Sparkle.Core.Signal.Signal.ult {dom : Domain.DomainConfig} {n : Nat} (a b : Signal dom (BitVec n)) : Signal dom Bool

Unsigned less-than on BitVec signals.

Equations

• a.ult b = (fun (x1 x2 : BitVec n) => x1.ult x2) <$> a <*> b

def Sparkle.Core.Signal.Signal.sle {dom : Domain.DomainConfig} {n : Nat} (a b : Signal dom (BitVec n)) : Signal dom Bool

Signed less-or-equal on BitVec signals.

Equations

• a.sle b = (fun (x1 x2 : BitVec n) => x1.sle x2) <$> a <*> b

def Sparkle.Core.Signal.Signal.ule {dom : Domain.DomainConfig} {n : Nat} (a b : Signal dom (BitVec n)) : Signal dom Bool

Unsigned less-or-equal on BitVec signals.

Equations

• a.ule b = (fun (x1 x2 : BitVec n) => x1.ule x2) <$> a <*> b

def Sparkle.Core.Signal.Signal.ashr {dom : Domain.DomainConfig} {n : Nat} (a b : Signal dom (BitVec n)) : Signal dom (BitVec n)

Arithmetic shift right on BitVec signals.

Equations

• a.ashr b = (fun (x y : BitVec n) => x.sshiftRight y.toNat) <$> a <*> b

def Sparkle.Core.Signal.Signal.sltC {dom : Domain.DomainConfig} {n : Nat} (a : Signal dom (BitVec n)) (b : BitVec n) : Signal dom Bool

Equations

• a.sltC b = (fun (x : BitVec n) => x.slt b) <$> a

def Sparkle.Core.Signal.Signal.ultC {dom : Domain.DomainConfig} {n : Nat} (a : Signal dom (BitVec n)) (b : BitVec n) : Signal dom Bool

Equations

• a.ultC b = (fun (x : BitVec n) => x.ult b) <$> a

def Sparkle.Core.Signal.Signal.ashrC {dom : Domain.DomainConfig} {n : Nat} (a : Signal dom (BitVec n)) (b : BitVec n) : Signal dom (BitVec n)

Equations

• a.ashrC b = (fun (x : BitVec n) => x.sshiftRight b.toNat) <$> a

instance Sparkle.Core.Signal.instNegSignalBitVec {dom : Domain.DomainConfig} {n : Nat} : Neg (Signal dom (BitVec n))

Equations

• Sparkle.Core.Signal.instNegSignalBitVec = { neg := fun (a : Sparkle.Core.Signal.Signal dom (BitVec n)) => (fun (x : BitVec n) => -x) <$> a }

def Sparkle.Core.Signal.Signal.beq {α : Type} {dom : Domain.DomainConfig} [BEq α] (a b : Signal dom α) : Signal dom Bool

Hardware equality: a === b compares two signals element-wise each cycle.

Equations

• a.beq b = (fun (x1 x2 : α) => x1 == x2) <$> a <*> b

def Sparkle.Core.Signal.«term_===_» : Lean.TrailingParserDescr

Equations

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

@[reducible, inline]

abbrev Sparkle.Core.Signal.Signal.lit {α : Type u_1} (dom : Domain.DomainConfig) (x : α) : Signal dom α

Constant signal with explicit domain binding. Use instead of Signal.pure when the domain can't be inferred: let rnd := Signal.lit dom 32#16 instead of let rnd := Signal.pure 32#16

Equations

• Sparkle.Core.Signal.Signal.lit dom x = Sparkle.Core.Signal.Signal.pure x

def Sparkle.Core.Signal.instCoeBitVecSignal {dom : Domain.DomainConfig} {n : Nat} : Coe (BitVec n) (Signal dom (BitVec n))

Equations

• Sparkle.Core.Signal.instCoeBitVecSignal = { coe := fun (x : BitVec n) => Sparkle.Core.Signal.Signal.pure x }

def Sparkle.Core.Signal.instCoeBoolSignal {dom : Domain.DomainConfig} : Coe Bool (Signal dom Bool)

Equations

• Sparkle.Core.Signal.instCoeBoolSignal = { coe := fun (x : Bool) => Sparkle.Core.Signal.Signal.pure x }

def Sparkle.Core.Signal.Signal.lift2 {dom : Domain.DomainConfig} {α β γ : Type u} (f : α → β → γ) (sa : Signal dom α) (sb : Signal dom β) : Signal dom γ

Lift a binary operation to signals (combinational logic)

Equations

• Sparkle.Core.Signal.Signal.lift2 f sa sb = f <$> sa <*> sb

def Sparkle.Core.Signal.Signal.delay {dom : Domain.DomainConfig} {α : Type u} (n : Nat) (init : α) (s : Signal dom α) : Signal dom α

Delay a signal by n cycles, filling with initial value

Equations

• Sparkle.Core.Signal.Signal.delay n init s = { val := fun (t : Nat) => if t < n then init else s.val (t - n) }

def Sparkle.Core.Signal.Signal.counter {dom : Domain.DomainConfig} : Signal dom Nat

Create a signal that counts up from 0

Equations

• Sparkle.Core.Signal.Signal.counter = Sparkle.Core.Signal.Signal.counter.cnt

partial def Sparkle.Core.Signal.Signal.counter.cnt {dom : Domain.DomainConfig} : Signal dom Nat

def Sparkle.Core.Signal.Signal.mux {dom : Domain.DomainConfig} {α : Type u} (cond : Signal dom Bool) (thenSig elseSig : Signal dom α) : Signal dom α

Mux (multiplexer): select between two signals based on condition

Equations

• cond.mux thenSig elseSig = { val := fun (t : Nat) => if cond.val t = true then thenSig.val t else elseSig.val t }

@[implemented_by _private.Sparkle.Core.Signal.0.Sparkle.Core.Signal.Signal.memoryImpl]

opaque Sparkle.Core.Signal.Signal.memory {dom : Domain.DomainConfig} {addrWidth dataWidth : Nat} (writeAddr : Signal dom (BitVec addrWidth)) (writeData : Signal dom (BitVec dataWidth)) (writeEnable : Signal dom Bool) (readAddr : Signal dom (BitVec addrWidth)) : Signal dom (BitVec dataWidth)

@[implemented_by _private.Sparkle.Core.Signal.0.Sparkle.Core.Signal.Signal.memoryComboReadImpl]

opaque Sparkle.Core.Signal.Signal.memoryComboRead {dom : Domain.DomainConfig} {addrWidth dataWidth : Nat} (writeAddr : Signal dom (BitVec addrWidth)) (writeData : Signal dom (BitVec dataWidth)) (writeEnable : Signal dom Bool) (readAddr : Signal dom (BitVec addrWidth)) : Signal dom (BitVec dataWidth)

@[implemented_by _private.Sparkle.Core.Signal.0.Sparkle.Core.Signal.Signal.memoryWithInitImpl]

opaque Sparkle.Core.Signal.Signal.memoryWithInit {dom : Domain.DomainConfig} {addrWidth dataWidth : Nat} (initData : BitVec addrWidth → BitVec dataWidth) (writeAddr : Signal dom (BitVec addrWidth)) (writeData : Signal dom (BitVec dataWidth)) (writeEnable : Signal dom Bool) (readAddr : Signal dom (BitVec addrWidth)) : Signal dom (BitVec dataWidth)

@[irreducible]

def Sparkle.Core.Signal.Signal.loopGo {dom : Domain.DomainConfig} {α : Type} [Inhabited α] (f : Signal dom α → Signal dom α) (t : Nat) : α

The pure fixpoint value of a feedback loop, computed by strong recursion on the time index.

To compute the value at time t, we apply the loop body f to a signal that recursively supplies the already-computed values for every earlier cycle i < t and default at t and beyond. For a strictly causal f (every feedback path runs through a Signal.register, so the output at t reads only inputs strictly before t), the default placeholder at ≥ t is never observed, so this is exactly the loop's fixpoint — see loop_unfold in Sparkle/Verification/LoopProps.lean, now a theorem rather than an axiom.

The if i < t guard makes the recursion well-founded (t strictly decreases), so this is a total, axiom-free definition.

Runtime note: this naive form recomputes the < t prefix on every cycle (O(t) work per cycle → O(n²) for an n-cycle sim). The @[implemented_by loopImpl] on loop below swaps in the memoizing loopImpl for execution, keeping O(n); the pure loopGo/loop definitions are what the kernel and the proofs see.

Equations

• Sparkle.Core.Signal.Signal.loopGo f t = (f { val := fun (i : Nat) => if i < t then Sparkle.Core.Signal.Signal.loopGo f i else default }).val t

@[implemented_by _private.Sparkle.Core.Signal.0.Sparkle.Core.Signal.Signal.loopImpl]

def Sparkle.Core.Signal.Signal.loop {dom : Domain.DomainConfig} {α : Type} [Inhabited α] (f : Signal dom α → Signal dom α) : Signal dom α

Fixed-point combinator for feedback loops.

Logically this is the pure loopGo fixpoint (no axiom, no opaque, no unsafe). For execution it is compiled to the memoizing loopImpl via @[implemented_by], which keeps cycle-by-cycle simulation at O(n) instead of the O(n²) the naive loopGo would cost.

Equations

• Sparkle.Core.Signal.Signal.loop f = { val := Sparkle.Core.Signal.Signal.loopGo f }

theorem Sparkle.Core.Signal.Signal.loopGo_eq {dom : Domain.DomainConfig} {α : Type} [Inhabited α] (f : Signal dom α → Signal dom α) (t : Nat) : loopGo f t = (f { val := fun (i : Nat) => if i < t then loopGo f i else default }).val t

loopGo's defining equation, exposed for proofs.

@[implemented_by _private.Sparkle.Core.Signal.0.Sparkle.Core.Signal.Signal.memoizeImpl]

opaque Sparkle.Core.Signal.Signal.memoize {dom : Domain.DomainConfig} {α : Type} [Inhabited α] (s : Signal dom α) : Signal dom α

@[implemented_by _private.Sparkle.Core.Signal.0.Sparkle.Core.Signal.Signal.loopMemoImpl]

opaque Sparkle.Core.Signal.Signal.loopMemo {dom : Domain.DomainConfig} {α : Type} [Inhabited α] (f : Signal dom α → Signal dom α) : IO (Signal dom α)

def Sparkle.Core.Signal.Signal.cond {dom : Domain.DomainConfig} {α : Type u} (cases : List (Signal dom Bool × Signal dom α)) (default : Signal dom α) : Signal dom α

Chained conditional mux: priority-encoded multiplexer. Signal.cond [(c1, v1), (c2, v2), ...] default selects the first matching condition's value, falling back to default.

Equations

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

def Sparkle.Core.Signal.«termHw_cond_|_=>_» : Lean.ParserDescr

Hardware switch: replaces deeply nested Signal.mux chains. Default value comes first, then condition/value pairs (first match wins):

hw_cond fsmReg
  | startAndIdle  => (1#4 : Signal dom _)
  | stemDone      => (2#4 : Signal dom _)

expands to Signal.mux startAndIdle (1#4) (Signal.mux stemDone (2#4) fsmReg)

Equations

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

def Sparkle.Core.Signal.ashr {n : Nat} (a b : BitVec n) : BitVec n

Arithmetic shift right with BitVec shift amount. Wraps BitVec.sshiftRight (which takes Nat) so it can be used in the applicative Signal DSL pattern: (ashr · ·) <$> a <*> b

Equations

• Sparkle.Core.Signal.ashr a b = a.sshiftRight b.toNat

@[implemented_by _private.Sparkle.Core.Signal.0.Sparkle.Core.Signal.bundle2Impl]

def Sparkle.Core.Signal.bundle2 {dom : Domain.DomainConfig} {α β : Type u} (a : Signal dom α) (b : Signal dom β) : Signal dom (α × β)

Equations

• Sparkle.Core.Signal.bundle2 a b = (fun (x1 : α) (x2 : β) => (x1, x2)) <$> a <*> b

@[implemented_by _private.Sparkle.Core.Signal.0.Sparkle.Core.Signal.bundle3Impl]

def Sparkle.Core.Signal.bundle3 {dom : Domain.DomainConfig} {α β γ : Type u} (a : Signal dom α) (b : Signal dom β) (c : Signal dom γ) : Signal dom (α × β × γ)

Equations

• Sparkle.Core.Signal.bundle3 a b c = (fun (x1 : α) (x2 : β) (x3 : γ) => (x1, x2, x3)) <$> a <*> b <*> c

@[deprecated "Use `Signal.fst` and `Signal.snd` directly. Pattern-matching on `unbundle2` breaks in synthesis." (since := "2026-04-08")]

def Sparkle.Core.Signal.unbundle2 {dom : Domain.DomainConfig} {α β : Type u} (s : Signal dom (α × β)) : Signal dom α × Signal dom β

Unbundle a signal of pairs.

⚠️ Returns a Lean-level tuple. Pattern-matching on the result (let (a, b) := unbundle2 signal) silently breaks in synthesis because the tuple is destructured at elaboration time. Use Signal.fst / Signal.snd directly instead. This binding is kept only so legacy test files still compile.

Equations

• Sparkle.Core.Signal.unbundle2 s = (Sparkle.Core.Signal.Signal.map Prod.fst s, Sparkle.Core.Signal.Signal.map Prod.snd s)

@[implemented_by _private.Sparkle.Core.Signal.0.Sparkle.Core.Signal.fstImpl]

def Sparkle.Core.Signal.Signal.fst {dom : Domain.DomainConfig} {α β : Type u} (s : Signal dom (α × β)) : Signal dom α

Equations

• s.fst = Sparkle.Core.Signal.Signal.map Prod.fst s

@[implemented_by _private.Sparkle.Core.Signal.0.Sparkle.Core.Signal.sndImpl]

def Sparkle.Core.Signal.Signal.snd {dom : Domain.DomainConfig} {α β : Type u} (s : Signal dom (α × β)) : Signal dom β

Equations

• s.snd = Sparkle.Core.Signal.Signal.map Prod.snd s

@[deprecated "Use `Signal.proj3_1`, `Signal.proj3_2`, `Signal.proj3_3` directly." (since := "2026-04-08")]

def Sparkle.Core.Signal.unbundle3 {dom : Domain.DomainConfig} {α β γ : Type u} (s : Signal dom (α × β × γ)) : Signal dom α × Signal dom β × Signal dom γ

Unbundle a 3-tuple signal.

⚠️ Same caveat as unbundle2: the returned Lean tuple cannot be pattern-matched in synthesis code. Use Signal.proj3_1 / proj3_2 / proj3_3 instead.

Equations

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

def Sparkle.Core.Signal.Signal.proj3_1 {dom : Domain.DomainConfig} {α β γ : Type u} (s : Signal dom (α × β × γ)) : Signal dom α

Project first element from a 3-tuple signal

Equations

• s.proj3_1 = Sparkle.Core.Signal.Signal.map (fun (x : α × β × γ) => x.fst) s

def Sparkle.Core.Signal.Signal.proj3_2 {dom : Domain.DomainConfig} {α β γ : Type u} (s : Signal dom (α × β × γ)) : Signal dom β

Project second element from a 3-tuple signal

Equations

• s.proj3_2 = Sparkle.Core.Signal.Signal.map (fun (x : α × β × γ) => x.snd.fst) s

def Sparkle.Core.Signal.Signal.proj3_3 {dom : Domain.DomainConfig} {α β γ : Type u} (s : Signal dom (α × β × γ)) : Signal dom γ

Project third element from a 3-tuple signal

Equations

• s.proj3_3 = Sparkle.Core.Signal.Signal.map (fun (x : α × β × γ) => x.snd.snd) s

@[deprecated "Use `Signal.proj4_1..proj4_4` directly." (since := "2026-04-08")]

def Sparkle.Core.Signal.unbundle4 {dom : Domain.DomainConfig} {α β γ δ : Type u} (s : Signal dom (α × β × γ × δ)) : Signal dom α × Signal dom β × Signal dom γ × Signal dom δ

Unbundle a 4-tuple signal.

⚠️ Same caveat as unbundle2. Use Signal.proj4_1..proj4_4 instead.

Equations

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

def Sparkle.Core.Signal.Signal.proj4_1 {dom : Domain.DomainConfig} {α β γ δ : Type u} (s : Signal dom (α × β × γ × δ)) : Signal dom α

Project first element from a 4-tuple signal

Equations

• s.proj4_1 = Sparkle.Core.Signal.Signal.map (fun (x : α × β × γ × δ) => x.fst) s

def Sparkle.Core.Signal.Signal.proj4_2 {dom : Domain.DomainConfig} {α β γ δ : Type u} (s : Signal dom (α × β × γ × δ)) : Signal dom β

Project second element from a 4-tuple signal

Equations

• s.proj4_2 = Sparkle.Core.Signal.Signal.map (fun (x : α × β × γ × δ) => x.snd.fst) s

def Sparkle.Core.Signal.Signal.proj4_3 {dom : Domain.DomainConfig} {α β γ δ : Type u} (s : Signal dom (α × β × γ × δ)) : Signal dom γ

Project third element from a 4-tuple signal

Equations

• s.proj4_3 = Sparkle.Core.Signal.Signal.map (fun (x : α × β × γ × δ) => x.snd.snd.fst) s

def Sparkle.Core.Signal.Signal.proj4_4 {dom : Domain.DomainConfig} {α β γ δ : Type u} (s : Signal dom (α × β × γ × δ)) : Signal dom δ

Project fourth element from a 4-tuple signal

Equations

• s.proj4_4 = Sparkle.Core.Signal.Signal.map (fun (x : α × β × γ × δ) => x.snd.snd.snd) s

def Sparkle.Core.Signal.unbundle5 {dom : Domain.DomainConfig} {α β γ δ ε : Type u} (s : Signal dom (α × β × γ × δ × ε)) : Signal dom α × Signal dom β × Signal dom γ × Signal dom δ × Signal dom ε

Unbundle a 5-tuple signal

Equations

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

def Sparkle.Core.Signal.unbundle6 {dom : Domain.DomainConfig} {α β γ δ ε ζ : Type u} (s : Signal dom (α × β × γ × δ × ε × ζ)) : Signal dom α × Signal dom β × Signal dom γ × Signal dom δ × Signal dom ε × Signal dom ζ

Unbundle a 6-tuple signal

Equations

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

def Sparkle.Core.Signal.unbundle7 {dom : Domain.DomainConfig} {α β γ δ ε ζ η : Type u} (s : Signal dom (α × β × γ × δ × ε × ζ × η)) : Signal dom α × Signal dom β × Signal dom γ × Signal dom δ × Signal dom ε × Signal dom ζ × Signal dom η

Unbundle a 7-tuple signal

Equations

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

def Sparkle.Core.Signal.unbundle8 {dom : Domain.DomainConfig} {α β γ δ ε ζ η θ : Type u} (s : Signal dom (α × β × γ × δ × ε × ζ × η × θ)) : Signal dom α × Signal dom β × Signal dom γ × Signal dom δ × Signal dom ε × Signal dom ζ × Signal dom η × Signal dom θ

Unbundle an 8-tuple signal

Equations

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

def Sparkle.Core.Signal.termProjN!___ : Lean.ParserDescr

Project the i-th element (0-indexed) from a right-nested pair signal. projN! state n i extracts element i from n-element nested pair.

Example (4-element tuple (A × (B × (C × D)))): projN! s 4 0 → Signal.fst s -- A projN! s 4 1 → Signal.fst (Signal.snd s) -- B projN! s 4 2 → Signal.fst (Signal.snd (Signal.snd s)) -- C projN! s 4 3 → Signal.snd (Signal.snd (Signal.snd s)) -- D (last uses snd)

Equations

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

def Sparkle.Core.Signal.«termBundleAll![_]» : Lean.ParserDescr

Bundle a list of signals into a right-nested pair using bundle2. bundleAll! [a, b, c, d] → bundle2 a (bundle2 b (bundle2 c d))

For a single element, returns that element directly.

Equations

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

def Sparkle.Core.Signal.«termHw_let(_,_):=_;_» : Lean.ParserDescr

Destructure a 2-element right-nested pair signal into named bindings. hw_let (a, b) := sig; body expands to: let a := Signal.fst sig; let b := Signal.snd sig; body

Equations

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

def Sparkle.Core.Signal.«termHw_let(_,_,_):=_;_» : Lean.ParserDescr

Destructure a 3-element right-nested pair signal (A × (B × C)).

Equations

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

def Sparkle.Core.Signal.«termHw_let(_,_,_,_):=_;_» : Lean.ParserDescr

Destructure a 4-element right-nested pair signal (A × (B × (C × D))).

Equations

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

@[inline]

def Sparkle.Core.Signal.bitsHL {w : Nat} (x : BitVec w) (hi lo : Nat) : BitVec (hi - lo + 1)

Verilog-style slice: bitsHL inst hi lo ≡ inst[hi,lo].

Equations

• Sparkle.Core.Signal.bitsHL x hi lo = BitVec.extractLsb' lo (hi - lo + 1) x

def Sparkle.Core.Signal.«term__[_,_]» : Lean.TrailingParserDescr

Equations

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

class Sparkle.Core.Signal.HasBitSlice (α : Type) (β : outParam (Nat → Type)) : Type

• slice : α → (hi lo : Nat) → β (hi - lo + 1)

instance Sparkle.Core.Signal.instHasBitSliceBitVec {w : Nat} : HasBitSlice (BitVec w) BitVec

Equations

• Sparkle.Core.Signal.instHasBitSliceBitVec = { slice := fun (x : BitVec w) (hi lo : Nat) => BitVec.extractLsb' lo (hi - lo + 1) x }

instance Sparkle.Core.Signal.instHasBitSliceSignalBitVec {dom : Domain.DomainConfig} {w : Nat} : HasBitSlice (Signal dom (BitVec w)) fun (n : Nat) => Signal dom (BitVec n)

Equations

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