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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
\environment fonts_env
\environment lsr_env
\startcomponent introduction
\chapter{Introduction}
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 to design hardware that has quite regular control-flow and is
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.
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
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.
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.
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.
\desc{\in{Chapter}[sec:schedule]} describes the current implementation timeline.
\startmode[chapter]
\section{Bibliography}
\placelistofpublications
\stopmode
\stopcomponent
|
