Add more to verilog section

1 files changed, 14 insertions, 3 deletions

diff --git a/verilog.tex b/verilog.tex
index 5788070..d8ee140 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -10,13 +10,24 @@ The Verilog semantics are based on the semantics proposed by \citet{loow19_verif
 
 The semantics of Verilog differ from regular programming languages, as it is used to describe hardware directly, which is inherently parallel, instead of describing an algorithm, which is often done sequentially.  The main construct in Verilog is the always block, which is construct that contains statements.  A module can contain multiple always blocks, which all run in parallel.  These always blocks further contain statements such as if-statements or assignments to variables.  Each always block also contains a list of events at which it should trigger, which could either contain signals that are assigned to other signals in that always block, or a different signal such as a clock which will trigger the always block periodically, only the latter are actually supported in our target semantics.  An example of a rule in the semantics for executing an always block in the semantics shown below, where $\Sigma$ is the state of the registers in the module and $s$ is the statement inside the always block:
 
-\begin{align*}
+\begin{equation*}
   \inferrule[Always]{(\Sigma, s)\longrightarrow_{\text{stmnt}} \Sigma'}{(\Sigma, \yhkeyword{always @(posedge clk) } s) \longrightarrow_{\text{always}} \Sigma'}
-\end{align*}
+\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 which is what it is defined to do.
 
-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 directly in the always block for later signals to pick up.  To model both these assignments, the state $\Sigma$ has to be split into two parts: $\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)$.
+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 directly in the always block for later signals to pick up.  To model both these assignments, the state $\Sigma$ has to be split into two parts: $\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)$.  The nonblocking assignment can therefore be expressed as the following:
+
+\begin{equation*}
+  \inferrule[Nonblocking Reg]{(\Gamma, e) \longrightarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ <= } e) \longrightarrow_{\text{stmnt}} (\Gamma, \Delta [d \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, where $m$ is the module definition, $m_{i}$ is a list of variable declarations or always blocks inside $m$, $\sigma$ is the register that holds the current state the module is in, who's value should correspond to the program counter in 3AC and finally \textit{sf} is the current stack frame that has to be kept track on to uniquely identify the current state.
+
+\begin{equation*}
+\inferrule[Module]{\Gamma\ !\ \sigma = \texttt{Some } v_{\sigma} \\ (m_{i}, \Gamma, \epsilon)\ \longrightarrow_{\vec{m}} (m_{i}, \Gamma', \Delta') \\ (\Gamma' // \Delta')\ !\ \sigma = \texttt{Some }
+v_{\sigma}'}{\texttt{State } \textit{sf }\ m\ v_{\sigma}\ \Gamma \longrightarrow \texttt{State } \textit{sf }\ m\ v_{\sigma}'\ (\Gamma' // \Delta')}
+\end{equation*}
 
 When targeting a hardware description language such as Verilog, it is important to be consistent between simulating the hardware and the behaviour of the synthesised result on actual hardware.  In the target Verilog semantics, only clocked always blocks are supported as these ensure that there are not mismatches between simulation and synthesis, as combinational always blocks that trigger on any change of an internal signal may behave differently in simulation or synthesis based on the order of operations.  This limitation in the semantics therefore helps keep the Verilog correct and consistent.  In addition to that, only nonblocking assignment is used in signals that are used in multiple always blocks, which stops any race conditions from occurring as all the signal updates happen deterministically.  Finally, a specific order of evaluation for the always blocks is chosen, and because of the limitations listed before, choosing an order is guaranteed to have the same behaviour as executing the always blocks in any order.