Fix notes

1 files changed, 1 insertions, 3 deletions

diff --git a/main.tex b/main.tex
index eb30ac7..5f191f1 100644
--- a/main.tex
+++ b/main.tex
@@ -131,9 +131,7 @@ In what follows, we will argue our position by presenting several possible \emph
 \objection{Existing approaches for testing or formally verifying hardware designs are sufficient for ensuring reliability}{
 Besides the use of test benches to test designs produced by HLS, there has been research on performing equivalence checks between the output design and the behavioural input, focusing on creating translation validators~\cite{pnueli98_trans} to prove \JWcouldcut{the} equivalence between the design and \JW{the} input code, while supporting various 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, these aren't perfect solutions either, as there is no guarantee that these proofs really compose with each other.  In response, equivalence checkers are often designed to check the translation from start to finish, but this is computationally expensive, as well as possibly being highly incomplete.}
 
-\JW{Hm, the flow doesn't quite make sense around here. Objection 3 starts by saying that `existing approaches for testing or formally verifying hardware designs are sufficient' but Response 2 has already said that `existing verification techniques for checking the output of HLS tools may not be enough'. And the text at the end of Objection 3 is already saying that translation validators aren't very good -- it feels like that belongs in the `response' rather than the `objection' itself.
-
-One idea: you could end Response 2 after `catch them'. Then Objection 3 suggests a variety of techniques for checking the output of HLS tools (translation validation of each stage, equivalence checking of the whole thing, etc). Then Response 3 demolishes each in turn, ending up with formal verification as the only way forward.}
+\JW{Hm, the flow doesn't quite make sense around here. Objection 3 starts by saying that `existing approaches for testing or formally verifying hardware designs are sufficient' but Response 2 has already said that `existing verification techniques for checking the output of HLS tools may not be enough'. And the text at the end of Objection 3 is already saying that translation validators aren't very good -- it feels like that belongs in the `response' rather than the `objection' itself.  One idea: you could end Response 2 after `catch them'. Then Objection 3 suggests a variety of techniques for checking the output of HLS tools (translation validation of each stage, equivalence checking of the whole thing, etc). Then Response 3 demolishes each in turn, ending up with formal verification as the only way forward.}
 
 %\JW{could end sentence here, as the rest is a little convoluted and perhaps unnecessary} due to a combination of optimisations producing \JWreplace{an}{a correct} output that cannot be matched to the input, \JWcouldcut{even though it is correct.}