diff options
Diffstat (limited to 'chapters/background.tex')
| -rw-r--r-- | chapters/background.tex | 108 |
1 files changed, 70 insertions, 38 deletions
diff --git a/chapters/background.tex b/chapters/background.tex index 6ca5563..7208050 100644 --- a/chapters/background.tex +++ b/chapters/background.tex @@ -5,41 +5,19 @@ \chapter[sec:background]{Background} -%\begin{table} -% \centering -% \begin{tabular}{lccccc}\toprule -% \textbf{Tool} & \textbf{Implementation} & \textbf{Mainstream} & \textbf{Proof} & \textbf{Mechanised} & \textbf{HLS}\\ -% \midrule -% Catapult C~\cite{mentor20_catap_high_level_synth} & \cmark{} & \cmark{} & \cmark{} & \xmark{} & \cmark{}\\ -% Chapman \textit{et al.}~\cite{chapman92_verif_bedroc} & \cmark{} & \xmark{} & \cmark{} & \cmark{} & \cmark{}\\ -% Clarke \textit{et al.}~\cite{clarke03_behav_c_veril} & \cmark{} & \cmark{} & \cmark{} & \xmark{} & \cmark{}\\ -% Ellis~\cite{ellis08_correc} & \xmark{} & \xmark{} & \cmark{} & \cmark{} & \cmark{}\\ -% Karfa \textit{et al.}~\cite{karfa06_formal_verif_method_sched_high_synth} & \cmark{} & \xmark{} & \cmark{} & \xmark{} & \cmark{}\\ -% Kundu \textit{et al.}~\cite{kundu08_valid_high_level_synth} & \cmark{} & \xmark{} & \cmark{} & \xmark{} & \cmark\\ -% LegUp~\cite{canis13_legup} & \cmark{} & \cmark{} & \xmark{} & \xmark{} & \cmark{}\\ -% Lööw \textit{et al.}~\cite{loow19_verif_compil_verif_proces} & \cmark{} & \xmark{} & \cmark{} & \cmark{} & \xmark{}\\ -% OpenCL SDK~\cite{intel20_sdk_openc_applic} & \cmark{} & \xmark{} & \xmark{} & \xmark{} & \cmark{}\\ -% Perna \textit{et al.}~\cite{perna12_mechan_wire_wise_verif_handel_c_synth} & \cmark{} & \xmark{} & \cmark{} & \cmark{} & \xmark{}\\ -% Vivado HLS~\cite{xilinx20_vivad_high_synth} & \cmark{} & \cmark{} & \xmark{} & \xmark{} & \cmark{}\\ -% \bottomrule -% \end{tabular} -% \caption{Table showing the various related works and comparing them.}\label{tab:existing_tools} -%\end{table} - -This section describes the relevant literature around high-level synthesis, verified high-level -synthesis, and finally mechanised proofs of HLS. Table~\ref{tab:existing_tools} classifies -existing tools in the are of formal verification and high-level synthesis. The next section covers -the main different categories that the tools in Table~\ref{tab:existing_tools} show, which include -tools that cover \emph{implementation}, \emph{proof} and finally tools that are \emph{mechanically - verified}. +\startsynopsis + This chapter describes the current state-of-the-art optimisations implemented in high-level + synthesis tools, in particular focusing on static scheduling, loop pipelining and finally also + describing dynamic scheduling which is becoming a popular alternative. +\stopsynopsis \section{Implementation: High-level Synthesis} -High-level synthesis (HLS) is the transformation of software directly into hardware. There are many -different types of HLS, which can vary greatly with what languages they accept, however, they often -share similar steps in how the translation is performed, as they all go from a higher-level, -behavioural description of the algorithm to a timed hardware description. The main steps performed -in the translation are the following~\cite{coussy09_introd_to_high_level_synth,canis13_legup}: +\HLS\ is the transformation of software directly into hardware. There are many different types of +\HLS, which can vary greatly with what languages they accept, however, they often share similar +steps in how the translation is performed, as they all go from a higher-level, behavioural +description of the algorithm to a timed hardware description. The main steps performed in the +translation are the following~\cite{coussy09_introd_to_high_level_synth,canis13_legup}: \desc{Compilation of specification} First, the input specification has to be compiled into a representation that can be used to apply all the necessary optimisations. This can be an @@ -58,7 +36,7 @@ the input specification language is normally an untimed behavioural representati the spatial parallelism of the hardware can be taken advantage of, meaning operations that are not dependent on each other can run in parallel. There are various possible scheduling methods that could be used, such as static or dynamic scheduling, which are described further in -sections~\ref{sec:static_scheduling} and~\ref{sec:dynamic_scheduling}. +\in{Section}[sec:static_scheduling] and in \in{Section}[sec:dynamic_scheduling]. \desc{Operation and variable binding} After the operations have been scheduled, the operations and the variables need to be bound to hardware units and registers respectively. It is often not that @@ -79,6 +57,39 @@ tools take in languages that were designed for hardware such as Handel-C~\cite{aubury96_handel_c_languag_refer_guide}, where time is encoded as part of the semantics. +\subsection[sec:language-blocks]{Intermediate Language} + +This section describes some possible characteristics of a language that could be used as an input to +an \HLS\ tool. These language normally require some structure to allow for easier optimisation and +analysis passes. In particular, it is often useful to have contiguous blocks of instructions that +do not contain any control-flow in one list. This means that these instructions can safely be +rearranged by only looking at local information of the block itself, and in particular it allows for +complete removal of control-flow as only the data-flow is important in that block. + +\subsubsection{Basic blocks} + +%TODO: Finish the basic blocks section + +Basic blocks are the simplest form of structure, as these are only formed of lists of instructions +that do not include control-flow. + +\subsubsection{Superblocks} + +Superblocks extend the notion of basic blocks to contiguous regions without any incoming +control-flow, however, there can be multiple exits out of the block. The main benefit of this +definition is that due to the extra flexibility of allowing multiple exits, the basic blocks can be +extended, which often improves most optimisations that make use of basic blocks. However, the +downside is that the representation of the blocks can be more complex due to the introduction of the +extra control-flow. Any analysis passes will have to take into account the possibility of +control-flow being present and many simplifications will not be possible anymore. + +\subsubsection{Hyperblocks} + +Hyperblocks are also an extension of basic blocks similar to superblocks, but instead of introducing +special control-flow instructions into the block, every instruction is predicated. This leads to +possibly more complex control-flow than in both of the previous cases, however, it can be reasoned +with using a \SAT\ or \SMT\ solver. + \subsection[sec:static_scheduling]{Static Scheduling} Static scheduling is used by the majority of synthesis @@ -102,9 +113,8 @@ met. This is done until all the resources for the current clock cycle are used Static scheduling can normally produce extremely small circuits, however, it is often not possible to guarantee that the circuits will have the best throughput~\cite{cheng20_combin_dynam_static_sched_high_level_synth}, as this requires extensive -control-flow analysis and complex optimisations. Especially for loops, finding the optimal -initiation interval (II) can be tricky if there are loads and stores in the loop or if the loops are -nested. +control-flow analysis and complex optimisations. Especially for loops, finding the optimal \II\ can +be tricky if there are loads and stores in the loop or if the loops are nested. \subsection[sec:dynamic_scheduling]{Dynamic Scheduling} @@ -225,9 +235,31 @@ inlining~\cite{tristan08_formal_verif_trans_valid}. After RTL, each intermediat to get closer to the assembly language of the architecture, performing operations such as register allocation and making sure that the stack variables are correctly aligned. -\subsection{Isabelle HLS} +\subsubsection{CompCertSSA} + +CompCertSSA is an extension of CompCert with an additional \SSA\ intermediate language. This +language enforces \SSA\ properties and therefore allows for many convenient proofs about +optimisations performed on this intermediate language, as many assumptions about variables can be +made when these are encountered. The main interesting porperty that arises from using \SSA\ is the +\emph{equational lemma}, stating that given a variable, if it was assigned by an operation that does +not depend on memory, then loading the destination value of that variable is the same as recomputing +the value of that variable with the current context. + +Given a well formed SSA program $p$, a reachable state $\Sigma\ s\ f\ \sigma\ R\ M$, a memory +independent operation which was defined at a node $d$ as $\mono{Iop}\ \mathit{op}\ \vec{a}\ x\ n$ +assuming that $\sigma$ is dominated by $d$ ($p \le_{d} d$), then the following equation holds: + +\placeformula[eq:equational-lemma]\startformula + \left(\mathit{op}, \vec{a}\right) \Downarrow (R, M) = \left\lfloor R[x] \right\rfloor +\stopformula + +This is an important lemma as it essentially allows one to know the value of a register as long as +one knows that it's assignment dominates the current node and one knows what expressions it was +assigned. + +\subsection{HLS Formalised in Isabelle} -Martin Ellis' work on correct synthesis~\cite{ellis08} is the first example of a mechanically +Martin Ellis' work on correct synthesis~\cite{ellis08_correc} is the first example of a mechanically verified high-level synthesis tool, also called hardware/software compilers, as they produce software as well as hardware for special functional units that should be hardware accelerated. The main goal of the thesis is to provide a framework to prove hardware/software compilers correct, by |