Update on Overleaf.

1 files changed, 4 insertions, 5 deletions

diff --git a/introduction.tex b/introduction.tex
index 39da7ff..59e0fce 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -6,7 +6,7 @@
 
 %\NR{I couldn't have subsections in comments so I have appended my writing to the bottom of this file.}\YH{The original intro is in the archive, we can maybe merge them in the future a bit.}
 
-\subsection{Can you trust your high-level synthesis tool?}
+\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. 
 Alas, designing these accelerators can be a tedious and error-prone process using a hardware description language (HDL) such as Verilog.
@@ -23,7 +23,7 @@ For instance, Vivado HLS has been shown to apply pipelining optimisations incorr
 Meanwhile, \citet{lidbury15_many_core_compil_fuzzin} had to abandon their attempt to fuzz-test Altera's (now Intel's) OpenCL compiler since it ``either crashed or emitted an internal compiler error'' on so many of their test inputs.  
 And more recently, Du et al.~\cite{du+20} fuzz-tested three commercial HLS tools using Csmith~\cite{yang11_findin_under_bugs_c_compil}, and despite restricting the generated programs to the C fragment explicitly supported by all the tools, they still found that on average 2.5\% of test cases generated a design that did not match the behaviour of the input.  
 
-\subsection{Existing workarounds}
+\paragraph{Existing workarounds}
 
 Aware of the reliability shortcomings of HLS tools, hardware designers routinely check the generated hardware for functional correctness. This is commonly done by simulating the design against a large test-bench; however, the guarantees are only as good as the test-bench, meaning that if all the inputs were not covered exhaustively, there is a risk that bugs remain. 
 
@@ -33,11 +33,10 @@ 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.
 
-\subsection{Our solution}
+\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.
 
-\subsection{Contributions and Outline}
-
+\paragraph{Contributions and Outline}
 The contributions of this paper are as follows:
 
 \begin{itemize}