Add more changes

3 files changed, 36 insertions, 4 deletions

diff --git a/draft.org b/draft.org
index 423826f..92ffecd 100644
--- a/draft.org
+++ b/draft.org
@@ -24,3 +24,6 @@
 * Guarantees and trusted code
 
 * Performance of such a tool
+
+- ramp up more about the future.
+- formally verifying other algorithms
diff --git a/main.tex b/main.tex
index 5363671..f4a93f3 100644
--- a/main.tex
+++ b/main.tex
@@ -196,13 +196,15 @@ The solution to both of these points is to have a formally verified high-level s
 
 \section{Arguments against formalised HLS}
 
-\paragraph{People should not be designing hardware in C to begin with.}
+\subsection{People should not be designing hardware in C to begin with.}
 
-One might argue that HLS does not normally have to be reliable, and that it is important to instead focus on formalising different areas of hardware.  For example, there have been efforts formalising a Bluespec like language in K\^{o}ika~\cite{bourgeat20_essen_blues}, which is closer to a high-level hardware description language, or
+In fact, formally verifying HLS of C is the wrong approach, as it should not be used to design hardware, let alone hardware that is important to be reliable. 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{HLS applications don't require the levels of reliability that a formally verified compiler affords.}
+However,
 
-One might argue that developing a formally verified tool in a theorem prover and proving correctness theorems about it might be too tedious and take too long.  However, we have already been developed our own verified HLS tool called \vericert{}~\cite{herklotz21_formal_verif_high_level_synth} based on \compcert{}, adding a Verilog back end to the compiler.  We currently have a completely verified translation from a large subset of C into Verilog, which fullfills the minimum requirements for an HLS tool.  We found that it normally takes $5\times$ or $10\times$ longer to prove a translation correct compared to writing the algorithm.
+\subsection{HLS applications don't require the levels of reliability that a formally verified compiler affords.}
+
+One might argue that developing a formally verified tool in a theorem prover and proving correctness theorems about it might be too tedious and take too long.  However, we have already been developed our own verified HLS tool called \vericert{}~\cite{herklotz21_formal_verif_high_level_synth} based on \compcert{}, adding a Verilog back end to the compiler.  We currently have a completely verified translation from a large subset of C into Verilog, which fulfills the minimum requirements for an HLS tool.  We found that it normally takes $5\times$ or $10\times$ longer to prove a translation correct compared to writing the algorithm.
 
 However, this could be seen as being beneficial, as proving the correctness of the HLS tool proves the absence of any bugs according to the language semantics, meaning much less time spent on fixing bugs.  In addition to that, even though simple testing would still be required to check the tool does indeed perform simple translations, and generates performant designs, these test benches would not have to cover every single edge case.  Finally, verification also forces the algorithm to deal with many different edge cases that may be hard to identify normally, and may even allow for more optimisations as one can be certain about assumptions one would usually have to make.
 
diff --git a/references.bib b/references.bib
index 9b5fd27..9ece4da 100644
--- a/references.bib
+++ b/references.bib
@@ -260,3 +260,30 @@
 	publisher = {Association for Computing Machinery},
 	series = {PLDI 2020}
 }
+
+@article{choi17_kami,
+	author = {Choi, Joonwon and Vijayaraghavan, Muralidaran and Sherman, Benjamin and Chlipala, Adam and Arvind},
+	title = {Kami: a Platform for High-Level Parametric Hardware Specification and Its Modular Verification},
+	tags = {verification},
+	journal = {Proc. ACM Program. Lang.},
+	volume = 1,
+	number = {ICFP},
+	pages = {24:1--24:30},
+	year = 2017,
+	doi = {10.1145/3110268},
+	url = {https://doi.org/10.1145/3110268},
+	acmid = 3110268,
+	address = {New York, NY, USA},
+	articleno = 24,
+	issn = {2475-1421},
+	issue_date = {September 2017},
+	month = aug,
+	numpages = 30,
+	publisher = {ACM}
+}
+
+@misc{singh_silver_oak,
+title = {{Silver Oak}},
+author = {Satnam Singh},
+url = {https://github.com/project-oak/silveroak},
+}