Update on Overleaf.

1 files changed, 17 insertions, 5 deletions

diff --git a/verilog.tex b/verilog.tex
index 0eef44e..d7e04bb 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -1,18 +1,30 @@
 \section{Verilog}\label{sec:verilog}
 
-This section describes the Verilog semantics that were chosen for the target language, including the changes that were made to the semantics to be a better fit as an HLS target.  The Verilog standard is quite large~\cite{06_ieee_stand_veril_hardw_descr_languag,05_ieee_stand_veril_regis_trans_level_synth}, however, the syntax and semantics can be reduced to a small subset that \vericert{} needs to target.
+\newcommand{\alwaysblock}{\texttt{always}-block}
 
-The Verilog semantics is based on the semantics proposed by \citet{loow19_verif_compil_verif_proces}, which was used to create a formal translation from a logic representation encoded in the HOL4~\cite{slind08_brief_overv_hol4} theorem prover into an equivalent Verilog design.  This semantics is quite practical as it is restricted to a small subset of Verilog, which can nonetheless be used to model all hardware constructs one would want to design.  The main features that are not supported by the syntax and semantics are continuous assignment and combinational always blocks.
+This section describes the Verilog semantics that were \JW{was} chosen for the target language, including the changes that were made to the semantics to make it \JWcouldcut{a better fit} a \JW{suitable} HLS target.  The Verilog standard is quite large~\cite{06_ieee_stand_veril_hardw_descr_languag,05_ieee_stand_veril_regis_trans_level_synth}, but the syntax and semantics can be reduced to a small subset that \vericert{} needs to target.
+\NR{Have we discussed what our options were and why we chose the HOL4 semantics?} \JW{Good point -- we should cite the Maude semantics too. I think that's the only viable alternative.}
 
-The semantics of Verilog differ from regular programming languages, as it is used to describe hardware directly, which is inherently parallel, instead of describing an algorithm, which is often done sequentially.  The main construct in Verilog is the always block, which is construct that contains statements.  A module can contain multiple always blocks, which all 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.  As hardware designs normally describe events that will be executed periodically for an infinite amount of time, the top-level of the semantics can be described using small-step semantics, whereas the execution of one small step is then described using big-step semantics.  An example of a rule in the semantics for executing an always block in the semantics shown below, where $\Sigma$ is the state of the registers in the module and $s$ is the statement inside the always block:
+The Verilog semantics \JW{we use is ported to Coq from} a semantics written in HOL4  by \citet{loow19_verif_compil_verif_proces}.% which was used to create a formal translation from a logic representation encoded in the HOL4~\cite{slind08_brief_overv_hol4} theorem prover into an equivalent Verilog design. 
+This semantics is quite practical as it is restricted to a small subset of Verilog, which can nonetheless be used to model all hardware constructs one would want to design.  The main features that are not supported by the syntax and semantics are continuous assignment and combinational always blocks.
+\NR{Shall we use special font fo always-blocks: maybe \alwaysblock{}}
+
+The semantics of Verilog differs from regular programming languages, as it is used to describe hardware directly, which is inherently parallel, rather than an algorithm, which is usually sequential.  The main construct in Verilog is the always block \JW{consider `always-block' as it's easier to parse}. \JWcouldcut{which is a construct that contains statements.}
+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.} \JW{Mm, }
+
+
+
+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*}
   \inferrule[Always]{(\Sigma, s)\longrightarrow_{\text{stmnt}} \Sigma'}{(\Sigma, \yhkeyword{always @(posedge clk) } s) \longrightarrow_{\text{always}} \Sigma'}
 \end{equation*}
 
-\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 which is what it is defined to do.
+\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.}
 
-Two types of assignments are supported in always blocks: nonblocking and blocking assignment.  Nonblocking assignment modifies the signal at the end of the timestep and atomically.  Blocking assignment, on the other hand, assigns the variable directly in the always block for later signals to pick up.  To model both these assignments, the state $\Sigma$ has to be split into two parts: $\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)$.  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 timestep 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 aybe asynchronous vs synchronous updates. }  The nonblocking assignment can therefore be expressed as the following:
 
 \begin{equation*}
   \inferrule[Nonblocking Reg]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \longrightarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ <= } e) \longrightarrow_{\text{stmnt}} (\Gamma, \Delta [n \mapsto v])}\\