Update on Overleaf.

1 files changed, 6 insertions, 2 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index 4c104ba..01eeeae 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -37,6 +37,7 @@ escapeinside=||,
 % e.g. \jwcomment[inline]{...} leaves an inline comment
 \newcommand{\jwcomment}[2][]{\todo[author={John}, color=ACMLightBlue, #1]{#2}}
 \newcommand{\yhcomment}[2][]{\todo[author={Yann}, color=ACMGreen, #1]{#2}}
+\newcommand{\mpcomment}[2][]{\todo[author={Michalis}, color=ACMMagenta, #1]{#2}}
 
 
 \newif\ifCOMMENTS
@@ -44,6 +45,7 @@ escapeinside=||,
 \newcommand{\Comment}[3]{\ifCOMMENTS\textcolor{#1}{{\bf [\![#2:} #3{\bf ]\!]}}\fi}
 \newcommand\JW[2][]{\st{#1}\Comment{red!75!black}{JW}{#2}}
 \newcommand\YH[2][]{\st{#1}\Comment{blue!50!green}{YH}{#2}}
+\newcommand\MP[2][]{\st{#1}\Comment{blue!50!magenta}{MP}{#2}}
 
 
 \newcommand{\citeintext}[1] {\citeauthor{#1} in \citeyear{#1}~\cite{#1}}
@@ -68,7 +70,7 @@ escapeinside=||,
 \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. 
   
-  In this paper, we present Vericert-Fun: Vericert extended with function-level resource sharing. Where original Vericert creates one block of hardware per function \emph{call}, Vericert-Fun 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 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 function \emph{call} \MP{Is this an over-simplification? We don't really generate a "block of hardware" for function calls}, Vericert-Fun 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 have extended Vericert's formal correctness proof to cover the translation from C source into this extended HTL language. \MP{Is this done?}
   
   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}
@@ -241,7 +243,7 @@ Figure~\ref{fig:example_3AC} shows the 3AC representation of that C program, as
 \label{fig:example_3AC}
 \end{figure}
 
-Figure~\ref{fig:example_HTL} depicts the result of converting those CFGs into two state machines. The conversion of 3AC instructions into Verilog instructions has been described already by \citeauthor{vericert}; what is new here is the handling of function calls, so the following description concentrates on that aspect. Before we proceed, there are three conventions worth noting: first, ``$*{\rightarrow}\langle\mathit{node}\rangle$'' should be interpreted as an abbreviation for edges from all nodes to $\langle\mathit{node}\rangle$; second, the dotted edges are intended to suggest how control is passed between the two state machines, but they carry no formal meaning; and third, we allow the \lstinline{main} machine to register $\langle\mathit{reg}\rangle$ in the \lstinline{add} machine using ``\lstinline{add.}$\langle\mathit{reg}\rangle$''.
+Figure~\ref{fig:example_HTL} depicts the result of converting those CFGs into two state machines. The conversion of 3AC instructions into Verilog instructions has been described already by \citeauthor{vericert}; what is new here is the handling of function calls, so the following description concentrates on that aspect. Before we proceed, there are three conventions worth noting: first, ``$*{\rightarrow}\langle\mathit{node}\rangle$'' should be interpreted as an abbreviation for edges from all nodes to $\langle\mathit{node}\rangle$; second, the dotted edges are intended to suggest how control is passed between the two state machines, but they carry no formal meaning \MP{There should be a better way to show the CFG. The lines from main to add show the initiation of a parallel execution. The ones from add to main show its ending (roughly). This is also not quite correct since functions are, conceptually, all executing at all times}; and third, we allow the \lstinline{main} machine to register $\langle\mathit{reg}\rangle$ in the \lstinline{add} machine using ``\lstinline{add.}$\langle\mathit{reg}\rangle$''.
 
 \definecolor{background}{HTML}{eeeeee}
 \begin{figure}
@@ -343,6 +345,8 @@ The same sequence of events can also be understood using a timing diagram, as gi
 \label{fig:timingdiagram}
 \end{figure}
 
+\section{Proving Vericert-Fun correct}
+
 
 \section{Rough notes}
 A few points that we might want to address at some point: