Add more text

2 files changed, 22 insertions, 1 deletions

diff --git a/main.tex b/main.tex
index 6408051..cf618c0 100644
--- a/main.tex
+++ b/main.tex
@@ -178,10 +178,14 @@ 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.
+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.
 
 \section{How to prove an HLS tool correct}
 
+\paragraph{How could such a tool be constructed?}
+
+The radical solution to this problem is to formally verify the complete tool, writing the complete tool in Coq~\cite{coquand86}
+
 \section{Guarantees of trusted code}
 
 \section{Performance of such a tool}
diff --git a/references.bib b/references.bib
index 0d4c2f4..840a580 100644
--- a/references.bib
+++ b/references.bib
@@ -18,3 +18,20 @@
 	author = {Canis, Andrew Christopher},
 	year = {2015}
 }
+
+@book{bertot04_inter_theor_provin_progr_devel,
+	keywords = {coq, verification},
+	author = {Yves Bertot and Pierre Cast{\'{e}}ran},
+	title = {Interactive Theorem Proving and Program Development},
+	year = 2004,
+	publisher = {Springer Berlin Heidelberg},
+	url = {https://doi.org/10.1007/978-3-662-07964-5},
+	doi = {10.1007/978-3-662-07964-5}
+}
+
+@phdthesis{coquand86,
+	title = {The calculus of constructions},
+	author = {Coquand, Thierry and Huet, G{\'e}rard},
+	year = {1986},
+	school = {INRIA}
+}