VCD File Format

VCD files contain:

1. Header (date, version, timescale)
2. Scope and variable declarations
3. Initial values
4. Timestamped value changes

Example:

$date Thu Jan 30 2026 $end
$version Sparkle HDL $end
$timescale 1ns $end
$scope module top $end
$var wire 16 ! signal_name $end
$upscope $end
$enddefinitions $end
$dumpvars
b0000000000000000 !
$end
#0
#1
b0000000000001010 !

def Sparkle.Backend.VCD.makeIdentifier (idx : Nat) : String

Signal identifier in VCD (!, ", #, $, etc.)

Equations

• Sparkle.Backend.VCD.makeIdentifier idx = String.singleton (Char.ofNat (33 + idx))

def Sparkle.Backend.VCD.bitVecToBinary {n : Nat} (bv : BitVec n) : String

Convert BitVec to binary string for VCD

Equations

• Sparkle.Backend.VCD.bitVecToBinary bv = String.ofList (List.map (fun (i : Nat) => if (bv.toNat >>> i &&& 1 == 1) = true then '1' else '0') (List.range n)).reverse

def Sparkle.Backend.VCD.boolToVCD (b : Bool) : String

Convert Bool to VCD bit

Equations

• Sparkle.Backend.VCD.boolToVCD b = if b = true then "1" else "0"

structure Sparkle.Backend.VCD.VCDVar : Type

VCD variable declaration

• name : String
• identifier : String
• width : Nat

def Sparkle.Backend.VCD.instReprVCDVar.repr : VCDVar → Nat → Std.Format

Equations

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

instance Sparkle.Backend.VCD.instReprVCDVar : Repr VCDVar

Equations

• Sparkle.Backend.VCD.instReprVCDVar = { reprPrec := Sparkle.Backend.VCD.instReprVCDVar.repr }

def Sparkle.Backend.VCD.instInhabitedVCDVar.default : VCDVar

Equations

• Sparkle.Backend.VCD.instInhabitedVCDVar.default = { name := default, identifier := default, width := default }

instance Sparkle.Backend.VCD.instInhabitedVCDVar : Inhabited VCDVar

Equations

• Sparkle.Backend.VCD.instInhabitedVCDVar = { default := Sparkle.Backend.VCD.instInhabitedVCDVar.default }

inductive Sparkle.Backend.VCD.VCDValue : Type

VCD value at a specific time

• bit : Bool → VCDValue
• vector {n : Nat} : BitVec n → VCDValue

def Sparkle.Backend.VCD.instReprVCDValue.repr : VCDValue → Nat → Std.Format

Equations

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

instance Sparkle.Backend.VCD.instReprVCDValue : Repr VCDValue

Equations

• Sparkle.Backend.VCD.instReprVCDValue = { reprPrec := Sparkle.Backend.VCD.instReprVCDValue.repr }

def Sparkle.Backend.VCD.formatVCDValue (val : VCDValue) (id : String) : String

Format VCD value for output

Equations

• Sparkle.Backend.VCD.formatVCDValue (Sparkle.Backend.VCD.VCDValue.bit a) id = toString (Sparkle.Backend.VCD.boolToVCD a) ++ toString id
• Sparkle.Backend.VCD.formatVCDValue (Sparkle.Backend.VCD.VCDValue.vector a_1) id = toString "b" ++ toString (Sparkle.Backend.VCD.bitVecToBinary a_1) ++ toString " " ++ toString id

VCD Writer State

Tracks variables and their values over time for VCD generation.

structure Sparkle.Backend.VCD.VCDWriter : Type

• moduleName : String
• variables : List VCDVar
• timescale : String

instance Sparkle.Backend.VCD.instReprVCDWriter : Repr VCDWriter

Equations

• Sparkle.Backend.VCD.instReprVCDWriter = { reprPrec := Sparkle.Backend.VCD.instReprVCDWriter.repr }

def Sparkle.Backend.VCD.instReprVCDWriter.repr : VCDWriter → Nat → Std.Format

Equations

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

def Sparkle.Backend.VCD.VCDWriter.new (moduleName : String) : VCDWriter

Create a new VCD writer

Equations

• Sparkle.Backend.VCD.VCDWriter.new moduleName = { moduleName := moduleName, variables := [] }

def Sparkle.Backend.VCD.VCDWriter.addVar (writer : VCDWriter) (name : String) (width : Nat) : VCDWriter

Add a variable to the VCD writer

Equations

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

VCD Header Generation

def Sparkle.Backend.VCD.generateHeader (writer : VCDWriter) : String

Generate VCD header

Equations

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

def Sparkle.Backend.VCD.generateVarDecls (writer : VCDWriter) : String

Generate variable declarations

Equations

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

VCD Trace Generation

Generate timestamped value changes from Signal simulations.

structure Sparkle.Backend.VCD.TraceEntry : Type

Record of a signal value at a specific time

• time : Nat
• varId : String
• value : VCDValue

def Sparkle.Backend.VCD.instReprTraceEntry.repr : TraceEntry → Nat → Std.Format

Equations

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

instance Sparkle.Backend.VCD.instReprTraceEntry : Repr TraceEntry

Equations

• Sparkle.Backend.VCD.instReprTraceEntry = { reprPrec := Sparkle.Backend.VCD.instReprTraceEntry.repr }

def Sparkle.Backend.VCD.sampleBitVecSignal {dom : Core.Domain.DomainConfig} {n : Nat} (sig : Core.Signal.Signal dom (BitVec n)) (varId : String) (cycles : Nat) : List TraceEntry

Sample a BitVec signal over time

Equations

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

def Sparkle.Backend.VCD.sampleBoolSignal {dom : Core.Domain.DomainConfig} (sig : Core.Signal.Signal dom Bool) (varId : String) (cycles : Nat) : List TraceEntry

Sample a Bool signal over time

Equations

• Sparkle.Backend.VCD.sampleBoolSignal sig varId cycles = List.map (fun (t : Nat) => { time := t, varId := varId, value := Sparkle.Backend.VCD.VCDValue.bit (sig.atTime t) }) (List.range cycles)

def Sparkle.Backend.VCD.generateDumpVars (entries : List TraceEntry) : String

Generate initial value dump

Equations

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

def Sparkle.Backend.VCD.groupByTime (entries : List TraceEntry) : List (Nat × List TraceEntry)

Group trace entries by time

Equations

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

def Sparkle.Backend.VCD.generateTimeSteps (entries : List TraceEntry) : String

Generate timestamped value changes

Equations

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

High-Level VCD Generation API

def Sparkle.Backend.VCD.generateVCD (writer : VCDWriter) (entries : List TraceEntry) : String

Generate complete VCD file from trace entries

Equations

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

def Sparkle.Backend.VCD.writeVCDFile (filename content : String) : IO Unit

Write VCD file to disk

Equations

• Sparkle.Backend.VCD.writeVCDFile filename content = do IO.FS.writeFile { toString := filename } content IO.println (toString "VCD file written to: " ++ toString filename)