Finish sentences

1 files changed, 1 insertions, 1 deletions

diff --git a/introduction.tex b/introduction.tex
index 458fddb..2e78bc3 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -20,7 +20,7 @@ However, the fact that the behaviour is preserved after HLS cannot be guaranteed
 %%\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.  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.  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.
 
-CompCert~\cite{leroy06_formal_certif_compil_back_end} is a C compiler that has been written and formally verified in the Coq theorem prover~\cite{bertot04_inter_theor_provin_progr_devel}.  First of all, most of the compiler passes in CompCert have been proven correct, meaning that once the compiler is built, the proofs can be erased as the algorithm has been shown to be correct independent of the input.  However, some optimisation passes such as software pipelining require translation validation~\cite{tristan08_formal_verif_trans_valid}, in which case the proof still happens at runtime.  The difference is that in this case, the verifier itself is actually formally verified in Coq and is therefore proven that it will only ever say that the input and output are equivalent if that is actually the case.
+CompCert~\cite{leroy06_formal_certif_compil_back_end} is a C compiler that has been written and formally verified in the Coq theorem prover~\cite{bertot04_inter_theor_provin_progr_devel}.  First of all, most of the compiler passes in CompCert have been proven correct, meaning that once the compiler is built, the proofs can be erased as the algorithm has been shown to be correct independent of the input.  However, some optimisation passes such as software pipelining require translation validation~\cite{tristan08_formal_verif_trans_valid}, in which case the correctness of the compiler pass needs to be checked at runtime.  However, even in this case the verifier itself is proven to only verify code correct that does indeed behave in the same way.
 
 %% Contributions of paper