diff options
| -rw-r--r-- | algorithm.tex | 14 | ||||
| -rw-r--r-- | evaluation.tex | 10 |
2 files changed, 21 insertions, 3 deletions
diff --git a/algorithm.tex b/algorithm.tex index 4c4c7d4..332ca92 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -1,11 +1,18 @@ \section{Adding an HLS back end to \compcert{}} +\JW{I think `Designing a verified HLS tool' is more appropriate, because one of the things this section aims to establish is whether CompCert is the right way to go.} + %\JW{The first part of this section (up to 2.1) is good but needs tightening up. Ultimately, the point of this section is to explain that there's an existing verified compiler called CompCert which has a bunch of stages, and we need to make a decision about where to tap into that pipeline. Too early and we miss out on some helpful optimisations; too late and we've ended up too target-specific. What if you put a few more stages into Figure 1 -- there aren't actually that many missing anyway. Suppose you add in Cminor between C\#minor and 3AC. Then the high-level structure of your argument in this subsection could be: (1) why Cminor is too early, (2) why LTL is too late, and then maybe (3) why 3AC is just right. The Goldilocks structure, haha!} -This section covers the main architecture of the HLS tool, and the way in which the back end was added to \compcert{}. This section will also cover an example of converting a simple C program into hardware, expressed in the Verilog language. +This section covers the main architecture of the HLS tool, and the way in which the back end was added to \compcert{}. This section will also cover an example of converting a simple C program into hardware, expressed in the Verilog language. \JW{I've experimented with adding a few paragraph headings to the text below -- see what you think. The advantage of headings is that it can make the text easier to read quickly.} + +\paragraph{Choice of source language} +First of all, the choice of C for the input language of \vericert{} is because it is the most widely supported language for HLS, and most major HLS tools also use it as an input. As a lot of existing code is also written in C for HLS, supporting C as an input language compared to a custom domain-specific language means that \vericert{} is more practical. \JW{Can we mention one or two alternatives that we considered?} -First of all, the choice of C for the input language of \vericert{} is because it is the most widely supported language for HLS, and most major HLS tools also use it as an input. As a lot of existing code is also written in C for HLS, supporting C as an input language compared to a custom domain-specific language means that \vericert{} is more practical. Next, Verilog~\cite{06_ieee_stand_veril_hardw_descr_languag} is a hardware description language commonly used to design hardware. A Verilog design can then be synthesised into logic gates which describes how different gates connect to each other, called a netlist. This representation can then be mapped onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASIC) to implement the design that was described in Verilog. Verilog was chosen as the output language for \vericert{} because it is one of the most popular hardware description languages and there already exist a few formal semantics for it that could be used as a target~\cite{loow19_verif_compil_verif_proces,meredith10_veril}. +\paragraph{Choice of target language} +Next, Verilog~\cite{06_ieee_stand_veril_hardw_descr_languag} is a hardware description language commonly used to design hardware. A Verilog design can then be synthesised into logic gates which describes how different gates connect to each other, called a netlist. This representation can then be mapped onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASIC) to implement the design that was described in Verilog. Verilog was chosen as the output language for \vericert{} because it is one of the most popular hardware description languages and there already exist a few formal semantics for it that could be used as a target~\cite{loow19_verif_compil_verif_proces,meredith10_veril}. \JW{Can we mention one or two alternatives that we considered? Bluespec or Chisel or one of Adam Chlipala's languages, perhaps?} +\paragraph{Choice of implementation language} The framework that was chosen for the frontend was \compcert{}, as it is a mature framework for simulation proofs about intermediate languages, in addition to already providing a validated parser~\cite{jourdan12_valid_lr_parser} from C into the internal representation of Clight. Other frameworks were also considered, such as Vellvm~\cite{zhao12_formal_llvm_inter_repres_verif_progr_trans}, as LLVM IR in particular is often used by HLS tools anyways, however, these would require more work to support a higher level language such as C as input, or even providing a parser for LLVM IR.\@ \begin{figure} @@ -40,9 +47,10 @@ The framework that was chosen for the frontend was \compcert{}, as it is a matur \label{fig:rtlbranch} \end{figure} +\paragraph{Architecture of \vericert{}} The main work flow of \vericert{} is shown in Figure~\ref{fig:rtlbranch}, which shows the parts of the translation that are performed in \compcert{}, and which have been added with \vericert{}. -\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 optimisations. When designing a new back end for \compcert{}, it is crucial to know where to branch off, so as to benefit from all the useful optimisations that \compcert{} performs, but not performing optimisations that are not useful, which include optimisations that are specific to the target CPU architecture or. These optimisations include register allocation, as there is not a fixed number of registers that need to be targeted. +\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 optimisations. When designing a new back end for \compcert{}, it is crucial to know where to branch off, so as to benefit from all the useful optimisations that \compcert{} performs, but not performing optimisations that are not useful, which include optimisations that are specific to the target CPU architecture. These optimisations include register allocation, as there is not a fixed number of registers that need to be targeted. To choose where to branch off at, each intermediate language in \compcert{} can be evaluated to see if it is suitable to be transformed into hardware. Existing HLS compilers often use LLVM IR as an intermediate representation when performing HLS-specific optimisations, as each instruction can be mapped quite well to hardware that performs the same behaviour. Looking at the intermediate languages in \compcert{} shown in Figure~\ref{fig:rtlbranch}, there are many languages to choose from. Clight and CminorSel are an abstract syntax tree (AST) representation of the C code, which does not correspond to a more assembly like language similar to LLVM IR.\@ In addition to that, looking at the languages from LTL to PPC, even though these languages do contain basic blocks, which are desirable when doing HLS, starting from LTL the number of registers is limited. Register allocation limits the number of registers when translating 3AC into LTL, and stores variables on the stack if that is required. This is not needed when performing HLS, as there are many more registers available, and it is preferable to use these instead of RAM whenever possible. diff --git a/evaluation.tex b/evaluation.tex index cb185ac..aada207 100644 --- a/evaluation.tex +++ b/evaluation.tex @@ -1,4 +1,14 @@ \section{Evaluation} +\NR{ +To-do list: +\begin{itemize} + \item Modifying the final checks of Polybench programs + \item Re-synthesis the polybench programs + \item Collect new compile times of Vericert + \item Collate the csv file again + % \item Re-run and synthesis adpcm and gsm with new Vericert for Table~\ref{tab:chstone} +\end{itemize} +} Our evaluation is designed to answer the following three research questions. \JW{How about adding one more RQ at the start called `How reliable is the hardware generated by \vericert{}, and how does this compare to existing HLS tools?' Then you can answer this by saying that you couldn't break your tool using the Csmith programs generated by Du et al., which did break all the other HLS tools.} \begin{description} |