Hyperblock Scheduling for a Verified High-Level Synthesis Tool

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

• Yann Herklotz Grave ( Imperial College)
• Monday 22 November 2021, 16:00-17:00
• Teams (in the "CAS Seminars" team).

If you have a question about this talk, please contact George A Constantinides.

The drive for fast and energy-efficient computation has led to a recent explosion of interest in application-specific accelerators. These are often obtained via high-level synthesis (HLS) from a software program written in a C-like language. In response to concerns about the trustworthiness of the current crop of HLS tools, we have developed Vericert, an open-source CompCert-style HLS tool that is proven correct in Coq. But although Vericert-generated accelerators are guaranteed to be correct, their performance cannot compete with those produced by mainstream (unverified) HLS tools.

In this talk I will present our efforts to close this performance gap, by implementing translation validated scheduling. Our scheduler works on hyperblocks (basic blocks of predicated instructions), and supports operation chaining (whereby dependent operations can be packed into a single clock cycle). I will talk about how the validator and proof of correctness was developed, as well as some preliminary results using the PolyBench/C benchmarks.

This talk is part of the CAS Talks series.

This talk is included in these lists:

• Andrea Picciau's list
• CAS Talks
• Circuits and Systems Group: Internal Seminars
• Teams (in the "CAS Seminars" team)

Note that ex-directory lists are not shown.