Update on Overleaf.

1 files changed, 6 insertions, 7 deletions

diff --git a/introduction.tex b/introduction.tex
index 656d17c..865dfd1 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -8,11 +8,10 @@
 
 \paragraph{Can you trust your high-level synthesis tool?}
 
-As latency, throughput and energy efficiency become increasingly important, custom hardware accelerators are being designed for numerous applications. 
+As latency, throughput and energy efficiency become increasingly important, custom hardware accelerators are being designed for numerous applications~\cite{??}. 
 Alas, designing these accelerators can be a tedious and error-prone process using a hardware description language (HDL) such as Verilog.
 An attractive alternative is high-level synthesis (HLS), in which hardware designs are automatically compiled from software written in a language like C. 
-Modern HLS tools such as \legup{}~\cite{canis11_legup}, Vivado HLS~\cite{xilinx20_vivad_high_synth}, Intel i++~\cite{intel_hls}, and Bambu HLS~\cite{bambu_hls} promise designs with comparable performance and energy-efficiency to those manually coded in HDL~\cite{homsirikamol+14, silexicahlshdl, 7818341}, while offering the convenient abstractions and rich ecosystem of software development.
-
+Modern HLS tools such as \legup{}~\cite{canis11_legup}, Vivado HLS~\cite{xilinx20_vivad_high_synth}, Intel i++~\cite{intel_hls}, and Bambu HLS~\cite{bambu_hls} promise designs with comparable performance and energy-efficiency to hand-written HDL designs~\cite{homsirikamol+14, silexicahlshdl, 7818341}, while offering the convenient abstractions and rich ecosystems of software development.
 But existing HLS tools cannot always guarantee that the hardware designs they produce are equivalent to the software they were given, and this undermines any reasoning conducted at the software level. 
 
 Indeed, there are reasons to doubt that HLS tools actually \emph{do} always preserve equivalence. 
@@ -34,15 +33,15 @@ For example, the translation validation for Catapult C~\cite{mentor20_catap_high
 Our position is that none of the above workarounds are necessary if the HLS tool can simply be trusted to work correctly.
 
 \paragraph{Our solution}
-We have written a new HLS tool in the Coq theorem prover~\cite{bertot04_inter_theor_provin_progr_devel} and proven that it any output it produces always has the same behaviour as its input. Our tool, which is called \vericert{},\ifANONYMOUS\footnote{Tool name has been changed for blind review.}\fi{} is automatically extracted to an OCaml program from Coq, which ensures that the object of the proof is the same as the implementation of the tool. \vericert{} is built by extending the \compcert{} verified C compiler~\cite{leroy09_formal_verif_realis_compil} with a new hardware-specific intermediate language and a Verilog back end. It supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables.
+We design a new HLS tool in the Coq theorem prover~\cite{bertot04_inter_theor_provin_progr_devel} and prove that it any output it produces always has the same behaviour as its input. Our tool, which is called \vericert{},\ifANONYMOUS\footnote{Tool name has been changed for blind review.}\fi{} is automatically extracted to an OCaml program from Coq, which ensures that the object of the proof is the same as the implementation of the tool. \vericert{} is built by extending the \compcert{} verified C compiler~\cite{leroy09_formal_verif_realis_compil} with a new hardware-specific intermediate language and a Verilog back end. It supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables.
 
 \paragraph{Contributions and Outline}
 The contributions of this paper are as follows:
 
 \begin{itemize}
-  \item We present \vericert{}, the first mechanically verified HLS tool that compiles C to Verilog. The design of \vericert{} is described in Section~\ref{sec:design}.
-  \item We prove \vericert{} correct w.r.t. an existing semantics for Verilog due to \citet{loow19_proof_trans_veril_devel_hol}. We describe in Section~\ref{sec:verilog} how we lightly extended this semantics to make it suitable as an HLS target. Section~\ref{sec:proof} describes the proof itself.
-  \item We have conducted a performance comparison between \vericert{} and a widely-used (unverified) HLS tool called \legup{}~\cite{canis11_legup} using the PolyBench benchmarks~\cite{polybench}. As described in Section~\ref{sec:evaluation}, \vericert{} generates hardware that is about 9x slower and 21x less area-efficient than that generated by \legup{}. We expect that these numbers will improve once we have extended \vericert{} with such optimisations as loop pipelining and scheduling.
+  \item We present \vericert{}, the first mechanically verified HLS tool that compiles C to Verilog. In Section~\ref{sec:design}, we describe the design of \vericert{}.
+  \item We prove \vericert{} correct w.r.t. an existing semantics for Verilog due to \citet{loow19_proof_trans_veril_devel_hol}. In Section~\ref{sec:verilog}, we describe how we lightly extended this semantics to make it suitable as an HLS target. Then, in  Section~\ref{sec:proof}, we describe the proof.
+  \item We evaluate \vericert{} on the Polybench/C benchmark suite~\cite{polybench}, and compare the performance of our generated hardware against and the well-known but  unverified \legup{} HLS tool~\cite{canis11_legup}. In Section~\ref{sec:evaluation}, we show that \vericert{}-generated Polybench hardware is 10x slower and 21x larger than, HLS-optimised but unverified, \legup{} hardware. We intend to bridge this performance gap in the future by introducing HLS optimisations of our own, such as scheduling and memory analysis.
 \end{itemize}
 
 \vericert{} is fully open source and available online.