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.

Quick Start: Tutorial walks from "hello counter" to formal verification in about 5 minutes. For the full Signal DSL syntax, see docs/SignalDSL_Syntax.md.

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/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.

-- 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.

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 — see docs/Tutorial.md.

• 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.md §5.4–5.6.
• 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).

Generate the full 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.md — 5-minute walkthrough + synthesis rules
  • docs/SignalDSL_Syntax.md — full DSL reference
  • docs/Troubleshooting_Synthesis.md
• Verification
  • docs/Verification_Framework.md — VDD patterns
  • Examples/TemporalLogicExample.md — LTL usage
• IP-specific docs
  • docs/BitNet.md · docs/YOLOv8.md
  • docs/RV32.md · docs/H264.md
  • docs/CDC.md
• Project meta
  • docs/CHANGELOG.md — release history
  • docs/STATUS.md — current capability matrix
  • docs/KnownIssues.md
  • docs/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/Troubleshooting_Synthesis.md and docs/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.

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