Add more

3 files changed, 79 insertions, 42 deletions

diff --git a/appendix.tex b/appendix.tex
index 1e3cdb3..39dd72d 100644
--- a/appendix.tex
+++ b/appendix.tex
@@ -70,6 +70,42 @@
   \label{fig:inferrence_module}
 \end{figure*}
 
+\begin{figure}
+  \centering
+\begin{minted}{coq}
+Inductive match_states :
+  3AC.state -> HTL.state -> Prop :=
+| match_state : forall asa asr sf f sp
+    sp' rs mem m st res
+    (MASSOC : match_assocmaps f rs asr)
+    (TF : tr_module f m)
+    (WF : state_st_wf m (HTL.State res m st asr asa))
+    (MF : match_frames sf res)
+    (MARR : match_arrs m f sp mem asa)
+    (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0))
+    (RSBP : reg_stack_based_pointers sp' rs)
+    (ASBP : arr_stack_based_pointers sp' mem
+              (f.(3AC.fn_stacksize)) sp)
+    (BOUNDS : stack_bounds sp (f.(3AC.fn_stacksize)) mem)
+    (CONST : match_constants m asr),
+    match_states
+      (3AC.State sf f sp st rs mem)
+      (HTL.State res m st asr asa)
+| match_returnstate : forall v v' stack mem res
+    (MF : match_frames stack res),
+    val_value_lessdef v v' ->
+    match_states
+      (3AC.Returnstate stack v mem)
+      (HTL.Returnstate res v')
+| match_initial_call :
+  forall f m m0 (TF : tr_module f m),
+    match_states
+      (3AC.Callstate nil (AST.Internal f) nil m0)
+      (HTL.Callstate nil m nil).
+\end{minted}
+  \caption{\texttt{match\_states} predicate used to match an 3AC state to the equivalent HTL state.}\label{fig:match_states}
+\end{figure}
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "main"
diff --git a/proof.tex b/proof.tex
index a01b688..fcad541 100644
--- a/proof.tex
+++ b/proof.tex
@@ -25,42 +25,6 @@ The forward simulation between C and Verilog can be separated into forward simul
 
 As HTL is quite different to 3AC, this first translation is the most involved translation and therefore requires a larger proof, as the translation from 3AC instructions to Verilog statements needs to be proven correct.  In addition to that, the semantics of HTL are also quite different to the 3AC semantics, as instead of defining small-step semantics for each construct in Verilog, the semantics are instead defined over one clock cycle.
 
-\begin{figure}
-  \centering
-\begin{minted}{coq}
-Inductive match_states :
-  3AC.state -> HTL.state -> Prop :=
-| match_state : forall asa asr sf f sp
-    sp' rs mem m st res
-    (MASSOC : match_assocmaps f rs asr)
-    (TF : tr_module f m)
-    (WF : state_st_wf m (HTL.State res m st asr asa))
-    (MF : match_frames sf res)
-    (MARR : match_arrs m f sp mem asa)
-    (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0))
-    (RSBP : reg_stack_based_pointers sp' rs)
-    (ASBP : arr_stack_based_pointers sp' mem
-              (f.(3AC.fn_stacksize)) sp)
-    (BOUNDS : stack_bounds sp (f.(3AC.fn_stacksize)) mem)
-    (CONST : match_constants m asr),
-    match_states
-      (3AC.State sf f sp st rs mem)
-      (HTL.State res m st asr asa)
-| match_returnstate : forall v v' stack mem res
-    (MF : match_frames stack res),
-    val_value_lessdef v v' ->
-    match_states
-      (3AC.Returnstate stack v mem)
-      (HTL.Returnstate res v')
-| match_initial_call :
-  forall f m m0 (TF : tr_module f m),
-    match_states
-      (3AC.Callstate nil (AST.Internal f) nil m0)
-      (HTL.Callstate nil m nil).
-\end{minted}
-  \caption{\texttt{match\_states} predicate used to match an 3AC state to the equivalent HTL state.}\label{fig:match_states}
-\end{figure}
-
 The first step in proving the forward simulation is to define a relation that matches an 3AC state to an HTL state, which shows when the states are equivalent.  This relation also defines assumptions that are made about the 3AC code that we receive, so that these assumptions can be used to prove the translations correct.  These assumptions then have to be proven to always hold assuming the HTL code was created by the translation algorithm.  The \texttt{match\_states} predicate that is used to match the states of the 3AC code to the HTL code is shown in Figure~\ref{fig:match_states}.  The type \texttt{match\_states} declared in Figure~\ref{fig:match_states} has three constructors.
 
 \begin{enumerate}
diff --git a/verilog.tex b/verilog.tex
index 95ec74e..8c63b86 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -19,17 +19,16 @@ The semantics of Verilog differ from regular programming languages, as it is use
 Two types of assignments are supported in always blocks: nonblocking and blocking assignment.  Nonblocking assignment modifies the signal at the end of the timestep and atomically.  Blocking assignment, on the other hand, assigns the variable directly in the always block for later signals to pick up.  To model both these assignments, the state $\Sigma$ has to be split into two parts: $\Gamma$, containing the current values of all variables, and $\Delta$, containing the values that will be assigned to the variables at the end of the clock cycle, we can therefore say that $\Sigma = (\Gamma, \Delta)$.  The nonblocking assignment can therefore be expressed as the following:
 
 \begin{equation*}
-  \inferrule[Nonblocking Reg]{(\Gamma, e) \longrightarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ <= } e) \longrightarrow_{\text{stmnt}} (\Gamma, \Delta [d \mapsto v])}\\
+  \inferrule[Nonblocking Reg]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \longrightarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ <= } e) \longrightarrow_{\text{stmnt}} (\Gamma, \Delta [n \mapsto v])}\\
 \end{equation*}
 
