Update on Overleaf.

1 files changed, 9 insertions, 6 deletions

diff --git a/verilog.tex b/verilog.tex
index 380bbcb..ed2e7af 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -5,7 +5,7 @@
 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.
 
 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 all hardware constructs one would want to use.  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.
+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 use. \JP{``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.
 
 The semantics of Verilog differs from regular programming languages, as it is used to describe hardware directly, which is inherently parallel, rather than an algorithm, which is usually sequential.  The main construct in Verilog is the \alwaysblock{}.
 A module can contain multiple \alwaysblock{}s, all of which run in parallel.  These \alwaysblock{}s further contain statements such as if-statements or assignments to variables.  We support only \emph{synchronous} logic, which means that the \alwaysblock{} is triggered on (and only on) the rising edge of a clock signal.
@@ -60,6 +60,7 @@ which modifies one array element using blocking assignment and then a second usi
 \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}
+\label{sec:verilog:integrating}
 
 \begin{figure*}
   \centering
@@ -100,11 +101,13 @@ Figure~\ref{fig:inferrence_module} shows the inference rules for moving between
 
 Note that there is no step from \texttt{State} to \texttt{Callstate}; this is because function calls are not supported, and it is therefore impossible in our semantics to ever reach a \texttt{Callstate} except for the initial call to main. So the \textsc{Call} rule is only used at the very beginning of execution; likewise, the \textsc{Return} rule is only matched for the final return value from the main function. %as there is no rule that allocates another stack frame \textit{sf} except for the initial call to main.  
 Therefore, in addition to the rules shown in Figure~\ref{fig:inferrence_module}, an initial state and final state need to be defined:
-\begin{align*}
-  \texttt{initial:}\quad &\forall P,\ \yhconstant{Callstate } []\ P.\texttt{main } []\\
-  \texttt{final:}\quad &\forall n,\ \yhconstant{Returnstate } []\ n \implies n
-\end{align*}
-\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$, and the final state results in the program output of value $n$ when reaching a \texttt{Returnstate} with an empty stack frame.
+
+\begin{gather*}
+  \inferrule[Initial]{\yhfunction{is\_internal}\ (P.\texttt{main})}{\yhfunction{initial\_state}\ (\yhconstant{Callstate } []\ (P.\texttt{main})\ [])}\\
+  \inferrule[Final]{ }{\yhfunction{final\_state}\ (\yhconstant{Returnstate } []\ n)\ n}
+\end{gather*}
+
+\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.
 
 %%% Local Variables:
 %%% mode: latex