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
|
\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.
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{intel_hls}, and Bambu HLS~\cite{bambu_hls} promise designs with comparable performance and energy-efficiency to those manually coded in HDL~\cite{homsirikamol+14, silexicahlshdl, 7818341}, 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, 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.
%Some of these reasons are general: HLS tools are large pieces of software, they perform a series of complex analyses and transformations, and the HDL output they produce has superficial syntactic similarities to a software language but a subtly different semantics.
%Hence, the premise of this work is: Can we trust these compilers to translate high-level languages like C/C++ to HDL correctly?
%Other reasons are more specific:
For instance, 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}}
Meanwhile, \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.
And 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.
\subsection{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 design against a large test-bench; however, the guarantees are only as good as the test-bench, meaning that if all the inputs were not covered exhaustively, there is a risk that bugs remain.
An alternative is to use \emph{translation validation} to formally prove the input and output equivalent~\cite{pnueli98_trans}. 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}.
Yet translation validation must be repeated every time the compiler is invoked, and it is an expensive task, especially for large designs.
For example, the translation validation for Catapult C~\cite{mentor20_catap_high_level_synth, slec_whitepaper} may require several rounds of expert modifications 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, which is seldom the case.
Our position is that none of the above workarounds are necessary if the HLS tool can simply be trusted to work correctly.
\subsection{Our solution}
We have written a new HLS tool in the Coq theorem prover~\cite{bertot04_inter_theor_provin_progr_devel} and proven that it any output it produces always has the same behaviour as its input. Our tool, which is called \vericert{}, is automatically extracted to an OCaml program from Coq, which ensures that the object of the proof is the same as the implementation of the tool. \vericert{} is built by extending the \compcert{} verified C compiler~\cite{leroy09_formal_verif_realis_compil} with a new hardware-specific intermediate language and a Verilog back end. It supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables.
\subsection{Contributions and Outline}
The contributions of this paper are as follows:
\begin{itemize}
\item We present \vericert{}, the first mechanically verified HLS tool that compiles C to Verilog. The design of \vericert{} is described in Section~\ref{sec:design}.
\item We prove \vericert{} correct w.r.t. an existing semantics for Verilog due to \citet{loow19_formalise}. We describe in Section~\ref{sec:verilog} how we lightly extended this semantics to make it suitable as an HLS target. Section~\ref{sec:proof} describes the proof itself.
\item We have conducted a performance comparison between \vericert{} and a widely-used (unverified) HLS tool called \legup{}~\cite{canis11_legup} using the PolyBench benchmarks. As described in Section~\ref{sec:evaluation}, \vericert{} generates hardware that is about 9x slower and 21x less area-efficient than that generated by \legup{}. We expect that these numbers will improve when we extend \vericert{} with such optimisations as loop pipelining and scheduling.
\end{itemize}
\vericert{} is fully open source and available online. \JW{We'll have to blind this (and maybe even the name of the tool itself) for submission.}
\begin{center}
\url{https://github.com/ymherklotz/vericert}
\end{center}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:
|
