Update on Overleaf.

1 files changed, 1 insertions, 1 deletions

diff --git a/introduction.tex b/introduction.tex
index 359455b..c2bb83d 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -74,7 +74,7 @@ Meanwhile, Xilinx's Vivado HLS has been shown to apply pipelining optimisations
 \subsection{Existing approach: HLS-generated hardware verification}
 
 It is rather difficult to exhaustively test to prove the absence of bugs on these large HLS codebases, which include custom compiler directives.
-Hence, most existing work on verifying HLS tools proving that the translate of a particular  the correctness of the generated hardware by proving its equivalence with to the input C program. 
+Hence, most existing work on verifying HLS tools proving that the translate of a particular C program  the correctness of the generated hardware by proving its equivalence with to the input C program. 
 
 To mitigate the problems about the unreliability of synthesis tool, it is often required to check the generated hardware for functional correctness.  This is commonly done by simulating the design with a large test-bench, however, the guarantees are only as good as the test-bench, meaning if all the inputs were not covered, there is a risk that bugs remain in the untested code.  To ensure that the hardware does indeed behave in the same way as the C code, it may therefore 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.  One example is Catapult C~\cite{mentor20_catap_high_level_synth}, which allows the use of translation validation between the C and RTL code, however, as they mention themselves~\cite{whitepaper}, this process might require quite a bit of iteration on the C code so that the equivalence checker can prove this correctly.  This can be a tedious process, as one cannot be sure about what sections in the C need to change to help the equivalence checker prove the equality.  In addition to that, the larger the design, the more infeasible using an equivalence checking tool like this would be.