Update on Overleaf.

1 files changed, 7 insertions, 6 deletions

diff --git a/verilog.tex b/verilog.tex
index 9b19b87..d144f90 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -2,7 +2,7 @@
 
 \newcommand{\alwaysblock}{always-block}
 
-This section describes the Verilog semantics that was chosen for the target language, including the changes that were made to the semantics to make it a 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.
+This section describes the Verilog semantics that was chosen for the target language, including the changes that were made to the semantics to make it a 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.  This section  also describes how \vericert{}'s representation of memory differs from \compcert{}'s memory model.
 
 The Verilog semantics we use is ported to Coq from a semantics written in HOL4 by \citet{loow19_proof_trans_veril_devel_hol} and 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 the hardware constructs required for HLS.  The main features that are excluded are continuous assignment and combinational \alwaysblock{}s; these are modelled in other semantics such as that by~\citet{meredith10_veril}. %however, these are not necessarily needed, but require more complicated event queues and execution model.
@@ -119,10 +119,6 @@ Therefore, in addition to the rules shown in Figure~\ref{fig:inference_module},
 
 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 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 all compiler passes in \compcert{}, such as Comp\-Cert\-S~\cite{besson18_compc}, 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 finitely sized arrays that can be represented in Verilog, leaving the compiler passes intact.
 
-%\JW{It's not completely clear what the relationship is between your work and those works. The use of `only' suggests that you've re-done a subset of work that has already been done -- is that the right impression?}\YH{Hopefully that's more clear.}
-
-This translation is represented in Figure~\ref{fig:memory_model_transl}, where \compcert{} defines a map from blocks to maps from memory address to memory contents.  Instead, our Verilog semantics define two finitely sized arrays of optional values, one for the blocking assignments map $\Gamma_{\rm a}$ and one for the nonblocking assignments map $\Delta_{\rm a}$.  The optional values are present to ensure correct merging of the two association maps at the end of the clock cycle.
-
 \begin{figure}
   \centering
   \begin{tikzpicture}
@@ -132,6 +128,7 @@ This translation is represented in Figure~\ref{fig:memory_model_transl}, where \
     \node[right] at (7,-0.3) {\small \textbf{Verilog Memory Representation}};
     \node[right] (x0) at (0.2,-1.9) {\small 0};
     \node[right] (x1) at (0.2,-2.5) {\small 1};
+    \node[rotate=90] (x2) at (0.43,-3.1) {$\cdots$};
     \foreach \x in {0,...,6}{%
       \node[right] (s\x) at (2.5,-1-\x*0.3) {\small \x};
       \node[right] (t\x) at (4,-1-\x*0.3) {};
@@ -191,9 +188,13 @@ This translation is represented in Figure~\ref{fig:memory_model_transl}, where \
     \draw (7,-4.3) -- (12,-4.3);
     \node at (9.5,-4.7) {\small \texttt{stack[0] <= 0xDEADBEEF;}};
   \end{tikzpicture}
-  \caption{Change in the memory model during the translation of 3AC to HTL.  This is immediately after the assignment to the array.}\label{fig:memory_model_transl}
+  \caption{Change in the memory model during the translation of 3AC to HTL.  The state of the memories in each case is right after the execution of the store to memory.}\label{fig:memory_model_transl}
 \end{figure}
 
+%\JW{It's not completely clear what the relationship is between your work and those works. The use of `only' suggests that you've re-done a subset of work that has already been done -- is that the right impression?}\YH{Hopefully that's more clear.}
+
+This translation is represented in Figure~\ref{fig:memory_model_transl}, where \compcert{} defines a map from blocks to maps from memory address to memory contents.  Each block represents an area in memory, for example, a block can represent a global variable or a stack for a function.  Instead, our Verilog semantics define two finitely sized arrays of optional values, one for the blocking assignments map $\Gamma_{\rm a}$ and one for the nonblocking assignments map $\Delta_{\rm a}$.  The optional values are present to ensure correct merging of the two association maps at the end of the clock cycle.  During our translation we only convert block 0 to a Verilog memory, and ensure that it is the only block that is present.  This means that the block necessarily represents the stack of the main function.  The invariant that then has to hold in the proofs, is that block 0 should be equivalent to the merged representation of the $\Gamma_{rm a}$ and $\Delta_{rm a}$ maps.
+
 %However, in practice, assigning and reading from an array directly in the state machine will not produce a memory in the final hardware design, as the synthesis tool cannot identify the array as having the necessary properties that a RAM needs, even though this is the most natural formulation of memory.  Even though theoretically the memory will only be read from once per clock cycle, the synthesis tool cannot ensure that this is true, and will instead create a register for each memory location.  This increases the size of the circuit dramatically, as the RAM on the FPGA chip will not be reused.  Instead, the synthesis tool expects a specific interface that ensures these properties, and will then transform the interface into a proper RAM during synthesis.  Therefore, a translation has to be performed from the naive use of memory in the state machine, to a proper use of a memory interface.
 
 %\begin{figure}