From aeb7b75278c6affa9499b03f592f6869ae2ca19f Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 15 Apr 2022 22:33:49 +0100
Subject: Add text to lsr

---
 chapters/introduction.tex | 50 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

(limited to 'chapters/introduction.tex')

diff --git a/chapters/introduction.tex b/chapters/introduction.tex
index 623b56a..d96ff55 100644
--- a/chapters/introduction.tex
+++ b/chapters/introduction.tex
@@ -2,4 +2,54 @@
 
 \chapter{Introduction}
 
+\startthesis
+An optimising high-level synthesis 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.
+
+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{\goto{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{\goto{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 \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
+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.} 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 against a large test-bench. But unless the test-bench covers all
+inputs exhaustively -- which is often infeasible -- there is a risk that bugs remain.
+
+One alternative is to use \emph{translation validation}~\cite{pnueli98_trans} to prove equivalence
+between the input program and the output design. Translation validation has been successfully
+applied to several HLS
+optimisations~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth,banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}.
+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
+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.
+
 \stopcomponent
-- 
cgit 

