From c9fb024ac728134eba560c96871119f589922468 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 10 Sep 2021 18:49:37 +0100 Subject: Add to proof section --- proof.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proof.tex') diff --git a/proof.tex b/proof.tex index 1ec8367..944649e 100644 --- a/proof.tex +++ b/proof.tex @@ -147,7 +147,7 @@ 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 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. +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. 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