diff options
| -rw-r--r-- | verilog.tex | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/verilog.tex b/verilog.tex index d8ee140..7227ce8 100644 --- a/verilog.tex +++ b/verilog.tex @@ -25,10 +25,12 @@ Two types of assignments are supported in always blocks: nonblocking and blockin \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')} +\inferrule[Module]{\Gamma\ !\ \sigma = \yhconstant{Some } v_{\sigma} \\ (m_{i}, \Gamma, \epsilon)\ \longrightarrow_{\vec{m}} (m_{i}, \Gamma', \Delta') \\ (\Gamma' // \Delta')\ !\ \sigma = \yhconstant{Some } +v_{\sigma}'}{\yhconstant{State } \textit{sf }\ m\ v_{\sigma}\ \Gamma \longrightarrow \yhconstant{State } \textit{sf }\ m\ v_{\sigma}'\ (\Gamma' // \Delta')} \end{equation*} +This rule describes how the top-level \texttt{State} used in the + 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. \subsection{Changes to the Semantics} |