diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-09-11 20:02:03 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-09-11 20:02:03 +0100 |
| commit | c7dc8c7f5140166b3a3424f3db83fbe5604084cb (patch) | |
| tree | 1d77040204b5012dc3e7f495fcc80852bf59d2c1 /algorithm.tex | |
| parent | 1698908a04f6886f97ad7566928dfcf9c55acb59 (diff) | |
| download | oopsla21_fvhls-c7dc8c7f5140166b3a3424f3db83fbe5604084cb.tar.gz oopsla21_fvhls-c7dc8c7f5140166b3a3424f3db83fbe5604084cb.zip | |
Add title and email
Diffstat (limited to 'algorithm.tex')
| -rw-r--r-- | algorithm.tex | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/algorithm.tex b/algorithm.tex index 82a70c6..41870a8 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -2,6 +2,8 @@ This section describes the main architecture of the HLS tool, and the way in which the Verilog back end was added to \compcert{}. This section also covers an example of converting a simple C program into hardware, expressed in the Verilog language. +\subsection{Main Design Decisions} + \paragraph{Choice of source language} C was chosen as the source language as it remains the most common source language amongst production-quality HLS tools~\cite{canis11_legup, xilinx20_vivad_high_synth, intel_hls, bambu_hls}. This, in turn, may be because it is ``[t]he starting point for the vast majority of algorithms to be implemented in hardware''~\cite{5522874}, lending a degree of practicality. The availability of \compcert{}~\cite{leroy09_formal_verif_realis_compil} also provides a solid basis for formally verified C compilation. |