Clean up file and add more to introduction

1 files changed, 41 insertions, 54 deletions

diff --git a/main.tex b/main.tex
index bd15da2..6035fc3 100644
--- a/main.tex
+++ b/main.tex
@@ -18,7 +18,7 @@
 \acmNumber{CONF} % CONF = POPL or ICFP or OOPSLA
 \acmArticle{1}
 \acmYear{2018}
-\acmMonth{1}\acmDOI{} % \acmDOI{10.1145/nnnnnnn.nnnnnnn};'--
+\acmMonth{1}\acmDOI{}
 \startPage{1}
 
 %% Copyright information
@@ -29,22 +29,12 @@
 %\setcopyright{acmcopyright}
 %\setcopyright{acmlicensed}
 %\setcopyright{rightsretained}
-%\copyrightyear{2018}           %% If different from \acmYear
+%\copyrightyear{2018}
 
 %% Bibliography style
 \bibliographystyle{ACM-Reference-Format}
 %% Citation style
-%% Note: author/year citations are required for papers published as an
-%% issue of PACMPL.
-\citestyle{acmauthoryear}   %% For author/year citations
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% Note: Authors migrating a paper from PACMPL format to traditional
-%% SIGPLAN proceedings format must update the '\documentclass' and
-%% topmatter commands above; see 'acmart-sigplanproc-template.tex'.
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
+\citestyle{acmauthoryear}
 
 \usepackage{amsmath}
 \usepackage{booktabs}
@@ -85,73 +75,63 @@
 
 %% Author with single affiliation.
 \author{Yann Herklotz}
-%\authornote{with author1 note}          %% \authornote is optional;
-                                        %% can be repeated if necessary
-\orcid{0000-0002-2329-1029}             %% \orcid is optional
+\orcid{0000-0002-2329-1029}
 \affiliation{
 %  \position{PhD Student}
-%  \department{Electrical and Electronic Engineering} %% \department is recommended
-  \institution{Imperial College London} %% \institution is required
+%  \department{EEE}
+  \institution{Imperial College London}
 %  \streetaddress{South Kensington Campus}
 %  \city{London}
-  \state{}
+%  \state{}
 %  \postcode{SW7 2AZ}
-  \country{UK}                    %% \country is recommended
+  \country{UK}
 }
-\email{yann.herklotz15@imperial.ac.uk}          %% \email is recommended
+\email{yann.herklotz15@imperial.ac.uk}
 
 \author{James Pollard}
-%\authornote{with author1 note}          %% \authornote is optional;
-                                        %% can be repeated if necessary
-\orcid{0000-0003-1404-1527}             %% \orcid is optional
+\orcid{0000-0003-1404-1527}
 \affiliation{
 %  \position{PhD Student}
-%  \department{Electrical and Electronic Engineering} %% \department is recommended
-  \institution{Imperial College London} %% \institution is required
+%  \department{EEE}
+  \institution{Imperial College London}
 %  \streetaddress{South Kensington Campus}
 %  \city{London}
-  \state{}
+%  \state{}
 %  \postcode{SW7 2AZ}
-  \country{UK}                    %% \country is recommended
+  \country{UK}
 }
-\email{james.pollard16@imperial.ac.uk}          %% \email is recommended
+\email{james.pollard16@imperial.ac.uk}
 
 \author{Nadesh Ramanathan}
-%\authornote{with author1 note}          %% \authornote is optional;
-                                        %% can be repeated if necessary
-\orcid{0000-0000-0000-0000}             %% \orcid is optional
+\orcid{0000-0000-0000-0000}
 \affiliation{
 %  \position{PhD Student}
-%  \department{Electrical and Electronic Engineering} %% \department is recommended
-  \institution{Imperial College London} %% \institution is required
+%  \department{EEE}
+  \institution{Imperial College London}
 %  \streetaddress{South Kensington Campus}
 %  \city{London}
-  \state{}
+%  \state{}
 %  \postcode{SW7 2AZ}
-  \country{UK}                    %% \country is recommended
+  \country{UK}
 }
-\email{n.ramanathan14@imperial.ac.uk}          %% \email is recommended
+\email{n.ramanathan14@imperial.ac.uk}
 
 \author{John Wickerson}
