Add to proof section

1 files changed, 2 insertions, 2 deletions

diff --git a/verilog.tex b/verilog.tex
index 1f3a3dc..03cafad 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -5,7 +5,7 @@
 This section describes the Verilog semantics that were \JW{was} chosen for the target language, including the changes that were made to the semantics to make it \JWcouldcut{a better fit} a \JW{suitable} HLS target.  The Verilog standard is quite large~\cite{06_ieee_stand_veril_hardw_descr_languag,05_ieee_stand_veril_regis_trans_level_synth}, but the syntax and semantics can be reduced to a small subset that \vericert{} needs to target.
 \NR{Have we discussed what our options were and why we chose the HOL4 semantics?} \JW{Good point -- we should cite the Maude semantics too. I think that's the only viable alternative.}\YH{Yes, I should make that more clear, I cited Meredith semantics in the algorithm section, will add maude as well, the main reason is practicality and we don't need continuous assignment, basically the same reasons that Loow used to justify creating his own semantics.}
 
-The Verilog semantics \JW{we use is ported to Coq from} a semantics written in HOL4  by \citet{loow19_verif_compil_verif_proces}.% which was used to create a formal translation from a logic representation encoded in the HOL4~\cite{slind08_brief_overv_hol4} theorem prover into an equivalent Verilog design. 
+The Verilog semantics we use is ported to Coq from a semantics written in HOL4  by \citet{loow19_proof_trans_veril_devel_hol}, used to prove the translation from HOL4 to Verilog~\cite{loow19_verif_compil_verif_proces}.% which was used to create a formal translation from a logic representation encoded in the HOL4~\cite{slind08_brief_overv_hol4} theorem prover into an equivalent Verilog design. 
 This semantics is quite practical as it is restricted to a small subset of Verilog, which can nonetheless be used to model all hardware constructs one would want to design.  The main features that are not supported by the syntax and semantics are continuous assignment and combinational always blocks.
 \NR{Shall we use special font fo always-blocks: maybe \alwaysblock{}}
 
@@ -44,7 +44,7 @@ When targeting a hardware description language such as Verilog, it is important
 
 \subsection{Changes to the Semantics}
 
-Some small changes were made to the semantics proposed by \citet{loow19_verif_compil_verif_proces} to make it suitable as a HLS target.
+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 always blocks simultaneously.  Consider the following Verilog code: