diff options
Diffstat (limited to 'proof.tex')
| -rw-r--r-- | proof.tex | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -171,7 +171,7 @@ The other invariants and assumptions for defining two matching states in HTL are Given an HTL program, the forward simulation relation should hold after inserting the RAM and wiring the load, store and control signals. \begin{align*} - &\forall h, B \in \texttt{Safe}, \yhfunction{tr\_ram}(h) = h' \land h \Downarrow B \implies h' \Downarrow B. + &\forall\ h\ B, B \in \texttt{Safe} \land \yhfunction{tr\_ram}(h) = h' \land h \Downarrow B \implies h' \Downarrow B. \end{align*} \end{lemma} @@ -183,7 +183,7 @@ The HTL-to-Verilog simulation is conceptually simple, as the only transformation \begin{lemma}[Forward simulation from HTL to Verilog]\label{lemma:verilog} We write $\yhfunction{tr\_verilog}$ for the translation from HTL to Verilog. (Note that this translation cannot fail, so we do not need the \yhconstant{OK} constructor here.) \begin{align*} - &\forall h, V, B \in \texttt{Safe}, \yhfunction{tr\_verilog} (h) = V \land h \Downarrow B \implies V \Downarrow B. + &\forall\ h\ V\ B, B \in \texttt{Safe} \land \yhfunction{tr\_verilog} (h) = V \land h \Downarrow B \implies V \Downarrow B. \end{align*} \end{lemma} @@ -202,7 +202,7 @@ The final lemma we need is that the Verilog we generate is deterministic. This r If a Verilog program $V$ admits both behaviours $B_1$ and $B_2$, then $B_1$ and $B_2$ must be the same. \begin{equation*} - \forall V, B_{1}, B_{2}, V \Downarrow B_{1} \land V \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} |