From c7dc8c7f5140166b3a3424f3db83fbe5604084cb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 11 Sep 2021 20:02:03 +0100 Subject: Add title and email --- algorithm.tex | 2 ++ 1 file changed, 2 insertions(+) (limited to 'algorithm.tex') 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. -- cgit