Update some sections

1 files changed, 38 insertions, 38 deletions

diff --git a/related.tex b/related.tex
index 6457913..5cdee3a 100644
--- a/related.tex
+++ b/related.tex
@@ -1,59 +1,59 @@
 \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}
+  \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}}
+    \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[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);
+    \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{canis+11, vivadohls, intelopencl, dahlia}};
-\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{koika_pldi2020}};
-\node[align=left] at (-1.5,0.0) {L\"o\"ow et al.~\cite{loow}};
+    \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 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};
+    \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{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 adress 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}
+  \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. \@
+      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}
+  \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}.}