Formal Verification of High-Level Synthesis

on YouTube ↗15m

" summary

Presents a mechanically verified HLS tool called Vericert that extends CompCert and is proved correct in Coq, translating CompCert 3AC into an HTL FSM and then to Verilog with a proven RAM implementation. Supports integer ops, function calls, local arrays, structs/unions and general control flow; performs RAM inference to use FPGA RAM blocks. Runs 27 of 30 PolyBench programs, is ~27× slower with division and ~2× slower without division versus LegUp, and after fixing a pretty-print bug shows 0% runtime errors under Csmith fuzzing.

AI-written summary · about

" chapters (13)

1. 0:00The Need to Design Hardware Accelerators
2. 1:17Where does the flexibility of FPGAs come from?
3. 1:54So How do we Program an FPGA?
4. 3:25Motivation for Formal Verification
5. 3:49Solution
6. 4:36Outline
7. 5:07HTL Overview
8. 6:07Translation (3ACHTL)
9. 6:55Memory Inference Pass
10. 9:56Main Challenges in Proof
11. 12:54The better news: without division about 2x slower
12. 13:16Fuzzing Vericert with Csmith
13. 13:49Conclusion