Add inference rules

1 files changed, 53 insertions, 5 deletions

diff --git a/main.tex b/main.tex
index 20d415a..d475cdd 100644
--- a/main.tex
+++ b/main.tex
@@ -189,12 +189,60 @@
 
 \section{Verilog Semantics}
 
-\begin{align}
+Definition of stmntrun.
+
+\begin{equation}
   \label{eq:1}
-  \inferrule[Skip]{ }{\text{stmntrun}\ f\ a\ \text{Vskip}\ a} \\
-  \inferrule[CondTrue]{\text{exprrun}\ f\ \Delta\ c\ vc \\ \text{valToB}\ vc = \text{false} \\
-  \text{stmntrun}\ f\ as0\ stf\ as1}{\text{stmntrun}\ f\ as0\ (\text{Vcond}\ c\ stt\ stf)\ as1}
-\end{align}
+  \inferrule[Skip]{ }{\text{stmntrun}\ f\ a\ \mathtt{Vskip}\ a}
+\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}
+\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}
+\end{equation}
+
+\begin{equation}
+  \label{eq:3}
+  \inferrule[Seq]{\text{stmntrun}\ f\ as0\ st1\ as1 \\ \text{stmntrun}\ f\ as1\ st2\ as2}{
+  \text{stmntrun}\ f\ as0\ (\mathtt{Vseq}\ st1\ st2)\ as2}
+\end{equation}
+
+\begin{equation}
+  \label{eq:4}
+  \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}
+\end{equation}
+
+\begin{equation}
+  \label{eq:5}
+  \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}
+\end{equation}
+
+\begin{equation}
+  \label{eq:6}
+  \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}
+\end{equation}
+
+\begin{equation}
+  \label{eq:7}
+  \inferrule[Blocking]{}{x}
+\end{equation}
+
+\begin{equation}
+  \label{eq:7}
+  \inferrule[Nonblocking]{}{x}
+\end{equation}
 
 %% Acknowledgments
 \begin{acks}                            %% acks environment is optional