Move textit to mathit

1 files changed, 13 insertions, 13 deletions

diff --git a/verilog.tex b/verilog.tex
index c0eced8..67ae148 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -72,13 +72,13 @@ The main execution of the module $\downarrow_{\text{module}}$ is split into $\do
   \centering
   \begin{minipage}{1.0\linewidth}
     \begin{gather*}
-      \inferrule[Step]{\Gamma_r[\textit{rst}] = 0 \\ \Gamma_r[\textit{fin}] = 0 \\ (m, (\Gamma_r, \Gamma_a))\ \downarrow_{\text{program}} (\Gamma_r', \Gamma_a')}{\yhconstant{State } \textit{sf }\ m\ \ \Gamma_r[\sigma]\ \ \Gamma_r\ \Gamma_a \longrightarrow \yhconstant{State } \textit{sf }\ m\ \ \Gamma_r'[\sigma]\ \ \Gamma_r'\ \Gamma_a'}\\
+      \inferrule[Step]{\Gamma_r[\mathit{rst}] = 0 \\ \Gamma_r[\mathit{fin}] = 0 \\ (m, (\Gamma_r, \Gamma_a))\ \downarrow_{\text{program}} (\Gamma_r', \Gamma_a')}{\yhconstant{State } \mathit{sf }\ m\ \ \Gamma_r[\sigma]\ \ \Gamma_r\ \Gamma_a \longrightarrow \yhconstant{State } \mathit{sf }\ m\ \ \Gamma_r'[\sigma]\ \ \Gamma_r'\ \Gamma_a'}\\
       %
-      \inferrule[Finish]{\Gamma_r[\textit{fin}] = 1}{\yhconstant{State } \textit{sf }\ m\ \sigma\ \Gamma_r\ \Gamma_a \longrightarrow \yhconstant{Returnstate } \textit{sf }\ \Gamma_r[ \textit{ret}]}\\
+      \inferrule[Finish]{\Gamma_r[\mathit{fin}] = 1}{\yhconstant{State } \mathit{sf }\ m\ \sigma\ \Gamma_r\ \Gamma_a \longrightarrow \yhconstant{Returnstate } \mathit{sf }\ \Gamma_r[ \mathit{ret}]}\\
       %
-      \inferrule[Call]{ }{\yhconstant{Callstate } \textit{sf }\ m\ \vec{r} \longrightarrow \yhconstant{State } \textit{sf }\ m\ n\ ((\yhfunction{init\_params}\ \vec{r}\ a)[\sigma \mapsto n, \textit{fin} \mapsto 0, \textit{rst} \mapsto 0])\ \epsilon}\\
+      \inferrule[Call]{ }{\yhconstant{Callstate } \mathit{sf }\ m\ \vec{r} \longrightarrow \yhconstant{State } \mathit{sf }\ m\ n\ ((\yhfunction{init\_params}\ \vec{r}\ a)[\sigma \mapsto n, \mathit{fin} \mapsto 0, \mathit{rst} \mapsto 0])\ \epsilon}\\
       %
-      \inferrule[Return]{ }{\yhconstant{Returnstate } (\yhconstant{Stackframe } r\ m\ \textit{pc }\ \Gamma_r\ \Gamma_a :: \textit{sf})\ v \longrightarrow \yhconstant{State } \textit{sf }\ m\ \textit{pc }\ (\Gamma_{r} [ \sigma \mapsto \textit{pc}, r \mapsto v ])\ \Gamma_{a}}
+      \inferrule[Return]{ }{\yhconstant{Returnstate } (\yhconstant{Stackframe } r\ m\ \mathit{pc }\ \Gamma_r\ \Gamma_a :: \mathit{sf})\ v \longrightarrow \yhconstant{State } \mathit{sf }\ m\ \mathit{pc }\ (\Gamma_{r} [ \sigma \mapsto \mathit{pc}, r \mapsto v ])\ \Gamma_{a}}
     \end{gather*}
   \end{minipage}
   \caption{Top-level small-step semantics for Verilog modules in \compcert{}'s computational framework.}%
@@ -89,25 +89,25 @@ The \compcert{} computation model defines a set of states through which executio
 
 \compcert{} executions pass through three main states:
 \begin{description}
-  \item[\texttt{State} \textit{sf} $m$ $v$ $\Gamma_{r}$ $\Gamma_{a}$] The main state when executing a function, with stack frame \textit{sf}, current module $m$, current state $v$ and variable states $\Gamma_{r}$ and $\Gamma_{a}$.
-  \item[\texttt{Callstate} \textit{sf} $m$ $\vec{r}$] The state that is reached when a function is called, with the current stack frame \textit{sf}, current module $m$ and arguments $\vec{r}$.
-  \item[\texttt{Returnstate} \textit{sf} $v$] The state that is reached when a function returns back to the caller, with stack frame \textit{sf} and return value $v$.
+  \item[\texttt{State} $\mathit{sf}$ $m$ $v$ $\Gamma_{r}$ $\Gamma_{a}$] The main state when executing a function, with stack frame $\mathit{sf}$, current module $m$, current state $v$ and variable states $\Gamma_{r}$ and $\Gamma_{a}$.
+  \item[\texttt{Callstate} $\mathit{sf}$ ${r}$] The state that is reached when a function is called, with the current stack frame $\mathit{sf}$, current module $m$ and arguments $\vec{r}$.
+  \item[\texttt{Returnstate} $\mathit{sf}$ $v$] The state that is reached when a function returns back to the caller, with stack frame $\mathit{sf}$ and return value $v$.
 \end{description}
 
 To support this computational model, we extend the Verilog module we generate with the following four registers and a RAM block:
 
 \begin{description}
   \item[program counter] The program counter can be modelled using a register that keeps track of the state, denoted as $\sigma$.
-  \item[function entry point] When a function is called, the entry point denotes the first instruction that will be executed. This can be modelled using a reset signal that sets the state accordingly, denoted as \textit{rst}.
-  \item[return value] The return value can be modelled by setting a finished flag to 1 when the result is ready, and putting the result into a 32-bit output register. These are denoted as \textit{fin} and \textit{ret} respectively.
+  \item[function entry point] When a function is called, the entry point denotes the first instruction that will be executed. This can be modelled using a reset signal that sets the state accordingly, denoted as $\mathit{rst}$.
+  \item[return value] The return value can be modelled by setting a finished flag to 1 when the result is ready, and putting the result into a 32-bit output register. These are denoted as $\mathit{fin}$ and $\mathit{ret}$ respectively.
 %\JW{Is there a mismatch between `ret' in the figure and `rtrn' in the text?}
-  \item[stack] The function stack can be modelled as a RAM block, which is implemented using an array in the module, and denoted as \textit{stk}.
-%\JW{Is there a mismatch between `st' in the figure and `stk' in the text?}\YH{It was actually between $\Gamma_{a}$ and \textit{stk}.  The \textit{st} should have been $\sigma$.}
+  \item[stack] The function stack can be modelled as a RAM block, which is implemented using an array in the module, and denoted as $\mathit{stk}$.
+%\JW{Is there a mismatch between `st' in the figure and `stk' in the text?}\YH{It was actually between $\Gamma_{a}$ and \mathit{stk}.  The \mathit{st} should have been $\sigma$.}
 \end{description}
 
-Figure~\ref{fig:inference_module} shows the inference rules for moving between the computational states.  The first, \textsc{Step}, is the normal rule of execution.  It defines one step in the \texttt{State} state, assuming that the module is not being reset, that the finish state has not been reached yet, that the current and next state are $v$ and $v'$, and that the module runs from state $\Gamma$ to $\Gamma'$ using the \textsc{Step} rule.  The \textsc{Finish} rule returns the final value of running the module and is applied when the \textit{fin} register is set; the return value is then taken from the \textit{ret} register.
+Figure~\ref{fig:inference_module} shows the inference rules for moving between the computational states.  The first, \textsc{Step}, is the normal rule of execution.  It defines one step in the \texttt{State} state, assuming that the module is not being reset, that the finish state has not been reached yet, that the current and next state are $v$ and $v'$, and that the module runs from state $\Gamma$ to $\Gamma'$ using the \textsc{Step} rule.  The \textsc{Finish} rule returns the final value of running the module and is applied when the $\mathit{fin}$ register is set; the return value is then taken from the $\mathit{ret}$ register.
 
-Note that there is no step from \texttt{State} to \texttt{Callstate}; this is because function calls are not supported, and it is therefore impossible in our semantics ever to reach a \texttt{Callstate} except for the initial call to main. So the \textsc{Call} rule is only used at the very beginning of execution; likewise, the \textsc{Return} rule is only matched for the final return value from the main function. %as there is no rule that allocates another stack frame \textit{sf} except for the initial call to main.  
+Note that there is no step from \texttt{State} to \texttt{Callstate}; this is because function calls are not supported, and it is therefore impossible in our semantics ever to reach a \texttt{Callstate} except for the initial call to main. So the \textsc{Call} rule is only used at the very beginning of execution; likewise, the \textsc{Return} rule is only matched for the final return value from the main function.
 Therefore, in addition to the rules shown in Figure~\ref{fig:inference_module}, an initial state and final state need to be defined:
 
 \begin{gather*}