Finish fixing algorithm section

1 files changed, 1 insertions, 1 deletions

diff --git a/verilog.tex b/verilog.tex
index ad9af9f..e77aa97 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -110,7 +110,7 @@ Therefore, in addition to the rules shown in Figure~\ref{fig:inferrence_module},
 
 \noindent where the initial state is the \texttt{Callstate} with an empty stack frame and no arguments for the \texttt{main} function of program $P$, where this \texttt{main} function needs to be in the current translation unit.  The final state results in the program output of value $n$ when reaching a \texttt{Returnstate} with an empty stack frame.
 
-\subsection{Memory Model}
+\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 need 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 that are used in Verilog.  The \compcert{} memory model is infinite, whereas our representation of arrays in Verilog is inherently finite.  There have already been various efforts to define a finite memory model for \compcert{}, such as CompCertS~\cite{besson18_compc}, CompCertELF~\cite{wang20_compc} and CompCertTSO~\cite{sevcik13_compc}, however, we only define the translation from \compcert{}'s standard infinite memory model to finitely sized arrays that can be represented in Verilog.