Update: Starting off our compiler social will be a talk by Yann Herklotz (EPFL) titled:
Hyperblock Scheduling for Verified High-Level Synthesis
Abstract:
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.
Celebrating Computer Architecture
For anyone curious, the day before the social, June 18th, there is also an event celebrating Computer Architecture in the same venue as the social: https://www.cst.cam.ac.uk/news/celebrating-computer-architecture