Update on Overleaf.

1 files changed, 6 insertions, 3 deletions

diff --git a/main.tex b/main.tex
index dbca92f..9ed50ec 100644
--- a/main.tex
+++ b/main.tex
@@ -40,6 +40,7 @@
 \usepackage{booktabs}
 \usepackage{mathpartir}
 \usepackage{pgfplots}
+\usepackage{soul}
 \usepackage{subcaption}
 \usepackage{tikz}
 \usepackage{minted}
@@ -54,6 +55,8 @@
 \newcommand\JP[1]{\Comment{blue!50!black}{JP}{#1}}
 \newcommand\NR[1]{\Comment{yellow!50!black}{NR}{#1}}
 
+\newcommand\JWcouldcut[1]{{\setstcolor{red!75!black}\st{#1}}}
+
 \definecolor{compcert}{HTML}{66c2a5}
 \definecolor{formalhls}{HTML}{fc8d62}
 \definecolor{keywordcolour}{HTML}{8f0075}
@@ -66,8 +69,8 @@
 \newcommand\yhfunction[1]{\texttt{\textcolor{functioncolour}{#1}}}
 \newcommand\yhconstant[1]{\texttt{\textcolor{constantcolour}{#1}}}
 
-\newcommand{\vericert}{Vericert}%
-\newcommand{\compcert}{CompCert}%
+\newcommand{\vericert}{Veri\-cert}%
+\newcommand{\compcert}{Comp\-Cert}%
 
 \begin{document}
 
@@ -133,7 +136,7 @@
   % \JW{‘Not generating hardware’ isn’t too bad, and indeed VeriCert is guilty of that too, when presented with C programs that contain features that it can’t yet handle. The real problem is the HLS tool crashing unceremoniously.}
   High-level synthesis (HLS) refers to automatically compiling software into hardware.  In a world increasingly reliant on application-specific hardware accelerators, HLS provides a higher-level of abstraction for hardware designers, while also allowing the designers to benefit from the rich software ecosystem to verify the functionality of their designs.  However, adoption of HLS in safety-critical applications is still limited, because it may be infeasible to verify that the hardware implements the same behaviour as the software it was generated from, eliminating the benefits that software verification may provide.  There is also evidence that HLS tools tend to be quite unreliable instead, either generating wrong hardware or sometimes crashing in unexpected ways for supported inputs.
 
-  We present the first mechanically verified HLS tool that preserves the behaviour of the software according to our semantics.  Our tool, called \vericert{}, extends the \compcert{} verified C compiler and consists of a new hardware-specific intermediate language and a Verilog back end, which has been proven correct in Coq.  \vericert{} supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables.  It has been evaluated on all suitable PolyBench benchmarks, which indicates that it generates hardware with area and cycle count around a magnitude larger than an existing, unverified HLS tool. \JW{Hopefully in due course we can nuance this a bit by adding in some figures relating to the unverified \vericert{} extensions.}\YH{This might be the case, but maybe we want to keep that for a completely new paper as discussed.}
+  We present the first mechanically verified HLS tool that preserves the behaviour of the software according to our semantics.  Our tool, called \vericert{}, extends the \compcert{} verified C compiler and consists of a new hardware-specific intermediate language and a Verilog back end, which has been proven correct in Coq.  \vericert{} supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables.  It has been evaluated on all suitable PolyBench benchmarks, which indicates that it generates hardware with area and cycle count around a magnitude larger than an existing, unverified HLS tool.
 \end{abstract}
 
 %% 2012 ACM Computing Classification System (CSS) concepts