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