From 2474cfa79cbb9c3afd0ca96a3ad1e0c998bf062b Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 17 Apr 2022 11:22:41 +0100
Subject: Adding more files

---
 chapters/introduction.tex | 35 +++++++++++++++++++++--------------
 1 file changed, 21 insertions(+), 14 deletions(-)

(limited to 'chapters/introduction.tex')

diff --git a/chapters/introduction.tex b/chapters/introduction.tex
index d96ff55..8588d3f 100644
--- a/chapters/introduction.tex
+++ b/chapters/introduction.tex
@@ -3,21 +3,28 @@
 \chapter{Introduction}
 
 \startthesis
-An optimising high-level synthesis tool can be proven correct using an interactive theorem prover
-while also remaining practical.
+  An optimising \infull{HLS} tool can be proven correct using an interactive theorem prover while
+  also remaining practical.
 \stopthesis
 
 \noindent 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.  An attractive alternative is \emph{high-level synthesis} (HLS), in which hardware
-designs are automatically compiled from software written in a high-level 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 hand-written in an HDL~\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.
+such as Verilog.  An attractive alternative is \emph{\infull{HLS}} (\HLS), in which hardware designs
+are automatically compiled from software written in a high-level language like C.  Modern \HLS\
+tools such as LegUp~\cite{canis11_legup}, Vivado HLS~\cite{xilinx20_vivad_high_synth}, Intel
+i++~\cite{intel20_high_synth_compil}, and Bambu HLS~\cite{pilato13_bambu} promise designs with
+comparable performance and energy-efficiency to those hand-written in an
+HDL~\cite{homsirikamol14_can, gauthier20_high_level_synth, pelcat16_desig_hdl}, while offering the
+convenient abstractions and rich ecosystems of software development.
+
+There are two main use-cases of \HLS.  Firstly, it is a very convenient tool to use for prototyping
+designs, as this means that the software model can be reused for the initial design of the hardware.
+Secondly, \HLS\ is also often used design hardware that has quite regular control-flow and is
+compute intensive, one example being DSP hardware design.
+
+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.
 For instance, Vivado HLS has been shown to apply pipelining optimisations
@@ -27,7 +34,7 @@ supports.\footnote{\goto{bit.ly/vivado-hls-pointer-bug}[url(https://bit.ly/vivad
 Meanwhile, \cite{lidbury15_many_core_compil_fuzzin} had to abandon their attempt to fuzz-test
 Altera's (now Intel's) OpenCL compiler since it \quotation{either crashed or emitted an internal
   compiler error} on so many of their test inputs.  More recently,
-\cite{herklotz21_empir_study_reliab_high_level_synth_tools} fuzz-tested three commercial HLS tools
+\citef{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.
@@ -44,9 +51,9 @@ 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[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
+`adjustments'~\cite[alternative=authoryear,right={, p.~3)}][chauhan20_formal_ensur_equiv_c_rtl] 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[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
-- 
cgit 

