diff options
| -rw-r--r-- | verilog.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/verilog.tex b/verilog.tex index e16a524..2ac4f12 100644 --- a/verilog.tex +++ b/verilog.tex @@ -12,7 +12,7 @@ A module can contain multiple \alwaysblock{}s, all of which run in parallel. Th %\NR{We should mention that variables cannot be driven by multiple \alwaysblock{}s, since one might get confused with data races when relating to concurrent processes in software.} \JW{Given the recent discussion on Teams, it seems to me that we perhaps don't need to mention here what happens if a variable is driven multiple times per clock cycle, especially since Vericert isn't ever going to do that.} The semantics combines the big-step and small-step styles. The overall execution of the hardware is described using a small-step semantics, with one small step per clock cycle; this is appropriate because hardware is routinely designed to run for an unlimited number of clock cycles and the big-step style is ill-suited to describing infinite executions. Then, within each clock cycle, a big-step semantics is used to execute all the statements. -An example of a rule for executing an \alwaysblock{} is shown below, where $\Sigma$ is the state of the registers in the module and $s$ is the statement inside the \alwaysblock{}: +An example of a rule for executing an \alwaysblock{} that is triggered at the positive edge of the clock is shown below, where $\Sigma$ is the state of the registers in the module and $s$ is the statement inside the \alwaysblock{}: \begin{equation*} \inferrule[Always]{(\Sigma, s)\downarrow_{\text{stmnt}} \Sigma'}{(\Sigma, \yhkeyword{always @(posedge clk) } s) \downarrow_{\text{always}^{+}} \Sigma'} |