Add two-dimensional

1 files changed, 2 insertions, 2 deletions

diff --git a/verilog.tex b/verilog.tex
index e3b09fa..79b4f83 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -39,7 +39,7 @@ where $\Gamma$ is the initial state of all the variables, and $\vec{m}$ is a lis
 
 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.
 
-The main change is the addition of support for two-dimensional 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:
+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{minted}{verilog}
 always @(posedge clk) begin
@@ -88,7 +88,7 @@ However, as Verilog behaves quite differently to software programming languages,
   \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, denoted as $rst$.
   \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}.
+  \item[stack] The function stack can be modelled as a RAM using a two-di\-men\-sion\-al array in the module, denoted as \textit{stk}.
 \end{description}
 
 Figure~\ref{fig:inferrence_module} 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{Step} 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.