More changes to proof and text

1 files changed, 17 insertions, 0 deletions

diff --git a/proof.tex b/proof.tex
index 4926d1f..804a36a 100644
--- a/proof.tex
+++ b/proof.tex
@@ -38,6 +38,23 @@ The forward simulation between C and Verilog can be separated into forward simul
 
 \subsubsection{3AC to HTL forward simulation}
 
+\begin{figure}
+  \centering
+  \begin{tikzpicture}
+    \begin{scope}
+      \node[circle,minimum size=2] (s1) at (0,3) {$S_{1}$};
+      \node[circle,minimum size=2] (r1) at (4,3) {$R_{1}$};
+      \node[circle,minimum size=2] (s2) at (0,0) {$S_{2}$};
+      \node[circle,minimum size=2] (r2) at (4,0) {$R_{2}$};
+      \draw (s1) -- node[above] {\textasciitilde{}} node[below] {\small\texttt{match\_states}} ++ (r1);
+      \draw[-{Latex[length=3mm]}] (s1) -- (s2);
+      \draw[dashed] (s2) -- node[above] {\textasciitilde{}} node[below] {\small\texttt{match\_states}} ++ (r2);
+      \draw[-{Latex[length=3mm]},dashed] (r1) -- node[left] {+} ++ (r2);
+    \end{scope}
+  \end{tikzpicture}
+  \caption{Simulation diagram proving the correctness of the translation from 3AC to HTL.}\label{fig:simulation_diagram}
+\end{figure}
+
 As HTL is quite different to 3AC, this first translation is the most involved and therefore requires a larger proof, because the translation from 3AC instructions to Verilog statements needs to be proven correct in this step.  In addition to that, the semantics of HTL are also quite different to the 3AC semantics, as instead of defining small-step semantics for each construct in Verilog, the semantics are instead defined over one clock cycle and mirror the semantics defined for Verilog.
 
 The first step in proving the forward simulation is to define a relation that matches an 3AC state to an HTL state, which shows when the states are equivalent.  This relation also defines assumptions that are made about the 3AC code that we receive, so that these assumptions can be used to prove the translations correct.  These assumptions then have to be proven to always hold assuming the HTL code was created by the translation algorithm.  The \texttt{match\_states} predicate that is used to match the states of the 3AC code to the HTL code is shown in Figure~\ref{fig:match_states}.  The type \texttt{match\_states} declared in Figure~\ref{fig:match_states} has three constructors.