They're the same picture: a software-verification flow adapted for hardware verification
summary
Claims that the CakeML software-verification flow maps to hardware by replacing source functions with shallow-embedded Verilog, compiler correctness with a verified Verilog-to-netlist tool, and machine code with netlists, all formalized in HOL4 formalization. Built a verified synthesis backend called Lucy verified synthesis tool, verified a realistic CPU that runs CakeML, handled Verilog quirks (blocking vs non-blocking, X values, simulation vs synthesis), and reports the workflow works with no show-stoppers plus an interactive Verilog semantics visualizer.
AI-written summary · about
chapters (15)
- 0:00Intro
- 0:50Context
- 1:18Motivation
- 1:51Flow
- 3:19Synthesis tools
- 3:36Software verification flow
- 4:03KML ecosystem
- 4:53The flow
- 5:34Hardware verification
- 6:40Differences
- 8:20Simulationsynthesis mismatches
- 9:54Why Verilog
- 12:26Formalizing Pro Standards
- 13:24Formal Semantic Visualization
- 14:14Conclusion
related talks
01h 05mMuch Still to Do in Compiler Verification (A Perspective from the CakeML Project)
43mFrom CakeML to Proof Checking, and Back Again
24mCakes That Bake Cakes: Dynamic Computation in CakeML
17mPureCake: A Verified Compiler for a Lazy Functional Language
21mVerified VCG and Verified Compiler for Dafny
22mHyperblock Scheduling for Verified High-Level Synthesis
17mLet It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow
56mProof Assistants At the Hardware-Software Interface