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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
|
\newpage
\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{Inference rules for statements.}\label{fig:inference_statements}
\end{figure*}
\begin{figure}
\centering
\begin{minted}{coq}
Inductive match_states :
3AC.state -> HTL.state -> Prop :=
| match_state : forall asa asr sf f sp
sp' rs mem m st res
(MASSOC : match_assocmaps f rs asr)
(TF : tr_module f m)
(WF : state_st_wf m (HTL.State res m st asr asa))
(MF : match_frames sf res)
(MARR : match_arrs m f sp mem asa)
(SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0))
(RSBP : reg_stack_based_pointers sp' rs)
(ASBP : arr_stack_based_pointers sp' mem
(f.(3AC.fn_stacksize)) sp)
(BOUNDS : stack_bounds sp (f.(3AC.fn_stacksize)) mem)
(CONST : match_constants m asr),
match_states
(3AC.State sf f sp st rs mem)
(HTL.State res m st asr asa)
| match_returnstate : forall v v' stack mem res
(MF : match_frames stack res),
val_value_lessdef v v' ->
match_states
(3AC.Returnstate stack v mem)
(HTL.Returnstate res v')
| match_initial_call :
forall f m m0 (TF : tr_module f m),
match_states
(3AC.Callstate nil (AST.Internal f) nil m0)
(HTL.Callstate nil m nil).
\end{minted}
\caption{\texttt{match\_states} predicate used to match an 3AC state to the equivalent HTL state.}\label{fig:match_states}
\end{figure}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% TeX-command-extra-options: "-shell-escape"
%%% End:
|
