Add more semantics

1 files changed, 12 insertions, 0 deletions

diff --git a/verilog.tex b/verilog.tex
index 8c1d6fa..3529866 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -40,6 +40,18 @@ We can then define how one step in the semantics looks like.  We therefore first
                                      &\mathtt{stacksize} : n\ \big\}
 \end{align*}
 
+We can then define the semantics of running the module for one clock cycle in the following way:
+
+\begin{gather*}
+  \inferrule[Module]{\Gamma_{r} ! s_{t} = \texttt{Some } v \\ (m_{i}, \Gamma_{r}^{0}, \Gamma_{a}^{0}, \epsilon, \epsilon\ l)\ \longrightarrow_{\vec{m}} (m_{i}, \Gamma_{r}^{1}, \Gamma_{a}^{1}, \Delta_{r}^{1}, \Delta_{a}^{1}) \\ (\Gamma_{r}^{1} // \Delta_{r}^{1}) ! s_{t} = \texttt{Some } v'}{\texttt{State } \textit{sf }\ m\ v\ \Gamma_{r}^{0}\ \Gamma_{a}^{0} \longrightarrow \texttt{State } \textit{sf }\ m\ v'\ (\Gamma_{r}^{1} // \Delta_{r}^{1})\ (\Gamma_{a}^{1} // \Delta_{a}^{1})}\\
+%
+  \inferrule[Finish]{\Gamma_{r}!\textit{fin} = \texttt{Some } 1 \\ \Gamma_{r}!\textit{ret} = \texttt{Some } r}{\texttt{State } \textit{sf }\ m\ s_{t}\ \Gamma_{r}\ \Gamma_{a} \longrightarrow \texttt{Returnstate } \textit{sf }\ r}\\
+%
+  \inferrule[Call]{ }{\texttt{Callstate } \textit{st }\ m\ \vec{r} \longrightarrow \texttt{State } \textit{st }\ m\ n\ (\textit{init\_params }\ \vec{r}\ a // \{s_{t} \rightarrow n\})}\\
+%
+  \inferrule[Return]{ }{\texttt{Returnstate } (\texttt{Stackframe } r\ m\ \textit{pc }\ \Gamma_{r}\ \Gamma_{a} :: \textit{sf}) \longrightarrow \texttt{State } \textit{sf }\ m\ \textit{pc }\ (\Gamma_{r} // \{ \textit{st} \rightarrow \textit{pc}, r \rightarrow i \})\ \epsilon}
+\end{gather*}
+
 The top level structure of a Verilog module consists of a list of module items $\vec{m}$.  These are then executed sequentially while changing the associations of all the variables.  We can define a function \textit{mis\_step}, which steps through all of the module items and executes them.
 
 Definition of stmntrun.