Update on Overleaf.

3 files changed, 6 insertions, 6 deletions

diff --git a/algorithm.tex b/algorithm.tex
index 8a619e4..c81cbfa 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -113,7 +113,7 @@ module main(reset, clk, finish, return_val);
   reg [0:0] en = 0, u_en = 0;
   reg [31:0] state = 0, reg_2 = 0, reg_4 = 0, d_out = 0, reg_1 = 0;
   reg [31:0] stack [1:0];
-  // RAM Template
+  // RAM template
   always @(negedge clk)
     if ({u_en != en}) begin
       if (wr_en) stack[addr] <= d_in;
@@ -149,7 +149,7 @@ module main(reset, clk, finish, return_val);
          endcase
 endmodule
 \end{minted}
-\caption{Verilog produced by \vericert{}. It demonstrates the instantiation of the RAM, the data-path and finally the control logic.}\label{fig:accumulator_v}
+\caption{Verilog produced by \vericert{}. It demonstrates the instantiation of the RAM (lines 9--15), the data-path (lines 16--32) and the control logic (lines 33--42).}\label{fig:accumulator_v}
 \end{subfigure}
   \caption{Translating a simple program from C to Verilog.}\label{fig:accumulator_c_rtl}
 \end{figure}
diff --git a/evaluation.tex b/evaluation.tex
index 93f89d6..ac67ec7 100644
--- a/evaluation.tex
+++ b/evaluation.tex
@@ -11,7 +11,7 @@ Our evaluation is designed to answer the following three research questions.
 \subsection{Experimental Setup}
 \label{sec:evaluation:setup}
 
-\paragraph{Choice of HLS tool for comparison.} We compare \vericert{} against \legup{} 5.1 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 HLS tool for comparison.} We compare \vericert{} against \legup{} 5.1 \JW{4.0 now, right?} 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 and preparation of benchmarks.} We evaluate \vericert{} using the \polybench{} benchmark suite (version 4.2.1)~\cite{polybench}, which consists of a collection of 30 numerical kernels. \polybench{} is popular in the HLS context~\cite{choi+18,poly_hls_pouchet2013polyhedral,poly_hls_zhao2017,poly_hls_zuo2013}, since it has affine loop bounds, making it attractive for streaming computation on FPGA architectures.
 We were able to use 27 of the 30 programs; three had to be discarded (\texttt{correlation},~\texttt{gramschmidt} and~\texttt{deriche}) because they involve square roots, requiring floats, which we do not support. 
@@ -85,7 +85,7 @@ We configured \polybench{}'s parameters so that only integer types are used, sin
       \legend{\vericert{},\legup{} w/o opt+chain,\legup{} w/o opt};
     \end{groupplot}
   \end{tikzpicture}
-  \caption{\polybench{} with division enabled.}
+  \caption{\polybench{} with division enabled. \JW{More descriptive caption needed (and next figure too)}}
 \end{figure}
 
 \pgfplotstableread[col sep=comma]{results/rel-time-nodiv.csv}{\nodivtimingtable}
diff --git a/proof.tex b/proof.tex
index a24aac8..aaac99c 100644
--- a/proof.tex
+++ b/proof.tex
@@ -194,9 +194,9 @@ The final lemma we need is that the Verilog we generate is deterministic. This r
   \label{tab:proof_statistics}
 \end{table*}
 
-The lines of code for the implementation and proof of \vericert{} can be found in Table~\ref{tab:proof_statistics}.  Overall, it took about 1.5 person-year to build \vericert{} -- about two person-months on implementation and ten person-months on proofs. The largest proof is the correctness proof for the HTL generation, which required equivalence proofs between all integer operations supported by \compcert{} and those supported in hardware.  From the 3069 lines of proof code in the HTL generation, 1189 are for the correctness proof of just the load and store instructions.  These were tedious to prove correct because of the substantial difference between the memory models used, and the need to prove properties such as stores outside of the allocated memory being undefined, so that a finite array could be used. In addition to that, since pointers in HTL and Verilog are represented as integers, whereas there is a separate pointer value in the \compcert{} semantics, it was painful to reason about them and many new theorems had to be proven about integers and pointers in \vericert{}.  In addition to that, the second largest proof of the correct RAM generation includes many proofs about the extensional equality of array operations, such as merging arrays with different assignments.  As the negative edge implies two merges take place every clock cycle, the proofs about the equality of the arrays becomes more tedious as well.
+The lines of code for the implementation and proof of \vericert{} can be found in Table~\ref{tab:proof_statistics}.  Overall, it took about 1.5 person-years to build \vericert{} -- about two person-months on implementation and ten person-months on proofs. \JW{That doesn't add up to 18 months :)} The largest proof is the correctness proof for the HTL generation, which required equivalence proofs between all integer operations supported by \compcert{} and those supported in hardware.  From the 3069 lines of proof code in the HTL generation, 1189 are for the correctness proof of just the load and store instructions.  These were tedious to prove correct because of the substantial difference between the memory models used, and the need to prove properties such as stores outside of the allocated memory being undefined, so that a finite array could be used. In addition to that, since pointers in HTL and Verilog are represented as integers, whereas there is a separate pointer value in the \compcert{} semantics, it was painful to reason about them and many new theorems had to be proven about integers and pointers in \vericert{}.  In addition to that, the second largest proof of the correct RAM generation includes many proofs about the extensional equality of array operations, such as merging arrays with different assignments.  As the negative edge implies two merges take place every clock cycle, the proofs about the equality of the arrays becomes more tedious as well.
 
-Looking at the trusted base of \vericert{}, the Verilog semantics are 431.  This, together with the Clight semantics from \compcert{}, are the only parts of the compiler that need to be trusted.  Compared to the 1721 lines of the implementation that are written in Coq, which are the verified parts of the synthesis tool, this is larger than the 431 lines of Verilog semantics specification, even if the Clight semantics are added.  In addition to that, reading semantics specifications is simpler than trying to understand algorithms, meaning the trusted base has been successfully reduced.
+Looking at the trusted base of \vericert{}, the Verilog semantics are 431 \JW{units?}.  This, together with the Clight semantics from \compcert{}, are the only parts of the compiler that need to be trusted.  Compared to the 1721 lines of the implementation that are written in Coq, which are the verified parts of the synthesis tool, this is larger than the 431 lines of Verilog semantics specification, even if the Clight semantics are added.  In addition to that, reading semantics specifications is simpler than trying to understand algorithms, meaning the trusted base has been successfully reduced.
 
 %\JW{Can we include a comment about the size of the trusted base, in case we get that reviewer again?}