Sparkle HDL

A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.

Documentation

• Tutorial — chapter-by-chapter walk-through of the Signal DSL, register patterns, Verilog synthesis, formal proofs, and FPGA bring-up.
• JupyterLite — run the tutorial chapters in your browser (xlean WASM kernel, no install required).
• API reference — generated from source by doc-gen4. Covers Sparkle.Core, every IP.* library, the SVParser toolchain, and the Display helpers.

Benchmarks

• RV32 SoC — Verilator vs JIT
• LiteX + PicoRV32 — Verilator vs JIT
• Multi-core (8-core LiteX PicoRV32)

Source

github.com/Verilean/sparkle