1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
\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{figure}
\centering
\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{\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 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.}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:
|
