Write hardware in Lean 4. Prove it correct. Generate Verilog.

A type-safe hardware description language that brings dependent types and theorem proving to hardware design.

Live docs & benchmarks: the project publishes three hosted pages at verilean.github.io/sparkle:

• 📘 Tutorial (JupyterLite) — the multi-chapter beginner course, runnable in-browser via xeus-lean. (Known issue: some environments fail to boot the Lean kernel or load Sparkle; when that happens, read the rendered notebooks under docs/tutorial/Notebooks/ or use the Docker path in Quick Start below.)
• 🔎 API reference (doc-gen4) — fully cross-linked documentation for every public definition, generated from the source with lake build Sparkle:docs.
• 📈 Benchmarks — CI-driven history of the RV32 JIT vs Verilator numbers: RV32 SoC · LiteX PicoRV32 · Multi-core (8-thread)

Quick Start: the multi-chapter tutorial walks from "hello counter" through Verilog generation, proofs, and FPGA bring-up. Run it in Docker, in your browser via xeus-lean's JupyterLite, or read the rendered notebooks directly on GitHub. For the full Signal DSL syntax, see docs/reference/SignalDSL_Syntax.md.

Try it in the browser: Sparkle plugs into xeus-lean's WASM kernel via the EXTRA_WASM_DIRS extension point. See tools/wasm/ for the staging-builder script. #synthesizeVerilog, #showVerilog, and pure Signal.atTime simulation all work under WASM; the native JIT path (Sparkle.Core.JIT.compileAndLoad) is stubbed and only available from a native lake exe build.

1. Write a pure Lean spec — define behaviour as pure functions.
2. Prove properties — safety, liveness, fairness via Lean's theorem prover.
3. Implement via Signal DSL — express the same logic using Signal combinators.
4. Generate Verilog — #synthesizeVerilog / #writeVerilogDesign emit SystemVerilog.

See docs/reference/Verification_Framework.md for patterns and a worked Round-Robin Arbiter example (10 formal proofs).

Sparkle ships with production-grade IP cores — each with pure Lean specs, formal proofs, and synthesizable Signal DSL implementations.

Full UART → SLIP → IPv4 → TCP → HTTP round-trip, live on Tang Nano 50K. lake exe usb-webserver-jit-test runs a GET request end-to-end in seconds. See docs/ip-catalog/Networking.md for the full layer-stack breakdown, bring-up notes, and sim entry points.

-- Write this in Lean...
def counter {dom : DomainConfig} : Signal dom (BitVec 8) :=
  Signal.circuit do
    let count ← Signal.reg 0#8
    count <~ count + 1#8
    return count

#synthesizeVerilog counter

// ...and get this Verilog
module counter (
    input  logic clk,
    input  logic rst,
    output logic [7:0] out
);
    logic [7:0] count;

    always_ff @(posedge clk) begin
        if (rst)
            count <= 8'h00;
        else
            count <= count + 8'h01;
    end

    assign out = count;
endmodule

Three powerful ideas in one language:

1. Simulate — cycle-accurate functional simulation with pure Lean functions.
2. Synthesize — automatic compilation to clean, synthesizable SystemVerilog.
3. Verify — formal correctness proofs using Lean's theorem prover.

Chisel + FIRRTL solve many logical hardware bugs (latches, comb loops) but leave you fighting timing-closure with external linters. Sparkle gives you both out of the box:

• Logical Safety — Signal enforces a strict DAG for combinational logic; feedback is only possible through explicit Signal.register / Signal.loop. Pattern-match exhaustiveness catches unhandled cases at compile time. Unintended latches are impossible by construction.
• Physical / Timing Safety — a built-in DRC pass (inspired by the STARC guidelines) enforces registered outputs so Static Timing Analysis is predictable and critical paths don't cross module boundaries.
• Readable Verilog — Sparkle's IR keeps a 1:1 structural correspondence with your Lean code. When the DRC flags a timing issue you can actually read the generated SV to fix it.

Prerequisites: a glibc ≥ 2.34 Linux (Ubuntu 22.04+, Debian 12+, Fedora 35+), macOS, or WSL2. Older systems (e.g. Ubuntu 20.04, glibc 2.31) fail during lake build with

.../bin/cadical: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.34' not found

— cadical is the SAT solver bundled with the Lean 4.28 toolchain (used by bv_decide / omega), and it is linked against glibc 2.34. This is a Lean-toolchain requirement, not a Sparkle one; upgrade the OS (or use the Docker path in the tutorial) if you hit it.

git clone https://github.com/Verilean/sparkle.git
cd sparkle
lake build                                # ~5 min first time
lake env lean --run Examples/Counter.lean # smoke-test

A minimal register chain:

import Sparkle
open Sparkle.Core.Domain
open Sparkle.Core.Signal

-- Three-cycle delay line, polymorphic over clock domains.
def registerChain {dom : DomainConfig}
    (input : Signal dom (BitVec 8)) : Signal dom (BitVec 8) :=
  let d1 := Signal.register 0#8 input
  let d2 := Signal.register 0#8 d1
  Signal.register 0#8 d2

#synthesizeVerilog registerChain

For the full tour — VCD waveforms, JIT simulation, formal equivalence commands, clock-domain crossings, and the synthesizable subset of Lean — work through docs/tutorial/.

• Cycle-accurate simulation — the same semantics as the emitted Verilog, runnable from Lean with #eval and sample.
• Automatic Verilog generation — #synthesizeVerilog handles clocks, resets, register inference, bit-width checking, and feedback-loop resolution.
• Formal verification ready — bv_decide + simp + Temporal.lean (LTL) for safety/liveness/fairness proofs directly against Signal code.
• One-line equivalence checks — #verify_eq, #verify_eq_at, #verify_eq_git auto-generate theorems and discharge them with bv_decide. See docs/tutorial/notebooks/ch07-equivalence.ipynb.
• Signal DSL with imperative feel — Signal.circuit macro gives you <~ register assignment without losing the functional semantics.
• Vector / array types — HWVector α n with compile-time-checked indexing for register files.
• Memory primitives — Signal.memory generates synchronous-write / registered-read BRAM-style RAMs.
• Technology library support — primitiveModule wraps vendor cells (SRAMs, PLLs, transceivers) into the type system.
• JIT simulation — sim! / #sim compile to native C++ via dlopen for 10–100× faster simulation than the Lean interpreter.
• CDC-aware multi-domain simulation — runSim auto-selects the fastest backend (single-domain or lock-free SPSC queue between threads).
• Temporal logic — LTL operators (always, eventually, next, Until) with induction principles, enabling cycle-skipping optimisation.

Each feature is exercised in the tutorial or one of the IPs; see the links in the IP Catalog above.

# Core simulation + Verilog generation
lake env lean --run Examples/Counter.lean
lake env lean --run Examples/LoopSynthesis.lean
lake env lean --run Examples/SimpleMemory.lean

# The 16-bit Sparkle-16 CPU (ALU / RegisterFile / Core / ISA proofs)
lake env lean --run Examples/Sparkle16/Core.lean
lake env lean --run Examples/Sparkle16/ISAProofTests.lean

# Clock-domain crossing demo
lake env lean --run Examples/CDC/MultiClockSim.lean

# RV32IMA SoC, BitNet, YOLOv8, H.264 — run via the test suite
lake test

# Verilator: build the SoC and boot firmware
cd verilator && make build && ./obj_dir/Vrv32i_soc ../firmware/firmware.hex 500000

Each IP has a dedicated getting-started recipe in its own doc (BitNet, RV32, H264, YOLOv8, CDC).

• Hosted (built by CI, always up-to-date with main):
  • 📘 Tutorial (JupyterLite) — in-browser, xeus-lean kernel. (Boot issues on some machines — see "Live docs & benchmarks" at the top of this README for the fallback.)
  • 🔎 API reference — doc-gen4 site covering every public definition.
  • 📈 Benchmarks — RV32 SoC, LiteX PicoRV32, Multi-core 8-thread.
• Generate the API reference locally with doc-gen4:

lake -R -Kenv=dev build Sparkle:docs
open .lake/build/doc/index.html

Pointers to the hand-written docs:

