Figure -> Fig.

1 files changed, 3 insertions, 3 deletions

diff --git a/proof.tex b/proof.tex
index 6446c9b..19d21d5 100644
--- a/proof.tex
+++ b/proof.tex
@@ -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 Figure~\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 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.
 
 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.
 
@@ -143,7 +143,7 @@ We can now define the simulation diagram for the translation. The 3AC state can
   \caption{Specification for the memory implementation in HTL, where $r$ is the RAM, which is then implemented by equivalent Verilog code.}\label{fig:htl_ram_spec}
 \end{figure}
 
-HTL can only represent a single state machine, it is therefore necessary to model the RAM abstractly to reason about the correctness of replacing the direct read and writes to the array by loads and stores to a RAM.  The specification used to model the RAM is shown in Figure~\ref{fig:htl_ram_spec}, which defines how the RAM $r$ will behave for all the possible combinations of the input signals.
+HTL can only represent a single state machine, it is therefore necessary to model the RAM abstractly to reason about the correctness of replacing the direct read and writes to the array by loads and stores to a RAM.  The specification used to model the RAM is shown in Fig.~\ref{fig:htl_ram_spec}, which defines how the RAM $r$ will behave for all the possible combinations of the input signals.
 
 \subsubsection{From Implementation to Specification}
 
@@ -207,7 +207,7 @@ The final lemma we need is that the Verilog we generate is deterministic. This r
 \end{lemma}
 
 \begin{proof}[Proof sketch]
-  The Verilog semantics is deterministic because the order of operation of all the constructs is defined, and there is therefore only one way to evaluate the module and hence only one possible behaviour. This was proven for the small-step semantics shown in Figure~\ref{fig:inference_module}.
+  The Verilog semantics is deterministic because the order of operation of all the constructs is defined, and there is therefore only one way to evaluate the module and hence only one possible behaviour. This was proven for the small-step semantics shown in Fig.~\ref{fig:inference_module}.
 \end{proof}
 
 %\subsection{Coq Mechanisation}