diff options
| -rw-r--r-- | algorithm.tex | 4 | ||||
| -rw-r--r-- | proof.tex | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/algorithm.tex b/algorithm.tex index 6282664..930ce00 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -121,7 +121,7 @@ endmodule \node[draw,circle,inner sep=6pt] (s0) at (0,0) {$S_{\mathit{start}} / \texttt{x}$}; \node[draw,circle,inner sep=8pt] (s1) at (1.5,-3) {$S_{0} / \texttt{1}$}; \node[draw,circle,inner sep=8pt] (s2) at (3,0) {$S_{1} / \texttt{1}$}; - \node (s2s) at ($(s2.west) + (-0.3,1)$) {\texttt{x0}}; + \node (s2s) at ($(s2.west) + (-0.3,1)$) {\texttt{00}}; \node (s2ss) at ($(s2.east) + (0.3,1)$) {\texttt{1x}}; \draw[-{Latex[length=2mm,width=1.4mm]}] ($(s0.west) + (-0.3,1)$) to [out=0,in=120] (s0); \draw[-{Latex[length=2mm,width=1.4mm]}] (s0) @@ -137,7 +137,7 @@ endmodule \end{tikzpicture} \end{subfigure} \Description{Verilog code of a state machine, and its equivalent state machine diagram.} - \caption{A simple state machine implemented in Verilog, with its diagrammatic representation on the right. The x's stand for don't cares and each transition is labelled with the values of the inputs \texttt{rst} and \texttt{y} that trigger the transition. The output that will be produced is shown in each state.}% + \caption{A simple state machine implemented in Verilog, with its diagrammatic representation on the right. The \texttt{x} stands for ``don't care'' and each transition is labelled with the values of the inputs \texttt{rst} and \texttt{y} that trigger the transition. The output that will be produced is shown in each state.}% \label{fig:tutorial:state_machine} \end{figure} @@ -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\_ins}(h) = h' \land h \Downarrow B \implies h' \Downarrow B. + \forall h, h', B \in \texttt{Safe},\quad \yhfunction{tr\_ram\_ins}(h) = h' \land h \Downarrow B \implies h' \Downarrow B. \end{align*} \end{lemma} |