blob: 8bee352fd560efccc6bc5d3a32756ec97ea3cd33 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
\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, observable behaviours of C are actually not that important when translating directly to hardware, as there are no external function calls that produce events. Therefore, the only result that matters is the return value of the function, making sure that it is the same result as the original C code when executed with the same inputs.
\subsection{Coq Mechanisation}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:
|
