Update on Overleaf.

1 files changed, 54 insertions, 0 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
new file mode 100644
index 0000000..2395afb
--- /dev/null
+++ b/verified_resource_sharing.tex
@@ -0,0 +1,54 @@
+\documentclass[hyphens,prologue,x11names,rgb,sigconf]{acmart}
+
+\usepackage[textsize=small,shadow]{todonotes}%
+
+% Leave review comments using
+% \jwcomment{...} (for John) or \yhcomment{...} (for Yann)
+% Using either directly leaves a margin note, using it as,
+% e.g. \jwcomment[inline]{...} leaves an inline comment
+\newcommand{\jwcomment}[2][]{\todo[author={John}, color=ACMLightBlue, #1]{#2}}
+\newcommand{\yhcomment}[2][]{\todo[author={Yann}, color=ACMGreen, #1]{#2}}
+
+\newcommand{\citeintext}[1] {\citeauthor{#1} in \citeyear{#1}~\cite{#1}}
+\newcommand{\citeshort}[1] {\citeauthor{#1} \citeyear{#1}~\cite{#1}}
+
+\begin{document}
+
+\title{Resource Sharing for Verified High-Level Synthesis}
+
+\author{Michail Pardalos}
+\email{michail.pardalos17@imperial.ac.uk}
+\affiliation{\institution{Imperial College London}}
+
+\author{Yann Herklotz}
+\email{yann.herklotz15@imperial.ac.uk}
+\affiliation{\institution{Imperial College London}}
+
+\author{John Wickerson}
+\email{j.wickerson@imperial.ac.uk}
+\affiliation{\institution{Imperial College London}}
+
+\begin{abstract}
+  High-level synthesis is playing an ever-increasing role in hardware design, but concerns have been raised about its reliability. Seeking to address these concerns, Herklotz et al. have recently developed a high-level synthesis compiler, called Vericert, that has been mechanically proven correct \jwcomment{in the sense that every Verilog design produced by Vericert is guaranteed to be behaviourally equivalent to its input C program}. Unfortunately, Vericert's output cannot compete performance-wise with established HLS tools such as LegUp or Bambu \jwcomment{this list should include the HLS tools we actually compare against, once we've settled on which tools those will be}. One reason for this is Vericert's complete lack of support for resource sharing. In this paper, we present an extension to Vericert to implement function-level resource sharing. We extend the formal proof of correctness of the compiler to fully cover our changes. This involves extending the semantics of HTL, an internal, Verilog-like language of Vericert. Our benchmarking using the PolyBench/C benchmark suite shows the generated hardware having a resource usage of 61\% of the original on average and 46\% in the best case, for only a 3\% average decrease in max frequency and 1\% average increase in cycle count. \jwcomment{I'd be tempted to put the experimental results last, after the discussion of your implementation and proof.}
+\end{abstract}
+
+\maketitle
+
+\section{Introduction}
+\label{sec:introduction}
+
+The need for faster, more energy-efficient computation has, in recent years, caused a surge in the need for custom hardware accelerators. Such devices are commonly designed using a hardware description language such as Verilog or VHDL.\@ The complexities of designing hardware in such a language, as well as the abundance of engineers trained in software rather than hardware development has meant that high-level synthesis tools have become an enticing option. These tools, while incredibly useful, are also known to be unreliable.
+
+Previous work by \citeintext{Herklotz2021_shouldbeproven} has found extensive \emph{miscompilation} bugs in commercial HLS tools including Vivado HLS (now Vitis HLS)~\cite{xilinx_vitis}, Intel i++~\cite{intel_hls} and LegUp~\cite{legup_CanisAndrew2011}\todo{Maybe more evidence of instability}. This instability can be a significant hindrance in the development process. This is compounded by the longer iteration times of hardware design compared to software, making the setback when a bug is encountered much more significant. It is therefore essential to ensure that all software used in this process, including the high-level synthesis tool, is as reliable as possible.
+
+Vericert~\cite{Herklotz2020} is a High-Level Synthesis compiler which aims to address this issue. It has been verified correct by the highest possible standard: machine-checked formal proof. It achieves that by providing a proof, checked using the Coq proof assistant, that every step of its translation from C to Verilog preserves the semantics of (i.e.\ behaves the same way as) its input program. This proof means that we can always trust any Verilog produced by Vericert to behave the same way as the C program given to it as input. It is based on the CompCert~\cite{compcert_Leroy2009} verified C compiler.
+
+Clearly, however, it is not enough for a high-level synthesis tool to simply be \emph{correct}. The generated hardware needs to also satisfy a number of other qualities, including high throughput, low latency, and \emph{area efficiency}. A common optimisation in HLS tools for improving area usage is \emph{resource sharing}. That is, avoiding generating the same hardware more than once, and, instead, re-using that hardware for more than one purpose.\todo{This is not the clearest explanation. It might be OK to completely remove it and explain resource sharing in the background}
+
+Our work implements a resource sharing optimisation in Vericert. Keeping with the aims of the project, we also extend the correctness proof
+
+
+\bibliographystyle{ACM-Reference-Format}
+\bibliography{references}
+
+\end{document}