Update on Overleaf.

1 files changed, 5 insertions, 2 deletions

diff --git a/introduction.tex b/introduction.tex
index aac8580..5383dba 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -74,8 +74,11 @@ 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 translation of a program instance to hardware is equaivalent, as known as translation validation. 
-Translation validation proves t
+Hence, most existing work on verifying HLS tools proving that HLS-generated hardware is equivalent to its software counterpart for all possible inputs of the program, as known as translation validation~\cite{pnueli98_trans}. 
+Translation validation 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, translation validation often suffers from one key problem: the validator itself might not have been mechanically proven to be correct.
+The proof of the valide
+
 
 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.