From 619ab60893cbd1377120de3c22a006a9df7d058a Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 13 Apr 2021 20:05:46 +0100
Subject: Add to verilog

---
 verilog.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'verilog.tex')

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'}
-- 
cgit 

