Restructure the file

1 files changed, 52 insertions, 4 deletions

diff --git a/main.tex b/main.tex
index 44b2e4a..43c7852 100644
--- a/main.tex
+++ b/main.tex
@@ -46,14 +46,18 @@
 \usepackage{booktabs}
 \usepackage{mathpartir}
 \usepackage{subcaption}
+\usepackage{tikz}
 
 \newif\ifCOMMENTS
-\COMMENTStrue
+\COMMENTSfalse
 \newcommand{\Comment}[3]{\ifCOMMENTS\textcolor{#1}{{\bf [\![#2:} #3{\bf ]\!]}}\fi}
 \newcommand\JW[1]{\Comment{red!75!black}{JW}{#1}}
 \newcommand\YH[1]{\Comment{green!50!blue}{YH}{#1}}
 \newcommand\JP[1]{\Comment{blue!50!black}{JP}{#1}}
 
+\definecolor{compcert}{HTML}{66c2a5}
+\definecolor{formalhls}{HTML}{fc8d62}
+
 \begin{document}
 
 %% Title information
@@ -210,13 +214,57 @@ CoqUp is open source and is hosted on Github\footnote{https://github.com/ymherkl
 
 %%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}
+    [language/.style={fill=white,rounded corners=2pt}]
+    \fill[compcert,rounded corners=3pt] (-1,-1) rectangle (9,1.5);
+    \fill[formalhls,rounded corners=3pt] (-1,-1.5) rectangle (9,-2.5);
+    \node[language] at (0,0) (clight) {Clight};
+    \node[language] at (2,0) (cminor) {C\#minor};
+    \node[language] at (4,0) (rtl) {RTL};
+    \node[language] at (6,0) (ltl) {LTL};
+    \node[language] at (8,0) (ppc) {PPC};
+    \node[language] at (4,-2) (dfgstmd) {HTL};
+    \node[language] at (7,-2) (verilog) {Verilog};
+    \node at (0,1) {CompCert};
+    \node at (0,-2) {CoqUp};
+    \draw[->] (clight) -- (cminor);
+    \draw[->,dashed] (cminor) -- (rtl);
+    \draw[->] (rtl) -- (ltl);
+    \draw[->,dashed] (ltl) -- (ppc);
+    \draw[->] (rtl) -- (dfgstmd);
+    \draw[->] (dfgstmd) -- (verilog);
+  \end{tikzpicture}
+  \caption{Verilog backend branching off at the RTL stage.}\label{fig:rtlbranch}
+\end{figure}
+
 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.
 
-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.
+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 an infinite number of pseudo-registers and each instruction maps well 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.  The complete flow that CoqUp takes is show in figure~\ref{fig:rtlbranch}.
+
+%%TODO: Maybe add why LTL and the other smaller languages are not that well suited
 
 \subsection{CompCert RTL}
 
-CompCert RTL is the main intermediate representation of CompCert, where most of the optimisations are performed.
+All CompCert intermediate language follow the similar structure below:
+
+\begin{align*}
+  \mathit{program} \quad ::= \{ &\mathbf{variables} : (\mathit{id} * \mathit{data}), \\
+                 &\mathbf{functions} : (\mathit{id} * \mathit{function\_def}),\\
+                 &\mathbf{main} : \mathit{id} \}
+\end{align*}
+
+\noindent where function definitions can either be internal or external.  External functions are functions that are not defined in the current translation unit, and are therefore not part of the current translation.  The difference in between the CompCert intermediate languages is therefore how the internal function is defined, as that defines the structure of the language itself.
+
+%% Describe RTL
+RTL function definitions are a sequence of instructions encoded in a control-flow graph, with each instruction linking to the next instruction that should be executed.
+
+%%TODO: Finish this section and describe the syntax and semantics of RTL.
+
+\subsection{HTL}
+
+RTL is first translated to an intermediate language called hardware transfer language (HTL), which is a finite state machine with datapath (FSMD) representation of the RTL code.  HTL, like all CompCert intermediate languages, has the same program structure as RTL, but internal functions now contain logic to control the order of execution, and a datapath that transforms the data in the registers.  This is represented by having two maps that link states to the control logic and to the current position in the datapath, which are both expressed using Verilog statements.
 
 \subsection{HLS Algorithm}
 
@@ -285,7 +333,7 @@ based on what they evaluate to. For case I think that would end up being a three
 
 \section{Proof}
 
-\section{Coq Mechanisation}
+\subsection{Coq Mechanisation}
 
 \section{Related Work}