Update on Overleaf.

1 files changed, 2 insertions, 2 deletions

diff --git a/main.tex b/main.tex
index 4c84ad0..d8c201b 100644
--- a/main.tex
+++ b/main.tex
@@ -163,9 +163,9 @@
 
 Research in high-level synthesis (HLS) often concentrates on performance: trying to achieve the lowest area with the shortest run-time.  What is often overlooked is ensuring that the HLS tool is indeed correct, which means that it outputs hardware designs that are equivalent to the behavioural input.
 
-It is often assumed when working with HLS tools, that they transform the behavioural input into a semantically equivalent design.  This assumption is made in \citet{lahti19_are_we_there_yet} for example.  However, this is not the case, and as with all complex pieces of software there are bugs in HLS tools as well.  For example, Vivado HLS was found to incorrectly apply pipelining optimisations\footnote{\url{https://bit.ly/vivado-hls-pipeline-bug}} or generate wrong designs with valid C code as input.  These types of bugs are difficult to identify, and exist because firstly it is not quite clear what input these tools support, and secondly whether the output design actually behaves the same as the input.
+\JWreplace{It is often assumed when working with HLS tools,}{When working with HLS tools, it is often assumed} that they transform the behavioural input into a semantically equivalent design.  This assumption is made in \citet{lahti19_are_we_there_yet} for example.  However, this is not the case, and as with all complex pieces of software there are bugs in HLS tools as well.  For example, Vivado HLS was found to incorrectly apply pipelining optimisations\footnote{\url{https://bit.ly/vivado-hls-pipeline-bug}} or generate wrong designs with valid C code as input \JW{citation needed for this claim too?}.  These types of bugs are difficult to identify, and exist because firstly it is not quite clear what input these tools support, and secondly whether the output design actually behaves the same as the input.
 
-\paragraph{Our position} We believe that a formally verified high-level synthesis tool could be the solution to these problems.  It not only guarantees that the output is correct, but also brings a formal specification of the input and output language semantics.  These are the only parts of the compiler that need to be trusted, and if these are well-specified, then the behaviour of the resulting design can be fully trusted.  In addition to that, if the semantics of the input semantics are taken from a tool that is widely trusted already, then there should not be any strange behaviour; the resultant design will either behave exactly like the input specification, or the translation will fail early at compile time.  To this end, we have built a formally verified HLS tool called \vericert{}~\cite{herklotz21_formal_verif_high_level_synth}.
+\paragraph{Our position} We believe that a formally verified high-level synthesis tool could be the solution to these problems.  It not only guarantees that the output is correct, but also brings a formal specification of the input and output language semantics.  These are the only parts of the compiler that need to be trusted, and if these are well-specified, then the behaviour of the resulting design can be fully trusted.  In addition to that, if the semantics of the input semantics \JW{repeated `semantics'} are taken from a tool that is widely trusted already, then there should not be any strange behaviour; the resultant design will either behave exactly like the input specification, or the translation will fail early at compile time.  To this end, we have built a formally verified HLS tool called \vericert{}~\cite{herklotz21_formal_verif_high_level_synth}.
 
 In what follows, we will argue our position by presenting several possible \emph{objections} to our position, and then responding to each in turn.