Finish most of abstract draft

1 files changed, 1 insertions, 1 deletions

diff --git a/main.tex b/main.tex
index f701d8e..74eeb57 100644
--- a/main.tex
+++ b/main.tex
@@ -153,7 +153,7 @@
 %% Note: \begin{abstract}...\end{abstract} environment must come
 %% before \maketitle command
 \begin{abstract}
-  High-level synthesis (HLS) is the process of converting an algorithmic description, often written in C, to specialised hardware with the same behaviour, expressed in a hardware description language.  HLS is becoming increasingly popular, as it allows for faster prototyping as well as simpler behavioural verification, as all the software tools can be used.  The HLS process has to be trusted though to be sure that .  C constructs are also often not supported in various combinations, which make existing tools quite brittle.  Our work focuses on formally verifying the high-level synthesis process from C to Verilog by proving that the behaviour remains the same according to the C and Verilog semantics.
+  High-level synthesis (HLS) is the process of converting an algorithmic description, often written in C, to specialised hardware with the same behaviour, expressed in a hardware description language.  HLS is becoming increasingly popular, as it allows for faster prototyping of hardware designs, as well as simpler behavioural verification using all the tools available in the software ecosystem.  However, for software verification to be useful, the HLS process has to be trusted to be sure that the properties proven in software also apply to the hardware.  Current HLS tools do not provide this guarantee, meaning verification is often performed again at the hardware level, which is inefficient.  Our work focuses on formally verifying the high-level synthesis process from C to Verilog by proving that the behaviour remains the same according to the C and Verilog semantics.  We use the CompCert frontend to process Clight and add a Verilog backend to get a fully verified HLS tool.
 \end{abstract}