diff options
| -rw-r--r-- | proof.tex | 14 | ||||
| -rw-r--r-- | verilog.tex | 2 |
2 files changed, 8 insertions, 8 deletions
@@ -112,13 +112,13 @@ The Verilog semantics that are used are deterministic, as the order of operation \toprule & \textbf{Coq code} & \textbf{OCaml code} & \textbf{Specifications} & \textbf{Theorems \& Proofs} & \textbf{Total}\\ \midrule - {Data structures and libraries} & 274 & - & - & 654 & 928 \\ - {Integers and values} & 98 & - & 15 & 744 & 857 \\ - {HTL semantics} & - & - & 174 & - & 174 \\ - {HTL generation} & 655 & - & 79 & 3349 & 4083 \\ - {Verilog semantics} & - & - & 739 & 174 & 913 \\ - {Verilog generation} & 68 & - & - & 396 & 464 \\ - {Top-level driver, pretty printers} & 89 & 747 & - & 209 & 1045 \\ + {Data structures and libraries} & 274 & --- & --- & 654 & 928 \\ + {Integers and values} & 98 & --- & 15 & 744 & 857 \\ + {HTL semantics} & --- & --- & 174 & --- & 174 \\ + {HTL generation} & 655 & --- & 79 & 3349 & 4083 \\ + {Verilog semantics} & --- & --- & 739 & 174 & 913 \\ + {Verilog generation} & 68 & --- & --- & 396 & 464 \\ + {Top-level driver, pretty printers} & 89 & 747 & --- & 209 & 1045 \\ \midrule \textbf{Total} & 1184 & 747 & 1007 & 5526 & 8464 \\ \bottomrule diff --git a/verilog.tex b/verilog.tex index ae30c9c..708ed1f 100644 --- a/verilog.tex +++ b/verilog.tex @@ -24,7 +24,7 @@ An example of a rule \JWcouldcut{in the semantics} for executing an always block \noindent which shows that assuming the statement $s$ in the always block runs with state $\Sigma$ and produces the new state $\Sigma'$, the always block will result in the same final state. As only clocked always blocks are supported, and one step in the semantics correspond to one clock cycle, it means that this rule is run once per clock cycle \NRcouldcut{which is what it is defined to do}. \NR{The mention about small steps being one cycle and 'only clocked/synchronous \alwaysblock{} are supported' can move earlier.} \JW{Actually couldn't this rule be run multiple times per clock cycle in the case where you have multiple always blocks in your module all triggered on the same rising edge?}\YH{Yes, it is run multiple times, which is controlled by the \textsc{Module} rule, which runs the always blocks sequentially. This is controlled by another big step semantics that either takes the Cons of the list and runs the left and right hand sides, or nil which returns the same state.} -Two types of assignments are supported in always blocks: nonblocking and blocking assignment. Nonblocking assignment modifies the signal at the end of the timestep \JW{Assuming `timestep' and `clock cycle' are the same, I suggest we stick with `clock cycle' everywhere.} and atomically. Blocking assignment, on the other hand, assigns the variable \NRreplace{directly}{instantaneously?} in the always block for later signals to pick up. To model both these assignments, the state $\Sigma$ has to be split into two \NRreplace{parts}{sets?}: $\Gamma$, containing the current values of all variables, and $\Delta$, containing the values that will be assigned to the variables at the end of the clock cycle, we can therefore say that $\Sigma = (\Gamma, \Delta)$.~\NR{Can we say that $\Gamma$ contains instantaneous (ephemeral) updates for the current cycle and $\Delta$ contains periodical updates for the next cycle? Will be good to distinguish those two updates with the same terms across the paper, which can tie in with small-step and big-step distinction maybe asynchronous vs synchronous updates. }\YH{Hmm, so I don't think nonblocking and blocking ties in with big-step and smallstep, but yes it would be better to use the same terms throughoug the paper} The nonblocking assignment can therefore be expressed as the following: +Two types of assignments are supported in always blocks: nonblocking and blocking assignment. Nonblocking assignment modifies the signal at the end of the clock cycle and atomically. Blocking assignment, on the other hand, assigns the variable \NRreplace{directly}{instantaneously?} in the always block for later signals to pick up. To model both these assignments, the state $\Sigma$ has to be split into two \NRreplace{parts}{sets?}: $\Gamma$, containing the current values of all variables, and $\Delta$, containing the values that will be assigned to the variables at the end of the clock cycle, we can therefore say that $\Sigma = (\Gamma, \Delta)$.~\NR{Can we say that $\Gamma$ contains instantaneous (ephemeral) updates for the current cycle and $\Delta$ contains periodical updates for the next cycle? Will be good to distinguish those two updates with the same terms across the paper, which can tie in with small-step and big-step distinction maybe asynchronous vs synchronous updates. }\YH{Hmm, so I don't think nonblocking and blocking ties in with big-step and smallstep, but yes it would be better to use the same terms throughoug the paper} The nonblocking assignment can therefore be expressed as the following: \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])}\\ |