Add main.tex

3 files changed, 53 insertions, 5 deletions

diff --git a/draft.org b/draft.org
new file mode 100644
index 0000000..455142f
--- /dev/null
+++ b/draft.org
@@ -0,0 +1,17 @@
+#+title: Paper Outline and Draft
+#+author: Yann Herklotz
+
+- Performance vs correctness.
+
+* Introduction
+
+- Importance of correctness, especially in HLS.
+- [cite:lahti19_are_we_there_yet]: Talks about being able to trust synthesis tools.
+- Current focus of HLS is mainly on optimisations
+- Correctness guarantees help with duplicate verificaton
+
+* How can we prove an HLS tool correct?
+
+* Guarantees and trusted code
+
+* Performance of such a tool
diff --git a/main.tex b/main.tex
index 640540f..9ee0bd9 100644
--- a/main.tex
+++ b/main.tex
@@ -45,6 +45,7 @@
 \usepackage{tikz}
 \usepackage{minted}
 \usepackage{microtype}
+\usepackage{csquotes}
 
 \usetikzlibrary{shapes,calc,arrows.meta}
 \pgfplotsset{compat=1.16}
@@ -96,7 +97,7 @@
 \begin{document}
 
 %% Title information
-\title[Formal Verification of HLS]{Formal Verification of High-Level Synthesis}
+\title[All HLS Tools Should be Proven Correct]{All High-Level Synthesis Tools Should be Proven Correct}
                                         %% when present, will be used in
                                         %% header instead of Full Title.
 %\titlenote{with title note}             %% \titlenote is optional;
@@ -136,9 +137,7 @@
 \email{j.wickerson@imperial.ac.uk}
 
 \begin{abstract}
-  High-level synthesis (HLS), which refers to the automatic compilation of software into hardware, is rapidly gaining popularity.  In a world increasingly reliant on application-specific hardware accelerators, HLS promises hardware designs of comparable performance and energy efficiency to those coded by hand in a hardware description language like Verilog, while maintaining the convenience and the rich ecosystem of software development.  However, current HLS tools cannot always guarantee that the hardware designs they produce are equivalent to the software they were given, thus undermining any reasoning conducted at the software level.  Worse, there is mounting evidence that existing HLS tools are quite unreliable, sometimes generating wrong hardware or crashing when given valid inputs.
-
-  To address this problem, we present the first HLS tool that is mechanically verified to preserve the behaviour of its input software.  Our tool, called \vericert{}, extends the \compcert{} verified C compiler with a new hardware-oriented intermediate language and a Verilog back end, and has been proven correct in Coq.  \vericert{} supports all C constructs except for case statements, function pointers, recursive function calls, integers larger than 32 bits, floats, and global variables.  An evaluation on the PolyBench/C benchmark suite indicates that \vericert{} generates hardware that is around an order of magnitude slower and larger than hardware generated by an existing, optimising (but unverified) HLS tool.
+  High-level synthesis is increasingly being relied upon
 \end{abstract}
 
 %% 2012 ACM Computing Classification System (CSS) concepts
@@ -169,7 +168,19 @@
 
 \maketitle
 
-Random text
+\section{Introduction}
+
+\begin{displayquote}[\citet{canis15_legup}]
+  High-level synthesis research and development is inherently prone to introducing bugs or regressions in the final circuit functionality.
+\end{displayquote}
+
+Research in high-level synthesis (HLS) often concentrates on performance, trying to achieve the lowest area with the shortest run-time.
+
+\section{How to prove an HLS tool correct}
+
+\section{Guarantees of trusted code}
+
+\section{Performance of such a tool}
 
 %% Acknowledgments
 %\begin{acks}                            %% acks environment is optional
diff --git a/references.bib b/references.bib
new file mode 100644
index 0000000..0d4c2f4
--- /dev/null
+++ b/references.bib
@@ -0,0 +1,20 @@
+@article{lahti19_are_we_there_yet,
+	author = {S. {Lahti} and P. {Sj{\"o}vall} and J. {Vanne} and T. D. {H{\"a}m{\"a}l{\"a}inen}},
+	title = {Are We There Yet? a Study on the State of High-Level Synthesis},
+	journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
+	volume = {38},
+	number = {5},
+	pages = {898-911},
+	year = {2019},
+	doi = {10.1109/TCAD.2018.2834439},
+	url = {https://doi.org/10.1109/TCAD.2018.2834439},
+	ISSN = {1937-4151},
+	month = {May}
+}
+
+@phdthesis{canis15_legup,
+	keywords = {high-level synthesis, hardware/software co-simulation, FPGA},
+	title = {Legup: open-source high-level synthesis research framework},
+	author = {Canis, Andrew Christopher},
+	year = {2015}
+}