summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--algorithm.tex15
-rw-r--r--references.bib8
2 files changed, 17 insertions, 6 deletions
diff --git a/algorithm.tex b/algorithm.tex
index 429f627..0f2f5d5 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -7,11 +7,12 @@ This section covers the main architecture of the HLS tool, and the way in which
First of all, the choice of C for the input language of \vericert{} is simply because it is what most major HLS tools use~\cite{canis11_legup, xilinx20_vivad_high_synth, intel_hls, bambu_hls}. This, in turn, may be because C is ``[t]he starting point for the vast majority of algorithms to be implemented in hardware''~\cite{5522874}.
%Since a lot of existing code for HLS is written in C, supporting C as an input language, rather than a custom domain-specific language, means that \vericert{} is more practical.
%An alternative was to support LLVM IR as an input language, however, to get a full work flow from a higher level language to hardware, a front end for that language to LLVM IR would also have to be verified. \JW{Maybe save LLVM for the `Choice of implementation language'?}
-We considered following~\citet{page91_compil_occam} by using an Occam-like language, as it has built-in parallel constructs that map well to parallel hardware. however, this would not qualify as being high-level synthesis due to the manual parallelism that would have to be performed. \JW{I don't think the presence of parallelism stops it being proper HLS.} \JP{I think I agree with Yann here, but it could be worded better. At any rate not many people have experience writing what is essentially syntactic sugar over a process calculus.}
+\JW{We considered Bluespec~\cite{}, but decided that although it ``can be classed as a high-level language''~\cite{greaves_note}, it is too hardware-oriented to be considered proper HLS.}
+We also considered following the lead of \citet{page91_compil_occam} by using an Occam-like language, as it has built-in parallel constructs that map well to parallel hardware. However, this would not qualify as being high-level synthesis due to the manual parallelism that would have to be performed. \JW{I don't think the presence of parallelism stops it being proper HLS.} \JP{I think I agree with Yann here, but it could be worded better. At any rate not many people have experience writing what is essentially syntactic sugar over a process calculus.}
\paragraph{Choice of target language}
-Verilog~\cite{06_ieee_stand_veril_hardw_descr_languag} is an HDL that can be synthesised into logic gates \JP{Should we say ``logic cells'' instead? FPGAs target LUTs, and ASIC processes target standard cells (which may or may not be logic gates).} \JW{Fine by me.} which can be either placed onto a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASIC). Verilog was chosen as the output language for \vericert{} because it is one of the most popular HDLs 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}. Other possible targets could have been Bluespec, a higher level hardware description language, for which there exists a formally verified translation to circuits using K\^{o}ika~\cite{bourgeat20_essen_blues}, however, targeting this language would not be trivial as it is not meant to be targeted by an automatic tool. Finally, a custom circuit language could also have been targeted, which can then be translated to Verilog in an unverified way, however, some guarantees would be lost and it would not be possible to completely trust the output. \JP{Is this meant to be a dig at Koika :p It feels a bit odd mentioning Koika and then saying this without any comment or evaluation.} \JP{What about that IR from ETH (I think) at PLDI 2020? Obviously didn't exist at the start, but might be worth comment.} %\JW{Can we mention one or two alternatives that we considered? Bluespec or Chisel or one of Adam Chlipala's languages, perhaps?}
+Verilog~\cite{06_ieee_stand_veril_hardw_descr_languag} is an HDL that can be synthesised into logic cells which can be either placed onto a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASIC). Verilog was chosen as the output language for \vericert{} because it is one of the most popular HDLs 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}. Other possible targets could have been Bluespec, a higher level hardware description language, for which there exists a formally verified translation to circuits using K\^{o}ika~\cite{bourgeat20_essen_blues}, however, targeting this language would not be trivial as it is not meant to be targeted by an automatic tool. Finally, a custom circuit language could also have been targeted, which can then be translated to Verilog in an unverified way, however, some guarantees would be lost and it would not be possible to completely trust the output. \JP{Is this meant to be a dig at Koika :p It feels a bit odd mentioning Koika and then saying this without any comment or evaluation.}\YH{Yeah not at all, I guess it could have been another avenue to go down, don't know how to not make it sound like a dig, it's quite likely an author of koika might review this :)} \JP{What about that IR from ETH (I think) at PLDI 2020? Obviously didn't exist at the start, but might be worth comment.}\YH{Yeah, LLHD might be worth mentioning, but I think we can just say lack of formalisation makes it difficult} %\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.\@ \JP{No mention of Coq here.}
@@ -51,11 +52,13 @@ The framework that was chosen for the frontend was \compcert{}, as it is a matur
\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. \JP{Nit: the languages don't contain optimisations, the translation processes do. Maybe we should rephrase this slightly.} 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.
+\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 the translations may contain various optimisations.
+%\JP{Nit: the languages don't contain optimisations, the translation processes do. Maybe we should rephrase this slightly.}
+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.
-\compcert{}'s three-address code (3AC)\footnote{Three-address code (3AC) is also known as register transfer language (RTL) in the \compcert{} literature, however, 3AC is used in this paper instead so as not to confuse it with register-transfer level (RTL), which is another name for the final hardware target of the HLS tool.} 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 \JP{This needs qualification since the instructions are the target instructions of the architecture (i.e.\ they aren't a fixed set).}. 3AC is represented as a control flow graph (CFG) in CompCert. Each instruction is a node in the graph and links to the instructions that follow it. This CFG then describes how the computation should proceed, and is a good representation for performing optimisations on as well as local transformations. However, one difference between LLVM IR and 3AC is that 3AC uses operations of the target architecture and performs architecture specific optimisations as well, which is not the case in LLVM IR where all the instructions are quite abstract. This can be mitigated by making \compcert{} target a specific architecture such as x86\_32, where most operations translate quite well into hardware. In addition to that, many optimisations that are also useful for HLS are performed in 3AC, 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 back end. The complete flow that \vericert{} takes is show in figure~\ref{fig:rtlbranch}.
+\compcert{}'s three-address code (3AC)\footnote{Three-address code (3AC) is also known as register transfer language (RTL) in the \compcert{} literature, however, 3AC is used in this paper instead so as not to confuse it with register-transfer level (RTL), which is another name for the final hardware target of the HLS tool.} 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, even though in the case of 3AC uses the instructions of the target architecture whereas LLVM IR instructions are more abstract. 3AC is represented as a control flow graph (CFG) in CompCert. Each instruction is a node in the graph and links to the instructions that follow it. This CFG then describes how the computation should proceed, and is a good representation for performing optimisations on as well as local transformations. However, one difference between LLVM IR and 3AC is that 3AC uses operations of the target architecture and performs architecture specific optimisations as well, which is not the case in LLVM IR where all the instructions are quite abstract. This can be mitigated by making \compcert{} target a specific architecture such as x86\_32, where most operations translate quite well into hardware. In addition to that, many optimisations that are also useful for HLS are performed in 3AC, 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 back end. The complete flow that \vericert{} takes is show in figure~\ref{fig:rtlbranch}.
\begin{figure}
\centering
@@ -220,11 +223,11 @@ However, the memory model that \compcert{} uses for its intermediate languages~\
% Mention that this optimisation is not performed sometimes (clang -03).
-\vericert{} performs some optimisations at the level of the instructions that are generated, so that the hardware performs the instructions as quickly as possible and so that the maximum frequency at which the hardware can run is increased. One of the main constructs that cripple performance of the generated hardware is the instantiation of divider circuits in the hardware. In the case of \vericert{}, it requires the result of the divide operation to be ready in the same clock cycle, meaning the divide circuit needs to be implemented fully combinationally. This is inefficient in terms of hardware size, but also in terms of latency, because it means that the maximum frequency of the hardware needs to be reduced dramatically so that the divide circuit has enough time to finish. \JP{Multi-cycle paths might be something worth exploring in future work: fairly error-prone/dangerous for hand-written code, but might be interesting in generated code.}
+\vericert{} performs some optimisations at the level of the instructions that are generated, so that the hardware performs the instructions as quickly as possible and so that the maximum frequency at which the hardware can run is increased. One of the main constructs that cripple performance of the generated hardware is the instantiation of divider circuits in the hardware. In the case of \vericert{}, it requires the result of the divide operation to be ready in the same clock cycle, meaning the divide circuit needs to be implemented fully combinationally. This is inefficient in terms of hardware size, but also in terms of latency, because it means that the maximum frequency of the hardware needs to be reduced dramatically so that the divide circuit has enough time to finish. \JP{Multi-cycle paths might be something worth exploring in future work: fairly error-prone/dangerous for hand-written code, but might be interesting in generated code.}\YH{Definitely is on the list for next things to look into, will make divide so much more efficient.}
These small optimisations were found to be the most error prone, and guaranteeing that the new representation is equivalent to representation used in the \compcert{} semantics is difficult without proving this for all possible inputs.
-Dividing by a constant can often be optimised to a more efficient operation, especially if the denominator is a factor of two. \JP{People will laugh at us if we don't use the term ``strength-reduction'' somewhere here} In \compcert{}, the \texttt{Oshrximm} instruction does exactly this, and a normal signed divide operation can be replaced by the \texttt{Oshrximm} instruction, performing the following operation, which is transformed to our optimal representation on the right, where $\div$ stands for integer signed division:
+Dividing by a constant can often be optimised to a more efficient operation, especially if the denominator is a factor of two. In \compcert{}, the \texttt{Oshrximm} is a strength-reduced version of a signed divide operation, performing the following operation, which is transformed to our optimal representation on the right, where $\div$ stands for integer signed division and $>>$ stands for a logical right shift:
\begin{align*}
&\forall x, y \in \mathbb{Z},\ \ 0 \leq y < 31,\ \ -2^{31} \leq x < 2^{31},\\
diff --git a/references.bib b/references.bib
index 2212317..3c54005 100644
--- a/references.bib
+++ b/references.bib
@@ -48,6 +48,14 @@ year = {2020},
number={},
pages={857-858},
doi={10.1145/1837274.1837489}}
+
+@article{greaves_note,
+ author = {David J. Greaves},
+ title = {Research Note: An Open Source Bluespec Compiler},
+ journal = {CoRR},
+ volume = {abs/1905.03746},
+ year = {2019}
+}
@article{takach16_high_level_synth,
author = {A. {Takach}},