Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow
summary
Wavelet is a formally verified compiler that translates a capability-annotated imperative IR into asynchronous dataflow graphs, mechanized in Lean and checked with SMT for the typechecker. Core passes prove forward simulation and determinacy, giving deadlock- and data-race freedom while supporting pipelining via fences. Evaluation shows Wavelet produces graphs comparable to unverified backends: about 1.7× slower and 2.3× larger than RipTide (and it surfaces a RipTide bug), and about 1.2× slower but lower FPGA resource use than LLVM CIRCT, averaging ~1.4× slower overall.
AI-written summary · about
chapters (10)
- 0:00Formal dataflow compiler intro
- 1:04Heterogeneous computing motivation
- 2:53Reconfigurable dataflow HLS
- 4:58Async compilation challenges
- 6:21Wavelet compiler goals
- 8:28Control flow conversion
- 11:41Memory sync type system
- 12:44Compiler pass guarantees
- 14:49Evaluation vs unverified compilers
- 16:57Conclusion
related talks
21mFlowCert: Translation Validation for Asynchronous Dataflow Programs via Dynamic(…)
01h 02mHydroflow: A Compiler Target for Fast, Correct Distributed Programs
21mRipple: Asynchronous Programming for Spatial Dataflow Architectures
36mTowards a Formally-verified Software Toolchain for open ISAs
19mPanel: Compilation Frameworks
25mCertiCoq-Wasm: Verified compilation from Coq to WebAssembly
15mThey're the same picture: a software-verification flow adapted for hardware verification
18mA Verified Compiler for a Functional Tensor Language