Add more to the verilog section

1 files changed, 34 insertions, 24 deletions

diff --git a/verilog.tex b/verilog.tex
index 3529866..d4954d7 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -15,8 +15,8 @@ The Verilog semantics are based on the semantics proposed by \citet{loow19_verif
   s ::=&\; s\ \texttt{;}\ s\ |\ \texttt{;}\\[-2pt]
   |&\; \texttt{if } e \texttt{ then } s \texttt{ else } s\\[-2pt]
   |&\; \texttt{case } e\ [e : s] \texttt{ endcase}\\[-2pt]
-  |&\; e \texttt{ = } e\\[-2pt]
-  |&\; e \texttt{ <= } e\\
+  |&\; e = e\\[-2pt]
+  |&\; e \Leftarrow e\\
   d ::=&\; \texttt{[n-1:0] } r\ |\ \texttt{[n-1:0] } r \texttt{ [m-1:0]}\\
   m ::=&\ \texttt{reg } d \texttt{;}\ |\ \texttt{input wire } d \texttt{;}\ |\ \texttt{output reg } d \texttt{;}\\
 |&\; \text{\tt always @(posedge clk)}\ s
@@ -40,43 +40,53 @@ 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:
+The two main evaluation functions are then \textit{erun}, which takes in the current state together with an expression and returns a value, and \textit{srun}, which takes the current state and a statement as input, and returns the updated state.  The inductive rules defining \textit{srun} are shown below:
 
 \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})}\\
+  \label{eq:1}
+  \inferrule[Skip]{ }{\textit{srun}\ s\ \epsilon = s}\\
 %
-  \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[Seq]{\textit{srun}\ s_{0}\ \textit{st}_{1}\ s_{1} \\ \textit{srun}\ s_{1}\ \textit{st}_{2}\ s_{2}}{\textit{srun}\ s_{0}\ (\textit{st}_{1}\ \texttt{;}\ \textit{st}_{2})\ s_{2}}\\
 %
-  \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[CondTrue]{\textit{erun}\ \Gamma_{0}\ c\ v_{c} \\ \texttt{valToB}\ v_{c} = \texttt{true} \\ \textit{srun}\ s_{0}\ \textit{stt}\ s_{1}}{\textit{srun}\ s_{0}\ (\texttt{if } c \texttt{ then  } \textit{stt} \texttt{ else } \textit{stf}\,)\ s_{1}}\\
 %
-  \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.
-
-\begin{gather*}
-  \label{eq:1}
-  \inferrule[Skip]{ }{\texttt{srun}\ f\ s\ \texttt{Vskip} = s}\\
+  \inferrule[CondFalse]{\textit{erun}\ \Gamma_{0}\ c\ v_{c} \\ \texttt{valToB}\ v_{c} = \texttt{false} \\ \textit{srun}\ s_{0}\ \textit{stf}\ s_{1}}{\textit{srun}\ s_{0}\ (\texttt{if } c \texttt{ then  } \textit{stt} \texttt{ else } \textit{stf}\,)\ s_{1}}\\
 %
-  \inferrule[Seq]{\texttt{srun}\ f\ s_{0}\ \textit{st}_{1}\ s_{1} \\ \texttt{srun}\ f\ s_{1}\ \textit{st}_{2}\ s_{2}}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vseq}\ \textit{st}_{1}\ \textit{st}_{2})\ s_{2}}\\
+  \inferrule[CaseNoMatch]{\textit{srun}\ s_{0}\ (\texttt{case}\ e\ cs\ \textit{def})\ s_{1} \\ \textit{erun}\  \Gamma_{0}\ me\ mve \\ \textit{erun}\  \Gamma_{0}\ e\ ve \\ mve \neq ve}{\textit{srun}\  s_{0}\ (\texttt{case}\ e\ ((me,\ sc) :: cs)\ \textit{def})\ s_{1}}\\
 %
-  \inferrule[CondTrue]{\texttt{erun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \texttt{valToB}\ v_{c} = \texttt{true} \\ \texttt{srun}\ f\ s_{0}\ \textit{stt}\ s_{1}}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcond}\ c\ \textit{stt}\ \textit{stf}\,)\ s_{1}}\\
+  \inferrule[CaseMatch]{\textit{srun}\  s_{0}\ sc\ s_{1} \\ \textit{erun}\  \Gamma_{0}\ e\ ve \\ \textit{erun}\  \Gamma_{0}\ me\ mve \\ mve = ve}{\textit{srun}\  s_{0}\ (\texttt{case}\ e\ ((me,\ sc) :: cs)\ \textit{def})\ s_{1}}\\
 %
-  \inferrule[CondFalse]{\texttt{erun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \texttt{valToB}\ v_{c} = \texttt{false} \\ \texttt{srun}\ f\ s_{0}\ \textit{stf}\ s_{1}}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcond}\ c\ \textit{stt}\ \textit{stf}\,)\ s_{1}}\\
+  \inferrule[CaseDefault]{\textit{srun}\  s_{0}\ st\ s_{1}}{\textit{srun}\  s_{0}\ (\texttt{case}\ e\ []\ (\texttt{Some}\ st))\ s_{1}}\\
 %
