Update on Overleaf.

1 files changed, 11 insertions, 21 deletions

diff --git a/related.tex b/related.tex
index 7b519e7..88cd60a 100644
--- a/related.tex
+++ b/related.tex
@@ -12,24 +12,24 @@
     \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=colorusabletool] (-1.1,1.6) ellipse (3.1 and 2.3);
     \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=colormechanised] (0,0) ellipse (3 and 1.0);
 
-    \draw[myoutline] (-1.1,1.8) ellipse (2.9 and 2.1);
+    \draw[myoutline] (-1.1,1.6) ellipse (3.1 and 2.3);
     \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] (0,0) ellipse (3 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[align=left] at (-1.8,0.4) {Koika~\cite{bourgeat20_essen_blues}};
+    \node[align=left] at (-1.8,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 (2.2,0.2) {Ellis~\cite{ellis08}};
+    \node at (-1.3,-0.4) {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};
@@ -44,21 +44,11 @@
 
 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.
+Most practical HLS tools~\cite{canis11_legup,xilinx20_vivad_high_synth,intel20_sdk_openc_applic,nigam20_predic_accel_desig_time_sensit_affin_types} fit into the category of usable tools that take high-level inputs.  On the other spectrum, there are tools such as BEDROC~\cite{chapman92_verif_bedroc} for which there is no practical tool, and even though it is described as high-level synthesis, it resembles today's hardware description tools more.
 
-\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}
-}
+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.
 
-\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.}
+Finally, there are a few relevant mechanically verified tools.  First, K\^{o}ika is a formally verified translation from a core subset of BlueSpec into a circuit representation which can then be printed as a Verilog design.  This is a translation from a high-level hardware description language into an equivalent circuit representation, which is a different approach to HLS.  \citet{loow19_proof_trans_veril_devel_hol} used a verified translation from HOL4 code describing state transitions into Verilog to design a verified processor~\cite{loow19_verif_compil_verif_proces}.  Their approach translated a shallow embedding in HOL4 into a deep embedding of Verilog.  Perna et al.\cite{perna12_mechan_wire_wise_verif_handel_c_synth,perna11_correc_hardw_synth} designed a formally verified translation from a deep embedding of Handel-C~\cite{aubury1996handel}, which is translated to a deep embedding of a circuit.  Finally, Ellis' work~\cite{ellis08} implemented and reasoned about intermediate languages for software/hardware compilation, where parts could be implemented in hardware and the correctness could still be shown.
 
 %%% Local Variables:
 %%% mode: latex