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
|
\section{Proof}
This section describes the main correctness theorem that was proven and the main ideas behind the proofs.
The main correctness theorem 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$. The following theorem describes this property.
\begin{equation*}
\forall C, V, B \notin \texttt{Wrong},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land C \Downarrow B \implies V \Downarrow_{s} B.
\end{equation*}
However, this forward simulation might still allow for wrong behaviour of the target code in cases where there are multiple possible behaviours in the target language. This means that there may be cases where it executes correctly, however, there may also be other behaviours that are also valid. However, if the target language is deterministic, meaning there is only one possible behaviour for all possible states, then this implies that the backwards simulation also holds.
\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 statement, we therefore have to prove that the Verilog semantics are deterministic and that the forward simulation between the C and the Verilog holds as well.
\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. We therefore only have to prove a forward simulation for the RTL to HTL translation, and for the HTL to Verilog translation.
\subsubsection{RTL to HTL forward simulation}
As HTL is quite similar to RTL, this first translation is the most involved translation and therefore requires a larger proof, as the translation from RTL instructions to Verilog statements needs to be proven correct. In addition to that, the semantics of HTL are also quite different to the RTL semantics, as instead of defining small-step semantics for each construct in Verilog, the semantics are instead defined over one clock cycle.
The first step in proving the forward simulation is to define a relation that matches an RTL state to an HTL state, which shows when the states are equivalent. This relation also defines assumptions that are made about the RTL 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 from
\subsubsection{HTL to Verilog forward simulation}
\subsection{Deterministic Semantics}
\subsection{Coq Mechanisation}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:
|
