Imperial College London > Talks@ee.imperial > CAS Talks > Resource Sharing for Verified High-Level Synthesis

Resource Sharing for Verified High-Level Synthesis

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Changes to Talks@imperial | Privacy and Publicity