diff options
| -rw-r--r-- | proof.tex | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -130,10 +130,10 @@ The HTL to Verilog simulation is conceptually simple, as the only transformation Finally, to prove the backward simulation given the forward simulation, it has to be shown that if we generate hardware with a specific behaviour, that it is the only possible program with that behaviour. This only has to be performed for the final intermediate language, which is Verilog, so that the backward simulation holds for the whole chain from Clight to Verilog. \begin{lemma}\label{lemma:deterministic} - Semantics are deterministic if it can be shown that two behaviours $B_{1}$ and $B_{2}$ for the same program implies that the behaviours are the same. + Semantics are deterministic if it can be shown that two behaviours $B_{1}$ and $B_{2}$ for the same Verilog program $V$ implies that the behaviours are the same. \begin{equation*} - C \Downarrow B_{1} \land C \Downarrow B_{2} \implies B_{1} = B_{2}. + \forall V, B_{1}, B_{2}, V \Downarrow B_{1} \land V \Downarrow B_{2} \implies B_{1} = B_{2}. \end{equation*} \end{lemma} |