diff options
| -rw-r--r-- | proof.tex | 8 | ||||
| -rw-r--r-- | verilog.tex | 2 |
2 files changed, 8 insertions, 2 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} diff --git a/verilog.tex b/verilog.tex index 7b951c7..f11b6a2 100644 --- a/verilog.tex +++ b/verilog.tex @@ -93,7 +93,7 @@ We then define the semantics of running the module for one clock cycle in the fo The \textsc{Module} rule is the main rule for the execution of one clock cycle of the module. Given that the value of the $s_{t}$ register is the value of the program counter at the current instruction and that the value of the $s_{t}$ register in the resulting association map is equal to the next program counter value, we can then say that if all the module items in the body go from one state to another, that the whole module will step from that state to the other. -\input{verilog_notes} +%%\input{verilog_notes} %%% Local Variables: %%% mode: latex |