diff options
| author | John Wickerson <j.wickerson@imperial.ac.uk> | 2021-04-16 19:49:22 +0000 |
|---|---|---|
| committer | overleaf <overleaf@localhost> | 2021-04-16 19:52:07 +0000 |
| commit | 7d8150af139d30058a6be3b962f252505fd45d9b (patch) | |
| tree | 9a7519b6867964a2c47ca9dfe020b65bf39964c3 /proof.tex | |
| parent | a65bdc9ee527e66cf07dd0c4dea21ad342b141b6 (diff) | |
| download | oopsla21_fvhls-7d8150af139d30058a6be3b962f252505fd45d9b.tar.gz oopsla21_fvhls-7d8150af139d30058a6be3b962f252505fd45d9b.zip | |
Update on Overleaf.
Diffstat (limited to 'proof.tex')
| -rw-r--r-- | proof.tex | 1 |
1 files changed, 0 insertions, 1 deletions
@@ -14,7 +14,6 @@ The main correctness theorem is analogous to that stated in \compcert{}~\cite{le \end{theorem} The theorem is a `backwards simulation' result (from target to source). The theorem does not demand the `if' direction too, because compilers are permitted to resolve any non-determinism present in their source programs. - In practice, Clight programs are all deterministic, as are the Verilog programs in the fragment we consider. This means that we can prove the correctness theorem above by first inverting it to become a forwards simulation result, following standard \compcert{} practice. The second observation that needs to be made is that to prove this forward simulation, it suffices to prove forward simulations between each intermediate language, as these results can be composed to prove the correctness of the whole HLS tool. |