def Sparkle.Utils.HexLoader.hexToNat (s : String) : Nat

Parse a single hex string into a Nat. Returns 0 on invalid input.

Equations

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

def Sparkle.Utils.HexLoader.loadHex (path : System.FilePath) : IO (Array (BitVec 32))

Parse a $readmemh-format hex file into an array of 32-bit words.

Equations

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

def Sparkle.Utils.HexLoader.arrayToInitFn (arr : Array (BitVec 32)) : BitVec 12 → BitVec 32

Convert an array into a lookup function for memoryWithInit. Out-of-bounds addresses return 0.

Equations

• Sparkle.Utils.HexLoader.arrayToInitFn arr addr = if h : addr.toNat < arr.size then arr[addr.toNat] else 0#32

def Sparkle.Utils.HexLoader.arrayToInitFn' {n : Nat} (arr : Array (BitVec 32)) : BitVec n → BitVec 32

Convert an array into a lookup function with configurable address width.

Equations

• Sparkle.Utils.HexLoader.arrayToInitFn' arr addr = if h : addr.toNat < arr.size then arr[addr.toNat] else 0#32

def Sparkle.Utils.HexLoader.loadBinary (path : System.FilePath) : IO (Array UInt32)

Load a raw binary file as an array of 32-bit words (little-endian). Pads the last word with zeros if the file size is not a multiple of 4.

Equations

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

def Sparkle.Utils.HexLoader.loadBinaryToDRAM (handle : Core.JIT.JITHandle) (path : System.FilePath) (baseWordAddr : UInt32) (dramWords : UInt32 := 8388608) : IO Nat

Load a raw binary file into JIT DRAM byte-lane memories. The SoC has 8 DRAM byte-lane memories (4 data + 4 ifetch) that must all be loaded with the same data for coherent access.

Parameters:

• handle: JIT simulation handle
• path: Path to the binary file
• baseWordAddr: Starting word address in DRAM (e.g., 0x000000 for 0x80000000)

Returns: number of 32-bit words loaded

Equations

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