From c7dc8c7f5140166b3a3424f3db83fbe5604084cb Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
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 

