\section{Verilog}

Verilog is a hardware description language commonly used to design hardware.  A Verilog design can then be synthesised into logic gates which describes how different gates connect to each other, called a netlist.  This representation can then be mapped onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASIC) to implement the design that was described in Verilog.  The Verilog standard is quite large though, and not all Verilog features are needed to be able to describe hardware.  Many Verilog features are only useful for simulation and do not affect the actual hardware itself, we can therefore restrict the Verilog semantics to the synthesisable subset of Verilog~\cite{05_veril_regis_trans_level_synth}.  In addition to that, HLS dictates which Verilog constructs are generated, meaning the Verilog subset that has to be modelled by the semantics can be reduced even further to only support the constructs that are needed.~\NR{Didn't get this sentence? Do you mean that the HLS algo further restricts the synthesisable subset?}\YH{Yes basically, because we get to choose what we generate.  For example, we don't have to support combinational always blocks.}  Supporting a smaller subset in the semantics also means that there is less chance that the standard is misunderstood, and that the semantics actually model how the Verilog is simulated and synthesised by existing tools and how it is dictated by the standard.
\NR{What is the distinction here between the semantics and simulation? Discuss.}\YH{Tried to clarify that I meant simulation and synthesis by tools and how it should be understood from the standard}

The Verilog semantics are 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 circuit.  These semantics are quite practical as they restrict themselves to a small subset of Verilog, which can nonetheless be used to model all hardware constructs one would want to design. An abstraction of the Verilog syntax that is generated is shown below:
\NR{What is HOL? Was it discussed earlier?}\YH{Another theorem prover, have clarified hopefully.}

\begin{align*}
  v\quad ::=&\; \mathit{sz} \yhkeyword{'d} n\\
  \textit{op}\quad ::=&\; \yhkeyword{+ } | \yhkeywordsp{- } | \yhkeywordsp{* } \cdots \\
  e\quad ::=&\; v\;\; |\;\; x\;\; |\;\; e \yhkeyword{[} e \yhkeyword{]}\;\; |\;\; e\ \mathit{op}\ e\;\; |\;\; \yhkeyword{!} e\;\; |\;\; \yhkeyword{\textasciitilde} e\;\; |\;\; e \yhkeywordsp{? } e \yhkeywordsp{: } e\\
  s\quad ::=&\; s\ s\ |\ \epsilon\\[-2pt]
  |&\; \yhkeyword{if(} e \yhkeyword{) } s \yhkeywordsp{else } s\\[-2pt]
  |&\; \yhkeyword{case(} e \yhkeyword{) } e : s\ \{\ e : s\ \}\ [\ s\ ] \yhkeywordsp{endcase}\\[-2pt]
  |&\; e = e \yhkeyword{;}\\[-2pt]
  |&\; e \Leftarrow e \yhkeyword{;}\\
  d\quad ::=&\; \yhkeyword{[n-1:0] } r\ |\ \yhkeyword{[n-1:0] } r \yhkeywordsp{[m-1:0]}\\
  m\quad ::=&\; \yhkeyword{reg } d \yhkeyword{;}\ |\ \yhkeyword{input wire } d \yhkeyword{;}\ |\ \yhkeyword{output reg } d \yhkeyword{;}\\
|&\; \yhkeywordsp{always @(posedge clk) } s \\
  m \text{ list}\quad ::=&\; \{ m \}
\end{align*}

The main addition to the Verilog syntax is the explicit declaration of inputs and outputs, as well as variables and arrays.~\NR{Isn't the 'main' addition that the PL community may not have seen the always blocks? It can be counter-intuitive to them. Also have you intentionally avoided assign statements? Finally, what is $\epsilon$ in the syntax?}\YH{Yes, I will probably have to explain always blocks some more, I'll try and add a paragraph about them.  Yes, assign statements are quite complex to model and many semantics do not model them.  They are also not needed for translation.  The $\epsilon$ is an empty skip statement, which is just a semicolon.} This means that the declarations have to be handled in the semantics as well, adding to the safety that all the registers are declared properly with the right size, as this affects how the Verilog module is synthesised and simulated.  In addition to that, literal values are not represented by a list of nested Boolean values, but instead they are represented by a size and its value, meaning a Boolean is represented as a value with size one.  Finally, the last difference is that the syntax supports two dimensional arrays in Verilog explicitly which model memory so that we can reason about array loads and stores properly. \JW{In the $m$ category, should it be `reg d; m' rather than just `reg d;'?}\YH{Yes that's actually completely true, I added a $\vec{m}$ rule for now, but can also add the $m$ afterwards.}

\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 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.}
%~\NR{Oh, do we sequentialise always execution?}\YH{Yes}
%~\NR{Have you discussed what an association map is?}\YH{Will add a section about that.}
%~\NR{Do blocking and non-blocking assignments each have individual maps? Also, association map is used before definition in this paragraph.}
At the top-level, always blocks describe logic which is run every time some event occurs.  The only event that is supported by these semantics is detecting the rising rising edge of the clock, so that we can implement synchronous logic.  As soon as an event occurs, the hardware will be executed, meaning if there are multiple always blocks that get triggered by the event, these will run in parallel.  Assignments to a variable in multiple always blocks is not allowed, so that there cannot be any data races during assignments.  However, as the semantics should be deterministic, we impose an order on the always blocks and execute them sequentially.  However, to preserve the fact that the statements inside of the always block are executed in parallel, nonblocking assignments to variables need to be kept in a different association map compared to blocking assignments to variables, where association maps are mappings from a variable name to its current value.  This preserves the behaviour that blocking assignments change the value of the variable inside of the clock cycle, whereas the nonblocking assignments only take place at the end of the clock cycle, and in parallel.  We can denote these two association maps as $s = (\Gamma_{\rm r}, \Gamma_{\rm a}, \Delta_{\rm r}, \Delta_{\rm a})$, where $\Gamma_{\rm r}$ is the current value of the registers, $\Gamma_{\rm a}$ is the current value of the array, and $\Delta_{\rm r}$ and $\Delta_{\rm a}$ are the values of the variables and arrays when the clock cycle ends.  Blocking assignments will therefore modify $\Gamma_{\rm r}$ and $\Gamma_{\rm a}$, whereas nonblocking assignments modify $\Delta_{\rm r}$ and $\Delta_{\rm a}$

%~\NR{Are you referring to the C stack?}\YH{Yes}
We can then define how one step in the semantics looks like.  We therefore first need to define the structure of the main module which will contain the logic for the program.  In general, functions that are translated to hardware will require basic handshaking signals so that the translated function can be used in hardware.  Firstly, they require an input for the clock, so that all the sequential circuits are run at the right time.  They then require a start and reset input, so that the hardware generated from the function can be reused multiple times.  Finally, they need a finish and return signal, where finish will go high when the result is ready to be read.  In addition to that, the module could take an arbitrary number of inputs which act as arguments to the original function, so that the module may be instantiated with any number of arguments.  In addition to inputs and outputs to the module, we also need to keep track of some internal signals and properties about the module.  Firstly, we need to keep track of the internal variables that contain the current state of the module, and the current contents of the stack.  Next, the module contains the entry point of the module, the list of module items that declare all of the internal registers and the encoding of the state machine that behaves in the same way as the function.  We can therefore declare it in the following way:
~\NR{We should distinguish handshaking signals of a Verilog module to arguments of a sw function. In the sw world, an argument is either value or pointer. Values are unmodifiable, and pointers can be only be modified by the function body. In contrast, handshaking signals are constantly active, interacting with external modules. These signals can also be trigger events, such as the clock.}\YH{Yes that's true, although currently we don't really support modules and therefore assume that the signals do not change.}
~\NR{Also, I don't think a Verilog module is equivalent to a Verilog function. I think they both exist in Verilog. Please double-check this before we use module and function interchangably in the text above.}\YH{Clarified that, functions are indeed different to modules in Verilog, did not want to use them interchangably.}
%\JW{I'd be inclined to write `$r~\mathrm{list}$' rather than $\vec{r}$, as it's a little more readable. (Assuming it's more-or-less the same thing?)}

\begin{align*}
  \mathit{M} \quad ::= \quad \big\{\ &\mathtt{args} : r \text{ list}\\
                                     &\mathtt{body} : m \text{ list}\\
                                     &\mathtt{entrypoint} : n\\
                                     &\mathtt{st, stk, finish, return, start, reset, clk} : r\\
                                     &\mathtt{stacksize} : n\ \big\}
\end{align*}

