Add commands for compcert and vericert

1 files changed, 5 insertions, 5 deletions

diff --git a/main.tex b/main.tex
index 2c7620e..08b977f 100644
--- a/main.tex
+++ b/main.tex
@@ -147,7 +147,7 @@
 \begin{abstract}
   High-level synthesis (HLS) is increasingly being relied upon as the size of designs and needs for hardware accelerators increases.  However, HLS is known to be quite flaky with each tool supporting different input languages and sometimes generating incorrect designs.
 
-  A formally verified HLS tool would solve these issues by dramatically reducing the amount of trusted code, and providing a formal description of the input language that is supported.  In this respect, we have developed Vericert, a formally verified HLS tool, based on CompCert, a formally verified C compiler.
+  A formally verified HLS tool would solve these issues by dramatically reducing the amount of trusted code, and providing a formal description of the input language that is supported.  In this respect, we have developed \vericert{}, a formally verified HLS tool, based on \compcert{}, a formally verified C compiler.
 \end{abstract}
 
 %% 2012 ACM Computing Classification System (CSS) concepts
@@ -200,13 +200,13 @@ The standard methods for checking the outputs of the HLS tools are the following
 
 \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.  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.
+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.
+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, 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:
+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:
 
 \begin{equation*}
   \forall C, V, B \in \texttt{Safe},\, \yhfunction{hls} (C) = \yhconstant{OK} (V) \land V \Downarrow B \implies C \Downarrow B.
@@ -214,7 +214,7 @@ There are a couple of theorems one can prove about the HLS tool once it is writt
 
 \noindent Given a \textit{safe} behaviour $B$, meaning it does not contain undefined behaviour, we want to show that if the translation from C to Verilog succeeded, that executing the Verilog program with that behaviour implies that the C code will execute with the same behaviour.
 
-However, there are also assumptions that have to be made about the tool.  In the case of Vericert, the only assumption that needs to be made is if the C semantics and Verilog semantics can be trusted.  This is much simpler than checking that the translation algorithm is implemented properly.  Using that assumption, the proofs ensure that the translation preserves the behaviour and doesn't need to be trusted.
+However, there are also assumptions that have to be made about the tool.  In the case of \vericert{}, the only assumption that needs to be made is if the C semantics and Verilog semantics can be trusted.  This is much simpler than checking that the translation algorithm is implemented properly.  Using that assumption, the proofs ensure that the translation preserves the behaviour and doesn't need to be trusted.
 
 \section{Performance of such a tool}