Merge branch 'master' of https://git.overleaf.com/5ed78033b633200001e693d0

3 files changed, 6 insertions, 12 deletions

diff --git a/algorithm.tex b/algorithm.tex
index abec2bb..a4941d5 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -67,7 +67,7 @@ The .NET framework has been used as a basis for other HLS tools, such as Kiwi~\c
     \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}%}
-  \caption{\vericert{} as a Verilog back end to \compcert{}.}%
+  \caption{\vericert{} as a Verilog back end to \compcert{}. \JW{The placement of the `RAM insertion' label suggests that it's not part of Vericert. Maybe move it inside the orange rectangle?}}%
   \label{fig:rtlbranch}
 \end{figure}
 
@@ -88,7 +88,7 @@ It has an unlimited number of pseudo-registers, and is represented as a control
 This section will introduce Verilog for readers who may not be familiar with the language, concentrating on the features that are used in the output of \vericert{}.  Verilog is a hardware description language (HDL) and is used to design hardware ranging from complete CPUs that are eventually produced as an integrated circuit, to small application-specific accelerators that are placed on an FPGA.  Verilog is a popular language because it allows for fine-grained control over the hardware, and also provides high-level constructs to simplify the development.
 
 Verilog behaves quite differently to standard software programming languages due to it having to express the parallel nature of hardware.  The basic construct to achieve this is the always-block, which is a collection of assignments that are executed every time some event occurs.  In the case of \vericert{}, this event is either a positive (rising) or a negative (falling) clock edge.  All always-blocks triggering on the same event are executed in parallel. Always-blocks can also express control-flow using if-statements and case-statements.
-\NR{Might be useful to talk about registers must be updated only within an always-block.} \JW{That's important for Verilog programming in general, but is it necessary for understanding this paper?}\YH{Yeah, I don't think it is too important for this section.}
+%\NR{Might be useful to talk about registers must be updated only within an always-block.} \JW{That's important for Verilog programming in general, but is it necessary for understanding this paper?}\YH{Yeah, I don't think it is too important for this section.}
 
 \begin{figure}
   \centering
diff --git a/introduction.tex b/introduction.tex
index abf6271..1871a26 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -51,15 +51,9 @@ The contributions of this paper are as follows:
   \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{}. This performance gap can be largely attributed to \vericert{}'s current lack of support for instruction-level parallelism and the absence of an efficient, pipelined division operator. We intend to close this gap in the future by introducing (and verifying) HLS optimisations of our own, such as scheduling and memory analysis.  This section also reports on our campaign to fuzz-test \vericert{} using over a hundred thousand random C programs generated by Csmith~\cite{yang11_findin_under_bugs_c_compil} in order to confirm that its correctness theorem is watertight. %\NR{Question rather than comment: Will there be verification issues to add support for hard IPs like division blocks?}\YH{Not really any issues, just many different levels of reliability.  You don't have to prove IP correct, but theoretically could.}
 \end{itemize}
 %\JW{This sentence seems pretty good to me; is it up-to-date with the latest `challenges' you've faced?}
-\vericert{} is fully open source and available online~\cite{yann_herklotz_2021_5093839}.
-
-\begin{center}
-\ifANONYMOUS
-[GitHub link removed for blind review]
-\else 
-\url{https://github.com/ymherklotz/vericert}
-\fi
-\end{center}
+
+\paragraph{Companion material}
+\vericert{} is fully open source and available on GitHub at \url{https://github.com/ymherklotz/vericert}. A snapshot of the \vericert{} development is also available in a Zenodo repository~\cite{yann_herklotz_2021_5093839}, which also contains \JW{fill this in}.
 
 
 %%% Local Variables:
diff --git a/main.tex b/main.tex
index 57bca7c..9330e10 100644
--- a/main.tex
+++ b/main.tex
@@ -82,7 +82,7 @@
 \ANONYMOUSfalse
 
 \newif\ifCOMMENTS
-\COMMENTSfalse
+\COMMENTStrue
 \newcommand{\Comment}[3]{\ifCOMMENTS\textcolor{#1}{{\bf [\![#2:} #3{\bf ]\!]}}\fi}
 \newcommand\JW[1]{\Comment{red!75!black}{JW}{#1}}
 \newcommand\YH[1]{\Comment{green!50!blue}{YH}{#1}}