diff options
Diffstat (limited to 'verilog.tex')
| -rw-r--r-- | verilog.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/verilog.tex b/verilog.tex index b672145..cdcbe10 100644 --- a/verilog.tex +++ b/verilog.tex @@ -25,7 +25,7 @@ The main addition to the Verilog syntax is the explicit declaration of inputs an \subsection{Semantics} -An existing operational semantics for Verilog~\cite{loow19_verif_compil_verif_proces} was adapted for the semantics of the language that Vericert eventually targets. This semantics is a small-step operational semantics at the clock cycle level, as hardware typically does not terminate in any way, however, within each clock cycle the semantics are constructed in a big-step style semantics. This style of semantics matches the small-step operational semantics of \compcert{}'s register transfer language (RTL) quite well. +An existing operational semantics for Verilog~\cite{loow19_verif_compil_verif_proces} was adapted for the semantics of the language that Vericert eventually targets. This semantics is a small-step operational semantics at the clock cycle level, as hardware typically does not terminate in any way, however, within each clock cycle the semantics are constructed in a big-step style semantics. This style of semantics matches the small-step operational semantics of \compcert{}'s three address code (3AC) quite well. %~\NR{So the semantics does not support combinational always blocks or assignments?}\YH{Currently not, as they are not needed.} %~\NR{Does the semantics also enforce that variables can only be modified within one always block (multiple drivers not allowed)? PL community might think of data races. }\YH{Will add that.} |