Update on Overleaf.

3 files changed, 3 insertions, 3 deletions

diff --git a/algorithm.tex b/algorithm.tex
index 5ed47ad..f0c8ca2 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -288,7 +288,7 @@ However, the memory model that \compcert{} uses for its intermediate languages i
 
 % Mention that this optimisation is not performed sometimes (clang -03).
 
-Many of the \compcert{} instructions map well to hardware, but \texttt{Oshrximm} is expensive if implemented na\"ively. The problem is that in \compcert{} it is specified as a signed division:
+Many of the \compcert{} instructions map well to hardware, but \texttt{Oshrximm} (efficient signed division by a power of two using a logical shift) is expensive if implemented na\"ively. The problem is that in \compcert{} it is specified as a signed division:
 \begin{equation*}
   \texttt{Oshrximm } x\ y = \text{round\_towards\_zero}\left(\frac{x}{2^{y}}\right)
 \end{equation*}
diff --git a/conclusion.tex b/conclusion.tex
index 9a4bcfa..8ac9561 100644
--- a/conclusion.tex
+++ b/conclusion.tex
@@ -17,7 +17,7 @@ Beyond this, we plan to implement scheduling and loop pipelining, since this all
 Other optimisations include resource sharing to reduce the circuit area, and using tailored hardware operators that use hard IP blocks on chip and can be pipelined. 
 % this could include multi-cycle operations and pipelining optimisations so that division and multiplication operators also become more efficient.
 
-Finally, it's worth considering how trustworthy \vericert{} is compared to other HLS tools. The guarantee of full functional equivalence between input and output that $\vericert$ provides is a strong one, the semantics for the source and target languages are both well-established, and Coq is a mature and thoroughly tested system. However, \vericert{} cannot guarantee to provide an output for every valid input -- for instance, as remarked in Section~\ref{sec:proof:htl_verilog}, \vericert{} will error out if given a program with more than about four million instructions! -- but our evaluation indicates that it does not seem to error out too frequently. And of course, \vericert{} cannot guarantee that the final hardware produced will be correct, because the Verilog it generates must pass through a series of unverified tools along the way. This concern may be allayed in the future by ongoing work we are aware of to produce a verified hardware synthesis tool.
+Finally, it's worth considering how trustworthy \vericert{} is compared to other HLS tools. The guarantee of full functional equivalence between input and output that $\vericert$ provides is a strong one, the semantics for the source and target languages are both well-established, and Coq is a mature and thoroughly tested system. However, \vericert{} cannot guarantee to provide an output for every valid input -- for instance, as remarked in Section~\ref{sec:proof:htl_verilog}, \vericert{} will error out if given a program with more than about four million instructions! -- but our evaluation indicates that it does not seem to error out too frequently. And of course, \vericert{} cannot guarantee that the final hardware produced will be correct, because the Verilog it generates must pass through a series of unverified tools along the way. This concern may be allayed in the future by ongoing work we are aware of to produce a verified hardware synthesis tool. \JW{Is this tool citable yet?}
 
 
 %%% Local Variables:
diff --git a/related.tex b/related.tex
index 584653a..6e5dc2b 100644
--- a/related.tex
+++ b/related.tex
@@ -23,7 +23,7 @@
     \draw[myoutline] (0,0) ellipse (3 and 1.0);
 
     \node[align=center] at (0,2.8) {Standard HLS tools \\ \footnotesize\cite{canis11_legup,intel20_sdk_openc_applic} \\ \footnotesize\cite{nigam20_predic_accel_desig_time_sensit_affin_types,xilinx20_vivad_high_synth}};
-    \node[align=center] at (0,1.5) {Translation validation approaches \\ \footnotesize\cite{mentor20_catap_high_level_synth,kundu08_valid_high_level_synth,clarke03_behav_c_veril}};
+    \node[align=center] at (0.15,1.5) {Translation validation approaches \\ \footnotesize\cite{mentor20_catap_high_level_synth,kundu08_valid_high_level_synth,clarke03_behav_c_veril}};
     \node at (0,0.5) {\bf \vericert{}};
     \node[align=left] at (-1.8,0.0) {\footnotesize K\^oika \cite{bourgeat20_essen_blues}};
     \node[align=left] at (-1.8,0.32) { \footnotesize\citet{loow19_verif_compil_verif_proces}};