The two main evaluation functions are then \textit{erun}, which takes in the current state together with an expression and returns a value, and \textit{srun}, which takes the current state and a statement as input, and returns the updated state.  The inductive rules defining \textit{srun} are shown below, where $\sigma_{n} = (\Gamma_{\rm r}^{n}, \Gamma_{\rm a}^{n}, \Delta_{\rm r}^{n}, \Delta_{\rm a}^{n})$:
\NR{The evaluation function here relates to the semantics, right? Can it be confused with sw function and Verilog module?}

\begin{gather*}
  \label{eq:1}
  \inferrule[Skip]{ }{\textit{srun}\ \sigma\ \epsilon\ \sigma}\\
%
  \inferrule[Seq]{\textit{srun}\ \sigma_{0}\ \textit{s}_{1}\ \sigma_{1} \\ \textit{srun}\ \sigma_{1}\ \textit{s}_{2}\ \sigma_{2}}{\textit{srun}\ \sigma_{0}\ (\textit{s}_{1}\ \textit{s}_{2})\ \sigma_{2}}\\
%
  \inferrule[CondTrue]{\textit{erun}\ \Gamma_{\rm r}^{0}\ \Gamma_{\rm a}^{0}\ c\ v_{c} \\ \yhfunction{valToB}\ v_{c} = \yhconstant{true} \\ \textit{srun}\ \sigma_{0}\ \textit{st}\ \sigma_{1}}{\textit{srun}\ \sigma_{0}\ (\yhkeyword{if(} c \yhkeyword{) } \textit{st} \yhkeywordsp{else } \textit{sf})\ \sigma_{1}}\\
%
  \inferrule[CondFalse]{\textit{erun}\ \Gamma_{\rm r}^{0}\ \Gamma_{\rm a}^{0}\ c\ v_{\rm c} \\ \yhfunction{valToB}\ v_{\rm c} = \yhconstant{false} \\ \textit{srun}\ \sigma_{0}\ \textit{sf}\ \sigma_{1}}{\textit{srun}\ \sigma_{0}\ (\yhkeyword{if(} c \yhkeyword{) } \textit{st} \yhkeywordsp{else } \textit{sf})\ \sigma_{1}}\\
%
  \inferrule[CaseNoMatch]{\textit{srun}\ \sigma_{0}\ (\yhkeyword{case(} e \yhkeyword{) } cs\ \textit{def} \yhkeywordsp{endcase})\ \sigma_{1} \\ \textit{erun}\  \Gamma_{\rm r}^{0}\ \Gamma_{\rm a}^{0}\ me\ mve \\ \textit{erun}\  \Gamma_{\rm r}^{0}\ \Gamma_{\rm a}^{0}\ e\ ve \\ mve \neq ve}{\textit{srun}\  \sigma_{0}\ (\yhkeyword{case(} e \yhkeyword{) } ((me : sc) :: cs)\ \textit{def} \yhkeywordsp{endcase})\ \sigma_{1}}\\
%
  \inferrule[CaseMatch]{\textit{srun}\  \sigma_{0}\ sc\ \sigma_{1} \\ \textit{erun}\  \Gamma_{\rm r}^{0}\ \Gamma_{\rm a}^{0}\ e\ ve \\ \textit{erun}\  \Gamma_{\rm r}^{0}\ \Gamma_{\rm a}^{0}\ me\ mve \\ mve = ve}{\textit{srun}\  \sigma_{0}\ (\yhkeyword{case(} e \yhkeyword{) } ((me : sc) :: cs)\ \textit{def} \yhkeywordsp{endcase})\ \sigma_{1}}\\
%
  \inferrule[CaseDefault]{\textit{srun}\  \sigma_{0}\ s\ \sigma_{1}}{\textit{srun}\  \sigma_{0}\ (\yhkeyword{case(} e \yhkeyword{) } []\ (\yhconstant{Some}\ s) \yhkeywordsp{endcase})\ \sigma_{1}}\\
%
  \inferrule[Blocking Reg]{\yhfunction{name}\ \textit{lhs} = \yhconstant{OK}\ n \\ \textit{erun}\  \Gamma_{\rm r}\ \Gamma_{\rm a}\ \textit{rhs}\ v_{\rm rhs}}{\textit{srun}\  (\Gamma_{\rm r},\Gamma_{\rm a},\Delta_{\rm r},\Delta_{\rm a})\ (\textit{lhs} = \textit{rhs})\ (\Gamma_{\rm r} [n \mapsto v_{\rm rhs}], \Gamma_{\rm a}, \Delta_{\rm r}, \Delta_{\rm a})}\\
