Update on Overleaf.

1 files changed, 19 insertions, 7 deletions

diff --git a/main.tex b/main.tex
index f5768b3..cbb6516 100644
--- a/main.tex
+++ b/main.tex
@@ -45,7 +45,7 @@
 \usepackage{tikz}
 \usepackage{minted}
 \usepackage{microtype}
-\usepackage{csquotes}
+\usepackage{epigraph}
 
 \usetikzlibrary{shapes,calc,arrows.meta}
 \pgfplotsset{compat=1.16}
@@ -57,7 +57,7 @@
 \ANONYMOUSfalse
 
 \newif\ifCOMMENTS
-\COMMENTSfalse
+\COMMENTStrue
 \newcommand{\Comment}[3]{\ifCOMMENTS\textcolor{#1}{{\bf [\![#2:} #3{\bf ]\!]}}\fi}
 \newcommand\JW[1]{\Comment{red!75!black}{JW}{#1}}
 \newcommand\YH[1]{\Comment{green!50!blue}{YH}{#1}}
@@ -97,7 +97,7 @@
 \begin{document}
 
 %% Title information
-\title[All HLS Tools Should be Proven Correct]{All High-Level Synthesis Tools Should be Proven Correct}
+\title[HLS Tools Should be Proven Correct]{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;
@@ -138,6 +138,14 @@
 
 \begin{abstract}
   High-level synthesis is increasingly being relied upon
+  \JW{A possible story: \begin{itemize}
+  \item High-level synthesis is increasingly being relied upon.
+  \item But it's really flaky. (Cite bugs from FCCM submission etc.)
+  \item There exist some workarounds. (Testing the output, formally verifying the output, etc.)
+  \item The time has come to prove the tool itself correct. (Mention success of Compcert and other fully verified tools?)
+  \item We've made some encouraging progress on this front in a prototype tool called Vericert. (Summarise current state of Vericert, and how it compares performance-wise to LegUp.) 
+  \item But there's still a long way to go. (List the main things left to do, and how you expect Vericert to compare to LegUp after those things are done.)
+  \end{itemize}}
 \end{abstract}
 
 %% 2012 ACM Computing Classification System (CSS) concepts
@@ -170,11 +178,15 @@
 
 \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}
+%\JW{I removed the `All' from the title, as I think that's a bit strong; it also means that the title fit on one line now :).}
 
-Research in high-level synthesis (HLS) often concentrates on performance, trying to achieve the lowest area with the shortest run-time.  What is often overlooked is ensuring that the high-level synthesis tool is indeed correct, and that it outputs a correct hardware design.  Instead, the design is often meticulously tested, often using the higher level design as a model.  As these tests are performed on the hardware design directly, they have to be run on a simulator, which takes much longer than if the original C was tested.  Any formal properties obtained from the C code would also have to be checked again in the resulting design, to ensure that these hold there as well, as the synthesis tool may have translated the input incorrectly.
+\renewcommand{\epigraphsize}{\normalsize}
+\renewcommand{\epigraphflush}{center}
+\renewcommand{\epigraphrule}{0pt}
+\epigraph{\textit{High-level synthesis research and development is inherently prone to introducing bugs or regressions in the final circuit functionality.}}{--- Andrew Canis~\cite{canis15_legup}}
+
+%\JW{Nice quote; I'd be tempted to tinker with whether it can be formatted a bit more elegantly, like at https://style.mla.org/styling-epigraphs/} 
+Research in high-level synthesis (HLS) often concentrates on performance, trying to achieve the lowest area with the shortest run-time.  What is often overlooked is ensuring that the high-level synthesis tool is indeed correct, and \JW{why `and'? Perhaps `which means'?} that it outputs a correct hardware design.  Instead, the design is often meticulously tested, often using the higher level design as a model.  As these tests are performed on the hardware design directly, they have to be run on a simulator, which takes much longer than if the original C was tested.  Any formal properties obtained from the C code would also have to be checked again in the resulting design, to ensure that these hold there as well, as the synthesis tool may have translated the input incorrectly.
 
 It is often assumed that because current HLS tools should transform the input specification into a semantically equivalent design, such as mentioned in \citet{lahti19_are_we_there_yet}.  However, this is not the case, and as with all complex pieces of software there are bugs in HLS tools as well.  For example, Vivado HLS was found to incorrectly apply pipelining optimisations\footnote{\url{https://bit.ly/vivado-hls-pipeline-bug}} or generate wrong designs with valid C code as input, but which the HLS tool interprets differently compared to a C compiler, leading to undefined behaviour.  These types of bugs are difficult to identify, and exist because firstly it is not quite clear what input these tools support, and secondly if the output design actually behaves the same as the input.