From 0c5b604c798ae1ff7fd8f157c30d2253b784eeac Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 22 Feb 2021 22:20:02 +0000
Subject: Add more

---
 main.tex | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'main.tex')

diff --git a/main.tex b/main.tex
index 571028c..f206dc3 100644
--- a/main.tex
+++ b/main.tex
@@ -194,9 +194,11 @@ 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, and a lot of the
+
 \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.  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.
+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.
 
 \section{Guarantees of trusted code}
 
-- 
cgit 

