Update on Overleaf.

1 files changed, 5 insertions, 5 deletions

diff --git a/related.tex b/related.tex
index 88cd60a..e0cefa3 100644
--- a/related.tex
+++ b/related.tex
@@ -23,7 +23,7 @@
     \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[align=center] at (0,1.5) {Translation validation \\ approaches~\cite{mentor20_catap_high_level_synth,kundu08_valid_high_level_synth,clarke03_behav_c_veril}};
     \node at (0,0.5) {\bf \vericert{}};
     \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}};
@@ -42,13 +42,13 @@
   \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.
+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.
 
-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.
+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 more closely resembles today's hardware synthesis tools.
 
-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.
+Ongoing work in translation validation~\cite{pnueli98_trans} seeks to prove equivalence between the hardware generated by an HLS tool 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 3AC description to states in the original C code after an unverified translation.  Using translation validation is quite effective for verifying 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}, but the validation has to be run every time the HLS 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 hence could give false positives or false negatives.
 
-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.
+Finally, there are a few relevant mechanically verified tools.  First, K\^{o}ika is a formally verified translation from a core fragment 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, so 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~\cite{ellis08} used Isabelle to implement and reason 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