From 8507d0413b34fcc2744a922048ce55ca06b7978f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 9 Sep 2021 20:32:12 +0100 Subject: Move textit to mathit --- verilog.tex | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'verilog.tex') 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*} -- cgit