Update on Overleaf.

1 files changed, 12 insertions, 5 deletions

diff --git a/verilog.tex b/verilog.tex
index 79b4f83..2905d6e 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -37,22 +37,29 @@ where $\Gamma$ is the initial state of all the variables, and $\vec{m}$ is a lis
 
 \subsection{Changes to the Semantics}
 
-Some small changes were made to the semantics proposed by \citet{loow19_proof_trans_veril_devel_hol} to make it suitable as a HLS target.
+Four changes were made to the semantics proposed by \citet{loow19_proof_trans_veril_devel_hol} to make it suitable as a HLS target.
 
-The main change is the addition of support for two-di\-men\-sion\-al 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, which can also be expressed as an array of bitvectors, which is the path we took instead.  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{description}
+
+\item[Array support]
+    
+\end{description}
 
+
+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{minted}{verilog}
+reg [31:0] x [1:0];
 always @(posedge clk) begin
   x[0] = 1;
   x[1] <= 1;
 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.  Our state $\Gamma$ in practice are therefore split up into a map $\Gamma_{r}$, for instantaneous updates to variables, and $\Gamma_{a}$ for instantaneous updates to arrays, where the merge function then ensures that only the modified indices get updated when it is merged with the nonblocking map equivalent $\Delta_{a}$.
+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}$.
 
 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.
+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.
 
 \subsection{Verilog Semantics in \compcert{}'s Model}