From 3d60630d5a7cb366f9571f1b8d32d51b26b0a802 Mon Sep 17 00:00:00 2001 From: John Wickerson Date: Mon, 13 Sep 2021 08:31:57 +0000 Subject: Update on Overleaf. --- proof.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proof.tex b/proof.tex index 2423277..da4fab1 100644 --- a/proof.tex +++ b/proof.tex @@ -148,7 +148,7 @@ HTL can only represent a single state machine, so we must model the RAM abstract \subsubsection{From Implementation to Specification} -The first step in proving the simulation correct is to build a specification of the translation algorithm. There are three possibilities for the transformation of an instruction. For each Verilog statement in the map at location $i$, the statement is either a load, a store, or neither. The load or store is translated to the equivalent representation using the RAM specification and all other instructions are left intact. An example of the specification for the translation of the store instruction is shown below, where $\sigma$ is state register, $r$ is the RAM, $d$ and $c$ are the input data-path and control logic maps, and $i$ is the current state. $n$ is the newly inserted state (which only applies to the translation of loads). +The first step in proving the simulation correct is to build a specification of the translation algorithm. There are three possibilities for the transformation of an instruction. For each Verilog statement in the map at location $i$, the statement is either a load, a store, or neither. The load or store is translated to the equivalent representation using the RAM specification and all other instructions are left intact. An example of the specification for the translation of the store instruction is shown below, where $\sigma$ is state register, $r$ is the RAM, $d$ and $c$ are the input data-path and control logic maps, and $i$ is the current state. $n$ is the newly inserted state, which only applies to the translation of loads). \begin{gather*} \inferrule[Store Spec]{ d[i] = (r.mem\texttt{[}e_{1}\texttt{]} \texttt{ <= } e_{2}) \\ t = (r.u\_en \texttt{ <= } \neg r.u\_en; r.wr\_en \texttt{ <= } 1; r.d\_in \texttt{ <= } e_{2}; r.addr \texttt{ <= } e_{1})}% -- cgit