diff options
Diffstat (limited to 'proof.tex')
| -rw-r--r-- | proof.tex | 8 |
1 files changed, 7 insertions, 1 deletions
@@ -8,7 +8,13 @@ The main correctness theorem states that for all Clight source programs $C$, if \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. +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. + +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 proofs by forward simulation of each compiler pass \subsection{Coq Mechanisation} |