diff options
Diffstat (limited to 'chapters/introduction.tex')
| -rw-r--r-- | chapters/introduction.tex | 50 |
1 files changed, 50 insertions, 0 deletions
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 |