Add

1 files changed, 35 insertions, 25 deletions

diff --git a/hls.tex b/hls.tex
index 4feaa14..734463c 100644
--- a/hls.tex
+++ b/hls.tex
@@ -1,10 +1,13 @@
-\chapter{Formal Verification of High-Level Synthesis}
+\startcomponent hls
+\product main
 
-\newcommand{\slowdownOrig}{27}
-\newcommand{\slowdownDiv}{2}
-\newcommand{\areaIncr}{1.1}
+\def\slowdownOrig{27}
+\def\slowdownDiv{2}
+\def\areaIncr{1.1}
 
-\paragraph{Can you trust your high-level synthesis tool?}
+\chapter{High-Level Synthesis}
+
+{\bf 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
@@ -20,18 +23,18 @@ the software they were given, and this undermines any reasoning conducted at the
 
 Indeed, there are reasons to doubt that HLS tools actually \emph{do} always preserve equivalence.
 For instance, Vivado HLS has been shown to apply pipelining optimisations
-incorrectly\footnote{\url{https://bit.ly/vivado-hls-pipeline-bug}} or to silently generate wrong
+incorrectly\footnote{\goto{https://bit.ly/vivado-hls-pipeline-bug}[url(https://bit.ly/vivado-hls-pipeline-bug)]} or to silently generate wrong
 code should the programmer stray outside the fragment of C that it
-supports.\footnote{\url{https://bit.ly/vivado-hls-pointer-bug}} Meanwhile,
-\citet{lidbury15_many_core_compil_fuzzin} had to abandon their attempt to fuzz-test Altera's (now
+supports.\footnote{\goto{https://bit.ly/vivado-hls-pointer-bug}[url(https://bit.ly/vivado-hls-pointer-bug)]} Meanwhile,
+\cite{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.  More recently,
-\citet{herklotz21_empir_study_reliab_high_level_synth_tools} fuzz-tested three commercial HLS tools
+\cite{herklotz21_empir_study_reliab_high_level_synth_tools} 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 were compiled to designs that behaved incorrectly.
 
-\paragraph{Existing workarounds}
+{\bf 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 generated design
@@ -45,40 +48,40 @@ optimisations~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synt
 Nevertheless, it is an expensive task, especially for large designs, and it must be repeated every
 time the compiler is invoked.  For example, the translation validation for Catapult
 C~\cite{mentor20_catap_high_level_synth} may require several rounds of expert
-`adjustments'~\cite[p.~3]{slec_whitepaper} to the input C program before validation succeeds. And
+`adjustments'~\cite[alternative=authoryear,right={, p.~3)}][slec_whitepaper] to the input C program before validation succeeds. And
 even when it succeeds, translation validation does not provide watertight guarantees unless the
 validator itself has been mechanically proven
-correct~\cite[e.g.][]{tristan08_formal_verif_trans_valid}, which has not been the case in HLS tools
+correct~\cite[tristan08_formal_verif_trans_valid], which has not been the case in HLS tools
 to date.
 
 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}
+{\bf Our solution}
 
 We have designed a new HLS tool in the Coq theorem prover and proved that any output design it
 produces always has the same behaviour as its input program. Our tool, called Vericert, 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
+compiler~\cite[leroy09_formal_verif_realis_compil] with a new hardware-specific intermediate
 language and a Verilog back end. It supports most C constructs, including integer operations,
 function calls (which are all inlined), local arrays, structs, unions, and general control-flow
 statements, but currently excludes support for case statements, function pointers, recursive
 function calls, non-32-bit integers, floats, and global variables.
 
-\paragraph{Contributions and Outline}
+{\bf Contributions and Outline}
 The contributions of this paper are as follows:
 
-\begin{itemize}
+\startitemize[]
   \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, including certain
         optimisations related to memory accesses and division.
   \item We state the correctness theorem of Vericert with respect to an existing semantics for
-        Verilog due to \citet{loow19_proof_trans_veril_devel_hol}. In Section~\ref{sec:verilog}, we
-        describe how we extended this semantics to make it suitable as an HLS target.  We also
-        describe how the Verilog semantics is integrated into CompCert's language execution model
-        and its framework for performing simulation proofs. A mapping of CompCert's infinite memory
-        model onto a finite Verilog array is also described.
+    Verilog due to \cite[authoryear][loow19_proof_trans_veril_devel_hol]. In
+    Section~\ref{sec:verilog}, we describe how we extended this semantics to make it suitable as an
+    HLS target.  We also describe how the Verilog semantics is integrated into CompCert's language
+    execution model and its framework for performing simulation proofs. A mapping of CompCert's
+    infinite memory model onto a finite Verilog array is also described.
   \item In Section~\ref{sec:proof}, we describe how we proved the correctness theorem. The proof
         follows standard CompCert techniques -- forward simulations, intermediate specifications,
         and determinism results -- but we encountered several challenges peculiar to our
@@ -100,9 +103,16 @@ The contributions of this paper are as follows:
         on our campaign to fuzz-test Vericert using over a hundred thousand random C programs
         generated by Csmith~\cite{yang11_findin_under_bugs_c_compil} in order to confirm that its
         correctness theorem is watertight.
-\end{itemize}
+\stopitemize
 
-\paragraph{Companion material}
+{\bf Companion material}
 Vericert is fully open source and available on GitHub at
-\url{https://github.com/ymherklotz/vericert}. A snapshot of the Vericert development is also
-available in a Zenodo repository~\cite{yann_herklotz_2021_5093839}.
+
+\startalignment[center]
+\goto{\hyphenatedurl{https://github.com/ymherklotz/vericert}}[url(https://github.com/ymherklotz/vericert)].
+\stopalignment
+
+A snapshot of the Vericert development is also available in a Zenodo
+repository~\cite{yann_herklotz_2021_5093839}.
+
+\stopcomponent