From 0c5b604c798ae1ff7fd8f157c30d2253b784eeac Mon Sep 17 00:00:00 2001 From: Yann Herklotz 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