-
Notifications
You must be signed in to change notification settings - Fork 8
Expand file tree
/
Copy pathSparkle.lean
More file actions
32 lines (30 loc) · 896 Bytes
/
Sparkle.lean
File metadata and controls
32 lines (30 loc) · 896 Bytes
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
/-
Sparkle HDL - Root Module
A functional hardware description language in Lean 4.
Inspired by Haskell's Clash, designed for type-safe hardware design.
-/
import Sparkle.Core.Domain
import Sparkle.Core.Signal
import Sparkle.Core.StateMacro
import Sparkle.Core.Vector
import Sparkle.Core.OptimizedSim
import Sparkle.Data.BitPack
import Sparkle.IR.Type
import Sparkle.IR.AST
import Sparkle.IR.Builder
import Sparkle.IR.Optimize
import Sparkle.Compiler.Elab
import Sparkle.Compiler.DRC
import Sparkle.Backend.Verilog
import Sparkle.Backend.VCD
import Sparkle.Backend.CppSim
import Sparkle.Verification.Temporal
import Sparkle.Verification.Equivalence
import Sparkle.Core.JIT
import Sparkle.Core.JITLoop
import Sparkle.Core.SimParallel
import Sparkle.Core.Oracle
import Sparkle.Core.OracleSpec
import Sparkle.Core.MulOracle
import Sparkle.Verification.MulProps
import Sparkle.Utils.HexLoader