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
|
\section{Related Work}
\begin{figure}
\centering
\begin{tikzpicture}
\def\opacity{0.2}
\definecolor{colorusabletool}{HTML}{1b9e77}
\definecolor{colorhighlevel}{HTML}{d95f02}
\definecolor{colorproof}{HTML}{7570b3}
\definecolor{colormechanised}{HTML}{e7298a}
\tikzset{myellipse/.style={draw=none, fill opacity=0.2}}
\tikzset{myoutline/.style={draw=white, thick}}
\draw[myellipse, fill=colorusabletool] (-1.1,1.8) ellipse (2.9 and 2.1);
\draw[myellipse, fill=colorhighlevel] (1.1,1.8) ellipse (2.9 and 2.1);
\draw[myellipse, fill=colorproof] (0,0.3) ellipse (3.7 and 1.9);
\draw[myellipse, fill=colormechanised] (0,0) ellipse (2.7 and 1.0);
\draw[myoutline] (-1.1,1.8) ellipse (2.9 and 2.1);
\draw[myoutline] (1.1,1.8) ellipse (2.9 and 2.1);
\draw[myoutline] (0,0.3) ellipse (3.7 and 1.9);
\draw[myoutline] (0,0) ellipse (2.7 and 1.0);
\node[align=center] at (0,2.8) {Standard HLS \\ tools~\cite{canis11_legup,xilinx20_vivad_high_synth,intel20_sdk_openc_applic,nigam20_predic_accel_desig_time_sensit_affin_types}};
\node[align=center] at (0,1.5) {Translation validation \\ approaches~\cite{mentor20_catap_high_level_synth,kundu08_valid_high_level_synth, clarke_kroening_yorav_03}};
\node at (0,0.5) {\bf \vericert{}};
\node[align=left] at (-1.5,0.4) {Koika~\cite{bourgeat20_essen_blues}};
\node[align=left] at (-1.5,0.0) {L\"o\"ow et al.~\cite{loow19_verif_compil_verif_proces}};
\node at (1.8,0.2) {Ellis~\cite{ellis08}};
\node at (0,-0.6) {Perna et al.~\cite{perna12_mechan_wire_wise_verif_handel_c_synth}};
\node at (0,-1.3) {BEDROC~\cite{chapman92_verif_bedroc}};
\node[align=left] at (-2.9,-1.7) {\color{colorproof}Correctness \\ \color{colorproof}proof};
\draw[myoutline] (1.2,-0.9) to (2.6,-1.7);
\node[align=right] at (2.6,-1.7) {\color{colormechanised}Mechanised \\ \color{colormechanised}correctness proof};
\node at (-2.8,4.1) {\color{colorusabletool}\strut Usable tool};
\node at (2.1,4.1) {\color{colorhighlevel}\strut High-level software input};
\end{tikzpicture}
\caption{Summary of related work}\label{fig:related_venn}
\end{figure}
A summary of the related works can be found in Figure~\ref{fig:related_venn}, which is represented as a Venn diagram. The categories that were chosen for the Venn diagram are if the tool is usable and available, if it takes a high-level software language as input, if it has a correctness proof and finally if that proof is mechanised. The goal of \vericert{} is to cover all of these categories.
Work is being done to prove the equivalence between the generated hardware and the original behavioural description in C. An example of a tool that implements this is Mentor's Catapult~\cite{mentor20_catap_high_level_synth}, which tries to match the states in the three address code (3AC) description to states in the original C code after an unverified translation. This technique is called translation validation~\cite{pnueli98_trans}, whereby the translation that the HLS tool performed is proven to have been correct for that input, by showing that they behave in the same way for all possible inputs. Using translation validation is quite effective for proving complex optimisations such as scheduling~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth} or code motion~\cite{banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}, however, the validation has to be run every time the high-level synthesis is performed. In addition to that, the proofs are often not mechanised or directly related to the actual implementation, meaning the verifying algorithm might be wrong and could give false positives or false negatives.
\JW{Some papers to cite somewhere:
\begin{itemize}
\item \citet{kundu08_valid_high_level_synth} have done translation validation on an HLS tool called SPARK. They don't have \emph{very} strong evidence that HLS tools are buggy; they just say ``HLS tools are large and complex software systems, often with hundreds of
thousands of lines of code, and as with any software of this scale, they are prone
to logical and implementation errors''. They did, however, find two bugs in SPARK as a result of their efforts, so that provides a small bit of evidence that HLS tools are buggy. \@
\item \citet{chapman92_verif_bedroc} have proved (manually, as far as JW can tell) that the front-end and scheduler of the BEDROC synthesis system is correct. (NB:\@ Chapman also wrote a PhD thesis about this (1994) but it doesn't appear to be online.)
\item \citet{ellis08} wrote a PhD thesis that was supervised by Cliff Jones whom you met at the VeTSS workshop thing last year. At a high level, it's about verifying a high-level synthesis tool using Isabelle, so very relevant to this project, though scanning through the pdf, it's quite hard to ascertain exactly what the contributions are. Strange that they never published a paper about the work -- it makes it very hard to find!
\end{itemize}
}
\YH{Amazing, thank you, yes it seems like Kundu \textit{et al.} have quite a few papers on formal verification of HLS algorithms using translation validation, as well as~\citet{karfa06_formal_verif_method_sched_high_synth}, all using the SPARK~\cite{gupta03_spark} synthesis tool. And yes thank you, will definitely cite that paper. There seem to be similar early proofs of high-level synthesis like \citet{hwang91_formal_approac_to_sched_probl} or \citet{grass94_high}. There are also the Occam papers that I need to mention too, like \citet{page91_compil_occam}, \citet{jifeng93_towar}, \citet{perna11_correc_hardw_synth} and \citet{perna12_mechan_wire_wise_verif_handel_c_synth}.}
\JW{Well it's a good job there's no page limit on bibliographies these days then! I'll keep an eye out for more papers we could cite when I get a free moment. (No need to cite \emph{everything} of course.)}
\YH{Yes that's true, there are too many to cite! And great thank you, that would help a lot, I have quite a few papers I still want to cite, but have to think about where they will fit in.}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% TeX-command-extra-options: "-shell-escape"
%%% End:
|
