Hyperblock Scheduling for Verified High-Level Synthesis
summary
A verified HLS backend implements a hyperblock scheduler with operation chaining and a system-of-difference-constraints LP scheduler, emits schedules checked by a Coq-verified validator that calls a SAT solver, and uses final-state predicates and value summaries to avoid exponential blowup in validation. Experiments on PolyBench/C show Vericert-generated hardware runs about 2.1× faster, bringing a verified flow into practical competition with an open-source HLS tool when similar optimizations are enabled.
AI-written summary · about
chapters (8)
- 0:00Introduction to high-level synthesis challenges
- 1:27Verified hardware with Coq
- 2:54Hyperblock scheduling
- 5:03Difference constraints scheduler
- 6:50Performance vs Bamboo
- 9:01Scheduler verification
- 13:53Three-valued logic handling
- 16:45Conclusion
related talks
19mFormally Verified Superblock Scheduling
19mFully Verified Instruction Scheduling
15mCertified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors
19mFormally Verifying Optimizations with Block Simulations
15mThey're the same picture: a software-verification flow adapted for hardware verification
30mAutomated High-Level Synthesis Design Modularization via E-Graph Anti-Unification
24mVerified Tensor-Program Optimization Via High-Level Scheduling Rewrites
13mInteractive Bit Vector Reasoning using Verified Bitblasting