Fix more

1 files changed, 2 insertions, 2 deletions

diff --git a/related.tex b/related.tex
index 8bf6743..c2cd8ff 100644
--- a/related.tex
+++ b/related.tex
@@ -26,7 +26,7 @@
     \node[align=center] at (0.15,1.5) {Translation validation approaches \\ \footnotesize\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.0) {\footnotesize K\^oika \cite{bourgeat20_essen_blues}};
-    \node[align=left] at (-1.8,0.32) { \footnotesize\citet{loow19_verif_compil_verif_proces}};
+    \node[align=left] at (-1.8,0.32) { \footnotesize\citet{10.1145/3437992.3439916}};
 
     \node at (2.2,0.2) {\footnotesize\citet{ellis08}};
     \node at (-1.3,-0.32) { {\footnotesize\citet{perna12_mechan_wire_wise_verif_handel_c_synth}}};
@@ -48,7 +48,7 @@ Most practical HLS tools~\citep{canis11_legup,xilinx20_vivad_high_synth,intel20_
 
 Ongoing work in translation validation~\citep{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~\citep{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~\citep{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth} or code motion~\citep{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 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~\citep{loow19_verif_compil_verif_proces}. \JW{That sentence is a bit confusing because it's not clear why Loow is cited twice.} Their approach translated a shallow embedding in HOL4 into a deep embedding of Verilog.
+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, which is described in \citet{loow19_verif_compil_verif_proces}.  In addition to that, there is also work on formally verifying a synthesis tool to transform, which can transform hardware descriptions into low-level netlists~\cite{10.1145/3437992.3439916}. Their approach translated a shallow embedding in HOL4 into a deep embedding of Verilog.
 \citet{perna12_mechan_wire_wise_verif_handel_c_synth,perna11_correc_hardw_synth} designed a formally verified translation from a deep embedding of Handel-C~\citep{aubury1996handel}, which is translated to a deep embedding of a circuit.
 Finally, \citet{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.