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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
\section{Proof}
\label{sec:proof}
\NR{Now that we have adapted the Verilog semantics to the CompCert model, we are in a position to formally prove the correctness of our C to Verilog compilation.}
This section describes the main correctness theorem that was proven and the main ideas behind the proofs.
The main correctness theorem is the exact same correctness theorem as stated in \compcert{}~\cite{leroy09_formal_verif_realis_compil} which states that for all Clight source programs $C$, if the translation from the source to the target Verilog code succeeds, assuming that $C$ has correct observable behaviour $B$ when executed, then the target Verilog code will simulate with the same behaviour $B$, where behaviour can either be convergent, divergent or ``going wrong'' and is associated with a trace $t$ of any external function calls. The following backwards simulation theorem describes this property, where $\Downarrow_{s}$ and $\Downarrow$ stand for simulation and execution respectively.
\begin{equation*}
\forall C, V, B \notin \texttt{Wrong},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land V \Downarrow_{s} B \implies C \Downarrow B.
\end{equation*}
To prove this top-level theorem, a forward simulation has to be done between each intermediate language, which implies that the forward simulation between the C and Verilog also holds. To then prove the backward simulation, it suffices to show that the Verilog semantics are deterministic, which implies that there is only one possible behaviour for the Verilog output, and that it therefore also has to imply that $C$ has the same behaviour.
\subsection{Specification}
To simplify the proof, instead of using the translation algorithm as an assumption, as was done in the backward simulation stated above, a specification of the translation can be constructed instead which contains all the properties that are needed to prove the correctness. For example, for the translation from 3AC to HTL, the translation might be defined using the following function: $\yhfunction{transl\_{3ac}} (c) = \yhconstant{OK} (h)$, where $c$ is the 3AC input code and $h$. However, instead we can define a relation \texttt{tr\_htl} between the 3AC and HTL code, which contains all the properties about the translation that are needed, without any of the implementation. If the following can be proven, it can then be used instead of the translation algorithm when performing the proof of correctness.
\begin{equation*}
\forall\ c\ h,\ \yhfunction{transl\_3ac} (c) = \yhconstant{OK}(h) \implies \yhfunction{tr\_htl}\ c\ h.
\end{equation*}
One example is the translation of instructions, where the translation function might contain many implementation specific details, such as in which order instructions are added to the data path or the control path, whereas the specification describes only describes which instructions were added. The specification, \texttt{tr\_instr} can then be described as follows, where \textit{fin}, \textit{rtrn}, $\sigma$ and \textit{stk} are the registers for the finished signal, return value, current state and stack respectively, $i$ is the 3AC instruction being translated, and \textit{data} and \textit{control} are the data-flow and control logic map respectively.
\begin{equation*}
\yhfunction{tr\_instr } \textit{fin rtrn }\ \sigma\ \textit{stk }\ i\ \textit{data }\ \textit{control}
\end{equation*}
\noindent An specific example of a rule describing the translation of an \texttt{Iop} operation in 3AC is the following:
\begin{equation*}
\inferrule[Iop]{\yhfunction{tr\_op } \textit{op }\ \vec{a} = \yhconstant{OK } e}{\yhfunction{tr\_instr } \textit{fin rtrn }\ \sigma\ \textit{stk }\ (\yhconstant{Iop } \textit{op }\ \vec{a}\ d\ n)\ (d\ \yhkeyword{<=}\ e)\ (\sigma\ \yhkeyword{<=}\ n)}
\end{equation*}
\noindent This rule describes the specification of the translation by describing the nonblocking assignments that are added to the data path and control logic.
\subsection{Forward Simulation}
The forward simulation between C and Verilog can be separated into forward simulations of each compiler pass, which can then be composed to provide a whole proof from C to Verilog. Therefore, only the forward simulations from 3AC to HTL and from the HTL to Verilog need to be proven correct.
\subsubsection{3AC to HTL forward simulation}
As HTL is quite different to 3AC, this first translation is the most involved and therefore requires a larger proof, because the translation from 3AC instructions to Verilog statements needs to be proven correct in this step. In addition to that, the semantics of HTL are also quite different to the 3AC semantics, as instead of defining small-step semantics for each construct in Verilog, the semantics are instead defined over one clock cycle and mirror the semantics defined for Verilog.
The first step in proving the forward simulation is to define a relation that matches an 3AC state to an HTL state, which shows when the states are equivalent. This relation also defines assumptions that are made about the 3AC code that we receive, so that these assumptions can be used to prove the translations correct. These assumptions then have to be proven to always hold assuming the HTL code was created by the translation algorithm. Some of these assertions that need to be made about the 3AC and HTL code for a state to match are:
\begin{itemize}
\item the 3AC register file needs to match the HTL register file and the RAM values need to match the 3AC function's stack contents,
\item the \texttt{tr\_module} predicate needs to hold for the current 3AC function and HTL module.
\item the state is well formed, meaning the value of the state register matches the current value of the program counter,
\item the stack frames match,
\item all pointers in the program use the stack as a base pointer,
\item that a load and store to a location outside of the bounds of the stack does not occur, and does not modify the \compcert{} memory. Even if it occurs in the program, as it is undefined behaviour we can prove that our behaviour is still correct given the input.
\item that \textit{rst} and \textit{fin} are not modified and therefore stay at a constant 0 throughout execution.
\end{itemize}
This \texttt{match\_states} predicate that is used to match the states of the 3AC code to the HTL code is shown in Figure~\ref{fig:match_states}. The type \texttt{match\_states} declared in Figure~\ref{fig:match_states} has three constructors.
\begin{enumerate}
\item \texttt{match\_state} is the main constructor which matches an \texttt{3AC.State} to a \texttt{HTL.State}, which during the normal execution of instructions in the function.
\item \texttt{match\_returnstate} is the constructor used to match return statements in 3AC to HTL.\@ Even though function calls are not supported, there still has to be a notion of stack frames during the proof, as at the start of the program a stack frame is allocated, which then has to be deallocated (popped from the stack) when the main function returns its result.\YH{Maybe can remove because it's already mentioned in the semantics} The only condition on matching the return state is that the return values must be \emph{less defined} (either equal to, or if the C value is undefined any acceptable value is possible).
\item \texttt{match\_initial\_state} matches the initial call to the main function, and cannot be used for any other function calls, as the stack frame is assumed to be empty.
\end{enumerate}
Using the \texttt{match\_states}, we can then define the correctness theorem for the translation, shown as a simulation diagram below:
\begin{center}
\begin{tikzpicture}
\begin{scope}
\node[circle] (s1) at (0,1.5) {$R, M, \textit{pc}$};
\node[circle] (r1) at (6.5,1.5) {$\Gamma_{r}, \Gamma_{a}$};
\node[circle] (s2) at (0,0) {$R', M', \textit{pc}'$};
\node[circle] (r2) at (6.5,0) {$\Gamma_{r}', \Gamma_{a}'$};
\node at (6.8,0.75) {+};
\draw (s1) -- node[above] {$R \le \Gamma_{r} \land M \le \Gamma_{a} \land \textit{pc} = \Gamma_{r}!\sigma$} ++ (r1);
\draw[-{Latex}] ($(s1.south) + (0,0.4)$) -- ($(s2.north) - (0,0.4)$);
\draw[-{Latex},dashed] ($(r1.south) + (0,0.2)$) -- ($(r2.north) - (0,0.2)$);
\draw[dashed] (s2) -- node[above] {$R' \le \Gamma_{r}' \land M' \le \Gamma_{a}' \land \textit{pc}' = \Gamma_{r}'!\sigma$} ++ (r2);
\end{scope}
\end{tikzpicture}
\end{center}
$S_{1}$ and $S_{2}$ are 3AC states and $R_{1}$ and $R_{2}$, HTL states and $\xrightarrow{t}$ is one step in the semantics of 3AC and $\xrightarrow{t}_{+}$ is one or more steps in the semantics of HTL.\@ The correctness theorem then says that for all possible starting states $S_{1}$ and for the resulting state $S_{2}$ after one step in the semantics of 3AC, for all HTL states $R_{1}$ that matches the state $S_{1}$, there should exist a state $R_{2}$ such that $R_{2}$ is the result of the simulation of the HTL semantics and that the states $S_{2}$ and $R_{2}$ should match as well. Using this property, the forward simulation can then be proven correct by also showing that the initial and final states of the simulation match as well.
\subsubsection{HTL to Verilog forward simulation}
The HTL to Verilog simulation is quite simple, as the only transformation is from the map representation of the code to the case statement representation. As the representations are quite different though, to prove that they are equivalent the following observations have to be made.
The translation from maps to case statements is done by turning each node of the tree into a case expression with the statments in each being the same. The main difficulty for the proof is that a structure that can be directly accessed is transformed into an inductive structure where a certain number of constructors need to be called to get to the correct case. The proof of the translation from maps to case statements follows by induction over the list of elements in the map and the fact that each key in this list will be unique. In addition to that, the statement that is currently being evaluated is guaranteed by the correctness of the list of elements to be in that list. The latter fact therefore eliminates the base case, as an empty list does not contain the element we know is in the list. The other two cases follow by the fact that either the key is equal to the evaluated value of the case expression, or it isn't. In the first case we can then evaluate the statement and get the state after the case expression, as the uniqueness of the key tells us that the key cannot show up in the list anymore. In the other case we can just apply the inductive hypothesis and remove the current case from the case statement, as it did not match.
Another problem with the representation of the state as an actual register is that we have to make sure that the state does not overflow. Currently, the state register will always be 32 bits, meaning the maximum number of states can only be $2^{32} - 1$. We therefore have to prove that the state value will never go over that value. This means that during the translation we have to check for each state that it can fit into an integer. Finally, as we have to assume that there are $2^{32} - 1$ states, \vericert{} will error out when there are more instructions to be translated, which allows us to satisfy and prove that assumption correct.
\subsection{Deterministic Semantics}
Finally, to prove the backward simulation given the forward simulation, it has to be shown that if we generate hardware with a specific behaviour, that it is the only possible program with that behaviour. This only has to be performed for the final intermediate language, which is Verilog, so that the backward simulation holds for the whole chain from Clight to Verilog.
The Verilog semantics that are used are deterministic, as the order of operation of all the constructs is defined, and there is therefore only one way to evaluate the module and only one possible behaviour. This was proven correct for the small-step semantics shown in Figure~\ref{fig:inferrence_module}
%\subsection{Coq Mechanisation}
%\JW{Would be nice to include a few high-level metrics here. How many person-years of effort was the proof (very roughly)? How many lines of Coq? How many files, how many lemmas? How long does it take for the Coq proof to execute?}
\subsection{Coq Mechanisation}
\begin{table*}
\centering
\begin{tabular}{llllll}
\toprule
& \textbf{Coq code} & \textbf{OCaml code} & \textbf{Specifications} & \textbf{Theorems \& Proofs} & \textbf{Total}\\
\midrule
{Data structures and libraries} & 274 & - & - & 654 & 928 \\
{Integers and values} & 98 & - & 15 & 744 & 857 \\
{HTL semantics} & - & - & 174 & - & 174 \\
{HTL generation} & 655 & - & 79 & 3349 & 4083 \\
{Verilog semantics} & - & - & 739 & 174 & 913 \\
{Verilog generation} & 68 & - & - & 396 & 464 \\
{Top-level driver, pretty printers} & 89 & 747 & - & 209 & 1045 \\
\midrule
\textbf{Total} & 1184 & 747 & 1007 & 5526 & 8464 \\
\bottomrule
\end{tabular}
\caption{Statistics about the proof and implementation of \vericert{}.}
\label{tab:proof_statistics}
\end{table*}
The lines of code for the implementation and proof of \vericert{} can be found in Table~\ref{tab:proof_statistics}. In general it took 1 person year to finish the implementation and proofs of \vericert{}. The main proof is the correctness proof for the HTL generation, which required the equivalence proofs between all integer operations supported by \compcert{} and the ones supported in hardware. From the 3349 lines of proof code in the HTL generation, 1189 are only for the correctness proof of the load and store instructions. These were tedious to prove correct because of the large difference in memory models used, and the need to prove properties such as writes to the outside of the allocated memory being undefined, so that a finite sized array could be used. In addition to that, as pointers in HTL and Verilog are represented as integers, whereas there is a separate pointer value in the \compcert{} semantics, it was painful to reason about them and a many new theorems had to be proven about integers and pointers in \vericert{}.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:
|