%
  \inferrule[Nonblocking Reg]{\yhfunction{name}\ \textit{lhs} = \yhconstant{OK}\ n \\ \textit{erun}\  \Gamma_{\rm r}\ \Gamma_{\rm a}\ \textit{rhs}\ v_{\rm rhs}}{\textit{srun}\  (\Gamma_{\rm r}, \Gamma_{\rm a}, \Delta_{\rm r}, \Delta_{\rm a})\ (\textit{lhs} \Leftarrow \textit{rhs})\ (\Gamma_{\rm r}, \Gamma_{\rm a}, \Delta_{\rm r} [n \mapsto v_{\rm rhs}], \Delta_{\rm a})}
%
%  \inferrule[Blocking Array]{\yhkeyword{name}\ \textit{lhs} = \yhkeyword{OK}\ n \\ \textit{erun}\  \Gamma_{r}\ \Gamma_{a}\ \textit{rhs}\ v_{\textit{rhs}}}{\textit{srun}\  (\Gamma_{r},\Gamma_{a},\Delta_{r},\Delta_{a})\ (\textit{lhs} = \textit{rhs})\ (\Gamma_{r} // \{n \rightarrow v_{\textit{rhs}}\}, \Gamma_{a}, \Delta_{r}, \Delta_{a})}\\
%
%  \inferrule[Nonblocking Array]{\yhkeyword{name}\ \textit{lhs} = \yhkeyword{OK}\ n \\ \textit{erun}\  \Gamma\ \textit{rhs}\ v_{\textit{rhs}}}{\textit{srun}\  (\Gamma_{r}, \Gamma_{a}, \Delta_{r}, \Delta_{a})\ (\textit{lhs} \Leftarrow \textit{rhs})\ (\Gamma_{r}, \Gamma_{a}, \Delta_{r} // \{n \rightarrow v_{\textit{rhs}}\}, \Delta_{a})}
\end{gather*}

Taking the \textsc{CondTrue} rule as an example, this rule will only apply if the Boolean result of running the expression results in a \texttt{true} value.  It then also states that the statement in the true branch of the conditional statement \textit{stt}~\NR{\textit{st} or \textit{stt}?} runs from state $\sigma_{0}$ to state $\sigma_{1}$.  If both of these conditions hold~\NR{How are these conditions checked? Can \textit{erun} or \textit{srun} evaluate to false?}, we then get that the conditional statement will also run from state $\sigma_{0}$ to state $\sigma_{1}$.  The \textsc{Blocking} and \textsc{Nonblocking} rules are a bit more interesting, as these modify the blocking and nonblocking association maps respectively.

One main difference between these semantics and the Verilog semantics by \citet{loow19_verif_compil_verif_proces} is that there is no function for external nondeterministic effects, such as memories and inputs and outputs.  These are instead handled explicitly in the semantics by using two dimensional unpacked arrays to model memories and assuming that inputs to modules cannot change.  Another difference with these semantics is that partial updates to arrays are fully supported, due to the fact that there are two different queues for arrays and variables.  Originally, if there was a blocking assignment to an array, and then a nonblocking assignment to a different region in the array, then the blocking assignment would disappear at the end of the clock cycle.  This is because the complete array would be overwritten with the updated array in the nonblocking association maps.  However, in our semantics, only the values that were changed in the array are actually recorded in the nonblocking assignment queue, meaning once the blocking and nonblocking array association maps are merged, only the actual indices that changed with nonblocking assignment are updated in the blocking assignment map.
%\NR{I did not understand this paragraph. Discuss with Yann.}

In these semantics, module instantiations are not supported, as they can be modelled by inlining the logic that modules would have produced.  This therefore means that function calls are implemented by inlining all the functions as well.  Consequently, recursive function calls are not supported, however, these are not supported by other high-level synthesis tools either, as allocating memory dynamically is not possible with fixed size RAM blocks.
\NR{Were these last two paragraphs referring to your assumptions or limitations or simplications you made? Discuss with Yann.}

To integrate our semantics with \compcert{}, we need to define the same states that \compcert{} uses to define their semantics, which are the \texttt{State}, \texttt{Callstate} and \texttt{Returnstate}.  The \texttt{Callstate} and \texttt{Returnstate} are needed because the initial state describes a call to main, and the final state results in the return value from the main function.  Even though the Verilog semantics do not support function calls, semantics for the initial function call and final return state need to be implemented to be properly shown equivalent to the Verilog semantics.  Firstly, the \texttt{State} is contains all the information necessary to identify the current execution state of the function or module.  In Verilog, we therefore keep track of the current module $m$ we are working on, the current value of the program counter $v$, which translates to the current value of the state register $s_{t}$, the current contents of the stack frame \textit{sf} and finally the current states of the association maps for variables $\Gamma_{r}$ and arrays $\Gamma_{a}$.  We can therefore define the state as \texttt{State} \textit{sf} $m$ $v$ $\Gamma_{r}$ $\Gamma_{a}$.  The \texttt{Callstate} only needs to be supported for the initial call to the function and the \texttt{Returnstate} only needs to be supported for the return of the main function.  As function calls are not supported in the semantics, there cannot be any other possible calling state or return state in the program.
\NR{We had a lot of discussion on functions earlier in this section, but then now we claim that the Verilog semantics does not support functions. If I recall correctly, our C program can't have functions either, or we inline all functions. Aren't they contradicting? Discuss with Yann.}

We then define the semantics of running the module for one clock cycle in the following way:

\begin{figure*}
  \centering
  \begin{gather*}
    \inferrule[Module]{\Gamma_{r} ! s_{t} = \texttt{Some } v \\ (m_{i}, \Gamma_{r}^{0}, \Gamma_{a}^{0}, \epsilon, \epsilon\ l)\ \longrightarrow_{\vec{m}} (m_{i}, \Gamma_{r}^{1}, \Gamma_{a}^{1}, \Delta_{r}^{1}, \Delta_{a}^{1}) \\ (\Gamma_{r}^{1} // \Delta_{r}^{1}) ! s_{t} = \texttt{Some } v'}{\texttt{State } \textit{sf }\ m\ v\ \Gamma_{r}^{0}\ \Gamma_{a}^{0} \longrightarrow \texttt{State } \textit{sf }\ m\ v'\ (\Gamma_{r}^{1} // \Delta_{r}^{1})\ (\Gamma_{a}^{1} // \Delta_{a}^{1})}\\
    % 
    \inferrule[Finish]{\Gamma_{r}!\textit{fin} = \texttt{Some } 1 \\ \Gamma_{r}!\textit{ret} = \texttt{Some } r}{\texttt{State } \textit{sf }\ m\ s_{t}\ \Gamma_{r}\ \Gamma_{a} \longrightarrow \texttt{Returnstate } \textit{sf }\ r}\\
    % 
    \inferrule[Call]{ }{\texttt{Callstate } \textit{sf }\ m\ \vec{r} \longrightarrow \texttt{State } \textit{sf }\ m\ n\ (\textit{init\_params }\ \vec{r}\ a // \{s_{t} \rightarrow n\})}\\
    % 
    \inferrule[Return]{ }{\texttt{Returnstate } (\texttt{Stackframe } r\ m\ \textit{pc }\ \Gamma_{r}\ \Gamma_{a} :: \textit{sf}) \longrightarrow \texttt{State } \textit{sf }\ m\ \textit{pc }\ (\Gamma_{r} // \{ \textit{st} \rightarrow \textit{pc}, r \rightarrow i \})\ \epsilon}
  \end{gather*}
  \caption{Inferrence rules for modules}%
  \label{fig:inferrence_module}
\end{figure*}

\YH{TODO:\@ Need to fix the last rule, as it is actually only used for a case that shouldn't ever be hit.}

The \textsc{Module} rule is the main rule for the execution of one clock cycle of the module.  Given that the value of the $s_{t}$ register is the value of the program counter at the current instruction and that the value of the $s_{t}$ register in the resulting association map is equal to the next program counter value, we can then say that if all the module items in the body go from one state to another, that the whole module will step from that state to the other.

%\NR{Bigger picture question: Why don't always blocks show up in the rules?}\YH{Mainly because these are at a different level of abstraction, here only statements are modelled.}

%%\input{verilog_notes}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:
