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
|
\section{Introduction}
%% Motivation for why HLS might be needed
%\JW{A few high-level comments: \begin{enumerate} \item Create more tension from the start by making the reader doubt whether existing HLS tools are trustworthy. \item The intro currently draws quite a bit of motivation from Lidbury et al. 2015, but we should also now lean on our FPGA submission too. \item I wonder whether the paragraph `To mitigate the problems...' should be demoted to a `related work' discussion (perhaps as a subsection towards the end of the introduction). It outlines (and nicely dismisses) some existing attempts to tackle the problem, which is certainly useful motivation for your work, especially for readers already familiar with HLS, but I feel that it's not really on the critical path for understanding the paper.\end{enumerate}}
%\NR{I couldn't have subsections in comments so I have appended my writing to the bottom of this file.}\YH{The original intro is in the archive, we can maybe merge them in the future a bit.}
\subsection{Can you trust your high-level synthesis tool?}
As latency, throughput and energy efficiency become increasingly important, custom hardware accelerators are being designed for numerous applications~\cite{??}.
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 high-level synthesis (HLS), in which hardware designs are automatically compiled from software written in a language like C.
Modern HLS tools such as \legup{}~\cite{canis11_legup}, Vivado HLS~\cite{xilinx20_vivad_high_synth}, Intel i++~\cite{??}, and Bambu HLS~\cite{} can produce designs with comparable performance and energy-efficiency to those manually coded in HDL~\cite{bdti,autoesl}, while offering the convenient abstractions and rich ecosystem of software development.
But existing HLS tools cannot always guarantee that the hardware designs they produce are equivalent to the software they were given.
This undermines any reasoning conducted at the software level.
And there are reasons to doubt that HLS tools actually \emph{do} preserve equivalence. First, just like conventional compilers, HLS tools are large pieces of software that perform a series of complex analyses and transformations.
Second, unlike conventional compilers, HLS tools target HDL, which has superficial syntactic similarities to software languages but a subtly different semantics, making it easy to introduce behavioural mismatches between the output of the HLS tool and its input.
%Hence, the premise of this work is: Can we trust these compilers to translate high-level languages like C/C++ to HDL correctly?
\JW{These doubts have been shown to be justified by... / These doubts have been borne out by / corroborated... }
For instance, \citet{lidbury15_many_core_compil_fuzzin} had to abandon their attempt to fuzz-test Altera's (now Intel's) OpenCL compiler since it ``either crashed or emitted an internal compiler error'' on so many of their test inputs.
More recently, Du et al.~\cite{du+20} 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 generated a design that did not match the behaviour of the input.
%
Meanwhile, Xilinx's Vivado HLS has been shown to apply pipelining optimisations incorrectly\footnote{\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{\url{https://bit.ly/vivado-hls-pointer-bug}}.
\subsection{Existing verification workarounds}
It is rather difficult to exhaustively test a HLS tool to prove for the absence of bugs since these codebases are very large and often include custom passes and directives.
Hence, most existing work on verifying HLS tools focus on proving that HLS-generated hardware is equivalent to its software counterpart for all possible inputs of the program, or \emph{translation validation}~\cite{pnueli98_trans}.
Translation validation has been successfully applied to many 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}.
However, translation validation often suffers from one key problem: the validator itself might not have been mechanically proven to be correct and even it is proven there can be an interpretation gap between the mechanised proof and its implementation.
Furthermore, translation validation also has other practical problems: it needs to be invoked everytime a new program is compiled and it can also lead to exponential growth in state space.
For example, Catapult C's translation validation~\cite{mentor20_catap_high_level_synth} warns that it might require large number of iterations to perform validation.
\subsection{Our approach}
Proving the absence of bugs within HLS tools has always been a tricky and difficult process.
A radical solution is to write an HLS tool in a theorem prover such as Coq~\cite{bertot04_inter_theor_provin_progr_devel}, so that the translation algorithm can be proven correct in the theorem prover itself. The algorithm can then be extracted to executable code, which exhibits the same properties as the Coq code that was proven correct in the theorem prover. In this paper we describe a fully verified HLS tool called \vericert{}, which adds a Verilog back end to \compcert{}, an existing C compiler that has been written and formally verified in the Coq theorem prover, and proves that the behaviour of the C code is preserved with respect to an existing Verilog semantics. The main contributions of the paper are the following:
\begin{itemize}
\item We provide the first mechanised and formally verified HLS tool going from C to Verilog.
\item Description of how the Verilog semantics integrate into \compcert{} and how it interacts with \compcert{}'s intermediate language.
\item Benchmark comparisons between \vericert{} and LegUp~\cite{canis11_legup}, a well-known open source, unverified HLS tool on Polybench, a large C benchmark, and including some specific test cases from CHstone.
\end{itemize}
The first section will describe the Verilog semantics that were used and extended to fit into \compcert{}'s model. The second section will then describe the HLS algorithm, together with its proof.
\vericert{} is open source and is hosted on GitHub\footnote{\url{https://github.com/ymherklotz/vericert}}.
% }
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:
|
