Finish verilog section

1 files changed, 14 insertions, 7 deletions

diff --git a/verilog.tex b/verilog.tex
index 3380209..3db85fc 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -55,13 +55,13 @@ In addition to adding support for two-dimensional arrays, support for receiving
   \centering
   \begin{minipage}{1.0\linewidth}
     \begin{gather*}
-      \inferrule[Module]{\Gamma_{r} ! s_{t} = \yhconstant{Some } v \\ (m, \Gamma_{r}^{0}, \Gamma_{a}^{0}, \epsilon, \epsilon\ l)\ \longrightarrow_{m} (m_{i}, \Gamma_{r}^{1}, \Gamma_{a}^{1}, \Delta_{r}^{1}, \Delta_{a}^{1}) \\ (\Gamma_{r}^{1}\ //\ \Delta_{r}^{1}) ! s_{t} = \yhconstant{Some } v'}{\yhconstant{State } \textit{sf }\ m\ v\ \Gamma_{r}^{0}\ \Gamma_{a}^{0} \longrightarrow \yhconstant{State } \textit{sf }\ m\ v'\ (\Gamma_{r}^{1}\ //\ \Delta_{r}^{1})\ (\Gamma_{a}^{1}\ //\ \Delta_{a}^{1})}\\
+      \inferrule[Step]{\Gamma\ !\ \textit{rst} = \yhconstant{Some } 0 \\ \Gamma\ !\ \textit{fin} = \yhconstant{Some } 0 \\ \Gamma\ !\ \sigma = \yhconstant{Some } v \\ (m, \Gamma)\ \longrightarrow_{m} \Gamma' \\ \Gamma'\ !\ \sigma = \yhconstant{Some } v'}{\yhconstant{State } \textit{sf }\ m\ v\ \Gamma \longrightarrow \yhconstant{State } \textit{sf }\ m\ v'\ \Gamma'}\\
       %
-      \inferrule[Finish]{\Gamma_{r}!\textit{fin} = \yhconstant{Some } 1 \\ \Gamma_{r}!\textit{ret} = \yhconstant{Some } r}{\yhconstant{State } \textit{sf }\ m\ s_{t}\ \Gamma_{r}\ \Gamma_{a} \longrightarrow \yhconstant{Returnstate } \textit{sf }\ r}\\
+      \inferrule[Finish]{\Gamma\ !\ \textit{fin} = \yhconstant{Some } 1 \\ \Gamma\ !\ \textit{ret} = \yhconstant{Some } r}{\yhconstant{State } \textit{sf }\ m\ \sigma\ \Gamma \longrightarrow \yhconstant{Returnstate } \textit{sf }\ r}\\
       %
-      \inferrule[Call]{ }{\yhconstant{Callstate } \textit{sf }\ m\ \vec{r} \longrightarrow \yhconstant{State } \textit{sf }\ m\ n\ (\yhfunction{init\_params}\ \vec{r}\ a\ //\ \{s_{t} \rightarrow n\})}\\
+      \inferrule[Call]{ }{\yhconstant{Callstate } \textit{sf }\ m\ \vec{r} \longrightarrow \yhconstant{State } \textit{sf }\ m\ n\ ((\yhfunction{init\_params}\ \vec{r}\ a)[\sigma \mapsto n, \textit{fin} \mapsto 0, \textit{rst} \mapsto 0])}\\
       %
-      \inferrule[Return]{ }{\yhconstant{Returnstate } (\yhconstant{Stackframe } r\ m\ \textit{pc }\ \Gamma_{r}\ \Gamma_{a} :: \textit{sf}) \longrightarrow \yhconstant{State } \textit{sf }\ m\ \textit{pc }\ (\Gamma_{r}\ //\ \{ \textit{st} \rightarrow \textit{pc}, r \rightarrow i \})\ \epsilon}
+      \inferrule[Return]{ }{\yhconstant{Returnstate } (\yhconstant{Stackframe } r\ m\ \textit{pc }\ \Gamma :: \textit{sf}) \longrightarrow \yhconstant{State } \textit{sf }\ m\ \textit{pc }\ (\Gamma [ \textit{st} \mapsto \textit{pc}, r \mapsto i ])\ \epsilon}
     \end{gather*}
   \end{minipage}
   \caption{Inferrence rules for modules}%
@@ -80,14 +80,21 @@ However, as Verilog behaves quite differently to software programming languages,
 
 \begin{description}
   \item[program counter] First of all, the program counter needs to be modelled, which can be done using a register which keeps track of state, denoted as $\sigma$.
-  \item[function entry point] When a function is called, the entry point denotes the first instruction that will be executed, which can be modelled using a reset signal that sets the state accordingly.
+  \item[function entry point] When a function is called, the entry point denotes the first instruction that will be executed, which can be modelled using a reset signal that sets the state accordingly, denoted as $rst$.
   \item[return value] The return value can be modelled by setting a finished flag to one when the result is ready, and putting the result into a 32-bit output register, denoted as \textit{fin} and \textit{rtrn} respectively.
   \item[stack] The function stack can be modelled as a RAM using a two-dimensional array in the module, denoted as \textit{stk}.
 \end{description}
 
-Figure~\ref{fig:inferrence_module} shows the inferrence rules that convert from one state to another.  The first rule is the normal rule of execution
+Figure~\ref{fig:inferrence_module} shows the inferrence rules that convert from one state to another.  The first rule \textsc{Step} is the normal rule of execution.  Assuming that the module is not being reset, and that the finish state has not been reached yet and that the current and next state are $v$ and $v'$, and finally that the module runs from state $\Gamma$ to $\Gamma'$ using the \textsc{Module} rule, we can then define one step in the \texttt{State}.  The \textsc{Finish} rule is the rule that returns the final value of running the module and is applied when the \textit{fin} register is set.  The return value is then takeng from the \textit{ret} register.
 
-The first thing to note is that there is no step from \texttt{State} to \texttt{Callstate}, as function calls are not supported, and it is therefore impossible in our semantics to ever reach a \texttt{Callstate} except for the initial call to main.
+The first thing to note about the \textsc{Call} rule is that there is no step from \texttt{State} to \texttt{Callstate}, as function calls are not supported, and it is therefore impossible in our semantics to ever reach a \texttt{Callstate} except for the initial call to main.  The same can be said about the \textsc{Return} state rule, which will only be matched for the final return value from the main function, as there is no rule that allocates another stack frame \textit{sf} except for the initial call to main.  Therefore, in addition to the rules shown in Figure~\ref{fig:inferrence_module}, an initial state and final state need to be defined.
+
+\begin{align*}
+  \texttt{initial:}\quad &\forall P,\ \yhconstant{Callstate } []\ P.\texttt{main } []\\
+  \texttt{final:}\quad &\forall n,\ \yhconstant{Returnstate } []\ n \implies n
+\end{align*}
+
+\noindent where the initial state is defined as the \texttt{Callstate} with an empty stack frame and no arguments for the \texttt{main} function of program $P$, and the final state results in the program output of value $n$ when reaching a \texttt{Returnstate} with an empty stack frame.
 
 %%% Local Variables:
 %%% mode: latex