using numerical citations as per CFP. and adding a venn diagram of related work.

1 files changed, 43 insertions, 0 deletions

diff --git a/related.tex b/related.tex
index a2da530..bde0a8b 100644
--- a/related.tex
+++ b/related.tex
@@ -1,5 +1,47 @@
 \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{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.2) {L\"o\"ow \\ et al.~\cite{loow}};
+\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.7,4.1) {\color{colorhighlevel}\strut High-level input};
+
+
+\end{tikzpicture}
+\caption{Summary of related work}
+\label{fig:related_venn}
+\end{figure}
+
 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:
@@ -19,4 +61,5 @@ to logical and implementation errors''. They did, however, find two bugs in SPAR
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "main"
+%%% TeX-command-extra-options: "-shell-escape"
 %%% End: