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
71
72
73
74
75
76
77
|
\appendix
\section{Appendix}
\begin{figure*}
\centering
\begin{minipage}{1.0\linewidth}
\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*}
\end{minipage}
\caption{Verilog syntax for values $v$, expressions $e$, statements $s$ and module items $m$.}\label{fig:verilog_syntax}
\end{figure*}
\begin{figure*}
\centering
\begin{minipage}{1.0\linewidth}
\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*}
\end{minipage}
\caption{Inferrence rules for statements.}\label{fig:inferrence_statements}
\end{figure*}
\begin{figure*}
\centering
\begin{minipage}{1.0\linewidth}
\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*}
\end{minipage}
\caption{Inferrence rules for modules}%
\label{fig:inferrence_module}
\end{figure*}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% TeX-command-extra-options: "-shell-escape"
%%% End:
|
