diff options
Diffstat (limited to 'chapters/introduction.tex')
| -rw-r--r-- | chapters/introduction.tex | 112 |
1 files changed, 81 insertions, 31 deletions
diff --git a/chapters/introduction.tex b/chapters/introduction.tex index 8588d3f..7ab9d47 100644 --- a/chapters/introduction.tex +++ b/chapters/introduction.tex @@ -1,52 +1,57 @@ +\environment fonts_env +\environment lsr_env + \startcomponent introduction \chapter{Introduction} -\startthesis - 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{\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. +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 \HDL\ such as Verilog. An attractive alternative is +\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. +compute intensive, one example being \DSP\ hardware design~\cite{coussy08_gaut}. Ideally, \HLS\ +should also be good for projects that require detailed functional verification, as manual \HDL\ +designs cannot often be fully verified because of their size. \HLS\ would move the functional +verification problem to a higher-level, allowing for a much deeper understanding about the +functional behaviour of the design. A recent survey by \cite[authoryear][lahti19_are_we_there_yet] +describes that verification is still a time-consuming part of the design process though, even with +the use of \HLS, however, that in general it still reduced the verification effort by half. Most +papers that were surveyed did not mention verification of designs though and it therefore still +remains an underexplored area in \HLS\ research. -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 +This is especially important when 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, -\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 +\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. -\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. +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 +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 @@ -54,9 +59,54 @@ C~\cite{mentor20_catap_high_level_synth} may require several rounds of expert `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. +correct~\cite[tristan08_formal_verif_trans_valid], which has not been the case in \HLS\ tools to +date. + +The main thesis of this dissertation is therefore the following. + +\startthesis + An optimising high-level synthesis tool can be proven correct using an interactive theorem prover + while also remaining practical. +\stopthesis + +Our position is that is that none of these workarounds are necessary if the \HLS\ tool can be +trusted, and is proven to produce correct designs. This dissertation will describe the +implementation of a mechanically verified \HLS\ tool called Vericert, including two critical \HLS\ +optimisations to make Vericert practical. Vericert is fully open source and available on GitHub at + +\blank[big] +\startalignment[center] + \goto{\hyphenatedurl{https://github.com/ymherklotz/vericert}}[url(https://github.com/ymherklotz/vericert)]. +\stopalignment +\blank[big] + +A snapshot of the Vericert development is also available in a Zenodo +repository~\citef{herklotz21_veric}. + +\section{Outline and Contributions} + +The dissertation is split into the following sections: + +\desc{\in{Chapter}[sec:background]} covers background information about high-level synthesis, static +scheduling, loop pipelining (modulo scheduling) and dynamic scheduling. + +\desc{\in{Chapter}[sec:hls]} describes the initial implementation of Vericert without +any optimisations. It describes the addition of a new intermediate language called HTL, providing a +state machine language which has a closer structure to the final hardware implementation, but does +not yet have to be proper Verilog syntax.\footnote{In fact, HTL implements a \FSMD\ to simplify the + state machine representation and the number of states.} This chapter also describes the Verilog +semantics that were chosen as a target. + +\desc{\in{Chapter}[sec:scheduling]} describes the implementation of static hyperblock scheduling, +making use of validation to prove it correct. + +\desc{\in{Chapter}[sec:pipelining]} describes the current plan to implement loop pipelining in +Vericert by also using a validator. + +\desc{\in{Chapter}[sec:dynamic]} describes a possible extension to Vericert by implementing dynamic +scheduling instead of the current static scheduling implementation. This relies on ongoing work in +a fork of CompCert which implements \SSA\ as an intermediate language. -Our position is that none of the above workarounds are necessary if the HLS tool can simply be -trusted to work correctly. +\desc{\in{Chapter}[sec:schedule]} describes the current implementation timeline. \stopcomponent |