From 5ea6be2ade46c7150d33e9fb0c32046be74abb43 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 21 Jul 2021 22:54:28 +0200 Subject: Add some small fixes to the paper --- proof.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'proof.tex') diff --git a/proof.tex b/proof.tex index 1668d88..1218ecd 100644 --- a/proof.tex +++ b/proof.tex @@ -146,11 +146,11 @@ Another simulation proof is performed to prove that the insertion of the RAM is The other invariants and assumptions for defining two matching states in HTL are quite similar to the simulation performed in Lemma~\ref{lemma:simulation_diagram}, such as ensuring that the states have the same value, and that the values in the registers are less-defined. In particular, the less-defined relation matches up all the registers, except for the new registers introduced by the RAM. -\begin{lemma}[Forward simulation from HTL to Verilog]\label{lemma:htl_ram} - Given an HTL program, the forward simulation relation should hold after inserting the RAM. +\begin{lemma}[Forward simulation from HTL to HTL after inserting the RAM]\label{lemma:htl_ram} + 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{spec\_ram} (h) = h' \land h \Downarrow B \implies h' \Downarrow B. + &\forall h, B \in \texttt{Safe}, \yhfunction{tr\_ram}(h) = h' \land h \Downarrow B \implies h' \Downarrow B. \end{align*} \end{lemma} -- cgit