Add downarrow instead of longrightarrow

1 files changed, 5 insertions, 5 deletions

diff --git a/verilog.tex b/verilog.tex
index 8e13218..0694b20 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -18,7 +18,7 @@ As hardware designs normally describe events that will be executed periodically
 An example of a rule in the semantics for executing an always block is shown below, where $\Sigma$ is the state of the registers in the module and $s$ is the statement inside the always block: \JW{Switch $\rightarrow$ for $\Downarrow$ in big-step semantics.}
 
 \begin{equation*}
-  \inferrule[Always]{(\Sigma, s)\longrightarrow_{\text{stmnt}} \Sigma'}{(\Sigma, \yhkeyword{always @(posedge clk) } s) \longrightarrow_{\text{always}} \Sigma'}
+  \inferrule[Always]{(\Sigma, s)\downarrow_{\text{stmnt}} \Sigma'}{(\Sigma, \yhkeyword{always @(posedge clk) } s) \downarrow_{\text{always}} \Sigma'}
 \end{equation*}
 
 \noindent which shows that assuming the statement $s$ in the always block runs with state $\Sigma$ and produces the new state $\Sigma'$, the always block will result in the same final state.  As only clocked always blocks are supported, and one step in the semantics correspond to one clock cycle, it means that this rule is run once per clock cycle \NRcouldcut{which is what it is defined to do}.
@@ -27,13 +27,13 @@ An example of a rule in the semantics for executing an always block is shown bel
 Two types of assignments are supported in always blocks: nonblocking and blocking assignment.  Nonblocking assignment modifies the signal at the end of the timestep and atomically.  Blocking assignment, on the other hand, assigns the variable \NRreplace{directly}{instantaneously?} in the always block for later signals to pick up.  To model both these assignments, the state $\Sigma$ has to be split into two \NRreplace{parts}{sets?}: $\Gamma$, containing the current values of all variables, and $\Delta$, containing the values that will be assigned to the variables at the end of the clock cycle, we can therefore say that $\Sigma = (\Gamma, \Delta)$.~\NR{Can we say that $\Gamma$ contains instantaneous (ephemeral) updates for the current cycle and $\Delta$ contains periodical updates for the next cycle? Will be good to distinguish those two updates with the same terms across the paper, which can tie in with small-step and big-step distinction maybe asynchronous vs synchronous updates. }  The nonblocking assignment can therefore be expressed as the following:
 
 \begin{equation*}
-  \inferrule[Nonblocking Reg]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \longrightarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ <= } e) \longrightarrow_{\text{stmnt}} (\Gamma, \Delta [n \mapsto v])}\\
+  \inferrule[Nonblocking Reg]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \downarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ <= } e) \downarrow_{\text{stmnt}} (\Gamma, \Delta [n \mapsto v])}\\
 \end{equation*}
 
-\noindent where assuming that $\longrightarrow_{\text{expr}}$ evaluates an expression $e$ to a value $v$, then the nonblocking assignment $d\ \yhkeyword{ <= } e$ will update the future state of the variable $d$ with value $v$.  Finally, at the end of the clock cycle, the registers need to be updated with their future values in $\Delta$, which can be shown by the rule in the semantics that runs a whole module, $\vec{m}$ is a list of variable declarations and always blocks, and the $\longrightarrow_{\vec{m}}$ evaluates these sequentially and obtains the final state $(\Gamma', \Delta')$.
+\noindent where assuming that $\downarrow_{\text{expr}}$ evaluates an expression $e$ to a value $v$, then the nonblocking assignment $d\ \yhkeyword{ <= } e$ will update the future state of the variable $d$ with value $v$.  Finally, at the end of the clock cycle, the registers need to be updated with their future values in $\Delta$, which can be shown by the rule in the semantics that runs a whole module, $\vec{m}$ is a list of variable declarations and always blocks, and the $\down_{\vec{m}}$ evaluates these sequentially and obtains the final state $(\Gamma', \Delta')$.
 
 \begin{equation*}
-  \inferrule[Module]{(\Gamma, \epsilon, \vec{m})\ \longrightarrow_{\vec{m}} (\Gamma', \Delta')}{(\Gamma, \yhkeyword{module } \yhconstant{main} \yhkeyword{(...);}\ \vec{m}\ \yhkeyword{endmodule}) \longrightarrow_{m} (\Gamma' // \Delta')}
+  \inferrule[Module]{(\Gamma, \epsilon, \vec{m})\ \downarrow_{\vec{m}} (\Gamma', \Delta')}{(\Gamma, \yhkeyword{module } \yhconstant{main} \yhkeyword{(...);}\ \vec{m}\ \yhkeyword{endmodule}) \downarrow_{m} (\Gamma' // \Delta')}
 \end{equation*}
 
 \noindent This rule dictates how the whole module runs in one clock cycle, from an initial state of all the variables $\Gamma$, to a final state $(\Gamma' // \Delta')$, where $//$ defines a merge between the two maps from variable names to values, where the right hand side values take priority if there is a conflict.  This rule correctly implements the behaviours for the blocking and nonblocking assignment by overwriting the assignments made through blocking assignment at the end of the clock cycle with the atomic assignments from the nonblocking assignments.
@@ -65,7 +65,7 @@ In addition to adding support for two-dimensional arrays, support for receiving
   \centering
   \begin{minipage}{1.0\linewidth}
     \begin{gather*}
-      \inferrule[Step]{\Gamma\ !\ \textit{rst} = \yhconstant{Some } 0 \\ \Gamma\ !\ \textit{fin} = \yhconstant{Some } 0 \\ \Gamma\ !\ \sigma = \yhconstant{Some } v \\ (m, \Gamma)\ \longrightarrow_{m} \Gamma' \\ \Gamma'\ !\ \sigma = \yhconstant{Some } v'}{\yhconstant{State } \textit{sf }\ m\ v\ \Gamma \longrightarrow \yhconstant{State } \textit{sf }\ m\ v'\ \Gamma'}\\
+      \inferrule[Step]{\Gamma\ !\ \textit{rst} = \yhconstant{Some } 0 \\ \Gamma\ !\ \textit{fin} = \yhconstant{Some } 0 \\ \Gamma\ !\ \sigma = \yhconstant{Some } v \\ (m, \Gamma)\ \downarrow_{m} \Gamma' \\ \Gamma'\ !\ \sigma = \yhconstant{Some } v'}{\yhconstant{State } \textit{sf }\ m\ v\ \Gamma \longrightarrow \yhconstant{State } \textit{sf }\ m\ v'\ \Gamma'}\\
       %
       \inferrule[Finish]{\Gamma\ !\ \textit{fin} = \yhconstant{Some } 1 \\ \Gamma\ !\ \textit{ret} = \yhconstant{Some } r}{\yhconstant{State } \textit{sf }\ m\ \sigma\ \Gamma \longrightarrow \yhconstant{Returnstate } \textit{sf }\ r}\\
       %