Add comments by John

1 files changed, 5 insertions, 2 deletions

diff --git a/main.tex b/main.tex
index d5ac1e5..cdadd2c 100644
--- a/main.tex
+++ b/main.tex
@@ -125,9 +125,12 @@
 \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 \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.}
+  % \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.
 
-  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.}
+  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.}
 \end{abstract}
 
 %% 2012 ACM Computing Classification System (CSS) concepts