Add more

2 files changed, 17 insertions, 1 deletions

diff --git a/main.tex b/main.tex
index cc8550e..fb757a4 100644
--- a/main.tex
+++ b/main.tex
@@ -204,12 +204,20 @@ The radical solution to this problem is to formally verify the complete tool, wr
 
 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.
 
-However, this could be seen as being worth it, 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.
+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.
 
 \subsection{Current testing techniques are enough}
 
 Another argument against building a verified HLS tool is that current testing techniques for these tools are good enough.  There are many internal test benches that ensure the correctness of the HLS tool, as well as equivalence checkers to ensure that the final design behaves the same as the input.
 
+However, \citet{du21_fuzzin_high_level_synth_tools}, for example, show that on average 2.5\% of randomly generated C, tailored to the specific HLS tool, end up with incorrect designs.  This means that such test cases were not present in the internal test benches used to test the tools.  In addition to that, with the increasing complexity of HLS designs, it may sometimes not be possible to run an equivalence checker on the whole design, as the state space might be too big.
+
+\subsection{Will the generated designs be fast enough?}
+
+\subsection{A Verified tool can still be flaky and fail}
+
+It is true that a verified tool is still allowed to fail at compilation time, meaning none of the correctness proofs need to hold, as no output was produced.  However, this is only a matter of putting more engineering work into the tool to make it reliable and get it to output
+
 \section{Guarantees of trusted code}
 
 There are a couple of theorems one can prove about the HLS tool once it is written in Coq.  The first, which is the most important one, is that transforming the C code into Verilog is semantics preserving, meaning the translated code will behave the same as the C code.  The following backward simulation, as initially presented in \compcert{}, shows the main property that we should want to show:
diff --git a/references.bib b/references.bib
index 42de928..b66f288 100644
--- a/references.bib
+++ b/references.bib
@@ -185,6 +185,14 @@
 	note = {(under review)}
 }
 
+@unpublished{du21_fuzzin_high_level_synth_tools,
+  author          = {Du, Zewei and Herklotz, Yann and Ramanathan, Nadesh and Wickerson, John},
+  note            = {(under review)},
+  year            = 2021,
+  url             = {https://yannherklotz.com/docs/drafts/fuzzing_hls.pdf},
+  title           = {{Fuzzing High-Level Synthesis Tools}},
+}
+
 @misc{polybench,
 	author = {Pouchet, Louis-No\"el},
 	title = {PolyBench/C: the Polyhedral Benchmark suite},