PLDI 2024
Mon 24 - Fri 28 June 2024 Copenhagen, Denmark
Wed 26 Jun 2024 15:00 - 15:20 at Iceland / Denmark - Formal Verification 1 Chair(s): Jeehoon Kang

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. Herklotz et al. 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. This paper reports 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 is a key challenge, which we address by using final-state predicates and value summaries. 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.

slides (presentation.pdf)1003KiB

Wed 26 Jun

Displayed time zone: Windhoek change

13:40 - 15:20
Formal Verification 1PLDI Research Papers at Iceland / Denmark
Chair(s): Jeehoon Kang KAIST
13:40
20m
Talk
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language
PLDI Research Papers
Gaurav Parthasarathy ETH Zurich, Thibault Dardinier ETH Zurich, Benjamin Bonneau Verimag, Peter Müller ETH Zurich, Alexander J. Summers University of British Columbia
DOI
14:00
20m
Talk
Verified Extraction from Coq to OCaml
PLDI Research Papers
DOI
14:20
20m
Talk
Verification under Intel-x86 with Persistency
PLDI Research Papers
Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Ahmed Bouajjani IRIF, Université Paris Diderot, K Narayan Kumar Chennai Mathematical Institute, Prakash Saivasan The Institute of Mathematical Sciences, India
DOI
14:40
20m
Talk
RefinedRust: A Type System for High-Assurance Verification of Rust Programs
PLDI Research Papers
Lennard Gäher MPI-SWS, Michael Sammler MPI-SWS, Ralf Jung ETH Zurich, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS
DOI
15:00
20m
Talk
Hyperblock Scheduling for Verified High-Level Synthesis
PLDI Research Papers
Yann Herklotz Imperial College London, John Wickerson Imperial College London
DOI Pre-print File Attached