Update on Overleaf.

1 files changed, 11 insertions, 16 deletions

diff --git a/verilog.tex b/verilog.tex
index c232708..e36abc0 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -39,31 +39,26 @@ where $\Gamma$ is the initial state of all the variables, and $\vec{m}$ is a lis
 
 Four changes were made to the semantics proposed by \citet{loow19_proof_trans_veril_devel_hol} to make it suitable as a HLS target.
 
-\begin{description}
-
-\item[Adding array support] The main change is the addition of support for arrays, which are needed to model RAM in Verilog.  RAM is needed to model the stack in C efficiently, without having to declare a variable for each possible stack location. % In the original semantics, RAMs (as well as inputs and outputs to the module) could be modelled using a function from variable names (strings) to values, which could be modified accordingly to model inputs to the module.  This is quite an abstract description of memory and can also be expressed as an array of bitvectors instead, which is the path we took. This requires the addition of array operators to the semantics and correct reasoning of loads and stores to the array in different \alwaysblock{}s simultaneously.  
+\paragraph{Adding array support}
+The main change is the addition of support for arrays, which are needed to model RAM in Verilog.  RAM is needed to model the stack in C efficiently, without having to declare a variable for each possible stack location. % In the original semantics, RAMs (as well as inputs and outputs to the module) could be modelled using a function from variable names (strings) to values, which could be modified accordingly to model inputs to the module.  This is quite an abstract description of memory and can also be expressed as an array of bitvectors instead, which is the path we took. This requires the addition of array operators to the semantics and correct reasoning of loads and stores to the array in different \alwaysblock{}s simultaneously.  
 Consider the following Verilog code:
+\begin{center}
 \begin{minted}{verilog}
-reg [31:0] x [1:0];
+reg [31:0] x[1:0];
 always @(posedge clk) begin
   x[0] = 1;
   x[1] <= 1;
 end
 \end{minted}
-which modifies one array element using blocking assignment and then a second using nonblocking assignment. If the existing semantics were used to update the array, then during the merge, the entire array \texttt{x} from the nonblocking association map would replace the entire array from the blocking association map.  This would replace \texttt{x[0]} with its original value and therefore behave incorrectly. Accordingly, we modified the maps so they record updates on a per-element basis, and then merging in a fine-grained manner. Our state $\Gamma$ is therefore split up into a map $\Gamma_{r}$, for instantaneous updates to variables, and $\Gamma_{a}$ for instantaneous updates to arrays; $\Delta$ is split similarly. The merge function then ensures that only the modified indices get updated when it is merged with the nonblocking map equivalent $\Delta_{a}$.
-
-\item[Adding declarations] 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.
-    
-\end{description}
-
-
-
-
+\end{center}
+which modifies one array element using blocking assignment and then a second using nonblocking assignment. If the existing semantics were used to update the array, then during the merge, the entire array \texttt{x} from the nonblocking association map would replace the entire array from the blocking association map.  This would replace \texttt{x[0]} with its original value and therefore behave incorrectly. Accordingly, we modified the maps so they record updates on a per-element basis. Our state $\Gamma$ is therefore split up into $\Gamma_{r}$ for instantaneous updates to variables, and $\Gamma_{a}$ for instantaneous updates to arrays; $\Delta$ is split similarly. The merge function then ensures that only the modified indices get updated when $\Gamma_{a}$ is merged with the nonblocking map equivalent $\Delta_{a}$.
 
+\paragraph{Adding declarations} 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 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 its 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.
+\paragraph{Removing support for external inputs to modules} Support for receiving external inputs was removed from the semantics for simplicity, as these are not needed for an HLS target. The main module in Verilog models the main function in C, and since the inputs to a C function shouldn't change during its execution, there is no need for external inputs for Verilog modules.  
 
-\subsection{Verilog Semantics in \compcert{}'s Model}
+\paragraph{Simplifying representation of bitvectors} Finally, we use 32-bit integers to represent bitvectors rather of arrays of Booleans. This is because \vericert{} (currently) only supports types represented by 32 bits.
+\subsection{Integrating the Verilog Semantics into \compcert{}'s Model}
 
 \begin{figure*}
   \centering
@@ -82,7 +77,7 @@ In addition to adding support for arrays, support for receiving external inputs
   \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. 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{} has three main states that need to be defined:
+\compcert{} defines a specific model of computation that 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{} has three main states that need to be defined:
 
 \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}$.