diff options
Diffstat (limited to 'verilog.tex')
| -rw-r--r-- | verilog.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/verilog.tex b/verilog.tex index 11087b0..d7980f0 100644 --- a/verilog.tex +++ b/verilog.tex @@ -37,7 +37,7 @@ where $\Gamma$ is the initial state of all the variables, $\epsilon$ is the empt \subsection{Changes to the Semantics} -Five changes were made to the semantics proposed by \citet{loow19_proof_trans_veril_devel_hol} to make it suitable as a HLS target. +Five changes were made to the semantics proposed by \citet{loow19_proof_trans_veril_devel_hol} to make it suitable as an HLS target. \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. |