Add section to algorithm

1 files changed, 5 insertions, 1 deletions

diff --git a/main.tex b/main.tex
index 6ddfb15..a7e7fb5 100644
--- a/main.tex
+++ b/main.tex
@@ -142,10 +142,14 @@
 }
 \email{j.wickerson@imperial.ac.uk}
 
+% High-level synthesis (HLS) refers to the automatic compilation of software into hardware. In a world increasingly reliant on application-specific hardware accelerators, HLS allows developers to enjoy the high-level abstractions and mature tooling associated with software development, while still benefitting from the performance and energy-efficiency of custom hardware. However, its adoption in safety-critical contexts is limited because no existing HLS tool guarantees that the output hardware is behaviourally equivalent to the input software. Indeed, there is empirical evidence that existing HLS tools, being complex pieces of software that implement delicate algorithms, are quite buggy. This undermines any assurance provided by software-level analysis.
+
+% Aiming to rectify that shortcoming, we present the first HLS tool that is mechanically verified to be semantics-preserving. Our tool, called CoqUp, is realised as an extension to the CompCert verified C compiler. It consists of a new hardware-oriented intermediate language and a new Verilog-producing back-end, all proven correct in Coq. CoqUp supports the full C language as input, except recursion and non-integer datatypes. An evaluation on the standard CHStone benchmark indicates that CoqUp generates hardware that is slower than, but has a comparable area to, that generated by two existing (unverified) HLS tools.
+
 
 %% Abstract
 \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 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.
+  High-level synthesis (HLS) is the process of automatically compiling software into hardware.  HLS is becoming increasingly popular, as application-specific hardware accelerators become more important.  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}