diff options
Diffstat (limited to 'verilog.tex')
| -rw-r--r-- | verilog.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/verilog.tex b/verilog.tex index e68352d..709781f 100644 --- a/verilog.tex +++ b/verilog.tex @@ -66,7 +66,7 @@ The two main evaluation functions are then \textit{erun}, which takes in the cur % \inferrule[Nonblocking Array]{\yhkeyword{name}\ \textit{lhs} = \yhkeyword{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.} \JW{The `Skip' rule has an erroneous $=$.} \JW{You could use a bit of colour here, e.g. the keywords like `if' could be coloured for readability.} \JW{The difference between `s' and `st' is hard to remember, since both are prefixes of both `state' and `statement'! It's quite common to use `$\sigma$' for states, so you might consider `$s$' and `$\sigma$' for statements and states?} \JW{The function update syntax is not familiar to me, but perhaps it is what is used in Coq? More typical would be `$\Delta[n\mapsto v]$'.} +\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 $\sigma_{0}$ to state $\sigma_{1}$. If both of these conditions hold, we then get that the conditional statement will also run from state $\sigma_{0}$ to state $\sigma_{1}$. The \textsc{Blocking} and \textsc{Nonblocking} rules are a bit more interesting, as these modify the blocking and nonblocking association maps respectively. @@ -89,6 +89,7 @@ We then define the semantics of running the module for one clock cycle in the fo \end{gather*} \YH{TODO:\@ Need to fix the last rule, as it is actually only used for a case that shouldn't ever be hit.} +\YH{TODO:\@ Explain // notation} The \textsc{Module} rule is the main rule for the execution of one clock cycle of the module. Given that the value of the $s_{t}$ register is the value of the program counter at the current instruction and that the value of the $s_{t}$ register in the resulting association map is equal to the next program counter value, we can then say that if all the module items in the body go from one state to another, that the whole module will step from that state to the other. |