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
• 9 FPGA Bring-Up
• 10 Sparkle Architecture