From 79c53e5edbef589b82c5cbb1dbcc286a728f9e1d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 13 Sep 2021 09:03:48 +0100 Subject: Add C --- proof.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proof.tex b/proof.tex index ee8cf30..1654583 100644 --- a/proof.tex +++ b/proof.tex @@ -18,7 +18,7 @@ Together, these differences mean that translating 3AC directly to Verilog is inf \subsection{Formulating the Correctness Theorem} -The main correctness theorem is analogous to that stated in \compcert{}~\cite{leroy09_formal_verif_realis_compil}: for all Clight source programs $C$, if the translation to the target Verilog code succeeds, $\mathit{Safe}(C)$ holds and the target Verilog has behaviour $B$ when simulated, then the Clight source program will have the same behaviour $B$. $\mathit{Safe}(C)$ means all observable behaviours of $C$ are safe, which can be defined as $\forall B,\ C \Downarrow B \implies B \in \texttt{Safe}$. A behaviour is in \texttt{Safe} if it is either a final state (in the case of convergence) or divergent, but it cannot `go wrong', meaning the source program must not contain undefined behaviour. In \compcert{}, a behaviour is also associated with a trace of I/O events, but since external function calls are not supported in \vericert{}, this trace will always be empty. +The main correctness theorem is analogous to that stated in \compcert{}~\cite{leroy09_formal_verif_realis_compil}: for all Clight source programs $C$, if the translation to the target Verilog code succeeds, $\mathit{Safe}(C)$ holds and the target Verilog has behaviour $B$ when simulated, then $C$ will have the same behaviour $B$. $\mathit{Safe}(C)$ means all observable behaviours of $C$ are safe, which can be defined as $\forall B,\ C \Downarrow B \implies B \in \texttt{Safe}$. A behaviour is in \texttt{Safe} if it is either a final state (in the case of convergence) or divergent, but it cannot `go wrong', meaning the source program must not contain undefined behaviour. In \compcert{}, a behaviour is also associated with a trace of I/O events, but since external function calls are not supported in \vericert{}, this trace will always be empty. %This correctness theorem is also appropriate for HLS, as HLS is often used as a part of a larger hardware design that is connected together using a hardware description language like Verilog. This means that HLS designs are normally triggered multiple times and results are returned each time when the computation terminates, which is the property that the correctness theorem states. -- cgit