Update on Overleaf.

3 files changed, 509 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..c1c8340
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,304 @@
+
+# Created by https://www.toptal.com/developers/gitignore/api/tex
+# Edit at https://www.toptal.com/developers/gitignore?templates=tex
+
+### TeX ###
+## Core latex/pdflatex auxiliary files:
+*.aux
+*.lof
+*.log
+*.lot
+*.fls
+*.out
+*.toc
+*.fmt
+*.fot
+*.cb
+*.cb2
+.*.lb
+
+## Intermediate documents:
+*.dvi
+*.xdv
+*-converted-to.*
+# these rules might exclude image files for figures etc.
+# *.ps
+# *.eps
+# *.pdf
+
+## Bibliography auxiliary files (bibtex/biblatex/biber):
+*.bbl
+*.bcf
+*.blg
+*-blx.aux
+*-blx.bib
+*.run.xml
+
+## Build tool auxiliary files:
+*.fdb_latexmk
+*.synctex
+*.synctex(busy)
+*.synctex.gz
+*.synctex.gz(busy)
+*.pdfsync
+
+## Build tool directories for auxiliary files
+# latexrun
+latex.out/
+
+## Auxiliary and intermediate files from other packages:
+# algorithms
+*.alg
+*.loa
+
+# achemso
+acs-*.bib
+
+# amsthm
+*.thm
+
+# beamer
+*.nav
+*.pre
+*.snm
+*.vrb
+
+# changes
+*.soc
+
+# comment
+*.cut
+
+# cprotect
+*.cpt
+
+# elsarticle (documentclass of Elsevier journals)
+*.spl
+
+# endnotes
+*.ent
+
+# fixme
+*.lox
+
+# feynmf/feynmp
+*.mf
+*.mp
+*.t[1-9]
+*.t[1-9][0-9]
+*.tfm
+
+#(r)(e)ledmac/(r)(e)ledpar
+*.end
+*.?end
+*.[1-9]
+*.[1-9][0-9]
+*.[1-9][0-9][0-9]
+*.[1-9]R
+*.[1-9][0-9]R
+*.[1-9][0-9][0-9]R
+*.eledsec[1-9]
+*.eledsec[1-9]R
+*.eledsec[1-9][0-9]
+*.eledsec[1-9][0-9]R
+*.eledsec[1-9][0-9][0-9]
+*.eledsec[1-9][0-9][0-9]R
+
+# glossaries
+*.acn
+*.acr
+*.glg
+*.glo
+*.gls
+*.glsdefs
+*.lzo
+*.lzs
+
+# uncomment this for glossaries-extra (will ignore makeindex's style files!)
+# *.ist
+
+# gnuplottex
+*-gnuplottex-*
+
+# gregoriotex
+*.gaux
+*.glog
+*.gtex
+
+# htlatex
+*.4ct
+*.4tc
+*.idv
+*.lg
+*.trc
+*.xref
+
+# hyperref
+*.brf
+
+# knitr
+*-concordance.tex
+# TODO Uncomment the next line if you use knitr and want to ignore its generated tikz files
+# *.tikz
+*-tikzDictionary
+
+# listings
+*.lol
+
+# luatexja-ruby
+*.ltjruby
+
+# makeidx
+*.idx
+*.ilg
+*.ind
+
+# minitoc
+*.maf
+*.mlf
+*.mlt
+*.mtc[0-9]*
+*.slf[0-9]*
+*.slt[0-9]*
+*.stc[0-9]*
+
+# minted
+_minted*
+*.pyg
+
+# morewrites
+*.mw
+
+# newpax
+*.newpax
+
+# nomencl
+*.nlg
+*.nlo
+*.nls
+
+# pax
+*.pax
+
+# pdfpcnotes
+*.pdfpc
+
+# sagetex
+*.sagetex.sage
+*.sagetex.py
+*.sagetex.scmd
+
+# scrwfile
+*.wrt
+
+# sympy
+*.sout
+*.sympy
+sympy-plots-for-*.tex/
+
+# pdfcomment
+*.upa
+*.upb
+
+# pythontex
+*.pytxcode
+pythontex-files-*/
+
+# tcolorbox
+*.listing
+
+# thmtools
+*.loe
+
+# TikZ & PGF
+*.dpth
+*.md5
+*.auxlock
+
+# todonotes
+*.tdo
+
+# vhistory
+*.hst
+*.ver
+
+# easy-todo
+*.lod
+
+# xcolor
+*.xcp
+
+# xmpincl
+*.xmpi
+
+# xindy
+*.xdy
+
+# xypic precompiled matrices and outlines
+*.xyc
+*.xyd
+
+# endfloat
+*.ttt
+*.fff
+
+# Latexian
+TSWLatexianTemp*
+
+## Editors:
+# WinEdt
+*.bak
+*.sav
+
+# Texpad
+.texpadtmp
+
+# LyX
+*.lyx~
+
+# Kile
+*.backup
+
+# gummi
+.*.swp
+
+# KBibTeX
+*~[0-9]*
+
+# TeXnicCenter
+*.tps
+
+# auto folder when using emacs and auctex
+./auto/*
+*.el
+
+# expex forward references with \gathertags
+*-tags.tex
+
+# standalone packages
+*.sta
+
+# Makeindex log files
+*.lpz
+
+# xwatermark package
+*.xwm
+
+# REVTeX puts footnotes in the bibliography by default, unless the nofootinbib
+# option is specified. Footnotes are the stored in a file with suffix Notes.bib.
+# Uncomment the next line to have this generated file ignored.
+#*Notes.bib
+
+### TeX Patch ###
+# LIPIcs / OASIcs
+*.vtc
+
+# glossaries
+*.glstex
+
+# End of https://www.toptal.com/developers/gitignore/api/tex
+
+
+# Output
+*.pdf
+
diff --git a/references.bib b/references.bib
new file mode 100644
index 0000000..ed9e2bb
--- /dev/null
+++ b/references.bib
@@ -0,0 +1,151 @@
+@unpublished{Herklotz2020,
+  author          = {Herklotz, Yann and Pollard, James and Ramanathan, Nadesh
+                  and Wickerson, John},
+  title           = {Formal Verification of High-Level Synthesis},
+  year            = 2020,
+  url             = {https://yannherklotz.com/docs/drafts/formal_hls.pdf},
+  urldate         = {2021-1-30},
+  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 de-
+                  signs 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 hard- ware 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 in- put software. Our tool, called
+                  Vericert, extends the Comp- Cert verified C compiler with a
+                  new hardware-oriented in- termediate language and a Verilog
+                  back end, and has been proven correct in Coq. Vericert
+                  supports all C constructs ex- cept for case statements,
+                  function pointers, recursive func- tion calls, integers larger
+                  than 32 bits, floats, and global vari- ables. 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 gener- ated by an existing,
+                  optimising (but unverified) HLS tool.},
+  tags            = {Vericert,HLS,Verified},
+}
+
+@misc{intel_hls,
+  publisher       = {Intel},
+  title           = {Intel High Level Synthesis Compiler},
+  year            = 2021,
+  url             = {https://www.intel.com/content/www/us/en/software/programmable/quartus-prime/hls-compiler.html},
+}
+
+@misc{xilinx_vitis,
+  publisher       = {Xilinx Inc.},
+  title           = {Vitis HLS},
+  year            = 2021,
+  url             = {https://www.xilinx.com/products/design-tools/vivado/integration/esl-design.html},
+}
+
+@inproceedings{Herklotz2021_empiricalstudy,
+  author          = {Herklotz, Yann and Du, Zewei and Ramanathan, Nadesh and
+                  Wickerson, John},
+  booktitle       = {2021 IEEE 29th Annual International Symposium on
+                  Field-Programmable Custom Computing Machines (FCCM)},
+  title           = {An Empirical Study of the Reliability of High-Level
+                  Synthesis Tools},
+  year            = 2021,
+  pages           = {219-223},
+  abstract        = {High-level synthesis (HLS) is becoming an increasingly
+                  important part of the computing landscape, even in
+                  safety-critical domains where correctness is key. As such, HLS
+                  tools are increasingly relied upon. But are they trustworthy?
+                  We have subjected four widely used HLS tools - LegUp, Xilinx
+                  Vivado HLS, the Intel HLS Compiler and Bambu - to a rigorous
+                  fuzzing campaign using thousands of random, valid C programs
+                  that we generated using a modified version of the Csmith tool.
+                  For each C program, we compiled it to a hardware design using
+                  the HLS tool under test and checked whether that hardware
+                  design generates the same output as an executable generated by
+                  the GCC compiler. When discrepancies arose between GCC and the
+                  HLS tool under test, we reduced the C program to a minimal
+                  example in order to zero in on the potential bug. Our testing
+                  campaign has revealed that all four HLS tools can be made to
+                  generate wrong designs from valid C programs and one tool
+                  could be made to crash; this underlines the need for these
+                  increasingly trusted tools to be more rigorously engineered.
+                  Out of 6700 test-cases, we found 1191 programs that caused at
+                  least one tool to fail, out of which we were able to discern
+                  at least 8 unique bugs.},
+  doi             = {10.1109/FCCM51124.2021.00034},
+  ISSN            = {2576-2621},
+  month           = {May},
+}
+
+@inproceedings{Herklotz2021_shouldbeproven,
+  author          = {Herklotz, Yann and Wickerson, John},
+  title           = {High-Level Synthesis Tools should be Proven Correct},
+  year            = 2021,
+  url             = {https://yannherklotz.com/docs/drafts/formal_hls.pdf},
+  urldate         = {2021-1-30},
+}
+
+@article{compcert_Leroy2009,
+  author          = {Leroy, Xavier},
+  title           = {Formal Verification of a Realistic Compiler},
+  year            = 2009,
+  issue_date      = {July 2009},
+  publisher       = {Association for Computing Machinery},
+  address         = {New York, NY, USA},
+  volume          = 52,
+  number          = 7,
+  issn            = {0001-0782},
+  url             = {https://doi.org/10.1145/1538788.1538814},
+  doi             = {10.1145/1538788.1538814},
+  abstract        = {This paper reports on the development and formal
+                  verification (proof of semantic preservation) of CompCert, a
+                  compiler from Clight (a large subset of the C programming
+                  language) to PowerPC assembly code, using the Coq proof
+                  assistant both for programming the compiler and for proving
+                  its correctness. Such a verified compiler is useful in the
+                  context of critical software and its formal verification: the
+                  verification of the compiler guarantees that the safety
+                  properties proved on the source code hold for the executable
+                  compiled code as well.},
+  journal         = {Commun. ACM},
+  month           = {jul},
+  pages           = {107–115},
+  numpages        = 9,
+}
+
+@inproceedings{legup_CanisAndrew2011,
+  author          = {Canis, Andrew and Choi, Jongsok and Aldham, Mark and Zhang,
+                  Victor and Kammoona, Ahmed and Anderson, Jason H. and Brown,
+                  Stephen and Czajkowski, Tomasz},
+  title           = {LegUp: High-Level Synthesis for FPGA-Based
+                  Processor/Accelerator Systems},
+  year            = 2011,
+  isbn            = 9781450305549,
+  publisher       = {Association for Computing Machinery},
+  address         = {New York, NY, USA},
+  url             = {https://doi.org/10.1145/1950413.1950423},
+  doi             = {10.1145/1950413.1950423},
+  abstract        = {In this paper, we introduce a new open source high-level
+                  synthesis tool called LegUp that allows software techniques to
+                  be used for hardware design. LegUp accepts a standard C
+                  program as input and automatically compiles the program to a
+                  hybrid architecture containing an FPGA-based MIPS soft
+                  processor and custom hardware accelerators that communicate
+                  through a standard bus interface. Results show that the tool
+                  produces hardware solutions of comparable quality to a
+                  commercial high-level synthesis tool.},
+  booktitle       = {Proceedings of the 19th ACM/SIGDA International Symposium
+                  on Field Programmable Gate Arrays},
+  pages           = {33–36},
+  numpages        = 4,
+  keywords        = {fpgas, high-level synthesis, hardware/software co-design,
+                  field-programmable gate arrays},
+  location        = {Monterey, CA, USA},
+  series          = {FPGA '11},
+}
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}