summaryrefslogtreecommitdiffstats
path: root/proof.tex
diff options
context:
space:
mode:
Diffstat (limited to 'proof.tex')
-rw-r--r--proof.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/proof.tex b/proof.tex
index e8aa4ba..a24aac8 100644
--- a/proof.tex
+++ b/proof.tex
@@ -109,7 +109,7 @@ We can now define the simulation diagram for the translation. The 3AC state can
\subsection{Forward simulation of RAM insertion}\label{sec:proof:ram_insertion}
-HTL can only represent a single state machine, it is therefore necessary to model
+HTL can only represent a single state machine, it is therefore necessary to model the RAM abstractly to reason about the correctness of replacing the direct read and writes to the array to load and stores to a RAM. The abstract specification used for the RAM is shown in Figure~\ref{fig_htl_ram_spec}, which defines how the RAM $r$ will behave with all the possible combinations of the input signals.
\begin{figure}
\centering