From 55528c1f1a11988897d46993756d6aa5873095af Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 9 Sep 2021 21:09:05 +0100 Subject: Figure -> Fig. --- verilog.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'verilog.tex') diff --git a/verilog.tex b/verilog.tex index 67ae148..772fec7 100644 --- a/verilog.tex +++ b/verilog.tex @@ -105,10 +105,10 @@ To support this computational model, we extend the Verilog module we generate wi %\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 $\mathit{fin}$ register is set; the return value is then taken from the $\mathit{ret}$ register. +Fig.~\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. -Therefore, in addition to the rules shown in Figure~\ref{fig:inference_module}, an initial state and final state need to be defined: +Therefore, in addition to the rules shown in Fig.~\ref{fig:inference_module}, an initial state and final state need to be defined: \begin{gather*} \inferrule[Initial]{\yhfunction{is\_internal}\ (P.\texttt{main})}{\yhfunction{initial\_state}\ (\yhconstant{Callstate } []\ (P.\texttt{main})\ [])}\qquad @@ -197,7 +197,7 @@ The Verilog semantics do not define a memory model for Verilog, as this is not n %\JW{It's not completely clear what the relationship is between your work and those works. The use of `only' suggests that you've re-done a subset of work that has already been done -- is that the right impression?}\YH{Hopefully that's more clear.} -This translation is represented in Figure~\ref{fig:memory_model_transl}. \compcert{} defines a map from blocks to maps from memory addresses to memory contents. Each block represents an area in memory; for example, a block can represent a global variable or a stack for a function. As there are no global variables, the main stack can be assumed to be block 0, and this is the only block we translate. +This translation is represented in Fig.~\ref{fig:memory_model_transl}. \compcert{} defines a map from blocks to maps from memory addresses to memory contents. Each block represents an area in memory; for example, a block can represent a global variable or a stack for a function. As there are no global variables, the main stack can be assumed to be block 0, and this is the only block we translate. %\JW{So the stack frame for a function called by main would be in a different block, is that the idea? Seems unusual not to have a single stack.} %\YH{Yeah exactly, it makes it much easier to reason about though, because everything is nicely isolated. This is exactly what CompCertELF and CompCertS try and solve though.} %\JW{Would global variables normally be put in blocks 1, 2, etc.?} -- cgit