-  \inferrule[CaseNoMatch]{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcase}\ e\ cs\ \textit{def})\ s_{1} \\ \texttt{erun}\ f\ \Gamma_{0}\ me\ mve \\ \texttt{erun}\ f\ \Gamma_{0}\ e\ ve \\ mve \neq ve}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcase}\ e\ ((me,\ sc) :: cs)\ \textit{def})\ s_{1}}\\
+  \inferrule[Blocking Reg]{\texttt{name}\ \textit{lhs} = \texttt{OK}\ n \\ \textit{erun}\  \Gamma_{r}\ \Gamma_{a}\ \textit{rhs}\ v_{\textit{rhs}}}{\textit{srun}\  (\Gamma_{r},\Gamma_{a},\Delta_{r},\Delta_{a})\ (\textit{lhs} = \textit{rhs})\ (\Gamma_{r} // \{n \rightarrow v_{\textit{rhs}}\}, \Gamma_{a}, \Delta_{r}, \Delta_{a})}\\
 %
-  \inferrule[CaseMatch]{\texttt{srun}\ f\ s_{0}\ sc\ s_{1} \\ \texttt{erun}\ f\ \Gamma_{0}\ e\ ve \\ \texttt{erun}\ f\ \Gamma_{0}\ me\ mve \\ mve = ve}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcase}\ e\ ((me,\ sc) :: cs)\ \textit{def})\ s_{1}}\\
+  \inferrule[Nonblocking Reg]{\texttt{name}\ \textit{lhs} = \texttt{OK}\ n \\ \textit{erun}\  \Gamma\ \textit{rhs}\ v_{\textit{rhs}}}{\textit{srun}\  (\Gamma_{r}, \Gamma_{a}, \Delta_{r}, \Delta_{a})\ (\textit{lhs} \Leftarrow \textit{rhs})\ (\Gamma_{r}, \Gamma_{a}, \Delta_{r} // \{n \rightarrow v_{\textit{rhs}}\}, \Delta_{a})}
 %
-  \inferrule[CaseDefault]{\texttt{srun}\ f\ s_{0}\ st\ s_{1}}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcase}\ e\ []\ (\texttt{Some}\ st))\ s_{1}}\\
+%  \inferrule[Blocking Array]{\texttt{name}\ \textit{lhs} = \texttt{OK}\ n \\ \textit{erun}\  \Gamma_{r}\ \Gamma_{a}\ \textit{rhs}\ v_{\textit{rhs}}}{\textit{srun}\  (\Gamma_{r},\Gamma_{a},\Delta_{r},\Delta_{a})\ (\textit{lhs} = \textit{rhs})\ (\Gamma_{r} // \{n \rightarrow v_{\textit{rhs}}\}, \Gamma_{a}, \Delta_{r}, \Delta_{a})}\\
 %
-  \inferrule[Blocking]{\texttt{name}\ \textit{lhs} = \texttt{OK}\ n \\ \texttt{erun}\ f\ \Gamma\ \textit{rhs}\ v_{\textit{rhs}}}{\texttt{srun}\ f\ (\Gamma, \Delta)\ (\texttt{Vblock}\ \textit{lhs}\ \textit{rhs})\ (\Gamma ! n \rightarrow v_{\textit{rhs}}, \Delta)}\\
+%  \inferrule[Nonblocking Array]{\texttt{name}\ \textit{lhs} = \texttt{OK}\ n \\ \textit{erun}\  \Gamma\ \textit{rhs}\ v_{\textit{rhs}}}{\textit{srun}\  (\Gamma_{r}, \Gamma_{a}, \Delta_{r}, \Delta_{a})\ (\textit{lhs} \Leftarrow \textit{rhs})\ (\Gamma_{r}, \Gamma_{a}, \Delta_{r} // \{n \rightarrow v_{\textit{rhs}}\}, \Delta_{a})}
+\end{gather*}
+
+\YH{TODO: Add rules for blocking and nonblocking assignment to arrays.}
+
+Taking the \textsc{CondTrue} rule as an example, this rule will only apply if the boolean result of running the expression results in a \texttt{true} value.  It then also states that the statement in the true branch of the conditional statement \textit{stt} runs from state $s_{0}$ to state $s_{1}$.  If both of these conditions hold, we then get that the conditional statement will also run from state $s_{0}$ to state $s_{1}$.  The \textsc{Blocking} and \textsc{Nonblocking} rules are a bit more interesting, as these modify the blocking and nonblocking association maps respectively.
+
+One main difference between these semantics and the Verilog semantics by \citet{loow19_verif_compil_verif_proces} is that there is no function for external nondeterministic effects, such as memories and inputs and outputs.  These are instead handled explicitly in the semantics by using two dimensional unpacked arrays to model memories and assuming that inputs to modules cannot change.  Another difference with these semantics is that partial updates to arrays are fully supported, due to the fact that there are two different queues for arrays and variables.  Originally, if there was a blocking assignment to an array, and then a nonblocking assignment to a different region in the array, then the blocking assignment would disappear at the end of the clock cycle.  This is because the complete array would be overwritten with the updated array in the nonblocking association maps.  However, in our semantics, only the values that were changed in the array are actually recorded in the nonblocking assignment queue, meaning once the blocking and nonblocking array association maps are merged, only the actual indices that changed with nonblocking assignment are updated in the blocking assignment map.
+
+We 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[Nonblocking]{\texttt{name}\ \textit{lhs} = \texttt{OK}\ n \\ \texttt{erun}\ f\ \Gamma\ \textit{rhs}\ v_{\textit{rhs}}}{\texttt{srun}\ f\ (\Gamma, \Delta)\ (\texttt{Vnonblock}\ \textit{lhs}\ \textit{rhs}) (\Gamma, \Delta ! n \rightarrow v_{\textit{rhs}})}\\
+  \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.
+
 \input{verilog_notes}
 
 %%% Local Variables: