diff options
| -rw-r--r-- | algorithm.tex | 2 | ||||
| -rw-r--r-- | main.tex | 2 |
2 files changed, 3 insertions, 1 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. @@ -144,7 +144,7 @@ \institution{Imperial College London} \country{UK} } -%\email{james.pollard16@imperial.ac.uk} +\email{jamespollard@acm.org} \author{Nadesh Ramanathan} \orcid{0000-0001-9083-8349} |