• Getting started / writing synthesizable code
  • docs/tutorial/ — multi-chapter beginner course
  • docs/reference/SignalDSL_Syntax.md — full DSL reference
  • docs/reference/Troubleshooting_Synthesis.md
• Verification
  • docs/reference/Verification_Framework.md — VDD patterns
  • Examples/TemporalLogicExample.md — LTL usage
• IP-specific docs
  • docs/ip-catalog/BitNet.md · docs/ip-catalog/YOLOv8.md
  • docs/ip-catalog/RV32.md · docs/ip-catalog/H264.md
  • docs/architecture/CDC.md
• Project meta
  • docs/CHANGELOG.md — release history
  • docs/architecture/STATUS.md — current capability matrix
  • docs/known-issues/KnownIssues.md
  • docs/known-issues/BENCHMARK.md

┌──────────────────┐
│  Lean Signal DSL │   ===, &&&, |||, hw_cond, Coe
└──────┬───────────┘
       │
       ├──────────────┬──────────────────┬───────────────────┐
       ▼              ▼                  ▼                   ▼
┌─────────────┐ ┌────────────┐  ┌──────────────┐ ┌──────────────────┐
│ Simulation  │ │ JIT (FFI)  │  │  Verilator   │ │#synthesizeVerilog│
│  .atTime t  │ │ C++ dlopen │  │ .sv → C++    │ │  Lean → IR → DRC │
│  ~5K cyc/s  │ │ ~13.0M c/s │  │ ~11.1M c/s   │ │  → SystemVerilog │
│             │ │+oracle:1B+ │  │              │ │                  │
└─────────────┘ └────────────┘  └──────────────┘ └──────────────────┘

Core abstractions:

1. Domain — clock domain configuration (period, edge, reset).
2. Signal — stream-based hardware values, Signal d α ≈ Nat → α.
3. BitPack — type class for hardware serialisation.
4. Module / Circuit — IR for netlists.
5. Compiler — automatic Lean → IR translation via metaprogramming.

Type-safety example:

