Sparkle Tutorial

Chapters

• 0 Setup
• 1 Lean 4 for HDL Authors
• 1b Your First Sparkle Project
• 2 Combinational Circuits
• 3 Sequential Circuits
• 4 Modules and Composition
• 5 Verilog Generation
• 6 Proofs: LTL Invariants
• 7 Proofs: Equivalence Checking
• 7b Equivalence across number types (FP, fixed-point, quantisation)
• 8 Netlist Generation with Yosys
• 8b Three ways to simulate, one interface
• 8c From Signal to Silicon
• 9 FPGA Bring-Up
• 10 Sparkle Architecture
• 11 Running the web3 Signing Device on Real Hardware
• 12 Control, estimation, and the engineering of precision
• 13 GPU Simulation: Monte-Carlo Sweeps and Systolic Arrays
• 14 Market Making on Silicon: an HFT Quoting Engine with a Proved Position Bound