diff options
Diffstat (limited to 'verified_resource_sharing.tex')
| -rw-r--r-- | verified_resource_sharing.tex | 6 |
1 files changed, 2 insertions, 4 deletions
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} |