summaryrefslogtreecommitdiffstats
path: root/verilog.tex
diff options
context:
space:
mode:
authorJohn Wickerson <j.wickerson@imperial.ac.uk>2020-11-17 20:44:25 +0000
committeroverleaf <overleaf@localhost>2020-11-17 20:44:30 +0000
commit0f26740e1474d6b1bdf1b2a2d6ea9a20f8fa2eee (patch)
tree7d13c0b30083fd9af9ce0debecbd5f3c8e8c46dc /verilog.tex
parent03649c6d6f4d4dd0c06d5ca96451757a55bafe4a (diff)
downloadoopsla21_fvhls-0f26740e1474d6b1bdf1b2a2d6ea9a20f8fa2eee.tar.gz
oopsla21_fvhls-0f26740e1474d6b1bdf1b2a2d6ea9a20f8fa2eee.zip
Update on Overleaf.
Diffstat (limited to 'verilog.tex')
-rw-r--r--verilog.tex1
1 files changed, 0 insertions, 1 deletions
diff --git a/verilog.tex b/verilog.tex
index 355b91c..8315062 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -13,7 +13,6 @@ The semantics of Verilog differs from regular programming languages, as it is us
A module can contain multiple always blocks, all of which 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. \JW{That sentence is a bit wordy. Can you just say something like: `We support only \emph{synchronous} logic, which means that the always block is triggered on (and only on) the rising edge of a clock signal.'?}
\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.}
-
As hardware designs normally describe events that will be executed periodically for an infinite amount of time, the top-level of the semantics is best described using small-step semantics, whereas the execution of one small step is described using big-step semantics. An example of a rule in the semantics for executing an always block is shown below, where $\Sigma$ is the state of the registers in the module and $s$ is the statement inside the always block:
\begin{equation*}