Add correctness equation

1 files changed, 11 insertions, 1 deletions

diff --git a/main.tex b/main.tex
index f43cb22..420819e 100644
--- a/main.tex
+++ b/main.tex
@@ -204,10 +204,20 @@ In this respect, we have developed our own verified HLS tool called Vericert~\ci
 
 \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
+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.
+\end{equation*}
+
+\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.
 
 \section{Performance of such a tool}
 
+Finally, it is interesting to check the performance of Vericert compared to existing HLS tools, to see how correctness guarantees affect the size and speed of the final hardware.
+
 %% Acknowledgments
 %\begin{acks}%% acks environment is optional
 %% contents suppressed with 'anonymous'