Add HLS Algorithm section

2 files changed, 43 insertions, 36 deletions

diff --git a/main.tex b/main.tex
index 6d3b4e8..44b2e4a 100644
--- a/main.tex
+++ b/main.tex
@@ -196,35 +196,29 @@ CompCert~\cite{leroy06_formal_certif_compil_back_end} is a C compiler that has b
 In this paper we describe a fully verified high-level synthesis tool called CoqUp, which adds a Verilog backend to CompCert and proves that the behaviour of the C code does not change according to existing Verilog semantics.  The main contributions of the paper are the following:
 
 \begin{itemize}
-  \item first mechanised and formally verified HLS flow
+  \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 able to run HLS benchmarks which are now known to be correct.
+  \item Able to run HLS benchmarks which are now known to be correct.
 \end{itemize}
 
 CoqUp is open source and is hosted on Github\footnote{https://github.com/ymherklotz/coqup}.
 
-\section{Background}
+\section{Turning CompCert into an HLS tool}
 
-\subsection{Verilog}
+%% Should maybe go in the introduction instead.
 
-\subsection{CompCert / Coq / Proof by simulation}
+%%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.
 
-\subsection{HLS}
+This section covers the main architecture of the HLS tool, and how the backend was added to CompCert.  CompCert is made up of 11 intermediate languages in between the Clight input and the assembly output.  These intermediate languages each serve a different purpose and contain various different optimisations.  When designing a new backend for CompCert, it is therefore crucial to know where to branch off and start the hardware generation.  Many of the optimisations that the CompCert backend performs are not necessary when generating custom hardware and not relying on a CPU anymore, such as register allocation or even scheduling.  It is therefore important to find the right intermediate language so that the HLS tool still benefits from many of the generic optimisations that CompCert performs, but does not receive the code transformations that are specific to CPU architectures.
 
-\JW{Some papers to cite somewhere:
-\begin{itemize}
-    \item \citet{kundu08_valid_high_level_synth} have done translation validation on an HLS tool called SPARK. They don't have \emph{very} strong evidence that HLS tools are buggy; they just say ``HLS tools are large and complex software systems, often with hundreds of
-thousands of lines of code, and as with any software of this scale, they are prone
-to logical and implementation errors''. They did, however, find two bugs in SPARK as a result of their efforts, so that provides a small bit of evidence that HLS tools are buggy. \@
-    \item \citet{chapman92_verif_bedroc} have proved (manually, as far as JW can tell) that the front-end and scheduler of the BEDROC synthesis system is correct. (NB:\@ Chapman also wrote a PhD thesis about this (1994) but it doesn't appear to be online.)
-    \item \citet{ellis08} wrote a PhD thesis that was supervised by Cliff Jones whom you met at the VeTSS workshop thing last year. At a high level, it's about verifying a high-level synthesis tool using Isabelle, so very relevant to this project, though scanning through the pdf, it's quite hard to ascertain exactly what the contributions are. Strange that they never published a paper about the work -- it makes it very hard to find!
-\end{itemize}
-}
+Existing HLS compilers usually use LLVM IR as an intermediate representation when performing HLS specific optimisations, as each instruction can be mapped quite well to hardware which performs the same behaviour.  CompCert's RTL is the intermediate language that resembles LLVM IR the most, as it also has infinite registers and each instruction can also be translated to hardware.  In addition to that, many optimisations that are also useful for HLS are performed in RTL, which means that if it is supported as the input language, the HLS algorithm benefits from the same optimisations.  It is therefore a good candidate to be chosen as the input language to the HLS backend.
 
-\YH{Amazing, thank you, yes it seems like Kundu \textit{et al.} have quite a few papers on formal verification of HLS algorithms using translation validation, as well as~\citet{karfa06_formal_verif_method_sched_high_synth}, all using the SPARK~\cite{gupta03_spark} synthesis tool.  And yes thank you, will definitely cite that paper.  There seem to be similar early proofs of high-level synthesis like \citet{hwang91_formal_approac_to_sched_probl} or \citet{grass94_high}.  There are also the Occam papers that I need to mention too, like \citet{page91_compil_occam}, \citet{jifeng93_towar}, \citet{perna11_correc_hardw_synth} and \citet{perna12_mechan_wire_wise_verif_handel_c_synth}.} 
-\JW{Well it's a good job there's no page limit on bibliographies these days then! I'll keep an eye out for more papers we could cite when I get a free moment. (No need to cite \emph{everything} of course.)}
-\YH{Yes that's true, there are too many to cite! And great thank you, that would help a lot, I have quite a few papers I still want to cite, but have to think about where they will fit in.}
+\subsection{CompCert RTL}
+
+CompCert RTL is the main intermediate representation of CompCert, where most of the optimisations are performed.
+
+\subsection{HLS Algorithm}
 
 \section{Verilog Semantics}
 
@@ -244,22 +238,6 @@ based on what they evaluate to. For case I think that would end up being a three
 
 \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{align}
-    \text{srun}\ f\ s\ \mathtt{Vskip} &= \mathtt{Some}\ s\\
-    \text{srun}\ f\ s_0\ (\mathtt{Vseq}\ \mathit{st}_1\ \mathit{st}_2) &= \text{srun}\ f\
-    (\text{srun}\ f\ s_0\ \mathit{st}_1)\ \mathit{st}_2\\
-  \text{srun}\ f\ s\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf}) &= \begin{cases}
-    \text{srun}\ f\ s_{0}\ \mathit{stf},& \text{erun}\ f\ \Gamma_{0}\ c = 0\\
-    \text{srun}\ f\ s_{0}\ \mathit{stt},& \text{otherwise}
-  \end{cases}\\
-  \text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ \mathit{def}) &= \begin{cases}
-    \text{srun}\ f\ s_{0}\ sc,& \text{erun}\ f\ \Gamma_{0}\ me = \text{erun}\ f\ \Gamma_{0}\ e\\
-    \text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ cs\ \mathit{def}),& \text{otherwise}
-  \end{cases}\\
-  \text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ []\ (\mathtt{Some}\ st)) &= \text{srun}\ f\ s_{0}\ st\\
-  \text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ []\ \mathtt{None}) &= \mathtt{None}
-\end{align}
-
 \begin{equation}
   \label{eq:1}
   \inferrule[Skip]{ }{\text{srun}\ f\ s\ \mathtt{Vskip} = s}
