inductive Sparkle.IR.Type.HWType : Type

Hardware Type: The subset of types that can be synthesized to hardware.

• Bit: Single bit (wire)
• BitVector: n-bit vector
• Array: Fixed-size array (for memories/ROMs)

• bit : HWType
• bitVector (width : Nat) : HWType
• array (size : Nat) (elemType : HWType) : HWType

def Sparkle.IR.Type.instReprHWType.repr : HWType → Nat → Std.Format

Equations

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

instance Sparkle.IR.Type.instReprHWType : Repr HWType

Equations

• Sparkle.IR.Type.instReprHWType = { reprPrec := Sparkle.IR.Type.instReprHWType.repr }

instance Sparkle.IR.Type.instBEqHWType : BEq HWType

Equations

• Sparkle.IR.Type.instBEqHWType = { beq := Sparkle.IR.Type.instBEqHWType.beq }

def Sparkle.IR.Type.instBEqHWType.beq : HWType → HWType → Bool

Equations

• Sparkle.IR.Type.instBEqHWType.beq Sparkle.IR.Type.HWType.bit Sparkle.IR.Type.HWType.bit = true
• Sparkle.IR.Type.instBEqHWType.beq (Sparkle.IR.Type.HWType.bitVector a) (Sparkle.IR.Type.HWType.bitVector b) = (a == b)
• Sparkle.IR.Type.instBEqHWType.beq (Sparkle.IR.Type.HWType.array a a_1) (Sparkle.IR.Type.HWType.array b b_1) = (a == b && Sparkle.IR.Type.instBEqHWType.beq a_1 b_1)
• Sparkle.IR.Type.instBEqHWType.beq x✝¹ x✝ = false

def Sparkle.IR.Type.instDecidableEqHWType.decEq (x✝ x✝¹ : HWType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.IR.Type.instDecidableEqHWType.decEq Sparkle.IR.Type.HWType.bit Sparkle.IR.Type.HWType.bit = isTrue ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq Sparkle.IR.Type.HWType.bit (Sparkle.IR.Type.HWType.bitVector width) = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq Sparkle.IR.Type.HWType.bit (Sparkle.IR.Type.HWType.array size elemType) = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.bitVector width) Sparkle.IR.Type.HWType.bit = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.bitVector a) (Sparkle.IR.Type.HWType.bitVector b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.bitVector width) (Sparkle.IR.Type.HWType.array size elemType) = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.array size elemType) Sparkle.IR.Type.HWType.bit = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.array size elemType) (Sparkle.IR.Type.HWType.bitVector width) = isFalse ⋯

instance Sparkle.IR.Type.instDecidableEqHWType : DecidableEq HWType

Equations

• Sparkle.IR.Type.instDecidableEqHWType = Sparkle.IR.Type.instDecidableEqHWType.decEq

instance Sparkle.IR.Type.instInhabitedHWType : Inhabited HWType

Equations

• Sparkle.IR.Type.instInhabitedHWType = { default := Sparkle.IR.Type.instInhabitedHWType.default }

def Sparkle.IR.Type.instInhabitedHWType.default : HWType

Equations

• Sparkle.IR.Type.instInhabitedHWType.default = Sparkle.IR.Type.HWType.bit

def Sparkle.IR.Type.HWType.bitWidth : HWType → Nat

Get the bit width of a hardware type

Equations

• Sparkle.IR.Type.HWType.bit.bitWidth = 1
• (Sparkle.IR.Type.HWType.bitVector a).bitWidth = a
• (Sparkle.IR.Type.HWType.array a a_1).bitWidth = a * a_1.bitWidth

def Sparkle.IR.Type.HWType.isBit : HWType → Bool

Check if a hardware type is a single bit

Equations

• Sparkle.IR.Type.HWType.bit.isBit = true
• x✝.isBit = false

def Sparkle.IR.Type.HWType.isBitVector : HWType → Bool

Check if a hardware type is a bit vector

Equations

• (Sparkle.IR.Type.HWType.bitVector width).isBitVector = true
• x✝.isBitVector = false

def Sparkle.IR.Type.HWType.isArray : HWType → Bool

Check if a hardware type is an array

Equations

