Update on Overleaf.

1 files changed, 4 insertions, 0 deletions

diff --git a/verilog.tex b/verilog.tex
index e36abc0..e6a9a2d 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -58,6 +58,7 @@ which modifies one array element using blocking assignment and then a second usi
 \paragraph{Removing support for external inputs to modules} Support for receiving external inputs was removed from the semantics for simplicity, as these are not needed for an HLS target. The main module in Verilog models the main function in C, and since the inputs to a C function shouldn't change during its execution, there is no need for external inputs for Verilog modules.  
 
 \paragraph{Simplifying representation of bitvectors} Finally, we use 32-bit integers to represent bitvectors rather of arrays of Booleans. This is because \vericert{} (currently) only supports types represented by 32 bits.
+
 \subsection{Integrating the Verilog Semantics into \compcert{}'s Model}
 
 \begin{figure*}
@@ -77,6 +78,9 @@ which modifies one array element using blocking assignment and then a second usi
   \label{fig:inferrence_module}
 \end{figure*}
 
+The \compcert{} model defines a set of computational states.
+The \compcert{} computation model requires our Verilog semantics to be enriched. In order to support the three CompCert states, our module definitions require five additional Verilog registers.
+
 \compcert{} defines a specific model of computation that all semantics have to follow in order to prove properties about them. In this section, we first describe three of \compcert{}'s original computational states. Then, we describe the five registers and semantic rules we add to Verilog semantics to integrate it to the \compcert{} model.  \compcert{} has three main states that need to be defined:
 
 \begin{description}