Add grammar and main addition

1 files changed, 92 insertions, 66 deletions

diff --git a/main.tex b/main.tex
index 2f44d77..f879f01 100644
--- a/main.tex
+++ b/main.tex
@@ -202,18 +202,107 @@ In this paper we describe a fully verified high-level synthesis tool called CoqU
 \begin{itemize}
   \item First mechanised and formally verified HLS flow.
   \item Proof by simulation mechanised in Coq between CompCert's intermediate language and Verilog.
-  \item Description of the Verilog semantics used to integrate it into CompCert's model.
+  \item Description of the Verilog semantics used to integrate it into CompCert's model with some improvements.
   \item Able to run HLS benchmarks which are now known to be correct.
 \end{itemize}
 
+The first section will describe the Verilog semantics that were used and extended to fit into CompCert's model.  The second section will then describe the HLS algorithm, together with it's proof.
+
 CoqUp is open source and is hosted on Github\footnote{https://github.com/ymherklotz/coqup}.
 
+\section{Verilog}
+
+Verilog is a hardware description language commonly used to design hardware.  A Verilog design can then be synthesised into more basic logic which describes how different gates connect to each other, called a netlist.  This representation can then be put onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASPIC) to implement the design that was described in Verilog.  The Verilog standard is quite large though, and not all Verilog features are needed to be able to describe hardware.  Many Verilog features are only useful for simulation and do not affect the actual hardware itself, which means that these features do not have to be modelled in the semantics.  In addition to that, as the HLS algorithm dictates which Verilog constructs are generated, meaning the Verilog subset that has to be modelled by the semantics can be reduced even further to only support the constructs that are needed.  Only supporting a smaller subset in the semantics also means that there is less chance that the standard is misunderstood, and that the semantics actually model how the Verilog is simulated.
+
+The Verilog semantics are based on the semantics proposed by \citet{loow19_verif_compil_verif_proces}, which were used to create a formal translation from HOL logic into a Verilog circuit.  These semantics are quite practical as they restrict themselves to a small subset of Verilog, which can nonetheless be used to model all hardware constructs one would want to design.  The main syntax for the Verilog subset is the following:
+
+\begin{align*}
+  v ::=&\; \mathit{sz} * n\\
+  e ::=&\; v\\[-2pt]
+  |&\; x\\[-2pt]
+  |&\; e [e]\\[-2pt]
+  |&\; e\ \mathit{op}\ e\\[-2pt]
+  |&\; \texttt{!} e\ |\ \texttt{~} e\\[-2pt]
+  |&\; e \texttt{ ? } e \texttt{ : } e\\
+  s ::=&\; s\ \texttt{;}\ s\ |\ \texttt{;}\\[-2pt]
+  |&\; \texttt{if } e \texttt{ then } s \texttt{ else } s\\[-2pt]
+  |&\; \texttt{case } e\ [e : s] \texttt{ endcase}\\[-2pt]
+  |&\; e \texttt{ = } e\\[-2pt]
+  |&\; e \texttt{ <= } e\\
+  d ::=&\; \texttt{[n-1:0] } r\ |\ \texttt{[n-1:0] } r \texttt{ [m-1:0]}\\
+  m ::=&\ \texttt{reg } d \texttt{;}\ |\ \texttt{input wire } d \texttt{;}\ |\ \texttt{output reg } d \texttt{;}\\
+|&\; \text{\tt always @(posedge clk)}\ s
+\end{align*}
+
+The main addition to the Verilog syntax is the explicit declaration of inputs and outputs, as well as variables and arrays.  This means that the declarations have to be handled explicitly in the semantics as well, adding the safety that all the registers are declared properly with the right size, as this affects how the Verilog module is synthesised and simulated.  In addition to that, literal values cannot be represented by a list of nested boolean values, instead they are represented by a size and it's value.  Finally, the last difference is that the syntax supports memories in Verilog explicitly and we have separate semantics to handle nonblocking and blocking assignments to memory correctly.
+
+\subsection{Semantics}
+
+However, adjustments to these semantics had to be made to make it compatible with the CompCert small step semantics.  In addition to that, memory is not directly modelled in their semantics of Verilog, as well as handling of inputs and declarations in modules.
+
+\begin{equation}
+  \label{eq:10}
+  s = (\Gamma, \Delta)
+\end{equation}
+
+Definition of stmntrun. \JW{stmtntrun has four parameters, and if I read the rules correctly, it looks like the fourth parameter is uniquely determined by the first three. So, you could consider presenting stmntrun simply as a recursive definition, e.g. `stmntrun f s Vskip = s', `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2', and so on. That might (\emph{might}) be easier to read than the inference rule format.}
+
+\YH{It works well for Seq and Skip, but I think that CaseMatch and CaseNoMatch, or even if statements will be a bit clunky? We would have to use case statements in the function to do different things
+based on what they evaluate to. For case I think that would end up being a three way choice. I'll try it out though and see how nice it is.}
+
+\JP{I suppose this would essentially be an ``interpreter'' style semantics but we can prove equivalence pretty easily.}
+
+\YH{To add to that, I used to have both in the Coq code, but commented the recursive definition out, and now only have the inductive definition, which is basically what I copy pasted here.} \JW{Fair enough. Whatever you think ends up being the easiest to read and understand, really. There's something to be said for staying close to the Coq definitions anyway.} \YH{I have added more rules, we can always switch from one to the other now.  One more thing I noticed though is that recursive definitions will need an \texttt{option} type.} \JW{Oh, then my suggestion of `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2' is a bit ill-typed then, unless the second parameter becomes option-typed too. Maybe the inference rules are better overall then.} \YH{Ah yes, I actually didn't even notice that, it would need the do notation, just like the implementation in Coq, so it may be easier to just use the inference rules.}
+
+\begin{equation}
+  \label{eq:1}
+  \inferrule[Skip]{ }{\text{srun}\ f\ s\ \mathtt{Vskip} = s}
+\end{equation}
+
+\begin{equation}
+  \label{eq:4}
+  \inferrule[Seq]{\text{srun}\ f\ s_{0}\ \mathit{st}_{1}\ s_{1} \\ \text{srun}\ f\ s_{1}\ \mathit{st}_{2}\ s_{2}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vseq}\ \mathit{st}_{1}\ \mathit{st}_{2})\ s_{2}}
+\end{equation}
+
+\begin{equation}
+  \label{eq:2}
+  \inferrule[CondTrue]{\text{erun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \text{valToB}\ v_{c} = \mathtt{true} \\ \text{srun}\ f\ s_{0}\ \mathit{stt}\ s_{1}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf})\ s_{1}}
+\end{equation}
+
+\begin{equation}
+  \label{eq:3}
+  \inferrule[CondFalse]{\text{erun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \text{valToB}\ v_{c} = \mathtt{false} \\ \text{srun}\ f\ s_{0}\ \mathit{stf}\ s_{1}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf})\ s_{1}}
+\end{equation}
+
+\begin{equation}
+  \label{eq:5}
+  \inferrule[CaseNoMatch]{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ cs\ \mathit{def})\ s_{1} \\ \text{erun}\ f\ \Gamma_{0}\ me\ mve \\ \text{erun}\ f\ \Gamma_{0}\ e\ ve \\ mve \neq ve}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ \mathit{def})\ s_{1}}
+\end{equation}
+
+\begin{equation}
+  \label{eq:6}
+  \inferrule[CaseMatch]{\text{srun}\ f\ s_{0}\ sc\ s_{1} \\ \text{erun}\ f\ \Gamma_{0}\ e\ ve \\ \text{erun}\ f\ \Gamma_{0}\ me\ mve \\ mve = ve}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ \mathit{def})\ s_{1}}
+\end{equation}
+
+\begin{equation}
+  \label{eq:7}
+  \inferrule[CaseDefault]{\text{srun}\ f\ s_{0}\ st\ s_{1}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ []\ (\mathtt{Some}\ st))\ s_{1}}
+\end{equation}
+
+\begin{equation}
+  \label{eq:8}
+  \inferrule[Blocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{erun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{srun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vblock}\ \mathit{lhs}\ \mathit{rhs})\ (\Gamma ! n \rightarrow v_{\mathit{rhs}}, \Delta)}
+\end{equation}
+
+\begin{equation}
+  \label{eq:9}
+  \inferrule[Nonblocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{erun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{srun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vnonblock}\ \mathit{lhs}\ \mathit{rhs}) (\Gamma, \Delta ! n \rightarrow v_{\mathit{rhs}})}
+\end{equation}
+
 \section{Turning CompCert into an HLS tool}
 
 %% Should maybe go in the introduction instead.
 
