More changes to proof and text

3 files changed, 21 insertions, 1 deletions

diff --git a/main.tex b/main.tex
index 99d32aa..1b21848 100644
--- a/main.tex
+++ b/main.tex
@@ -45,6 +45,8 @@
 \usepackage{tikz}
 \usepackage{minted}
 
+\usetikzlibrary{shapes,calc,arrows.meta}
+
 \setminted{fontsize=\small}
 \usemintedstyle{manni}
 
@@ -75,7 +77,7 @@
 
 \newcommand{\vericert}{Veri\-cert}%
 \newcommand{\compcert}{Comp\-Cert}%
-\newcommand{\legup}{LegUp}%
+\newcommand{\legup}{Leg\-Up}%
 
 \begin{document}
 
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.
diff --git a/verilog.tex b/verilog.tex
index 8cfeb85..7db80a6 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -32,6 +32,7 @@ Two types of assignments are supported in always blocks: nonblocking and blockin
 
 \noindent where assuming that $\downarrow_{\text{expr}}$ evaluates an expression $e$ to a value $v$, then the nonblocking assignment $d\ \yhkeyword{ <= } e$ will update the future state of the variable $d$ with value $v$.  Finally, at the end of the clock cycle, the registers need to be updated with their future values in $\Delta$, which can be shown by the rule in the semantics that runs a whole module, $\vec{m}$ is a list of variable declarations and always blocks, and the $\downarrow_{\vec{m}}$ evaluates these sequentially and obtains the final state $(\Gamma', \Delta')$. \JW{I'm a little torn. On the one hand, this is interesting stuff, and I almost want to suggest putting in the `Blocking Reg' rule alongside the one above, because seeing the rules side-by-side makes it really clear how they both work. But I'm conscious that talking about the distinction between non-blocking and blocking assignments is all a bit moot because Vericert never produces blocking assignments (right?). And this text is all just explaining Loow's work, not your own work. So, in short, I'm a bit torn. Probably best to keep it as-is for now, but bear this in mind as a candidate for chopping nearer the deadline. What do yout think?}
 
+
 \begin{equation*}
   \inferrule[Module]{(\Gamma, \epsilon, \vec{m})\ \downarrow_{\vec{m}} (\Gamma', \Delta')}{(\Gamma, \yhkeyword{module } \yhconstant{main} \yhkeyword{(...);}\ \vec{m}\ \yhkeyword{endmodule}) \downarrow_{m} (\Gamma' // \Delta')}
 \end{equation*}