BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Hyperblock Scheduling for Verified High-Level Synthesis - Yann Her
 klotz (École Polytechnique Fédérale de Lausanne)
DTSTART:20240619T140000Z
DTEND:20240619T150000Z
UID:TALK217987@talks.cam.ac.uk
CONTACT:Markus Böck
DESCRIPTION:This talk is part of the Cambridge Compiler Social: https://gr
 osser.science/compiler-social-2024-06-19/\n\nHigh-level synthesis (HLS) is
  the automatic compilation of software programs into custom hardware desig
 ns. With programmable hardware devices (such as FPGAs) now widespread\, HL
 S is increasingly relied upon\, but existing HLS tools are too unreliable 
 for safety- and security-critical applications. We partially addressed thi
 s concern by building Vericert\, a prototype HLS tool that is proven corre
 ct in Coq (à la CompCert)\, but it cannot compete performance-wise with u
 nverified tools.\n\nIn 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 hype
 rblocks (basic blocks of predicated instructions) that supports operation 
 chaining (packing dependent operations into a single clock cycle). Correct
 ness 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 challe
 nge. Experiments on the PolyBench/C suite indicate that scheduling makes V
 ericert-generated hardware 2.1× faster\, thus bringing Vericert into comp
 etition with a state-of-the-art open-source HLS tool when a similar set of
  optimisations is enabled.\n\nAbout Yann Herklotz:\n\nYann is a postdoc at
  EPFL in the verification and computer architecture (VCA) lab led by Thoma
 s Bourgeat. He is working on dynamic high-level synthesis\, as well as on 
 the verification of hardware designs using interactive theorem provers\, t
 rying to make hardware proofs more compositional and scale better with the
  design size. Before that he was a PhD student supervised by John Wickerso
 n at Imperial College\, working on verified high-level synthesis and build
 ing Vericert with the aim of generating optimised hardware designs from ve
 rified software\, thereby moving verification to a higher level.
LOCATION:LT1\, Computer Laboratory\, William Gates Builiding\, West Cambri
 dge site
END:VEVENT
END:VCALENDAR