Update on Overleaf.

1 files changed, 13 insertions, 1 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index 2395afb..0fcda90 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -1,6 +1,7 @@
 \documentclass[hyphens,prologue,x11names,rgb,sigconf]{acmart}
 
 \usepackage[textsize=small,shadow]{todonotes}%
+\usepackage{soul}
 
 % Leave review comments using
 % \jwcomment{...} (for John) or \yhcomment{...} (for Yann)
@@ -9,6 +10,13 @@
 \newcommand{\jwcomment}[2][]{\todo[author={John}, color=ACMLightBlue, #1]{#2}}
 \newcommand{\yhcomment}[2][]{\todo[author={Yann}, color=ACMGreen, #1]{#2}}
 
+
+\newif\ifCOMMENTS
+\COMMENTStrue
+\newcommand{\Comment}[3]{\ifCOMMENTS\textcolor{#1}{{\bf [\![#2:} #3{\bf ]\!]}}\fi}
+\newcommand\JW[2][]{\st{#1}\Comment{red!75!black}{JW}{#2}}
+
+
 \newcommand{\citeintext}[1] {\citeauthor{#1} in \citeyear{#1}~\cite{#1}}
 \newcommand{\citeshort}[1] {\citeauthor{#1} \citeyear{#1}~\cite{#1}}
 
@@ -29,7 +37,11 @@
 \affiliation{\institution{Imperial College London}}
 
 \begin{abstract}
-  High-level synthesis 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 a high-level synthesis compiler, called Vericert, that has been mechanically proven correct \jwcomment{in the sense that every Verilog design produced by Vericert is guaranteed to be behaviourally equivalent to its input C program}. Unfortunately, Vericert's output cannot compete performance-wise with established HLS tools such as LegUp or Bambu \jwcomment{this list should include the HLS tools we actually compare against, once we've settled on which tools those will be}. One reason for this is Vericert's complete lack of support for resource sharing. In this paper, we present an extension to Vericert to implement function-level resource sharing. We extend the formal proof of correctness of the compiler to fully cover our changes. This involves extending the semantics of HTL, an internal, Verilog-like language of Vericert. Our benchmarking using the PolyBench/C benchmark suite shows the generated hardware having a resource usage of 61\% of the original on average and 46\% in the best case, for only a 3\% average decrease in max frequency and 1\% average increase in cycle count. \jwcomment{I'd be tempted to put the experimental results last, after the discussion of your implementation and proof.}
+  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. 
+  
+  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 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}
 
 \maketitle