This talk is part of the Cambridge Compiler Social: https://grosser.science/compiler-social-2024-06-19/
High-level synthesis (HLS) is the automatic compilation of software programs into custom hardware designs. With programmable hardware devices (such as FPGAs) now widespread, HLS is increasingly relied upon, but existing HLS tools are too unreliable for safety- and security-critical applications. We partially addressed this concern by building Vericert, a prototype HLS tool that is proven correct in Coq (à la CompCert), but it cannot compete performance-wise with unverified tools.
In this talk I'll report on our efforts to close this performance gap, thus obtaining the first practical verified HLS tool. We achieve this by implementing a flexible operation scheduler based on hyperblocks (basic blocks of predicated instructions) that supports operation chaining (packing dependent operations into a single clock cycle). Correctness is proven via translation validation: each schedule is checked using a Coq-verified validator that uses a SAT solver to reason about predicates. Avoiding exponential blow-up in this validation process was a key challenge. Experiments on the PolyBench/C suite indicate that scheduling makes Vericert-generated hardware 2.1× faster, thus bringing Vericert into competition with a state-of-the-art open-source HLS tool when a similar set of optimisations is enabled.
About Yann Herklotz:
Yann is a postdoc at EPFL in the verification and computer architecture (VCA) lab led by Thomas Bourgeat. He is working on dynamic high-level synthesis, as well as on the verification of hardware designs using interactive theorem provers, trying to make hardware proofs more compositional and scale better with the design size. Before that he was a PhD student supervised by John Wickerson at Imperial College, working on verified high-level synthesis and building Vericert with the aim of generating optimised hardware designs from verified software, thereby moving verification to a higher level.
