Clarify memory model section

1 files changed, 1 insertions, 1 deletions

diff --git a/verilog.tex b/verilog.tex
index 772fec7..82fc685 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -119,7 +119,7 @@ Therefore, in addition to the rules shown in Fig.~\ref{fig:inference_module}, an
 
 \subsection{Memory Model}\label{sec:verilog:memory}
 
-The Verilog semantics do not define a memory model for Verilog, as this is not needed for a hardware description language.  There is no preexisting architecture that Verilog will produce; it can describe any memory layout that is needed.  Instead of having specific semantics for memory, the semantics only needs to support the language features that can produce these different memory layouts, these being Verilog arrays.  We therefore define semantics for updating Verilog arrays using blocking and nonblocking assignment.  We then have to prove that the C memory model that \compcert{} uses matches with the interpretation of arrays used in Verilog.  The \compcert{} memory model is infinite, whereas our representation of arrays in Verilog is inherently finite.  There have already been efforts to define a general finite memory model for all compiler passes in \compcert{}, such as Comp\-Cert\-S~\cite{besson18_compc}, or to translate to a more concrete finite memory model such as in Comp\-Cert\-ELF~\cite{wang20_compc} and Comp\-Cert\-TSO~\cite{sevcik13_compc}, however, we define the translation from \compcert{}'s standard infinite memory model to finite arrays that can be represented in Verilog, leaving the compiler passes intact.  There is therefore no more memory model in Verilog, and all the interactions to memory are encoded in the hardware itself.
+The Verilog semantics do not define a memory model for Verilog, as this is not needed for a hardware description language.  There is no preexisting architecture that Verilog will produce; it can describe any memory layout that is needed.  Instead of having specific semantics for memory, the semantics only needs to support the language features that can produce these different memory layouts, these being Verilog arrays.  We therefore define semantics for updating Verilog arrays using blocking and nonblocking assignment.  We then have to prove that the C memory model that \compcert{} uses matches with the interpretation of arrays used in Verilog.  The \compcert{} memory model is infinite, whereas our representation of arrays in Verilog is inherently finite.  There have already been efforts to define a general finite memory model for all intermediate languages in \compcert{}, such as \compcert{}\-S~\cite{besson18_compc} or \compcert{}-TSO~\cite{sevcik13_compc}, or keeping the intermediate languages intact and translate to a more concrete finite memory model in the back end, such as in \compcert{}\-ELF~\cite{wang20_compc}.  We also define such a translation from \compcert{}'s standard infinite memory model to finite arrays that can be represented in Verilog.  There is therefore no more notion of an abstract memory model and all the interactions to memory are encoded in the hardware itself.
 
 %\JW{I'm not quite sure I understand. Let me check: Are you saying that previous work has shown how all the existing CompCert passes can be adapted from an infinite to a finite memory model, but what we're doing is leaving the default (infinite) memory model for the CompCert front end, and just converting from an infinite memory model to a finite memory model when we go from 3AC to HTL?}\YH{Yes exactly, most papers changed the whole memory model to thread through properties that were then needed in the back end, but we currently don't need to do that.  I need to double check though for CompCertELF, it doesn't actually seem to be the case.  Will edit this section later.}