Update on Overleaf.

1 files changed, 2 insertions, 2 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index 0fcda90..bd7cea2 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -37,9 +37,9 @@
 \affiliation{\institution{Imperial College London}}
 
 \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 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 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. 
   
-  In this paper, we present Vericert-Fun: Vericert extended with function-level resource sharing. Where original Vericert creates one block of hardware per \emph{function call}, Vericert-Fun creates one block of hardware per \emph{function}. The enabling innovation is to extend Vericert's intermediate language HTL with the ability to represent \emph{multiple} FSMDs, and then to add support for function calls that transfer control between these FSMDs. We have extended Vericert's formal correctness proof to cover the translation from C source into this extended HTL language. 
+  In this paper, we present Vericert-Fun: Vericert extended with function-level resource sharing. Where original Vericert creates one block of hardware per \emph{function call}, Vericert-Fun creates one block of hardware per \emph{function 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 have extended Vericert's formal correctness proof to cover the translation from C source into this extended HTL language. 
   
   In order to benchmark Vericert-Fun's performance, we have added an (unverified) Verilog-producing backend. Our results on the PolyBench/C benchmark suite show the generated hardware having a resource usage of 61\% of Vericert's on average and 46\% in the best case, for only a 3\% average decrease in max frequency and 1\% average increase in cycle count.
 \end{abstract}