-\noindent where assuming that $\longrightarrow_{\text{expr}}$ evaluates an expression $e$ to a value $v$, then the nonblocking assignment $d\ \yhkeyword{ <= } e$ will update the future state of the variable $d$ with value $v$.  Finally, at the end of the clock cycle, the registers need to be updated with their future values in $\Delta$, which can be shown by the rule in the semantics that runs a whole module, where $m$ is the module definition, $m_{i}$ is a list of variable declarations or always blocks inside $m$, $\sigma$ is the register that holds the current state the module is in, who's value should correspond to the program counter in 3AC and finally \textit{sf} is the current stack frame that has to be kept track on to uniquely identify the current state.
+\noindent where assuming that $\longrightarrow_{\text{expr}}$ evaluates an expression $e$ to a value $v$, then the nonblocking assignment $d\ \yhkeyword{ <= } e$ will update the future state of the variable $d$ with value $v$.  Finally, at the end of the clock cycle, the registers need to be updated with their future values in $\Delta$, which can be shown by the rule in the semantics that runs a whole module, $\vec{m}$ is a list of variable declarations and always blocks, and the $\longrightarrow_{\vec{m}}$ evaluates these sequentially and obtains the final state $(\Gamma', \Delta')$.
 
 \begin{equation*}
-\inferrule[Module]{\Gamma\ !\ \sigma = \yhconstant{Some } v_{\sigma} \\ (m_{i}, \Gamma, \epsilon)\ \longrightarrow_{\vec{m}} (m_{i}, \Gamma', \Delta') \\ (\Gamma' // \Delta')\ !\ \sigma = \yhconstant{Some }
-v_{\sigma}'}{\yhconstant{State } \textit{sf }\ m\ v_{\sigma}\ \Gamma \longrightarrow \yhconstant{State } \textit{sf }\ m\ v_{\sigma}'\ (\Gamma' // \Delta')}
+  \inferrule[Module]{(\Gamma, \epsilon, \vec{m})\ \longrightarrow_{\vec{m}} (\Gamma', \Delta')}{(\Gamma, \yhkeyword{module } \yhconstant{main} \yhkeyword{(...);}\ \vec{m}\ \yhkeyword{endmodule}) \longrightarrow_{m} (\Gamma' // \Delta')}
 \end{equation*}
 
-This rule describes how the top-level definition of \texttt{State} changes when one step is performed on a module $m$.
+\noindent This rule dictates how the whole module runs in one clock cycle, from an initial state of all the variables $\Gamma$, to a final state $(\Gamma' // \Delta')$, where $//$ defines a merge between the two maps from variable names to values, where the right hand side values take priority if there is a conflict.  This rule correctly implements the behaviours for the blocking and nonblocking assignment by overwriting the assignments made through blocking assignment at the end of the clock cycle with the atomic assignments from the nonblocking assignments.
 
 When targeting a hardware description language such as Verilog, it is important to be consistent between simulating the hardware and the behaviour of the synthesised result on actual hardware.  In the target Verilog semantics, only clocked always blocks are supported as these ensure that there are not mismatches between simulation and synthesis, as combinational always blocks that trigger on any change of an internal signal may behave differently in simulation or synthesis based on the order of operations.  This limitation in the semantics therefore helps keep the Verilog correct and consistent.  In addition to that, only nonblocking assignment is used in signals that are used in multiple always blocks, which stops any race conditions from occurring as all the signal updates happen deterministically.  Finally, a specific order of evaluation for the always blocks is chosen, and because of the limitations listed before, choosing an order is guaranteed to have the same behaviour as executing the always blocks in any order.
 
@@ -46,12 +45,50 @@ always @(posedge clk) begin
 end
 \end{minted}
 
-The code above modifies one array value using nonblocking assignment and it then modifies a second entry in the array with nonblocking assignment.  If the existing semantics used for values was used to update the array, then during the merge of values for the array, the array \texttt{x} from the nonblocking association map would replace the array from the blocking association map.  This would replace \texttt{x[0]} with it's original value and therefore behave incorrectly.  Instead, updates to arrays need to be recorded for each index in the array, and merging of the blocking and nonblocking queue needs to take into account each index separately.  
+The code above modifies one array value using nonblocking assignment and it then modifies a second entry in the array with nonblocking assignment.  If the existing semantics used for values was used to update the array, then during the merge of values for the array, the array \texttt{x} from the nonblocking association map would replace the array from the blocking association map.  This would replace \texttt{x[0]} with it's original value and therefore behave incorrectly.  Instead, updates to arrays need to be recorded for each index in the array, and merging of the blocking and nonblocking queue needs to take into account each index separately.
 
 Explicit support for declaring inputs, outputs and internal variables was added to the semantics to make sure that the generated Verilog also contains the correct declarations.  This adds some guarantees to the generated Verilog and ensures that it synthesises and simulates correctly.
 
 In addition to adding support for two-dimensional arrays, support for receiving external inputs was removed from the semantics for the case of simplicity, as these are not needed for an HLS target.  The main module in Verilog models the main function in C, and as the inputs to a C function shouldn't change during it's execution, there is no need to add support for external inputs for Verilog modules.  Finally, another simplification to the semantics that was made is to use 32 bit integers instead of arrays of booleans for the bitvector representation.  As the translation only currently has support for \texttt{int}, it is possible to simplify the semantics further and not have to handle bitvectors of an arbitrary size.
 
+\subsection{Integrating the Semantics in \compcert{}'s Model}
+
+\begin{figure*}
+  \centering
+  \begin{minipage}{1.0\linewidth}
+    \begin{gather*}
+      \inferrule[Module]{\Gamma_{r} ! s_{t} = \texttt{Some } v \\ (m_{i}, \Gamma_{r}^{0}, \Gamma_{a}^{0}, \epsilon, \epsilon\ l)\ \longrightarrow_{\vec{m}} (m_{i}, \Gamma_{r}^{1}, \Gamma_{a}^{1}, \Delta_{r}^{1}, \Delta_{a}^{1}) \\ (\Gamma_{r}^{1} // \Delta_{r}^{1}) ! s_{t} = \texttt{Some } v'}{\texttt{State } \textit{sf }\ m\ v\ \Gamma_{r}^{0}\ \Gamma_{a}^{0} \longrightarrow \texttt{State } \textit{sf }\ m\ v'\ (\Gamma_{r}^{1} // \Delta_{r}^{1})\ (\Gamma_{a}^{1} // \Delta_{a}^{1})}\\
+      %
+      \inferrule[Finish]{\Gamma_{r}!\textit{fin} = \texttt{Some } 1 \\ \Gamma_{r}!\textit{ret} = \texttt{Some } r}{\texttt{State } \textit{sf }\ m\ s_{t}\ \Gamma_{r}\ \Gamma_{a} \longrightarrow \texttt{Returnstate } \textit{sf }\ r}\\
+      %
+      \inferrule[Call]{ }{\texttt{Callstate } []\ m\ \vec{r} \longrightarrow \texttt{State } []\ m\ n\ (\textit{init\_params }\ \vec{r}\ a // \{s_{t} \rightarrow n\})}\\
+      %
+      \inferrule[Return]{ }{\texttt{Returnstate } (\texttt{Stackframe } r\ m\ \textit{pc }\ \Gamma_{r}\ \Gamma_{a} :: \textit{sf}) \longrightarrow \texttt{State } \textit{sf }\ m\ \textit{pc }\ (\Gamma_{r} // \{ \textit{st} \rightarrow \textit{pc}, r \rightarrow i \})\ \epsilon}
+    \end{gather*}
+  \end{minipage}
+  \caption{Inferrence rules for modules}%
+  \label{fig:inferrence_module}
+\end{figure*}
+
+\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}
+  \item[\texttt{State}] The main state when executing a function.
+  \item[\texttt{Callstate}] The state that is reached when a function is called.
+  \item[\texttt{Returnstate}] The state that is reached when a function returns back to the caller.
+\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.
+
+\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$.
+  \item[function entry point] When a function is called, the entry point denotes the first instruction that will be executed, which can be modelled using a reset signal that sets the state accordingly.
+  \item[return value] The return value can be modelled by setting a finished flag to one when the result is ready, and putting the result into a 32-bit output register, denoted as \textit{fin} and \textit{rtrn} respectively.
+  \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{Isn't the 'main' addition that the PL community may not have seen the always blocks? It can be counter-intuitive to them. Also have you intentionally avoided assign statements? Finally, what is $\epsilon$ in the syntax?}\YH{Yes, I will probably have to explain always blocks some more, I'll try and add a paragraph about them.  Yes, assign statements are quite complex to model and many semantics do not model them.  They are also not needed for translation.  The $\epsilon$ is an empty skip statement, which is just a semicolon.}
 
 %%% Local Variables: