Add more to introduction

1 files changed, 7 insertions, 5 deletions

diff --git a/main.tex b/main.tex
index 6035fc3..ced45f4 100644
--- a/main.tex
+++ b/main.tex
@@ -45,7 +45,7 @@
 \COMMENTStrue
 \newcommand{\Comment}[3]{\ifCOMMENTS\textcolor{#1}{{\bf [\![#2:} #3{\bf ]\!]}}\fi}
 \newcommand\JW[1]{\Comment{red!75!black}{JW}{#1}}
-\newcommand\YH[1]{\Comment{green!50!black}{YH}{#1}}
+\newcommand\YH[1]{\Comment{green!50!blue}{YH}{#1}}
 \newcommand\JP[1]{\Comment{blue!50!black}{JP}{#1}}
 
 \begin{document}
@@ -91,7 +91,7 @@
 \author{James Pollard}
 \orcid{0000-0003-1404-1527}
 \affiliation{
-%  \position{PhD Student}
+%  \position{}
 %  \department{EEE}
   \institution{Imperial College London}
 %  \streetaddress{South Kensington Campus}
@@ -105,7 +105,7 @@
 \author{Nadesh Ramanathan}
 \orcid{0000-0000-0000-0000}
 \affiliation{
-%  \position{PhD Student}
+%  \position{}
 %  \department{EEE}
   \institution{Imperial College London}
 %  \streetaddress{South Kensington Campus}
@@ -119,7 +119,7 @@
 \author{John Wickerson}
 \orcid{0000-0000-0000-0000}
 \affiliation{
-%  \position{PhD Student}
+%  \position{}
 %  \department{EEE}
   \institution{Imperial College London}
 %  \streetaddress{South Kensington Campus}
@@ -177,10 +177,12 @@ One possible solution to this is to use high-level synthesis (HLS), which is the
 
 %% Unreliability of HLS
 
-However, the fact that the behaviour is preserved after HLS cannot be guaranteed most existing tools.\YH{Mentor's catapult C can in some cases} 
+However, the fact that the behaviour is preserved after HLS cannot be guaranteed most existing tools,\YH{Mentor's catapult C can in some cases} meaning behavioural simulation of the hardware design still has to be performed.  HLS tools are also known to be quite unreliable, for example, Intel's (formerly Altera's) OpenCL SDK compiler contained too many bugs to even be considered for random testing, as more than 25\% of the testcases failed~\cite{lidbury15_many_core_compil_fuzzin}.  In addition to that, designers often feel like HLS tools are quite unreliable and fragile with respect to which language features that are supported.\YH{Need citation}  As HLS tools are extremely complex and can therefore incorrectly change the behaviour of the design, it is not possible to guarantee that all the properties of the code that were proven in software will also hold for the generated hardware.
 
 %% Current work in formal verification of HLS
 
+Therefore, work is being done to prove the equivalence between the generated hardware and the original behavioural description in C.  An example of a tool that implements this is Mentor's Catapult~\cite{mentor20_catap_high_level_synth}, which tries to match the states in the register transfer level (RTL) description to states in the original C code after an unverified translation.  This has also been the approach that is taken by
+
 %% Contributions of paper
 
 \section{Background}