Rewrite conclusion

1 files changed, 2 insertions, 2 deletions

diff --git a/main.tex b/main.tex
index bb65570..5874499 100644
--- a/main.tex
+++ b/main.tex
@@ -192,7 +192,7 @@ Research in high-level synthesis (HLS) often concentrates on performance, trying
 
 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.  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.
+Our position is 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.
 
 \section{Arguments against formalised HLS}
 
@@ -232,7 +232,7 @@ Finally, the input and output language semantics also need to be trusted, as the
 
 \section{Conclusion}
 
-In conclusion, we have shown that a verified HLS tool could achieve similar performance to an existing unverified HLS tool, while guaranteeing that the output is always correct.
+In conclusion, we have demonstrated that a realistic HLS tool should be proven correct, and even though the performance does not quite match state of the art HLS tools, as the optimisations are formally verified, and added, similar performance may be achieved.  In addition to that, a formally verified HLS tool, written in a theorem prover, would provide a good base to mechanically verify other HLS specific optimisations and help develop more reliable HLS tools in the future.
 
 %% Acknowledgments
 %\begin{acks}%% acks environment is optional