Adding more comments

1 files changed, 1 insertions, 1 deletions

diff --git a/introduction.tex b/introduction.tex
index c72f788..2ac9eba 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -18,7 +18,7 @@ However, the fact that the behaviour is preserved after HLS cannot be guaranteed
 %% Current work in formal verification of HLS
 %%\NR{This is a good paragraph, but we need to relate it more to this work and why this work is different.}
 %%\NR{Focus on more high-level of "why this work is interesting"? Two key points we want to get across to the reader is that in existing works: validation is neccessary every time a new program is compiled and the verifying algorithm is not verified.}
-%%\NR{Also define words like validation, verifying algorithm (can you use the word ``verifier'',mechanisation}
+%%\NR{Also define words like validation, verifying algorithm (can you use the word ``verifier'',mechanisation)}
 %%\NR{Having said that, keep the text for related work section.}\YH{Added into related works.}
 To mitigate the problems about the unreliability of synthesis tool, it is often required to check the generated hardware for functional correctness.  This can either be done by simulation with a large test bench, however, to be sure that the hardware does indeed behave in the same way as the C code, it may be necessary to prove that they are equivalent. \JW{I think that point could be strengthened by emphasising that simulation with a test-bench only provides guarantees that are as good as the test-bench! That is, if the test-bench does not cover all possible inputs then bugs may remain.} Translation validation~\cite{pnueli98_trans} is the main method which is used to prove that the HLS translation was successful, and has been successfully applied to many HLS optimisations~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth,banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}.  However, the main problem is that the validator itself has often not been mechanically proven correct, meaning that the implementation is quite separate from the proof.  In addition to that, with large designs it may not be feasible to perform translation validation, as the state space would grow exponentially. \JW{Does this link back to Mentor's Catapult-C, which you mentioned earlier? Does Catapult-C attempt to do translation validation as part of its HLS process? And if so, can you make the point that this effort is largely ineffective because once the design is a reasonable size, the translation validation usually fails anyway?} A mechanically verified HLS tool would remove the need to perform simulation after the synthesis process if one has proven desirable properties about the C code.  In addition to that, it would allow for the implementation of translation validated optimisation passes which are also proven correct mechanically, thereby greatly improving the reliability of these passes.