@@ -307,7 +285,23 @@ based on what they evaluate to. For case I think that would end up being a three
 
 \section{Proof}
 
-\section{Coq mechanisation}
+\section{Coq Mechanisation}
+
+\section{Related Work}
+
+\JW{Some papers to cite somewhere:
+\begin{itemize}
+    \item \citet{kundu08_valid_high_level_synth} have done translation validation on an HLS tool called SPARK. They don't have \emph{very} strong evidence that HLS tools are buggy; they just say ``HLS tools are large and complex software systems, often with hundreds of
+thousands of lines of code, and as with any software of this scale, they are prone
+to logical and implementation errors''. They did, however, find two bugs in SPARK as a result of their efforts, so that provides a small bit of evidence that HLS tools are buggy. \@
+    \item \citet{chapman92_verif_bedroc} have proved (manually, as far as JW can tell) that the front-end and scheduler of the BEDROC synthesis system is correct. (NB:\@ Chapman also wrote a PhD thesis about this (1994) but it doesn't appear to be online.)
+    \item \citet{ellis08} wrote a PhD thesis that was supervised by Cliff Jones whom you met at the VeTSS workshop thing last year. At a high level, it's about verifying a high-level synthesis tool using Isabelle, so very relevant to this project, though scanning through the pdf, it's quite hard to ascertain exactly what the contributions are. Strange that they never published a paper about the work -- it makes it very hard to find!
+\end{itemize}
+}
+
+\YH{Amazing, thank you, yes it seems like Kundu \textit{et al.} have quite a few papers on formal verification of HLS algorithms using translation validation, as well as~\citet{karfa06_formal_verif_method_sched_high_synth}, all using the SPARK~\cite{gupta03_spark} synthesis tool.  And yes thank you, will definitely cite that paper.  There seem to be similar early proofs of high-level synthesis like \citet{hwang91_formal_approac_to_sched_probl} or \citet{grass94_high}.  There are also the Occam papers that I need to mention too, like \citet{page91_compil_occam}, \citet{jifeng93_towar}, \citet{perna11_correc_hardw_synth} and \citet{perna12_mechan_wire_wise_verif_handel_c_synth}.}
+\JW{Well it's a good job there's no page limit on bibliographies these days then! I'll keep an eye out for more papers we could cite when I get a free moment. (No need to cite \emph{everything} of course.)}
+\YH{Yes that's true, there are too many to cite! And great thank you, that would help a lot, I have quite a few papers I still want to cite, but have to think about where they will fit in.}
 
 \section{Conclusion}
 
diff --git a/references.bib b/references.bib
index c72193a..76f7911 100644
--- a/references.bib
+++ b/references.bib
@@ -333,4 +333,17 @@
   school = {Newcastle University},
   url = {https://theses.ncl.ac.uk/jspui/handle/10443/828},
   year = {2008},
-}
\ No newline at end of file
+}
+
+@article{06_ieee_stand_veril_hardw_descr_languag,
+  author          = {},
+  title           = {{IEEE} Standard for Verilog Hardware Description Language},
+  journal         = {{IEEE} Std 1364-2005 (Revision of IEEE Std 1364-2001)},
+  volume          = {},
+  number          = {},
+  pages           = {1-590},
+  year            = {2006},
+  doi             = {10.1109/IEEESTD.2006.99495},
+  ISSN            = {},
+  month           = {April},
+}