Update on Overleaf.

1 files changed, 5 insertions, 2 deletions

diff --git a/verilog.tex b/verilog.tex
index bd36873..1f3a3dc 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -81,6 +81,8 @@ In addition to adding support for two-dimensional arrays, support for receiving
   \label{fig:inferrence_module}
 \end{figure*}
 
+\NR{Would signposting this section at the start: "\compcert{} defines a specific model of computation which all semantics have to follow in order to prove properties about them. In this section, we first describe three of \compcert{}'s original computational states. Then, we describe the five registers and semantic rules we add to Verilog semantics to integrate it to the \compcert{} model."} 
+
 \compcert{} defines a specific model of computation which all semantics have to follow in order to prove properties about them.  \compcert{} has three main states that need to be defined:
 
 \begin{description}
@@ -90,6 +92,7 @@ In addition to adding support for two-dimensional arrays, support for receiving
 \end{description}
 
 However, as Verilog behaves quite differently to software programming languages, this model does not match the Verilog semantics.  Instead, the module definition in Verilog needs to be enriched to support this model of computation, by adding required signals to the inputs and outputs of modules.
+\NR{I understand this better. Maybe a concise way of saying this is: "The CompCert computation model require our Verilog semantics to be enriched. In order to support the three CompCert states, our module definitions require five additional Verilog registers."}
 
 \begin{description}
   \item[program counter] First of all, the program counter needs to be modelled, which can be done using a register which keeps track of state, denoted as $\sigma$.
@@ -98,10 +101,10 @@ However, as Verilog behaves quite differently to software programming languages,
   \item[stack] The function stack can be modelled as a RAM using a two-dimensional array in the module, denoted as \textit{stk}.
 \end{description}
 
-Figure~\ref{fig:inferrence_module}\NR{This ref points to Figure 14 instead of Figure 5!} shows the inference rules that convert from one state to another.  The first rule \textsc{Step} is the normal rule of execution.  Assuming that the module is not being reset, and that the finish state has not been reached yet and that the current and next state are $v$ and $v'$, and finally that the module runs from state $\Gamma$ to $\Gamma'$ using the \textsc{Module} rule, we can then define one step in the \texttt{State}.  The \textsc{Finish} rule is the rule that 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:inferrence_module}\NR{This ref points to Figure 14 instead of Figure 5!} shows the inference rules that convert from one state to another.  The first rule \textsc{Step} is the normal rule of execution.  Assuming that the module is not being reset, and that the finish state has not been reached yet and that the current and next state are $v$ and $v'$, and finally that the module runs from state $\Gamma$ to $\Gamma'$ using the \textsc{Module} rule, we can then define one step in the \texttt{State}.\NR{No module rule in Fig. 5?}  The \textsc{Finish} rule is the rule that 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.
 
 
-The first thing to note about the \textsc{Call} rule is that there is no step from \texttt{State} to \texttt{Callstate}, as function calls are not supported, and it is therefore impossible in our semantics to ever reach a \texttt{Callstate} except for the initial call to main.  The same can be said about the \textsc{Return} state rule, which will only be 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.  Therefore, in addition to the rules shown in Figure~\ref{fig:inferrence_module}, an initial state and final state need to be defined.
+The first thing to note about the \textsc{Call} rule is that there is no step from \texttt{State} to \texttt{Callstate}, as function calls are not supported, and it is therefore impossible in our semantics to ever reach a \texttt{Callstate} except for the initial call to main.  The same can be said about the \textsc{Return} state rule, which will only be 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.  Therefore, in addition to the rules shown in Figure~\ref{fig:inferrence_module}\NR{Wrong figure again}, an initial state and final state need to be defined.
 
 \begin{align*}
   \texttt{initial:}\quad &\forall P,\ \yhconstant{Callstate } []\ P.\texttt{main } []\\