diff options
-rw-r--r-- | main.tex | 58 |
1 files changed, 53 insertions, 5 deletions
@@ -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 |