starting final complete pass (with word-chopping mode enabled)

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}