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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
\section{Verilog}
Verilog is a hardware description language commonly used to design hardware. A Verilog design can then be synthesised into more basic logic which describes how different gates connect to each other, called a netlist. This representation can then be put onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASPIC) 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, which means that these features do not have to be modelled in the semantics. In addition to that, as the HLS algorithm 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. Only 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.
The Verilog semantics are based on the semantics proposed by \citet{loow19_verif_compil_verif_proces}, which were used to create a formal translation from HOL logic into a 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. The main syntax for the Verilog subset is the following:
\begin{align*}
v ::=&\; \mathit{sz} * n\\
e ::=&\; v\\[-2pt]
|&\; x\\[-2pt]
|&\; e [e]\\[-2pt]
|&\; e\ \mathit{op}\ e\\[-2pt]
|&\; \texttt{!} e\ |\ \texttt{~} e\\[-2pt]
|&\; e \texttt{ ? } e \texttt{ : } e\\
s ::=&\; s\ \texttt{;}\ s\ |\ \texttt{;}\\[-2pt]
|&\; \texttt{if } e \texttt{ then } s \texttt{ else } s\\[-2pt]
|&\; \texttt{case } e\ [e : s] \texttt{ endcase}\\[-2pt]
|&\; e \texttt{ = } e\\[-2pt]
|&\; e \texttt{ <= } e\\
d ::=&\; \texttt{[n-1:0] } r\ |\ \texttt{[n-1:0] } r \texttt{ [m-1:0]}\\
m ::=&\ \texttt{reg } d \texttt{;}\ |\ \texttt{input wire } d \texttt{;}\ |\ \texttt{output reg } d \texttt{;}\\
|&\; \text{\tt always @(posedge clk)}\ s
\end{align*}
The main addition to the Verilog syntax is the explicit declaration of inputs and outputs, as well as variables and arrays. 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.
\subsection{Semantics}
In general, Verilog is used to model hardware which is intrinsically parallel. At the top-level, always block, describing logic which is run everytime some even occurs:
\begin{minted}{systemverilog}
always @(posedge clk)
\end{minted}
However, adjustments to these semantics had to be made to make it compatible with the CompCert small step semantics. In addition to that, memory is not directly modelled in their semantics of Verilog, as well as handling of inputs and declarations in modules.
\begin{equation}
\label{eq:10}
s = (\Gamma, \Delta)
\end{equation}
Definition of stmntrun.
\begin{gather*}
\label{eq:1}
\inferrule[Skip]{ }{\texttt{srun}\ f\ s\ \texttt{Vskip} = s}\\
%
\inferrule[Seq]{\texttt{srun}\ f\ s_{0}\ \textit{st}_{1}\ s_{1} \\ \texttt{srun}\ f\ s_{1}\ \textit{st}_{2}\ s_{2}}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vseq}\ \textit{st}_{1}\ \textit{st}_{2})\ s_{2}}\\
%
\inferrule[CondTrue]{\texttt{erun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \texttt{valToB}\ v_{c} = \texttt{true} \\ \texttt{srun}\ f\ s_{0}\ \textit{stt}\ s_{1}}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcond}\ c\ \textit{stt}\ \textit{stf}\,)\ s_{1}}\\
%
\inferrule[CondFalse]{\texttt{erun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \texttt{valToB}\ v_{c} = \texttt{false} \\ \texttt{srun}\ f\ s_{0}\ \textit{stf}\ s_{1}}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcond}\ c\ \textit{stt}\ \textit{stf}\,)\ s_{1}}\\
%
\inferrule[CaseNoMatch]{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcase}\ e\ cs\ \textit{def})\ s_{1} \\ \texttt{erun}\ f\ \Gamma_{0}\ me\ mve \\ \texttt{erun}\ f\ \Gamma_{0}\ e\ ve \\ mve \neq ve}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcase}\ e\ ((me,\ sc) :: cs)\ \textit{def})\ s_{1}}\\
%
\inferrule[CaseMatch]{\texttt{srun}\ f\ s_{0}\ sc\ s_{1} \\ \texttt{erun}\ f\ \Gamma_{0}\ e\ ve \\ \texttt{erun}\ f\ \Gamma_{0}\ me\ mve \\ mve = ve}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcase}\ e\ ((me,\ sc) :: cs)\ \textit{def})\ s_{1}}\\
%
\inferrule[CaseDefault]{\texttt{srun}\ f\ s_{0}\ st\ s_{1}}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcase}\ e\ []\ (\texttt{Some}\ st))\ s_{1}}\\
%
\inferrule[Blocking]{\texttt{name}\ \textit{lhs} = \texttt{OK}\ n \\ \texttt{erun}\ f\ \Gamma\ \textit{rhs}\ v_{\textit{rhs}}}{\texttt{srun}\ f\ (\Gamma, \Delta)\ (\texttt{Vblock}\ \textit{lhs}\ \textit{rhs})\ (\Gamma ! n \rightarrow v_{\textit{rhs}}, \Delta)}\\
%
\inferrule[Nonblocking]{\texttt{name}\ \textit{lhs} = \texttt{OK}\ n \\ \texttt{erun}\ f\ \Gamma\ \textit{rhs}\ v_{\textit{rhs}}}{\texttt{srun}\ f\ (\Gamma, \Delta)\ (\texttt{Vnonblock}\ \textit{lhs}\ \textit{rhs}) (\Gamma, \Delta ! n \rightarrow v_{\textit{rhs}})}\\
\end{gather*}
\input{verilog_notes}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:
|
