Update on Overleaf.

4 files changed, 23 insertions, 15 deletions

diff --git a/evaluation.tex b/evaluation.tex
index 8f20b29..5d2034e 100644
--- a/evaluation.tex
+++ b/evaluation.tex
@@ -15,21 +15,21 @@ Our evaluation is designed to answer the following three research questions. \JW
 \begin{description}
 \item[RQ1] How fast is the hardware generated by \vericert{}, and how does this compare to existing HLS tools?
 \item[RQ2] How area-efficient is the hardware generated by \vericert{}, and how does this compare to existing HLS tools?
-%\item[RQ3] How long does \vericert{} take to produce hardware?
+\item[RQ3] How long does \vericert{} take to produce hardware?
 \end{description}
 
 \subsection{Experimental Setup}
 
 \paragraph{Choice of HLS tool for comparison.} We compare \vericert{} against LegUp 4.0 because it is open-source and hence easily accessible, but still produces hardware ``of comparable quality to a commercial high-level synthesis tool''~\cite{canis11_legup}.
 
-\paragraph{Choice of benchmarks.} We evaluate \vericert{} using the PolyBench/C benchmark suite\footnote{\url{http://web.cs.ucla.edu/~pouchet/software/polybench/}} and some CHStone benchmarks\footnote{\url{http://www.ertl.jp/chstone/}}. \JW{I would make these footnotes into proper cites, because there is no limit on how long the bibliography can be.} PolyBench/C is a modern benchmark suite that has been previously used to evaluate HLS tools~\cite{choi+18}. For completeness, we use the full set of 24 benchmarks. We set the benchmark parameters so that all datatypes are integers (since \vericert{} only supports integers) and all datasets are `small' (to fit into the small on-chip memories). A current limitation of \vericert{}, as discussed in Section~\ref{?}, is that it does not support addition and subtraction operations involving integer literals not divisible by 4. To work around this, we lightly modified each benchmark program so that literals other than multiples of 4 are stored into variables before being added or subtracted. \JW{Any other notable changes to the benchmarks?}
+\paragraph{Choice of benchmarks.} We evaluate \vericert{} using the PolyBench/C benchmark suite~\cite{polybench}. PolyBench/C is a modern benchmark suite that has been previously used to evaluate HLS tools~\cite{choi+18}. For completeness, we use the full set of 24 benchmarks. We set the benchmark parameters so that all datatypes are integers (since \vericert{} only supports integers) and all datasets are `small' (to fit into the small on-chip memories). A current limitation of \vericert{}, as discussed in Section~\ref{?}, is that it does not support addition and subtraction operations involving integer literals not divisible by 4. To work around this, we lightly modified each benchmark program so that literals other than multiples of 4 are stored into variables before being added or subtracted. \JW{Any other notable changes to the benchmarks?}
 
 \paragraph{Experimental setup.} In order to generate a hardware implementation, the Verilog produced by the HLS tool-under-test must be synthesised to a netlist; the resultant netlist can then be placed-and-routed for a particular FPGA device. We use Intel Quartus~\cite{quartus} for both of these  tasks, and we target an Arria 10 FPGA.
 
 \begin{table*}
   \begin{tabular}{lcccccccccccc}
     \toprule
-    Bench & \multicolumn{2}{c}{Cycles} & \multicolumn{2}{c}{Frequency / MHz} & \multicolumn{2}{c}{LUTs} & \multicolumn{2}{c}{Reg} & \multicolumn{2}{c}{BRAMs} & \multicolumn{2}{c}{DSPs}\\
+    \textbf{Benchmark} & \multicolumn{2}{c}{\bf Cycles} & \multicolumn{2}{c}{\bf Frequency / MHz} & \multicolumn{2}{c}{\bf LUTs} & \multicolumn{2}{c}{\bf Registers} & \multicolumn{2}{c}{\bf Block RAMs} & \multicolumn{2}{c}{\bf DSPs}\\
     & L & V & L & V & L & V & L & V & L & V & L & V\\
     \midrule
     adpcm & 30241 & 121386 & 90.05 & 66.3 & 7719 & 51626 & 12034 & 42688 & 7 & 0 & 0 & 48\\
@@ -38,7 +38,7 @@ Our evaluation is designed to answer the following three research questions. \JW
     mips & 7754 & 18482 & 98.95 & 78.43 & 5049 & 10617 & 4185 & 7690 & 0 & 0 & 0 & 0\\
     \bottomrule
   \end{tabular}
-  \caption{CHStone programs synthesised in \legup{} 5.1 and with \vericert{}}\label{tab:chstone}
+  \caption{CHStone programs synthesised with \legup{} 5.1 (L) and with \vericert{} (V) \JW{I guess this table is for the chop?}}\label{tab:chstone}
 \end{table*}
 
 \subsection{RQ1: How fast is \vericert{}-generated hardware?}
diff --git a/introduction.tex b/introduction.tex
index b2d25b0..0f0c789 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -34,7 +34,7 @@ For example, the translation validation for Catapult C~\cite{mentor20_catap_high
 Our position is that none of the above workarounds are necessary if the HLS tool can simply be trusted to work correctly.
 
 \subsection{Our solution}
-We have written a new HLS tool in the Coq theorem prover~\cite{bertot04_inter_theor_provin_progr_devel} and proven that it any output it produces always has the same behaviour as its input. Our tool, which is called \vericert{}, is automatically extracted to an OCaml program from Coq, which ensures that the object of the proof is the same as the implementation of the tool. \vericert{} is built by extending the \compcert{} verified C compiler~\cite{leroy09_formal_verif_realis_compil} with a new hardware-specific intermediate language and a Verilog back end. It supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables.
+We have written a new HLS tool in the Coq theorem prover~\cite{bertot04_inter_theor_provin_progr_devel} and proven that it any output it produces always has the same behaviour as its input. Our tool, which is called \vericert{},\ifANONYMOUS\footnote{Tool name has been changed for blind review.}\fi{} is automatically extracted to an OCaml program from Coq, which ensures that the object of the proof is the same as the implementation of the tool. \vericert{} is built by extending the \compcert{} verified C compiler~\cite{leroy09_formal_verif_realis_compil} with a new hardware-specific intermediate language and a Verilog back end. It supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables.
 
 \subsection{Contributions and Outline}
 
@@ -42,7 +42,7 @@ The contributions of this paper are as follows:
 
 \begin{itemize}
   \item We present \vericert{}, the first mechanically verified HLS tool that compiles C to Verilog. The design of \vericert{} is described in Section~\ref{sec:design}.
-  \item We prove \vericert{} correct w.r.t. an existing semantics for Verilog due to \citet{loow19_formalise}. We describe in Section~\ref{sec:verilog} how we lightly extended this semantics to make it suitable as an HLS target. Section~\ref{sec:proof} describes the proof itself.
+  \item We prove \vericert{} correct w.r.t. an existing semantics for Verilog due to \citet{loow19_proof_trans_veril_devel_hol}. We describe in Section~\ref{sec:verilog} how we lightly extended this semantics to make it suitable as an HLS target. Section~\ref{sec:proof} describes the proof itself.
   \item We have conducted a performance comparison between \vericert{} and a widely-used (unverified) HLS tool called \legup{}~\cite{canis11_legup} using the PolyBench benchmarks. As described in Section~\ref{sec:evaluation}, \vericert{} generates hardware that is about 9x slower and 21x less area-efficient than that generated by \legup{}. We expect that these numbers will improve once we have extended \vericert{} with such optimisations as loop pipelining and scheduling.
 \end{itemize}
 
diff --git a/proof.tex b/proof.tex
index f9a41bf..292c364 100644
--- a/proof.tex
+++ b/proof.tex
@@ -104,17 +104,17 @@ The Verilog semantics that are used are deterministic, as the order of operation
 
 \begin{table*}
   \centering
-  \begin{tabular}{p{4cm}p{1cm}p{1cm}p{1cm}p{1.5cm}p{1cm}}
+  \begin{tabular}{llllll}
     \toprule
-    & \textbf{Coq Code} & \textbf{OCaml Code} & \textbf{Specifi\-cations} & \textbf{Theorems \& Proofs} & \textbf{Total}\\
+    & \textbf{Coq code} & \textbf{OCaml code} & \textbf{Specifications} & \textbf{Theorems \& Proofs} & \textbf{Total}\\
     \midrule
-    {\footnotesize Data structures and libraries}     & 274  & -   & -    & 654  & 928  \\
-    {\footnotesize Integers and values}               & 98   & -   & 15   & 744  & 857  \\
-    {\footnotesize HTL semantics}                     & -    & -   & 174  & -    & 174  \\
-    {\footnotesize HTL generation}                    & 655  & -   & 79   & 3349 & 4083 \\
-    {\footnotesize Verilog semantics}                 & -    & -   & 739  & 174  & 913  \\
-    {\footnotesize Verilog generation}                & 68   & -   & -    & 396  & 464  \\
-    {\footnotesize Top-level driver, pretty printers} & 89   & 747 & -    & 209  & 1045 \\
+    {Data structures and libraries}     & 274  & -   & -    & 654  & 928  \\
+    {Integers and values}               & 98   & -   & 15   & 744  & 857  \\
+    {HTL semantics}                     & -    & -   & 174  & -    & 174  \\
+    {HTL generation}                    & 655  & -   & 79   & 3349 & 4083 \\
+    {Verilog semantics}                 & -    & -   & 739  & 174  & 913  \\
+    {Verilog generation}                & 68   & -   & -    & 396  & 464  \\
+    {Top-level driver, pretty printers} & 89   & 747 & -    & 209  & 1045 \\
     \midrule
     \textbf{Total}                                    & 1184 & 747 & 1007 & 5526 & 8464 \\
     \bottomrule
diff --git a/references.bib b/references.bib
index c57bad9..00bcc64 100644
--- a/references.bib
+++ b/references.bib
@@ -32,6 +32,14 @@
   series          = {PLDI '15},
 }
 
+@misc{polybench,
+author = {Pouchet, Louis-No\"el},
+title = {PolyBench/C: the Polyhedral Benchmark suite},
+url = {http://web.cse.ohio-state.edu/~pouchet.2/software/polybench/},
+year = {2020},
+}
+
+
 @article{takach16_high_level_synth,
   author          = {A. {Takach}},
   title           = {High-Level Synthesis: Status, Trends, and Future