Resource Sharing for Verified High-Level Synthesis

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

• Michalis Pardalos
• Monday 01 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.

High-level synthesis is playing an ever-increasing role in hardware design, but concerns have been raised about its reliability. Seeking to address these concerns, Herklotz et al. have recently developed a high-level synthesis compiler, called Vericert, that has been mechanically proven correct. Unfortunately, Vericert’s output cannot compete performance-wise with established HLS tools suchas LegUp or Bambu. One reason for this is Vericert’s complete lack of support for resource sharing. In this paper, we present an extension to Vericert to implement function-level resource sharing. We extend the formal proof of correctness of the compiler to fully cover our changes. This involves extending the semantics of HTL , an internal, Verilog-like language of Vericert. Our benchmarking using the PolyBench/C benchmark suite shows the generated hardware having a resource usage of 61% of the original on average and 46% in the best case, for only a 3% average decrease in max frequency and 1% average increase in cycle count.

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.