summaryrefslogtreecommitdiffstats
path: root/verilog.tex
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-04-13 20:10:12 +0100
committerYann Herklotz <git@yannherklotz.com>2021-04-13 20:10:18 +0100
commit16b7d3d6fefaaa95b9ded5a4eb3b8536e2aed1f4 (patch)
tree20b099561fe1cc4be6c1e1ad47793e5823475795 /verilog.tex
parent619ab60893cbd1377120de3c22a006a9df7d058a (diff)
downloadoopsla21_fvhls-16b7d3d6fefaaa95b9ded5a4eb3b8536e2aed1f4.tar.gz
oopsla21_fvhls-16b7d3d6fefaaa95b9ded5a4eb3b8536e2aed1f4.zip
Add more
Diffstat (limited to 'verilog.tex')
-rw-r--r--verilog.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/verilog.tex b/verilog.tex
index 2ac4f12..b426861 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -21,7 +21,7 @@ An example of a rule for executing an \alwaysblock{} that is triggered at the po
\noindent This rule says that assuming the statement $s$ in the \alwaysblock{} runs with state $\Sigma$ and produces the new state $\Sigma'$, the \alwaysblock{} will result in the same final state. %Since only clocked \alwaysblock{} are supported, and one step in the semantics correspond to one clock cycle, it means that this rule is run once per clock cycle for each \alwaysblock{}.
Two types of assignments are supported in \alwaysblock{}s: nonblocking and blocking assignment. Nonblocking assignments all take effect simultaneously at the end of the clock cycle, %and atomically.
-while blocking assignments happen instantly so that later assignments in the clock cycle can pick them up. To model both of these assignments, the state $\Sigma$ has to be split into two maps: $\Gamma$, which contains the current values of all variables, and $\Delta$, which contains the values that will be assigned at the end of the clock cycle. %, we can therefore say that $\Sigma = (\Gamma, \Delta)$.
+while blocking assignments happen instantly so that later assignments in the clock cycle can pick them up. To model both of these assignments, the state $\Sigma$ has to be split into two maps: $\Gamma$, which contains the current values of all variables and arrays, and $\Delta$, which contains the values that will be assigned at the end of the clock cycle. %, we can therefore say that $\Sigma = (\Gamma, \Delta)$.
Nonblocking assignment can therefore be expressed as follows:
\begin{equation*}
\inferrule[Nonblocking Reg]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \downarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ <= } e) \downarrow_{\text{stmnt}} (\Gamma, \Delta [n \mapsto v])}\\