1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
\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.
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
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
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)}][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
trusted to work correctly.
\stopcomponent
|