-%%Verilog~\cite{06_ieee_stand_veril_hardw_descr_languag} is a hardware description language commonly to design hardware in directly.  The Verilog design can then be synthesised into more basic logic which describes how different gates connect to each other, called a netlist.  This representation can finally be put onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASPIC) to implement the design that was described in Verilog.  However, even though Verilog provides many useful features for designing hardware, it is not well suited for writing reusable designs, as the implementation often depends on what the final target actually is.  In addition to that, to use Verilog one has to be quite familiar with how hardware should be designed, therefore reducing the accessibility to it.  High-level synthesis is one possible solution to this problem, as it raises the level of abstraction, hiding implementation details so that the focus can be put on designing the algorithm and ensuring its correctness.
-
 \begin{figure}
   \centering
   \begin{tikzpicture}
@@ -281,69 +370,6 @@ RTL is first translated to an intermediate language called hardware transfer lan
 
 \subsection{HLS Algorithm}
 
-\section{Verilog Semantics}
-
-Definition of state.
-
-\begin{equation}
-  \label{eq:10}
-  s = (\Gamma, \Delta)
-\end{equation}
-
-Definition of stmntrun. \JW{stmtntrun has four parameters, and if I read the rules correctly, it looks like the fourth parameter is uniquely determined by the first three. So, you could consider presenting stmntrun simply as a recursive definition, e.g. `stmntrun f s Vskip = s', `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2', and so on. That might (\emph{might}) be easier to read than the inference rule format.}
-
-\YH{It works well for Seq and Skip, but I think that CaseMatch and CaseNoMatch, or even if statements will be a bit clunky? We would have to use case statements in the function to do different things
-based on what they evaluate to. For case I think that would end up being a three way choice. I'll try it out though and see how nice it is.}
-
-\JP{I suppose this would essentially be an ``interpreter'' style semantics but we can prove equivalence pretty easily.}
-
-\YH{To add to that, I used to have both in the Coq code, but commented the recursive definition out, and now only have the inductive definition, which is basically what I copy pasted here.} \JW{Fair enough. Whatever you think ends up being the easiest to read and understand, really. There's something to be said for staying close to the Coq definitions anyway.} \YH{I have added more rules, we can always switch from one to the other now.  One more thing I noticed though is that recursive definitions will need an \texttt{option} type.} \JW{Oh, then my suggestion of `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2' is a bit ill-typed then, unless the second parameter becomes option-typed too. Maybe the inference rules are better overall then.} \YH{Ah yes, I actually didn't even notice that, it would need the do notation, just like the implementation in Coq, so it may be easier to just use the inference rules.}
-
-\begin{equation}
-  \label{eq:1}
-  \inferrule[Skip]{ }{\text{srun}\ f\ s\ \mathtt{Vskip} = s}
-\end{equation}
-
-\begin{equation}
-  \label{eq:4}
-  \inferrule[Seq]{\text{srun}\ f\ s_{0}\ \mathit{st}_{1}\ s_{1} \\ \text{srun}\ f\ s_{1}\ \mathit{st}_{2}\ s_{2}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vseq}\ \mathit{st}_{1}\ \mathit{st}_{2})\ s_{2}}
-\end{equation}
-
-\begin{equation}
-  \label{eq:2}
-  \inferrule[CondTrue]{\text{erun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \text{valToB}\ v_{c} = \mathtt{true} \\ \text{srun}\ f\ s_{0}\ \mathit{stt}\ s_{1}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf})\ s_{1}}
-\end{equation}
-
-\begin{equation}
-  \label{eq:3}
-  \inferrule[CondFalse]{\text{erun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \text{valToB}\ v_{c} = \mathtt{false} \\ \text{srun}\ f\ s_{0}\ \mathit{stf}\ s_{1}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf})\ s_{1}}
-\end{equation}
-
-\begin{equation}
-  \label{eq:5}
-  \inferrule[CaseNoMatch]{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ cs\ \mathit{def})\ s_{1} \\ \text{erun}\ f\ \Gamma_{0}\ me\ mve \\ \text{erun}\ f\ \Gamma_{0}\ e\ ve \\ mve \neq ve}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ \mathit{def})\ s_{1}}
-\end{equation}
-
-\begin{equation}
-  \label{eq:6}
-  \inferrule[CaseMatch]{\text{srun}\ f\ s_{0}\ sc\ s_{1} \\ \text{erun}\ f\ \Gamma_{0}\ e\ ve \\ \text{erun}\ f\ \Gamma_{0}\ me\ mve \\ mve = ve}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ \mathit{def})\ s_{1}}
-\end{equation}
-
-\begin{equation}
-  \label{eq:7}
-  \inferrule[CaseDefault]{\text{srun}\ f\ s_{0}\ st\ s_{1}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ []\ (\mathtt{Some}\ st))\ s_{1}}
-\end{equation}
-
-\begin{equation}
-  \label{eq:8}
-  \inferrule[Blocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{erun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{srun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vblock}\ \mathit{lhs}\ \mathit{rhs})\ (\Gamma ! n \rightarrow v_{\mathit{rhs}}, \Delta)}
-\end{equation}
-
-\begin{equation}
-  \label{eq:9}
-  \inferrule[Nonblocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{erun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{srun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vnonblock}\ \mathit{lhs}\ \mathit{rhs}) (\Gamma, \Delta ! n \rightarrow v_{\mathit{rhs}})}
-\end{equation}
-
 \section{Proof}
 
 \subsection{Coq Mechanisation}