Add guarantees

2 files changed, 15 insertions, 3 deletions

diff --git a/main.tex b/main.tex
index 84d9c0d..f43cb22 100644
--- a/main.tex
+++ b/main.tex
@@ -194,14 +194,18 @@ The solution to both of these points is to have a formally verified high-level s
 
 \section{How to prove an HLS tool correct}
 
-The standard methods for checking the outputs of the HLS tools are the following.  First, the output could be checked by using a test bench and checking the outputs against the model.  However, this does not provide many guarantees, as many edge cases may never be tested.  Second, if testing is not rigorous enough, there has been research on checking that the generated hardware design has the same functionality as the input design, where the focus is on creating translation validators~\cite{pnueli98_trans} to prove the equivalence between the design and input code, while supporting various optimisations such as scheduling~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth} or code motion~\cite{banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}.  However, these aren't perfect solutions either, as there is no guarantee that these proofs really compose with each other.  In addition to that, these translation validation tools
+The standard methods for checking the outputs of the HLS tools are the following.  First, the output could be checked by using a test bench and checking the outputs against the model.  However, this does not provide many guarantees, as many edge cases may never be tested.  Second, if testing is not rigorous enough, there has been research on checking that the generated hardware design has the same functionality as the input design, where the focus is on creating translation validators~\cite{pnueli98_trans} to prove the equivalence between the design and input code, while supporting various optimisations such as scheduling~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth} or code motion~\cite{banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}.  However, these aren't perfect solutions either, as there is no guarantee that these proofs really compose with each other.  This means that an equivalence checker normally needs to work for the all of the translations that the HLS tool might perform, increasing the chances that it cannot check for equivalence anymore.
 
-\paragraph{How could such a tool be constructed?}
+\subsection{Construction of a realistic verified HLS tool}
 
-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.  In addition to that, recently Lutsig~\cite{loow21_lutsig}, a synthesis tool going from behavioural Verilog to a technology mapped netlist in Verilog, was also proven correct.
+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.  The reliability of formal verification in Coq 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.  In addition to that, recently Lutsig~\cite{loow21_lutsig}, a synthesis tool going from behavioural Verilog to a technology mapped netlist in Verilog, was also proven correct.
+
+In this respect, we have 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.
 
 \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
+
 \section{Performance of such a tool}
 
 %% Acknowledgments
diff --git a/references.bib b/references.bib
index 242532b..b0e661d 100644
--- a/references.bib
+++ b/references.bib
@@ -176,3 +176,11 @@
 	isbn = "978-3-540-69753-4",
 	publisher = "Springer Berlin Heidelberg"
 }
+
+@unpublished{herklotz21_formal_verif_high_level_synth,
+  author = {Herklotz, Yann and Pollard, James D. and Ramanathan, Nadesh and Wickerson, John},
+  title = {Formal Verification of High-Level Synthesis},
+  year = 2021,
+  url = {https://yannherklotz.com/docs/drafts/formal_hls.pdf},
+  note = {(under review)}
+}