Add John's notes to abstract

1 files changed, 2 insertions, 5 deletions

diff --git a/main.tex b/main.tex
index a1a8355..0fc1eea 100644
--- a/main.tex
+++ b/main.tex
@@ -132,12 +132,9 @@
 \email{j.wickerson@imperial.ac.uk}
 
 \begin{abstract}
-  % \JW{This sentence is slightly confused because it’s not really ‘HLS’ that benefits, it’s the HLS user who benefits.}
-  % \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}
-  % \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.
+  High-level synthesis (HLS), which refers to the automatic compilation of software into hardware, is rapidly gaining popularity.  In a world increasingly reliant on application-specific hardware accelerators, HLS promises hardware designs of comparable performance and energy efficiency to those coded by hand in a hardware description language like Verilog, while maintaining the convenience and the rich ecosystem of software development.  However, current HLS tools cannot always guarantee that the hardware designs they produce are equivalent to the software they were given, thus undermining any reasoning conducted at the software level.  Worse, there is mounting evidence that existing HLS tools are actually quite unreliable, sometimes generating wrong hardware or crashing when given valid 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.
+  To address this problem, we present the first HLS tool that is mechanically verified to preserve the behaviour of its input software.  Our tool, called \vericert{}, extends the \compcert{} verified C compiler with a new hardware-specific intermediate language and a Verilog back end, and has been proven correct in Coq.  \vericert{} supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables.  An evaluation on all suitable PolyBench benchmarks indicates that it generates hardware with area and cycle counts around a magnitude larger than an existing, unverified HLS tool.
 \end{abstract}
 
 %% 2012 ACM Computing Classification System (CSS) concepts