Small clarifications in proof

1 files changed, 3 insertions, 3 deletions

diff --git a/proof.tex b/proof.tex
index 19d21d5..4f58746 100644
--- a/proof.tex
+++ b/proof.tex
@@ -4,7 +4,7 @@ Now that the Verilog semantics have been adapted to the CompCert model, we are i
 
 \subsection{Main Challenges in the Proof}
 
-The proof of correctness of the Verilog back end is quite different from the usual proofs performed in CompCert, mainly because of the difference in Verilog semantics compared to the standard CompCert intermediate languages and because of the translation of the memory model.
+The proof of correctness of the Verilog back end is quite different from the usual proofs performed in CompCert, mainly because of the difference in the memory model and because of the difference in Verilog's semantics compared to the semantics of standard CompCert intermediate languages.
 
 \begin{itemize}
 \item As already mentioned in Section~\ref{sec:verilog:memory}, because the memory model in our Verilog semantics is finite and concrete, but the CompCert memory model is more abstract and infinite with additional bounds, the equivalence of both these models needs to be proven.  Moreover, our memory is word-addressed for efficiency reasons, whereas CompCert's memory is byte-addressed.
@@ -18,7 +18,7 @@ Together, these differences mean that translating 3AC directly to Verilog is inf
 
 \subsection{Formulating the Correctness Theorem}
 
-The main correctness theorem is analogous to that stated in \compcert{}~\cite{leroy09_formal_verif_realis_compil}: for all Clight source programs $C$, if the translation to the target Verilog code succeeds, and $C$ has safe observable behaviour $B$ when executed, then the target Verilog code will have the same behaviour $B$. Here, a `safe' execution is one that either converges or diverges, but does not `go wrong'. If the program does admit some wrong behaviour (such as undefined behaviour in C), the correctness theorem does not apply. A behaviour, then, is either a final state (in the case of convergence) or divergence. In \compcert{}, a behaviour is also associated with a trace of I/O events, but since external function calls are not supported in \vericert{}, this trace will always be empty.  
+The main correctness theorem is analogous to that stated in \compcert{}~\cite{leroy09_formal_verif_realis_compil}: for all Clight source programs $C$, if the translation to the target Verilog code succeeds, and $C$ has a safe observable behaviour $B$ when executed, then the target Verilog code will have the same behaviour $B$. Here, a `safe' execution is one that either converges or diverges, but does not `go wrong'. If the program does admit some wrong behaviour (such as undefined behaviour in C), the correctness theorem does not apply. A safe behaviour, then, is either a final state (in the case of convergence) or divergent. In \compcert{}, a behaviour is also associated with a trace of I/O events, but since external function calls are not supported in \vericert{}, this trace will always be empty.
 
 %This correctness theorem is also appropriate for HLS, as HLS is often used as a part of a larger hardware design that is connected together using a hardware description language like Verilog.  This means that HLS designs are normally triggered multiple times and results are returned each time when the computation terminates, which is the property that the correctness theorem states.
 
@@ -33,7 +33,7 @@ The main correctness theorem is analogous to that stated in \compcert{}~\cite{le
   \end{equation*}
 \end{theorem}
 
-Why is this correctness theorem also the right one for HLS? It could be argued that hardware inherently runs forever and therefore does not produce a definitive final result.  This would mean that the \compcert{} correctness theorem would likely not help with proving that the hardware is actually working correctly, as the behaviour would always be divergent.  However, in practice, HLS does not normally produce the top-level of the design that needs to connect to other components and would therefore need to run forever.  Rather, HLS often produces smaller components that take an input, execute, and then terminate with an answer.  To start the execution of the hardware and to signal to the HLS component that the inputs are ready, the $\mathit{rst}$ signal is set and unset.  Then, once the result is ready, the $\mathit{fin}$ signal is set and the result value is placed in $\mathit{ret}$.  These signals are also present in the semantics of execution shown in Fig.~\ref{fig:inference_module}.  The correctness theorem therefore also uses these signals, and the proof shows that once the $\mathit{fin}$ flag is set, the value in $\mathit{ret}$ is correct according to the semantics of Verilog and Clight.  Note that the compiler is allowed to fail and not produce any output; the correctness theorem only applies when the translation succeeds.
+Why is this correctness theorem also the right one for HLS? It could be argued that hardware inherently runs forever and therefore does not produce a definitive final result.  This would mean that the \compcert{} correctness theorem would likely not help with proving that the hardware is actually working correctly, as the behaviour would always be divergent.  However, in practice, HLS does not normally produce the top-level of the design that needs to connect to other components, therefore needing to run forever.  Rather, HLS often produces smaller components that take an input, execute, and then terminate with an answer.  To start the execution of the hardware and to signal to the HLS component that the inputs are ready, the $\mathit{rst}$ signal is set and unset.  Then, once the result is ready, the $\mathit{fin}$ signal is set and the result value is placed in $\mathit{ret}$.  These signals are also present in the semantics of execution shown in Fig.~\ref{fig:inference_module}.  The correctness theorem therefore also uses these signals, and the proof shows that once the $\mathit{fin}$ flag is set, the value in $\mathit{ret}$ is correct according to the semantics of Verilog and Clight.  Note that the compiler is allowed to fail and not produce any output; the correctness theorem only applies when the translation succeeds.
 
 How can we prove this theorem? First, note that the theorem is a `backwards simulation' result (every target behaviour must also be a source behaviour), following the terminology used in the \compcert{} literature~\cite{leroy09_formal_verif_realis_compil}. The reverse direction (every source behaviour must also be a target behaviour) is not demanded because compilers are permitted to resolve any non-determinism present in their source programs. However, since Clight programs are all deterministic, as are the Verilog programs in the fragment we consider, we can actually reformulate the correctness theorem above as a forwards simulation result (following standard \compcert{} practice), which makes it easier to prove.