Add other inference rules

1 files changed, 19 insertions, 20 deletions

diff --git a/main.tex b/main.tex
index 5e65db1..f7a6e72 100644
--- a/main.tex
+++ b/main.tex
@@ -189,59 +189,58 @@
 
 \section{Verilog Semantics}
 
+Definition of state.
+
+\begin{equation}
+  \label{eq:10}
+  s = (\Gamma, \Delta)
+\end{equation}
+
 Definition of stmntrun.
 
 \begin{equation}
   \label{eq:1}
-  \inferrule[Skip]{ }{\text{stmntrun}\ f\ a\ \mathtt{Vskip}\ a}
+  \inferrule[Skip]{ }{\text{stmntrun}\ f\ s\ \mathtt{Vskip}\ s}
 \end{equation}
 
 \begin{equation}
-  \label{eq:2}
-  \inferrule[CondTrue]{\text{exprrun}\ f\ \Delta\ c\ vc \\ \text{valToB}\ vc = \text{true} \\
-  \text{stmntrun}\ f\ as0\ stt\ as1}{\text{stmntrun}\ f\ as0\ (\mathtt{Vcond}\ c\ stt\ stf)\ as1}
+  \label{eq:4}
+  \inferrule[Seq]{\text{stmntrun}\ f\ s_{0}\ \mathit{st}_{1}\ s_{1} \\ \text{stmntrun}\ f\ s_{1}\ \mathit{st}_{2}\ s_{2}}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vseq}\ \mathit{st}_{1}\ \mathit{st}_{2})\ s_{2}}
 \end{equation}
 
 \begin{equation}
-  \label{eq:3}
-  \inferrule[CondFalse]{\text{exprrun}\ f\ \Delta\ c\ vc \\ \text{valToB}\ vc = \text{false} \\
-  \text{stmntrun}\ f\ as0\ stf\ as1}{\text{stmntrun}\ f\ as0\ (\mathtt{Vcond}\ c\ stt\ stf)\ as1}
+  \label{eq:2}
+  \inferrule[CondTrue]{\text{exprrun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \text{valToB}\ v_{c} = \mathtt{true} \\ \text{stmntrun}\ f\ s_{0}\ \mathit{stt}\ s_{1}}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf})\ s_{1}}
 \end{equation}
 
 \begin{equation}
-  \label{eq:4}
-  \inferrule[Seq]{\text{stmntrun}\ f\ as0\ st1\ as1 \\ \text{stmntrun}\ f\ as1\ st2\ as2}{
-  \text{stmntrun}\ f\ as0\ (\mathtt{Vseq}\ st1\ st2)\ as2}
+  \label{eq:3}
+  \inferrule[CondFalse]{\text{exprrun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \text{valToB}\ v_{c} = \mathtt{false} \\ \text{stmntrun}\ f\ s_{0}\ \mathit{stf}\ s_{1}}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf})\ s_{1}}
 \end{equation}
 
 \begin{equation}
   \label{eq:5}
-  \inferrule[CaseNoMatch]{\text{stmntrun}\ f\ as0\ (\mathtt{Vcase}\ e\ cs\ def)\ as1 \\ \text{exprrun}\ f\ \Delta_{0}\ me\ mve
-    \\ \text{exprrun}\ f\ \Delta_{0}\ e\ ve \\ mve \neq ve}{
-    \text{stmntrun}\ f\ as0\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ def)\ as1}
+  \inferrule[CaseNoMatch]{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ cs\ def)\ s_{1} \\ \text{exprrun}\ f\ \Gamma_{0}\ me\ mve \\ \text{exprrun}\ f\ \Gamma_{0}\ e\ ve \\ mve \neq ve}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ def)\ s_{1}}
 \end{equation}
 
 \begin{equation}
   \label{eq:6}
-  \inferrule[CaseMatch]{\text{stmntrun}\ f\ as0\ sc\ as1 \\ \text{exprrun}\ f\ \Delta_{0}\ e\ ve
-    \\ \text{exprrun}\ f\ \Delta_{0}\ me\ mve \\ mve = ve}{
-    \text{stmntrun}\ f\ as0\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ def)\ as1}
+  \inferrule[CaseMatch]{\text{stmntrun}\ f\ s_{0}\ sc\ s_{1} \\ \text{exprrun}\ f\ \Gamma_{0}\ e\ ve \\ \text{exprrun}\ f\ \Gamma_{0}\ me\ mve \\ mve = ve}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ def)\ s_{1}}
 \end{equation}
 
 \begin{equation}
   \label{eq:7}
-  \inferrule[CaseDefault]{\text{exprrun}\ f\ \Delta_{0}\ e ve \\ \text{stmntrun}\ f\ as0\ st\ as1}{
-  \text{stmntrun}\ f\ as0\ (\mathtt{Vcase}\ e\ []\ (\mathtt{Some}\ st))\ as1}
+  \inferrule[CaseDefault]{\text{exprrun}\ f\ \Gamma_{0}\ e\ ve \\ \text{stmntrun}\ f\ s_{0}\ st\ s_{1}}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ []\ (\mathtt{Some}\ st))\ s_{1}}
 \end{equation}
 
 \begin{equation}
   \label{eq:8}
-  \inferrule[Blocking]{}{x}
+  \inferrule[Blocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{exprrun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}} \\ \Gamma' = \Gamma ! n \rightarrow v_{\mathit{rhs}}}{\text{stmntrun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vblock}\ \mathit{lhs}\ \mathit{rhs})\ (\Gamma', \Delta)}
 \end{equation}
 
 \begin{equation}
   \label{eq:9}
-  \inferrule[Nonblocking]{}{x}
+  \inferrule[Nonblocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{exprrun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}} \\ \Delta' = \Delta ! n \rightarrow v_{\mathit{rhs}}}{\text{stmntrun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vnonblock}\ \mathit{lhs}\ \mathit{rhs})\ (\Gamma, \Delta')}
 \end{equation}
 
 %% Acknowledgments