From 311999d1c74ea03b57e7113335e0d2c88fa8f8cf Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 12 Sep 2021 20:55:43 +0100 Subject: Remove unnecessary sentence --- proof.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proof.tex') diff --git a/proof.tex b/proof.tex index 9a192c6..550fdd6 100644 --- a/proof.tex +++ b/proof.tex @@ -45,7 +45,7 @@ The forward simulation from 3AC to HTL is stated in Lemma~\ref{lemma:htl} (Secti As HTL is quite far removed from 3AC, this first translation is the most involved and therefore requires a larger proof, because the translation from 3AC instructions to Verilog statements needs to be proven correct in this step. In addition to that, the semantics of HTL are also quite different to the 3AC semantics. Instead of defining small-step semantics for each construct in Verilog, the semantics are defined over one clock cycle and mirror the semantics defined for Verilog. Lemma~\ref{lemma:htl} shows the result that needs to be proven in this subsection. \begin{lemma}[Forward simulation from 3AC to HTL]\label{lemma:htl} - We write \texttt{tr\_htl} for the translation from 3AC to HTL, assuming that the behaviour is safe. + We write \texttt{tr\_htl} for the translation from 3AC to HTL. \begin{equation*} \forall c, h, B \in \texttt{Safe},\quad \yhfunction{tr\_htl} (c) = \yhconstant{OK} (h) \land c \Downarrow B \implies h \Downarrow B. \end{equation*} -- cgit