Domain Module

Clock domain configuration for Sparkle HDL.

Purpose

This module defines clock domains, which specify timing and reset behavior for hardware signals. Each domain has:

• A clock period (in picoseconds)
• An active edge (rising or falling)
• A reset type (synchronous or asynchronous)

Type Safety

Signals are tagged with their domain at the type level (Signal d α), preventing accidental mixing of signals from different clock domains.

Usage

Define a custom clock domain:

def FastClock : DomainConfig where
  period := 5000        -- 5ns period (200MHz)
  activeEdge := .rising
  resetKind := .synchronous

Most designs use the default Domain:

def myCircuit : Signal Domain (BitVec 16) := do
  -- Your circuit here
  ...

Multi-Clock Designs

For designs with multiple clock domains, create separate domain configurations and use type-level tracking to ensure safety:

def Domain100MHz : DomainConfig where
  period := 10000       -- 10ns (100MHz)
  activeEdge := .rising
  resetKind := .synchronous

def Domain50MHz : DomainConfig where
  period := 20000       -- 20ns (50MHz)
  activeEdge := .rising
  resetKind := .synchronous

-- These cannot be mixed due to type safety!
def fast : Signal Domain100MHz (BitVec 8) := ...
def slow : Signal Domain50MHz (BitVec 8) := ...

See also: Sparkle.Core.Signal for signal operations.

@[reducible, inline]

abbrev Sparkle.Core.Domain.ResetKind : Type

ResetKind is defined in Sparkle.IR.Type so the IR layer can reference it without importing Core/Domain.lean. We alias it as Sparkle.Core.Domain.ResetKind for back-compat with user code that already qualifies it that way.

Equations

• Sparkle.Core.Domain.ResetKind = Sparkle.IR.Type.ResetKind

@[reducible, inline]

abbrev Sparkle.Core.Domain.ResetKind.synchronous : ResetKind

Equations

• Sparkle.Core.Domain.ResetKind.synchronous = Sparkle.IR.Type.ResetKind.synchronous

@[reducible, inline]

abbrev Sparkle.Core.Domain.ResetKind.asynchronous : ResetKind

Equations

• Sparkle.Core.Domain.ResetKind.asynchronous = Sparkle.IR.Type.ResetKind.asynchronous

inductive Sparkle.Core.Domain.ActiveEdge : Type

Active edge of a clock signal

• rising : ActiveEdge
• falling : ActiveEdge

instance Sparkle.Core.Domain.instReprActiveEdge : Repr ActiveEdge

Equations

• Sparkle.Core.Domain.instReprActiveEdge = { reprPrec := Sparkle.Core.Domain.instReprActiveEdge.repr }

def Sparkle.Core.Domain.instReprActiveEdge.repr : ActiveEdge → Nat → Std.Format

Equations

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

instance Sparkle.Core.Domain.instBEqActiveEdge : BEq ActiveEdge

Equations

• Sparkle.Core.Domain.instBEqActiveEdge = { beq := Sparkle.Core.Domain.instBEqActiveEdge.beq }

def Sparkle.Core.Domain.instBEqActiveEdge.beq : ActiveEdge → ActiveEdge → Bool

Equations

• Sparkle.Core.Domain.instBEqActiveEdge.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Sparkle.Core.Domain.instDecidableEqActiveEdge : DecidableEq ActiveEdge

Equations

• Sparkle.Core.Domain.instDecidableEqActiveEdge x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Sparkle.Core.Domain.DomainConfig : Type

Domain configuration specifying timing and reset behavior.

• period: Clock period in picoseconds (e.g., 10000 for 100MHz)
• activeEdge: Whether to trigger on rising or falling edge
• resetKind: Synchronous or asynchronous reset

• period : Nat
• activeEdge : ActiveEdge
• resetKind : ResetKind

instance Sparkle.Core.Domain.instReprDomainConfig : Repr DomainConfig

Equations

• Sparkle.Core.Domain.instReprDomainConfig = { reprPrec := Sparkle.Core.Domain.instReprDomainConfig.repr }

def Sparkle.Core.Domain.instReprDomainConfig.repr : DomainConfig → Nat → Std.Format

Equations

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

def Sparkle.Core.Domain.instBEqDomainConfig.beq : DomainConfig → DomainConfig → Bool

Equations

• Sparkle.Core.Domain.instBEqDomainConfig.beq { period := a, activeEdge := a_1, resetKind := a_2 } { period := b, activeEdge := b_1, resetKind := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Sparkle.Core.Domain.instBEqDomainConfig.beq x✝¹ x✝ = false

instance Sparkle.Core.Domain.instBEqDomainConfig : BEq DomainConfig

Equations

• Sparkle.Core.Domain.instBEqDomainConfig = { beq := Sparkle.Core.Domain.instBEqDomainConfig.beq }

instance Sparkle.Core.Domain.instDecidableEqDomainConfig : DecidableEq DomainConfig

Equations

• Sparkle.Core.Domain.instDecidableEqDomainConfig = Sparkle.Core.Domain.instDecidableEqDomainConfig.decEq

def Sparkle.Core.Domain.instDecidableEqDomainConfig.decEq (x✝ x✝¹ : DomainConfig) : Decidable (x✝ = x✝¹)

Equations

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

structure Sparkle.Core.Domain.Clock (dom : DomainConfig) : Type

Clock signal wrapper carrying domain information. The domain parameter ensures type-safe separation of different clock domains.

structure Sparkle.Core.Domain.Reset (dom : DomainConfig) : Type

Reset signal wrapper carrying domain information. Reset must belong to the same domain as the clock it synchronizes with.

structure Sparkle.Core.Domain.Enable (dom : DomainConfig) : Type

Enable signal wrapper carrying domain information. Enable controls whether registers in a domain are active.

def Sparkle.Core.Domain.defaultDomain : DomainConfig

Default domain configuration: 100MHz, rising edge, synchronous reset

Equations

• Sparkle.Core.Domain.defaultDomain = { period := 10000, activeEdge := Sparkle.Core.Domain.ActiveEdge.rising, resetKind := Sparkle.Core.Domain.ResetKind.synchronous }

def Sparkle.Core.Domain.domain50MHz : DomainConfig

Common 50MHz domain

Equations

• Sparkle.Core.Domain.domain50MHz = { period := 20000, activeEdge := Sparkle.Core.Domain.ActiveEdge.rising, resetKind := Sparkle.Core.Domain.ResetKind.synchronous }

def Sparkle.Core.Domain.domain200MHz : DomainConfig

Common 200MHz domain

Equations

• Sparkle.Core.Domain.domain200MHz = { period := 5000, activeEdge := Sparkle.Core.Domain.ActiveEdge.rising, resetKind := Sparkle.Core.Domain.ResetKind.synchronous }