diff options
Diffstat (limited to 'proof.tex')
| -rw-r--r-- | proof.tex | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -147,11 +147,11 @@ HTL can only represent a single state machine, it is therefore necessary to mode \subsubsection{From Implementation to Specification} -The first step in proving the simulation correct is to build a specification of the algorithm. The three possibilities of the transformation is that for each Verilog statement in the map at location $i$, either the statement is a load or a store, in which case it is translated to the equivalent signal representation, otherwise it is not changed. An example of the specification for 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$, either the statement is a load, a store or neither, in which case it is translated to the equivalent representation using the RAM specification, or is 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})}% - {\yhfunction{spec\_ram}\ \ \sigma\ r\ d\ c\ \ d[i \mapsto t]\ \ c\ i\ n} + {\yhfunction{spec\_ram\_tr}\ \sigma\ r\ d\ c\ d[i \mapsto t]\ c\ i\ n} \end{gather*} A similar specification is created for the load. We then also prove that the implementation of the translation proves that the specification holds. @@ -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},\quad \yhfunction{tr\_ram}(h) = h' \land h \Downarrow B \implies h' \Downarrow B. + \forall h, B \in \texttt{Safe},\quad \yhfunction{tr\_ram\_ins}(h) = h' \land h \Downarrow B \implies h' \Downarrow B. \end{align*} \end{lemma} |