path: root/verilog.tex

\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.  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{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.}
%\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 design.  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 in Figure~\ref{fig:verilog_syntax}.  The main features that are supported by the syntax and semantics are module items, such as variable declarations and always blocks, statements and expressions.
%\NR{What is HOL? Was it discussed earlier?}\YH{Another theorem prover, have clarified hopefully.}

\begin{figure}
  \centering
  \begin{align*}
    v\quad ::=&\; 32 \yhkeyword{'d} n\\
    \textit{op}\quad ::=&\; \yhkeyword{+ } | \yhkeywordsp{- } | \yhkeywordsp{* } \cdots \\
    e\quad ::=&\; v\;\; |\;\; x\;\; |\;\; e \yhkeyword{[} e \yhkeyword{]}\;\; |\;\; e\ \mathit{op}\ 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*}

  \caption{Verilog syntax for values $v$, expressions $e$, statements $s$ and module items $m$.}\label{fig:verilog_syntax}
\end{figure}

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

\subsection{Changes to the Semantics}

Some small changes were made to the semantics proposed by \citet{loow19_verif_compil_verif_proces} to adapt the semantics to work better as a HLS target, as well as adding support for features that were needed in the target language.

The main change to the semantics is the support for two-dimensional arrays, which are needed to model RAM in Verilog.  RAM is needed to model the stack in C efficiently, without having to declare a variable for each possible stack location.  In the original semantics, RAMs, as well as inputs and outputs to the module could be modelled using a function from variable names (strings) to values, which could be modified accordingly to model inputs to the module.  This is quite an abstract description of memory, which can also be expressed as an array of bitvectors, which is the path we took instead.  This requires the addition of array operators to the semantics and correct reasoning of loads and stores to the array in different always blocks simultaneously.  Consider the following Verilog code:

\begin{minted}{verilog}
always @(posedge clk) begin
  x[0] = 23;
  x[1] <= 1;
end
\end{minted}

The code above modifies one array value using nonblocking assignment and it then modifies a second entry in the array with nonblocking assignment.  If the existing semantics used for values was used to update the array, then during the merge of values for the array, the array \texttt{x} from the nonblocking association map would replace the array from the blocking association map.  This would replace \texttt{x[0]} with it's original value and therefore behave incorrectly.  Instead, updates to arrays need to be recorded for each index in the array, and merging of the blocking and nonblocking queue needs to take into account each index separately.  

Explicit support for declaring inputs, outputs and internal variables was added to the semantics to make sure that the generated Verilog also contains the correct declarations.  This adds some guarantees to the generated Verilog and ensures that it synthesises and simulates correctly.

In addition to adding support for two-dimensional arrays, support for receiving external inputs was removed from the semantics for the case of simplicity, as these are not needed for an HLS target.  The main module in Verilog models the main function in C, and as the inputs to a C function shouldn't change during it's execution, there is no need to add support for external inputs for Verilog modules.  Finally, another simplification to the semantics that was made is to use 32 bit integers instead of arrays of booleans for the bitvector representation.  As the translation only currently has support for \texttt{int}, it is possible to simplify the semantics further and not have to handle bitvectors of an arbitrary size.

%~\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.}

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