Update on Overleaf.

4 files changed, 12 insertions, 9 deletions

diff --git a/algorithm.tex b/algorithm.tex
index c81cbfa..1302d64 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -29,7 +29,8 @@ The .NET framework has been used as a basis for other HLS tools, such as Kiwi~\c
 
 \begin{figure}
   \centering
-  \resizebox{0.85\textwidth}{!}{
+  % JW: resizebox is associated with puppies dying
+  %\resizebox{0.85\textwidth}{!}{
   \begin{tikzpicture}
     [language/.style={fill=white,rounded corners=3pt,minimum height=7mm},
     continuation/.style={}]
@@ -56,7 +57,7 @@ The .NET framework has been used as a basis for other HLS tools, such as Kiwi~\c
     \draw[->,thick] (rtl) -- (htl);
     \draw[->,thick] (htl) -- (verilog);
     \draw[->,thick] (htl.west) to [out=180,in=150] (4,-2.2) to [out=330,in=270] (htl.south);
-  \end{tikzpicture}}
+  \end{tikzpicture}%}
   \caption{\vericert{} as a Verilog back end to \compcert{}}%
   \label{fig:rtlbranch}
 \end{figure}
diff --git a/introduction.tex b/introduction.tex
index 30ad118..b532112 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -34,14 +34,14 @@ 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.
 
 \paragraph{Our solution}
-We have designed a new HLS tool in the Coq theorem prover and proved that any output it produces always has the same behaviour as its input. Our tool, 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 case statements, function pointers, recursive function calls, integers larger than 32 bits, floats, and global variables.
+We have designed a new HLS tool in the Coq theorem prover and proved that any output it produces always has the same behaviour as its input. Our tool, 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 most C constructs, including integer operations, function calls, local arrays, structs, unions, and general control-flow statements, but currently excludes support for case statements, function pointers, recursive function calls, integers larger than 32 bits, floats, and global variables.
 
 \paragraph{Contributions and Outline}
 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. In Section~\ref{sec:design}, we describe the design of \vericert{}.
-  \item We state the correctness theorem of \vericert{} with respect to an existing semantics for Verilog due to \citet{loow19_proof_trans_veril_devel_hol}. In Section~\ref{sec:verilog}, we describe how we lightly extended this semantics to make it suitable as an HLS target.
+  \item We present \vericert{}, the first mechanically verified HLS tool that compiles C to Verilog. In Section~\ref{sec:design}, we describe the design of \vericert{}, \JW{including a few optimisations related to memory accesses and division.}
+  \item We state the correctness theorem of \vericert{} with respect to an existing semantics for Verilog due to \citet{loow19_proof_trans_veril_devel_hol}. In Section~\ref{sec:verilog}, we describe how we lightly \JW{Maybe remove `lightly' now -- the changes feel a bit more than just `light' nowadays!} extended this semantics to make it suitable as an HLS target.
   \item In Section~\ref{sec:proof}, we describe how we proved the correctness theorem. The proof follows standard \compcert{} techniques -- forward simulations, intermediate specifications, and determinism results -- but we encountered several challenges peculiar to our hardware-oriented setting.  These include handling discrepancies between byte- and word-addressable memories, different handling of unsigned comparisons between C and Verilog, correctly mapping CompCert's memory model onto a finite Verilog array and finally correctly rearranging memory reads and writes so that these behave properly as a RAM in hardware.
   \item In Section~\ref{sec:evaluation}, we evaluate \vericert{} on the \polybench{} benchmark suite~\cite{polybench}, and compare the performance of our generated hardware against an existing, unverified HLS tool called \legup{}~\cite{canis11_legup}. We show that \vericert{} generates hardware that is \slowdownOrig$\times$ slower (\slowdownDiv$\times$ slower in the absence of division) and \areaIncr$\times$ larger than that generated by \legup{}. We intend to bridge this performance gap in the future by introducing (and verifying) HLS optimisations of our own, such as scheduling and memory analysis.
 \end{itemize}
@@ -50,7 +50,7 @@ The contributions of this paper are as follows:
 
 \begin{center}
 \ifANONYMOUS
-\url{https://github.com/anonymised-for-blind-review}
+[GitHub link removed for blind review]
 \else 
 \url{https://github.com/ymherklotz/vericert}
 \fi
diff --git a/main.tex b/main.tex
index e221e39..c22ede0 100644
--- a/main.tex
+++ b/main.tex
@@ -1,5 +1,5 @@
 %% For double-blind review submission, w/o CCS and ACM Reference (max submission space)
-\documentclass[acmsmall,10pt,pagebackref=true,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
+\documentclass[acmsmall,10pt,pagebackref=true,review,anonymous]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
 %\documentclass[pagebackref=true,acmsmall,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
 %% For double-blind review submission, w/ CCS and ACM Reference
 %\documentclass[acmsmall,review,anonymous]{acmart}\settopmatter{printfolios=true}
@@ -56,7 +56,7 @@
 \usemintedstyle{manni}
 
 \newif\ifANONYMOUS
-\ANONYMOUSfalse
+\ANONYMOUStrue
 
 \newif\ifCOMMENTS
 \COMMENTStrue
diff --git a/related.tex b/related.tex
index 6e5dc2b..8bf6743 100644
--- a/related.tex
+++ b/related.tex
@@ -48,7 +48,9 @@ Most practical HLS tools~\citep{canis11_legup,xilinx20_vivad_high_synth,intel20_
 
 Ongoing work in translation validation~\citep{pnueli98_trans} seeks to prove equivalence between the hardware generated by an HLS tool and the original behavioural description in C.  An example of a tool that implements this is Mentor's Catapult~\citep{mentor20_catap_high_level_synth}, which tries to match the states in the 3AC description to states in the original C code after an unverified translation.  Using translation validation is quite effective for verifying complex optimisations such as scheduling~\citep{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth} or code motion~\citep{banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}, but the validation has to be run every time the HLS is performed.  In addition to that, the proofs are often not mechanised or directly related to the actual implementation, meaning the verifying algorithm might be wrong and hence could give false positives or false negatives.
 
-Finally, there are a few relevant mechanically verified tools.  First, K\^{o}ika is a formally verified translation from a core fragment of BlueSpec into a circuit representation which can then be printed as a Verilog design.  This is a translation from a high-level hardware description language into an equivalent circuit representation, so is a different approach to HLS.  \citet{loow19_proof_trans_veril_devel_hol} used a verified translation from HOL4 code describing state transitions into Verilog to design a verified processor~\citep{loow19_verif_compil_verif_proces}.  Their approach translated a shallow embedding in HOL4 into a deep embedding of Verilog.  Perna et al.~\citep{perna12_mechan_wire_wise_verif_handel_c_synth,perna11_correc_hardw_synth} designed a formally verified translation from a deep embedding of Handel-C~\citep{aubury1996handel}, which is translated to a deep embedding of a circuit.  Finally, Ellis~\citep{ellis08} used Isabelle to implement and reason about intermediate languages for software/hardware compilation, where parts could be implemented in hardware and the correctness could still be shown.
+Finally, there are a few relevant mechanically verified tools.  First, K\^{o}ika is a formally verified translation from a core fragment of BlueSpec into a circuit representation which can then be printed as a Verilog design.  This is a translation from a high-level hardware description language into an equivalent circuit representation, so is a different approach to HLS.  \citet{loow19_proof_trans_veril_devel_hol} used a verified translation from HOL4 code describing state transitions into Verilog to design a verified processor~\citep{loow19_verif_compil_verif_proces}. \JW{That sentence is a bit confusing because it's not clear why Loow is cited twice.} Their approach translated a shallow embedding in HOL4 into a deep embedding of Verilog.
+\citet{perna12_mechan_wire_wise_verif_handel_c_synth,perna11_correc_hardw_synth} designed a formally verified translation from a deep embedding of Handel-C~\citep{aubury1996handel}, which is translated to a deep embedding of a circuit.
+Finally, \citet{ellis08} used Isabelle to implement and reason about intermediate languages for software/hardware compilation, where parts could be implemented in hardware and the correctness could still be shown.
 
 %%% Local Variables:
 %%% mode: latex