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
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
One current approach to writing energy-efficient and high-throughput applications is to use application-specific hardware, instead of relying on a general-purpose CPU.\@ However, custom hardware designs come at the cost of having to design and produce them, which can be a tedious and error-prone process using hardware description languages (HDL) such as Verilog. High-level synthesis (HLS) is becoming a viable alternative, allowing designers to describe the hardware in a software programming language such as C, and inferring the hardware design from it. Can we really trust that the generated hardware functions correctly? It is often assumed that compilers do not change the behaviour of the original program through it's various transformations, however, as HLS tools perform complex transformations, this might not always be the case.
High-level synthesis is becoming increasingly important in the hardware design process. HLS elevates the level of abstraction, allowing designers to describe behaviour using an untimed representation, which reduces the amount of bugs that could be introduced into the design. The higher level of abstraction makes it easier to reason about the algorithms and therefore also facilitates maintaining them. In addition to reducing the time it takes hardware designers to produce hardware, it also reduces the barrier of entry to hardware design for software programmers. In both cases, correctness of the HLS tool is important, as it hinders the productivity of hardware designers by needing them to check the function correctness of the hardware, whereas software programmers may be unable to properly test the hardware as they may be unaware of the proper tools. In addition to that, functional verification of the design becomes much more efficient than at the HDL stage, since the entire software ecosystem can be mobilised for this task. However, any properties that were proven about the functionality of the design may not hold for the hardware design, which may require separate checks.
%% Definition and benefits of HLS
% \NR{The abstraction of HLS helps in two ways: improving productivity of hardware designers and reducing the entry barrier of hardware design for software programmers. Both these audiences stand to benefit from the guarantees provided by verified C-to-Verilog generation.} \JW{Yes, Nadesh makes a good point here. Worth incorporating.}\YH{Added.}
%% Unreliability of HLS
Bugs in HLS tools when designing hardware are detrimental, as it may not be possible to change the hardware once it is produced. It is therefore necessary to not only check the software version of the design correct, but also ensure that the generated hardware design works correctly, because the HLS tool can not be trusted, leading to duplicate testing and verifying of the resulting hardware design. However, with the growing size of hardware designs, it may not be feasible to check that the hardware is correct for all possible inputs. In addition to that, this duplicate checking discourages the use of HLS in safety-critical environments, where correctness is key. It is therefore considered safer to manually write and verify all the hardware designs, hindering the use of higher-level constructs, faster iteration on the designs and more maintainable designs as could be achieved using HLS.\@
This is further motivated by the fact that HLS tools are often considered to be quite unreliable and fragile with respect to which language features that are supported. Most HLS tools cannot guarantee that compilation is behaviour-preserving. In fact, on the contrary, there is some evidence that current HLS tools are actually quite \emph{unreliable} in this regard. For instance, an attempt by \citet{lidbury15_many_core_compil_fuzzin} to fuzz Altera's (now Intel's) OpenCL compiler had to be abandoned because the compiler ``either crashed or emitted an internal compiler error'' on a large number of their test inputs. In addition to that, work by Du \emph{et al.}~\cite{?} fuzz tested three major commercial HLS using Csmith~\cite{yang11_findin_under_bugs_c_compil}, while restricting the C programs to the constructs explicitly supported by the synthesis tools and 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}}.
% JW: Another candidate, probably less interesting:
% https://bit.ly/intel-hls-memory-bug
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}}.
% Maybe include example of C program that goes wrong.
\subsection{Background}
%% Current work in formal verification of HLS
%%\NR{This is a good paragraph, but we need to relate it more to this work and why this work is different.}
%%\NR{Focus on more high-level of "why this work is interesting"? Two key points we want to get across to the reader is that in existing works: validation is neccessary every time a new program is compiled and the verifying algorithm is not verified.}
%%\NR{Also define words like validation, verifying algorithm (can you use the word ``verifier'',mechanisation)}
%%\NR{Having said that, keep the text for related work section.}\YH{Added into related works.}
To mitigate the problems about the unreliability of synthesis tool, it is often required to check the generated hardware for functional correctness. This is commonly done by simulating the design with a large test-bench, however, the guarantees are only as good as the test-bench, meaning if all the inputs were not covered, there is a risk that bugs remain in the untested code. To ensure that the hardware does indeed behave in the same way as the C code, it may therefore be necessary to prove that they are equivalent. Translation validation~\cite{pnueli98_trans} is the main method which is used to prove that the HLS translation was successful, and 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, the main problem is that the validator itself has often not been mechanically proven correct, meaning that the implementation is quite separate from the proof. In addition to that, with large designs it may not be feasible to perform translation validation, as the state space would grow exponentially. One example is Catapult C~\cite{mentor20_catap_high_level_synth}, which allows the use of translation validation between the C and RTL code, however, as they mention themselves~\cite{whitepaper}, this process might require quite a bit of iteration on the C code so that the equivalence checker can prove this correctly. This can be a tedious process, as one cannot be sure about what sections in the C need to change to help the equivalence checker prove the equality. In addition to that, the larger the design, the more infeasible using an equivalence checking tool like this would be.
A mechanically verified HLS tool would remove the need to perform simulation after the synthesis process if one has proven desirable properties about the C code. In addition to that, it would allow for the implementation of optimisation passes which are also proven correct mechanically by translation validation, thereby greatly improving the reliability of these passes.
% \NR{
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
First of all, most of the compiler passes in \compcert{} have been proven correct, meaning that once the compiler is built, the proofs can be erased as the algorithm has been shown to be correct independent of the input. However, some optimisation passes such as software pipelining require translation validation~\cite{tristan08_formal_verif_trans_valid}, in which case the correctness of the compiler pass needs to be checked at runtime. However, even in this case the verifier itself is proven to only verify code correct that does indeed behave in the same way.
|
