diff options
author | John Wickerson <j.wickerson@imperial.ac.uk> | 2021-09-13 08:01:43 +0000 |
---|---|---|
committer | node <node@git-bridge-prod-0> | 2021-09-13 08:03:57 +0000 |
commit | dc1b004565974da11abf2aa3335dc6b09283d5ec (patch) | |
tree | 62fc6b2e7a9db76dd9fd51b9fe8cef06e1a4e749 | |
parent | faa0adab0bc5da26187168521585c268981a7df4 (diff) | |
download | oopsla21_fvhls-dc1b004565974da11abf2aa3335dc6b09283d5ec.tar.gz oopsla21_fvhls-dc1b004565974da11abf2aa3335dc6b09283d5ec.zip |
Update on Overleaf.
-rw-r--r-- | proof.tex | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -27,7 +27,7 @@ The main correctness theorem is analogous to that stated in \compcert{}~\cite{le %The following `backwards simulation' theorem describes the correctness theorem, where $\Downarrow$ stands for simulation and execution respectively. \begin{theorem} - Whenever the translation from $C$ succeeds and produces Verilog $V$, and all observable behaviours of $C$ are safe then $V$ has behaviour $B$ only if $C$ has behaviour $B$. + Whenever the translation from $C$ succeeds and produces Verilog $V$, and all observable behaviours of $C$ are safe, then $V$ has behaviour $B$ only if $C$ has behaviour $B$. \begin{equation*} \forall C, V, B,\quad \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land \mathit{Safe}(C) \implies (V \Downarrow B \implies C \Downarrow B). \end{equation*} |