• (Sparkle.IR.Type.HWType.array size elemType).isArray = true
• x✝.isArray = false

def Sparkle.IR.Type.HWType.toString : HWType → String

Convert hardware type to a human-readable string

Equations

• Sparkle.IR.Type.HWType.bit.toString = "Bit"
• (Sparkle.IR.Type.HWType.bitVector 1).toString = "Bit"
• (Sparkle.IR.Type.HWType.bitVector w).toString = toString "BitVec" ++ toString w
• (Sparkle.IR.Type.HWType.array size elemType).toString = toString "Array[" ++ toString size ++ toString "](" ++ toString elemType.toString ++ toString ")"

instance Sparkle.IR.Type.HWType.instToString : ToString HWType

Equations

• Sparkle.IR.Type.HWType.instToString = { toString := Sparkle.IR.Type.HWType.toString }

def Sparkle.IR.Type.toHWType (α : Type u) (n : Nat) [Data.BitPack.BitPack α n] : HWType

Convert a Lean type with BitPack instance to HWType

Equations

• Sparkle.IR.Type.toHWType α n = if (n == 1) = true then Sparkle.IR.Type.HWType.bit else Sparkle.IR.Type.HWType.bitVector n

def Sparkle.IR.Type.hwTypeFromWidth (w : Nat) : HWType

Helper to infer HWType from a Nat width

Equations

• Sparkle.IR.Type.hwTypeFromWidth w = if (w == 1) = true then Sparkle.IR.Type.HWType.bit else Sparkle.IR.Type.HWType.bitVector w

def Sparkle.IR.Type.byte : HWType

8-bit hardware type

Equations

• Sparkle.IR.Type.byte = Sparkle.IR.Type.HWType.bitVector 8

def Sparkle.IR.Type.word16 : HWType

16-bit hardware type

Equations

• Sparkle.IR.Type.word16 = Sparkle.IR.Type.HWType.bitVector 16

def Sparkle.IR.Type.word32 : HWType

32-bit hardware type

Equations

• Sparkle.IR.Type.word32 = Sparkle.IR.Type.HWType.bitVector 32

def Sparkle.IR.Type.word64 : HWType

64-bit hardware type

Equations

• Sparkle.IR.Type.word64 = Sparkle.IR.Type.HWType.bitVector 64

def Sparkle.IR.Type.hwBool : HWType

Boolean hardware type

Equations

• Sparkle.IR.Type.hwBool = Sparkle.IR.Type.HWType.bit

inductive Sparkle.IR.Type.ResetKind : Type

Reset kind: synchronous or asynchronous.

Lives here (not in Sparkle.Core.Domain) so the IR layer can reference it without importing Core/Domain.lean (which would create a layering inversion). Sparkle.Core.Domain re-exports this so user code keeps seeing Sparkle.Core.Domain.ResetKind.

• synchronous : ResetKind
• asynchronous : ResetKind

instance Sparkle.IR.Type.instReprResetKind : Repr ResetKind

Equations

• Sparkle.IR.Type.instReprResetKind = { reprPrec := Sparkle.IR.Type.instReprResetKind.repr }

def Sparkle.IR.Type.instReprResetKind.repr : ResetKind → Nat → Std.Format

Equations

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

def Sparkle.IR.Type.instBEqResetKind.beq : ResetKind → ResetKind → Bool

Equations

• Sparkle.IR.Type.instBEqResetKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Sparkle.IR.Type.instBEqResetKind : BEq ResetKind

Equations

• Sparkle.IR.Type.instBEqResetKind = { beq := Sparkle.IR.Type.instBEqResetKind.beq }

instance Sparkle.IR.Type.instDecidableEqResetKind : DecidableEq ResetKind

Equations

• Sparkle.IR.Type.instDecidableEqResetKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Sparkle.IR.Type.instInhabitedResetKind : Inhabited ResetKind

Equations

• Sparkle.IR.Type.instInhabitedResetKind = { default := Sparkle.IR.Type.instInhabitedResetKind.default }

def Sparkle.IR.Type.instInhabitedResetKind.default : ResetKind

Equations

• Sparkle.IR.Type.instInhabitedResetKind.default = Sparkle.IR.Type.ResetKind.synchronous