Hyperblock Scheduling for Verified High-Level Synthesis

Add to your list(s) Download to your calendar using vCal

• Yann Herklotz (École Polytechnique Fédérale de Lausanne)
• Wednesday 19 June 2024, 15:00-16:00
• LT1, Computer Laboratory, William Gates Builiding, West Cambridge site.

If you have a question about this talk, please contact Markus Böck.

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 FPG As) 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.

This talk is part of the mb2663's list series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Computer Architecture Group Meeting
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• LT1, Computer Laboratory, William Gates Builiding, West Cambridge site
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.