Update on Overleaf.

1 files changed, 15 insertions, 3 deletions

diff --git a/introduction.tex b/introduction.tex
index 7abed31..e2e2520 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -56,17 +56,29 @@ As such, high-level synthesis (HLS) is becoming an attractive alternative, since
 Modern HLS tools such as LegUp~\cite{}, Vivado HLS~\cite{}, and Intel i++~\cite{} can produce designs with comparable performance and energy-efficiency to those manually coded in HDL [citation needed], while offering the convenient abstractions and rich ecosystem of software development.
 
 \subsection{Can we trust our high-level synthesis tools?}
-The usual starting point for most HLS tool development is to leverage an existing software compiler framework like LLVM. 
-Re-using software concepts, optimisation and codebases make HLS compiliation as susceptible to bugs as any software compilers for the same reasons. 
+The common starting point for most HLS tool development is to leverage an existing software compiler framework like LLVM, such as LegUp HLS, Vivado HLS and Bambu HLS~\cite{}.
+Re-using software concepts, optimisation and codebases make HLS compiliation as susceptible to bugs as any software compilers. 
 These native codebases are large and they perform complex and non-trivial analyses and transformations to translate software into efficient assembly or HDL, in the case of HLS. 
 Consequently, HLS tools cannot always guarantee that the generated hardware is equivalent to the input program, undermining any reasoning conducted at the software level. 
 Furthermore, HDL design in itself is complex, error-prone and requires careful reasoning and formal verification to ensure behaviour, data-flow and structural correctness~\cite{}.
 The added complexity of HDL design thus increases the likelihood of HLS compilation mismatches. 
 % between the software program and the generated hardware. 
 % There are valid reasons to doubt that HLS tools actually \emph{do} preserve equivalence, not least because they are large pieces of software that perform complex transformations.
+
 Hence, the premise of this work is: Can we trust these compilers to translate high-level languages like C/C++ to HDL correctly? 
+For instance, \citet{lidbury15_many_core_compil_fuzzin} abandoned fuzzing Altera's (now Intel's) OpenCL compiler since it ``either crashed or emitted an internal compiler error'' on a large number of their test inputs.  
+Also, Du \emph{et al.}~\cite{?} fuzz tested three commercial HLS tools using Csmith~\cite{yang11_findin_under_bugs_c_compil}, while restricting the C programs to the constructs explicitly supported by the synthesis tools. 
+They found that on average 2.5\% of test cases generated a design that did not match the behaviour of the input.  
+Meanwhile, Xilinx's Vivado HLS has been shown to apply pipelining optimisations incorrectly\footnote{\url{https://bit.ly/vivado-hls-pipeline-bug}} or to silently generate wrong code should the programmer stray outside the fragment of C that it supports\footnote{\url{https://bit.ly/vivado-hls-pointer-bug}}.
+
+\subsection{Existing approach: HLS-generated hardware verification}
+
+It is rather difficult to exhaustively test these large HLS codebases, which include custom compiler directives.
+Hence, most existing work on verifying HLS tools 
 
-\subsection{Evidence of unreliability and previous works}
+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.
+
+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 optimisation passes which are also proven correct mechanically by translation validation, thereby greatly improving the reliability of these passes.
 
 \subsection{Our approach}