Resource Sharing for Verified High-Level Synthesis
Michalis Pardalos, Yann Herklotz, John Wickerson · 2022
High-level synthesis (HLS) is playing an ever-increasing role in hardware design, but concerns have been raised about its reliability. Seeking to address these, Herklotz et al. have developed an HLS compiler called Vericert that has been mechanically proven (using the Coq proof assistant) to output Verilog designs that are behaviourally equivalent to the input C program. Unfortunately, Vericert cannot compete performance-wise with established HLS tools, and a major reason for this is Vericert’s complete lack of support for resource sharing.This paper introduces Vericert-Fun: Vericert extended with function-level resource sharing. Where original Vericert creates one block of hardware per function call, Vericert-Fun creates one block of hardware per function definition. To enable this, we extend Vericert’s intermediate language HTL with the ability to represent multiple state machines, and we implement function calls by transferring control between these state machines. We are working to extend Vericert’s correctness proof to cover the translation from C into this extended HTL and thence to Verilog. Benchmarking on the PolyBench/C suite indicates that Vericert-Fun generates hardware with about 0.8× the resource usage of Vericert’s on average, with minimal impact on execution time.