Some more fixes

2 files changed, 12 insertions, 1 deletions

diff --git a/main.tex b/main.tex
index 611b951..c1b688b 100644
--- a/main.tex
+++ b/main.tex
@@ -175,7 +175,7 @@ In what follows, we will argue our position by presenting several possible \emph
 
 Formally verifying HLS of C is the wrong approach. C should not be used to design hardware, let alone hardware where reliability is crucial. Instead, there have been many efforts to formally verify the translation of high-level hardware description languages like Bluespec with K\^{o}i\-ka~\cite{bourgeat20_essen_blues}, formalising the synthesis of Verilog into technology-mapped net-lists with Lutsig~\cite{loow21_lutsig}, or work on formalising circuit design in Coq itself to ease design verification~\cite{choi17_kami,singh_silver_oak}.
 
-\paragraph{Response:} However, verifying HLS is also important.  Not only is HLS becoming more popular, as it requires much less design effort to produce new hardware~\cite{lahti19_are_we_there_yet}, but much of that convenience comes from the easy behavioural testing that HLS allows to ensure correct functionality of the design.  This assumes that HLS tools are correct.
+\paragraph{Response:} Verifying HLS is also important.  Firstly, C is often the starting point for hardware designs, as initial models are written in those languages to get a quick prototype~\cite{gajski10_what_hls}, so it is only natural to continue using C when designing the hardware.  Not only is HLS from C becoming more popular, but much of that convenience also comes from the easy behavioural testing that HLS allows to ensure correct functionality of the design~\cite{lahti19_are_we_there_yet}.  This assumes that HLS tools are correct.
 
 \objection{Current HLS tools are already reliable enough}
 
diff --git a/references.bib b/references.bib
index b3a6e1d..5dc3ae5 100644
--- a/references.bib
+++ b/references.bib
@@ -322,3 +322,14 @@ url = {https://github.com/project-oak/silveroak},
   publisher       = {Association for Computing Machinery},
   series          = {PLDI 2020},
 }
+
+@inproceedings{gajski10_what_hls,
+	author = {Gajski, Dan and Austin, Todd and Svoboda, Steve},
+	booktitle = {Design Automation Conference},
+	title = {What input-language is the best choice for high level synthesis (HLS)?},
+	year = {2010},
+	volume = {},
+	number = {},
+	pages = {857-858},
+	doi = {10.1145/1837274.1837489}
+}