-%\authornote{with author1 note}          %% \authornote is optional;
-                                        %% can be repeated if necessary
-\orcid{0000-0000-0000-0000}             %% \orcid is optional
+\orcid{0000-0000-0000-0000}
 \affiliation{
 %  \position{PhD Student}
-%  \department{Electrical and Electronic Engineering} %% \department is recommended
-  \institution{Imperial College London} %% \institution is required
+%  \department{EEE}
+  \institution{Imperial College London}
 %  \streetaddress{South Kensington Campus}
 %  \city{London}
-  \state{}
+%  \state{}
 %  \postcode{SW7 2AZ}
-  \country{UK}                    %% \country is recommended
+  \country{UK}
 }
-\email{j.wickerson@imperial.ac.uk}          %% \email is recommended
+\email{j.wickerson@imperial.ac.uk}
 
 
 %% Abstract
-%% Note: \begin{abstract}...\end{abstract} environment must come
-%% before \maketitle command
 \begin{abstract}
   High-level synthesis (HLS) is the process of converting an algorithmic description, often written in C, to specialised hardware with the same behaviour, expressed in a hardware description language.  HLS is becoming increasingly popular, as it allows for faster prototyping of hardware designs, as well as simpler behavioural verification using all the tools available in the software ecosystem.  However, for software verification to be useful, the HLS process has to be trusted to be sure that the properties proven in software also apply to the hardware.  Current HLS tools do not provide this guarantee, meaning verification is often performed again at the hardware level, which is inefficient.  Our work focuses on formally verifying the high-level synthesis process from C to Verilog by proving that the behaviour remains the same according to the C and Verilog semantics.  We use the CompCert frontend to process Clight and add a Verilog backend to get a fully verified HLS tool.
 \end{abstract}
@@ -181,20 +161,27 @@
 
 %% Keywords
 %% comma separated list
-\keywords{CompCert, Coq, high-level synthesis}  %% \keywords are mandatory in final camera-ready submission
+\keywords{CompCert, Coq, high-level synthesis}
 
-
-%% \maketitle
-%% Note: \maketitle command must come after title commands, author
-%% commands, abstract environment, Computing Classification System
-%% environment and commands, and keywords command.
 \maketitle
 
 \section{Introduction}
 
-The current approach to writing energy-efficient and high-throughput applications is to use custom hardware which has been specialised for that application, instead of relying on and optimising for a CPU.\@  This comes at the cost of having to design the customised hardware, which, if using hardware description languages such as Verilog can be tedious and quite error prone.  Especially with the size growing over the years, it can become difficult to verify that the hardware design behaves in the expected way, as simulation of hardware description languages can be quite inefficient.  Furthermore, the algorithms that are being accelerated in hardware often already have a software implemention, meaning they have to be reimplemented efficiently in a hardware description language which can be time consuming.
+%% Motivation for why HLS might be needed
+
+The current approach to writing energy-efficient and high-throughput applications is to use custom hardware which has been specialised for that application, instead of relying on and optimising for a CPU.\@  This comes at the cost of having to design the customised hardware, which, if using hardware description languages (HDL) such as Verilog can be tedious and quite error prone.  Especially with the size growing over the years, it can become difficult to verify that the hardware design behaves in the expected way, as simulation of hardware description languages can be quite inefficient.  Furthermore, the algorithms that are being accelerated in hardware often already have a software implementation, meaning they have to be reimplemented efficiently in a hardware description language which can be time consuming.
+
+%% Definition and benefits of HLS
+
+One possible solution to this is to use high-level synthesis (HLS), which is the process of generating custom hardware, represented in a hardware description language, based on a behavioural description, often a subset of C.  This elevates the level of abstraction, because the description of the algorithm in C is inherently untimed, meaning actions don't have to be scheduled into clock cycles.  The higher level of abstraction makes it easier to reason about the algorithms and therefore also makes them easier to maintain.  This already reduces the time taken to design the hardware, especially if a software description of the algorithm already exists, because it won't have to be designed again at a lower level and directly in hardware.  However, another benefit of using HLS to design the hardware, is that function verification of the design is much simpler and more efficient than if it was done at the HDL stage, as the whole software ecosystem can be used to do that.  Instead of having to run simulations of the hardware, the C code can just be compiled and executed natively, as the hardware design after HLS should have the same behaviour.
+
+%% Unreliability of HLS
+
+However, the fact that the behaviour is preserved after HLS cannot be guaranteed most existing tools.\YH{Mentor's catapult C can in some cases} 
 
+%% Current work in formal verification of HLS
 
+%% Contributions of paper
 
 \section{Background}