Add more changes

2 files changed, 8 insertions, 4 deletions

diff --git a/draft.org b/draft.org
index 455142f..409ee00 100644
--- a/draft.org
+++ b/draft.org
@@ -8,7 +8,7 @@
 - Importance of correctness, especially in HLS.
 - [cite:lahti19_are_we_there_yet]: Talks about being able to trust synthesis tools.
 - Current focus of HLS is mainly on optimisations
-- Correctness guarantees help with duplicate verificaton
+- Correctness guarantees help with duplicate verificaton.
 
 * How can we prove an HLS tool correct?
 
diff --git a/main.tex b/main.tex
index 9ee0bd9..6408051 100644
--- a/main.tex
+++ b/main.tex
@@ -174,7 +174,11 @@
   High-level synthesis research and development is inherently prone to introducing bugs or regressions in the final circuit functionality.
 \end{displayquote}
 
-Research in high-level synthesis (HLS) often concentrates on performance, trying to achieve the lowest area with the shortest run-time.
+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 high-level synthesis tool is indeed correct, and that it outputs a correct hardware design.  Instead, the design is often meticulously tested, often using the higher level design as a model.  As these tests are performed on the hardware design directly, they have to be run on a simulator, which takes much longer than if the original C was tested.  Any formal properties obtained from the C code would also have to be checked again in the resulting design, to ensure that these hold there as well, as the synthesis tool may have translated the input incorrectly.
+
+It is often assumed that because current HLS tools should transform the input specification into a semantically equivalent design, such as mentioned in \citet{lahti19_are_we_there_yet}.  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, but which the HLS tool interprets differently compared to a C compiler, leading to undefined behaviour.  These types of bugs are difficult to identify, and exist because firstly it is not quite clear what input these tools support, and secondly if the output design actually behaves the same as the input.
+
+The solution to both of these points is to have a formally verified high-level synthesis tool.  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.
 
 \section{How to prove an HLS tool correct}
 
@@ -183,8 +187,8 @@ Research in high-level synthesis (HLS) often concentrates on performance, trying
 \section{Performance of such a tool}
 
 %% Acknowledgments
-%\begin{acks}                            %% acks environment is optional
-                                        %% contents suppressed with 'anonymous'
+%\begin{acks}%% acks environment is optional
+%% contents suppressed with 'anonymous'
   %% Commands \grantsponsor{<sponsorID>}{<name>}{<url>} and
   %% \grantnum[<url>]{<sponsorID>}{<number>} should be used to
   %% acknowledge financial support and will be used by metadata