-- This won't compile — bit-width mismatch is a compile-time error.
def broken {dom : DomainConfig} : Signal dom (BitVec 8) :=
  Signal.register (0#16) (Signal.pure 0#16)  -- Error: expected BitVec 8

def fixed {dom : DomainConfig} : Signal dom (BitVec 8) :=
  let wide : Signal dom (BitVec 16) := Signal.register 0#16 (Signal.pure 0#16)
  wide.map (BitVec.extractLsb' 0 8 ·)  -- ✓ explicit truncation

See docs/reference/Troubleshooting_Synthesis.md and docs/known-issues/KnownIssues.md for the current list of:

• Imperative syntax limitations (<~ inside conditionals).
• Pattern matching on tuples in synthesizable contexts.
• if-then-else vs Signal.mux in Signal contexts.
• Signal.loop feedback rules.
• bv_decide hanging inside lake build on Lean 4.28 (interactive only).

lake test

Runs Signal simulation, Verilog generation, vector / memory ops, temporal logic, CPU ISA proofs, BitNet golden-value validation, RV32 firmware, H.264 pipelines, YOLOv8 primitives, CDC queue stress, and the Verilator co-simulation layer.

sparkle/
├── Sparkle/      # Core library (Signal DSL, IR, Compiler, Backend, Verification)
├── IP/           # Verified IP cores (BitNet, YOLOv8, RV32, Drone, Humanoid, Video, Bus)
├── Examples/     # Runnable demos (Counter, Sparkle16 CPU, CDC, LoopSynthesis, …)
├── Tests/        # LSpec test suites for everything above
├── Tools/        # SVParser, verilog! / sim! macros, Signal DSL helpers
├── verilator/    # Verilator co-simulation backend for the RV32IMA SoC
├── firmware/     # RV32 firmware + OpenSBI + Linux device tree
├── c_src/        # C FFI libraries (loop memoization, JIT dlopen)
├── scripts/      # Tutorial syntax check + golden-value generators
├── docs/         # Hand-written docs (Tutorial, per-IP, KnownIssues, BENCHMARK)
└── lakefile.lean # Build configuration

Sparkle is an educational project demonstrating functional hardware description, dependent types for hardware, theorem proving for verification, and compiler construction / metaprogramming.

Contributions welcome — good first areas:

• Verified standard IP (parameterised FIFO, N-way arbiter, TileLink / AXI4 interconnect) with formal proofs.
• FPGA tape-out flow examples.
• Additional IR optimisation passes.
• More tutorials and worked examples.

The IR elaborator's error surface is still rough. Two messages in particular bury the real cause:

Cannot synthesise <name>: not inlinable and not a hardware module
Sub-module synthesis failed for <name> (tagged @[hardware_module])

Both are emitted from Sparkle/Compiler/Elab.lean:handleDefinitionUnfold where an inner MetaM exception is swallowed by a catch _. When this hits you, follow this workflow:

1. Look at the error in context. If <name> is one of Sparkle.Core.runCircuitH, Bind.bind, Pure.pure, Sparkle.Core.Signal.bundle*, the elaborator's unfoldDefinition? peeled the surface def but choked on something inside your DSL body (typeclass projection, an Applicative lift, a multi-arg lambda). See docs/reference/Troubleshooting_Synthesis.md §"Synthesis Compiler Patterns" for the patterns the elaborator does accept — common rewrites are listed in §"Fix patterns".

2. Get the real inner error. Temporarily change the two catch _ => clauses near Sparkle/Compiler/Elab.lean:1620 and :1631 to catch e => ... e.toMessageData.toString so the inner throwError propagates into the outer message. Most "not inlinable" failures resolve to something specific like a missing pattern-match arm, an unhandled operator, or a BitVec.zeroExtend-style call the IR doesn't speak. Revert the change before committing — leaving raw MessageData in the user-facing error breaks the existing test fixtures.

3. Found a new pattern that fails? Add a one-liner to docs/reference/Troubleshooting_Synthesis.md under the appropriate "NOT supported" / "Fix patterns" bullet so the next contributor sees it before they re-derive the problem. Two recent examples of the kind of entry to add are "multi-arg user-defined function via f <$> a <*> b" (rewrite the body to use Signal-native operators directly) and "(fun v => 0#m ++ v ++ 0#n)" (split into a chain of ++).

4. If the elaborator itself should learn this case, file a followup under docs/known-issues/TODO.md §"Compiler / IR" so the rough surface can be filed down rather than papered over. The shipped error today is the cap on how fast a new contributor can debug their first synthesisable circuit, so work that reduces it is high-leverage.

The Sparkle/IP/Net/CRC32.lean development is a worked example: the byte-feed engine first failed with the generic "Sub-module synthesis failed" message, the inner error revealed Cannot synthesise runCircuitH, and the fix turned out to be rewriting crc32Step <$> crc <*> byte (a user-defined 2-arg function lifted through Applicative) as a Signal-native chain of ^^^/&&&/>>>/++/-.

Completed phases live in docs/CHANGELOG.md.

Next up:

• Verified Standard IP — Parameterised FIFO — generic depth / width FIFO.
• Verified Standard IP — N-way Arbiter — generalise the 2-client round-robin arbiter to N clients.
• Verified Standard IP — TileLink / AXI4 Interconnect — full AXI4 (bursts, IDs) and TileLink.
• GPGPU / Vector Core — apply the VDD framework to highly concurrent, memory-bound accelerator architectures.
• FPGA Tape-out Flow — end-to-end examples deploying Sparkle-generated Linux SoCs to physical FPGAs.

Junji Hashimoto — Twitter / X: @junjihashimoto3

Apache License 2.0 — see LICENSE.

• Inspired by Clash HDL
• Built with Lean 4
• Golden-reference cycle-accurate simulation via Verilator — used both as the CI co-sim reference and as the "if the JIT disagrees, the JIT is wrong" arbiter throughout the test suite.
• In-browser Lean via xeus-lean and JupyterLite — powers the hosted tutorial notebooks.
• Verilog toolchain integration via iverilog (round-trip checks) and Yosys (used in Ch 8 of the tutorial for equivalence checking / FPGA fit).

• Discord: https://discord.gg/94Xueve8WD — design discussion, weekly progress threads, beginner Q&A.