Add more references

2 files changed, 54 insertions, 2 deletions

diff --git a/main.tex b/main.tex
index cbb6516..571028c 100644
--- a/main.tex
+++ b/main.tex
@@ -186,7 +186,7 @@
 \epigraph{\textit{High-level synthesis research and development is inherently prone to introducing bugs or regressions in the final circuit functionality.}}{--- Andrew Canis~\cite{canis15_legup}}
 
 %\JW{Nice quote; I'd be tempted to tinker with whether it can be formatted a bit more elegantly, like at https://style.mla.org/styling-epigraphs/} 
-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 \JW{why `and'? Perhaps `which means'?} 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.
+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, which means 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.
 
@@ -196,7 +196,7 @@ The solution to both of these points is to have a formally verified high-level s
 
 \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}, an interactive theorem prover.
+The radical solution to this problem is to formally verify the complete tool, writing the complete tool in Coq~\cite{coquand86}, an interactive theorem prover.  This has been proven to be successful, for example, CompCert~\cite{leroy09_formal_verif_realis_compil} is a formally verified C compiler written in Coq.  This was demonstrated by CSmith~\cite{yang11_findin_under_bugs_c_compil}, a random C, valid C generator, which found more than 300 bugs in GCC and Clang, whereas only 5 bugs were found in the unverified parts of CompCert, which prompted the verification of those parts as well.
 
 \section{Guarantees of trusted code}
 
diff --git a/references.bib b/references.bib
index 840a580..24b1f75 100644
--- a/references.bib
+++ b/references.bib
@@ -35,3 +35,55 @@
 	year = {1986},
 	school = {INRIA}
 }
+
+@inproceedings{loow21_lutsig,
+	author = {L\"{o}\"{o}w, Andreas},
+	title = {Lutsig: A Verified Verilog Compiler for Verified Circuit Development},
+	year = {2021},
+	isbn = {9781450382991},
+	publisher = {Association for Computing Machinery},
+	address = {New York, NY, USA},
+	url = {https://doi.org/10.1145/3437992.3439916},
+	doi = {10.1145/3437992.3439916},
+	booktitle = {Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs},
+	pages = {46–60},
+	numpages = {15},
+	location = {Virtual, Denmark},
+	series = {CPP 2021}
+}
+
+@inproceedings{yang11_findin_under_bugs_c_compil,
+	author = {Yang, Xuejun and Chen, Yang and Eide, Eric and Regehr, John},
+	title = {Finding and Understanding Bugs in C Compilers},
+	booktitle = {Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design
+                  and Implementation},
+	year = 2011,
+	pages = {283-294},
+	doi = {10.1145/1993498.1993532},
+	url = {https://doi.org/10.1145/1993498.1993532},
+	address = {New York, NY, USA},
+	isbn = 9781450306638,
+	location = {San Jose, California, USA},
+	numpages = 12,
+	publisher = {Association for Computing Machinery},
+	series = {PLDI '11}
+}
+
+@article{leroy09_formal_verif_realis_compil,
+	author = {Leroy, Xavier},
+	title = {Formal Verification of a Realistic Compiler},
+	tags = {verification},
+	journal = {Commun. ACM},
+	volume = 52,
+	number = 7,
+	pages = {107--115},
+	year = 2009,
+	doi = {10.1145/1538788.1538814},
+	acmid = 1538814,
+	address = {New York, NY, USA},
+	issn = {0001-0782},
+	issue_date = {July 2009},
+	month = jul,
+	numpages = 9,
+	publisher = {ACM}
+}