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

1 files changed, 2 insertions, 2 deletions

diff --git a/main.tex b/main.tex
index 5dd538f..d5ac1e5 100644
--- a/main.tex
+++ b/main.tex
@@ -125,9 +125,9 @@
 \email{j.wickerson@imperial.ac.uk}
 
 \begin{abstract}
-  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 benefitting from the rich software ecosystem to verify the functionality of their designs.  However, adoption of HLS in safety-critical applications is still limited, because current tools cannot 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 even evidence that HLS tools tend to be quite unreliable instead, either generating wrong hardware or sometimes not generating any hardware at all.
+  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 benefitting from \JW{This sentence is slightly confused because it's not really `HLS' that benefits, it's the HLS user who benefits.} the rich software ecosystem to verify the functionality of their designs.  However, adoption of HLS in safety-critical applications is still limited, because current tools cannot verify \JW{`cannot verify' is a dubious claim -- I guess something like SLEC can technically verify that the hardware is correct, but it's a big faff to use it} that the hardware implements the same behaviour as the software it was generated from, eliminating the benefits that software verification may provide.  There is even evidence that HLS tools tend to be quite unreliable instead, either generating wrong hardware or sometimes not generating any hardware at all. \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.}
 
-  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.
+  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 \JW{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.}
 \end{abstract}
 
 %% 2012 ACM Computing Classification System (CSS) concepts