From 2abfb6d62237fbc64d57b9a9a25db8ef166efcdd Mon Sep 17 00:00:00 2001 From: John Wickerson Date: Mon, 17 Jan 2022 16:29:55 +0000 Subject: starting final complete pass (with word-chopping mode enabled) --- references.bib | 4 ++-- verified_resource_sharing.tex | 6 ++---- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/references.bib b/references.bib index b2a80ee..d2c6fab 100644 --- a/references.bib +++ b/references.bib @@ -24,7 +24,7 @@ } @misc{vericertfun-github, - author = {{Withheld for blind review}}, + author = {{Withheld for blind review but available from program chair}}, title = {Public Github repository for Vericert-Fun}, year = 2022, url = {https://github.com/[withheld]/Vericert-Fun}, @@ -441,7 +441,7 @@ year = {2016}, @techreport{pardalos_thesis, key = {zzzz}, -author = {{Withheld for blind review}}, +author = {{Withheld for blind review but available from program chair}}, title = {Formally verified resource sharing for High Level Synthesis}, year = 2021, diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex index 8eae906..5c7d44e 100644 --- a/verified_resource_sharing.tex +++ b/verified_resource_sharing.tex @@ -88,11 +88,9 @@ escapeinside=||, \maketitle \begin{abstract} - 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 concerns, Herklotz et al. have recently 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{}'s output cannot compete performance-wise with that of established HLS tools such as LegUp. A major reason for this is \vericert{}'s complete lack of support for resource sharing. +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 \emph{resource sharing}. - In this paper, we present \vericertfun: \vericert{} extended with function-level resource sharing. Where original \vericert{} creates one block of hardware per function \emph{call}, \vericertfun{} creates one block of hardware per function \emph{definition}. The enabling innovation is to extend \vericert{}'s intermediate language HTL with the ability to represent \emph{multiple} state machines, and then to add support for function calls that transfer control between these state machines. We are working to extend \vericert{}'s formal correctness proof to cover the translation from C source into this extended HTL language, and thence on to Verilog. - -We have benchmarked \vericertfun's performance on the PolyBench/C suite, and our results show the generated hardware having a resource usage of 0.49$\times$ \vericert{}'s on average, with a minimal increase (about 1\%) in execution time. +This paper introduces \vericertfun: \vericert{} extended with function-level resource sharing. Where original \vericert{} creates one block of hardware per function \emph{call}, \vericertfun{} creates one block of hardware per function \emph{definition}. The enabling innovation is to extend \vericert{}'s intermediate language HTL with the ability to represent \emph{multiple} state machines, and then to implement function calls by transferring control between these state machines. We are working to extend \vericert{}'s formal correctness proof to cover the translation from C source into this extended HTL language, and thence on to Verilog. We have benchmarked \vericertfun's performance on the PolyBench/C suite, and our results show the generated hardware having a resource usage of 0.49$\times$ \vericert{}'s on average, with a minimal increase (about 1\%) in execution time. \end{abstract} \section{Introduction} -- cgit