\documentclass[acmsmall,screen]{acmart}

\settopmatter{}
%\documentclass[pagebackref=true,acmsmall,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
%% For double-blind review submission, w/ CCS and ACM Reference
%\documentclass[acmsmall,review,anonymous]{acmart}\settopmatter{printfolios=true}
%% For single-blind review submission, w/o CCS and ACM Reference (max submission space)
%\documentclass[acmsmall,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
%% For single-blind review submission, w/ CCS and ACM Reference
%\documentclass[acmsmall,review]{acmart}\settopmatter{printfolios=true}
%% For final camera-ready submission, w/ required CCS and ACM Reference
%\documentclass[acmsmall]{acmart}\settopmatter{}

%% Journal information
%% Supplied to authors by publisher for camera-ready submission;
%% use defaults for review submission.
%%\acmJournal{PACMPL}
%%\acmVolume{1}
%%\acmNumber{CONF} % CONF = POPL or ICFP or OOPSLA
%%\acmArticle{1}
%%\acmYear{2018}
%%\acmMonth{1}\acmDOI{}
%%\startPage{1}

%% Copyright information
%% Supplied to authors (based on authors' rights management selection;
%% see authors.acm.org) by publisher for camera-ready submission;
%% use 'none' for review submission.
%\setcopyright{acmcopyright}
%\setcopyright{acmlicensed}
%\setcopyright{rightsretained}
%\copyrightyear{2018}

%% Bibliography style
\bibliographystyle{ACM-Reference-Format}
%% Citation style
\citestyle{acmauthoryear}


%%% If you see 'ACMUNKNOWN' in the 'setcopyright' statement below,
%%% please first submit your publishing-rights agreement with ACM (follow link on submission page).
%%% Then please update our instructions page and copy-and-paste the NEW commands into your article.
%%% Please contact us in case of questions; allow up to 10 min for the system to propagate the information.
%%%
%%% The following is specific to OOPSLA '21 and the paper
%%% 'Formal Verification of High-Level Synthesis'
%%% by Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson.
%%%
\setcopyright{none}
\acmPrice{}
\acmDOI{10.1145/3485494}
\acmYear{2021}
\copyrightyear{2021}
\acmSubmissionID{oopsla21main-p86-p}
\acmJournal{PACMPL}
\acmVolume{5}
\acmNumber{OOPSLA}
\acmArticle{117}
\acmMonth{10}

\usepackage{amsmath}
\usepackage{booktabs}
\usepackage{mathpartir}
\usepackage{pgfplots}
\usepackage{pgfplotstable}
\usepackage{soul}
\usepackage{subcaption}
\usepackage{tikz}
\usepackage{minted}
\usepackage{microtype}
\usepackage{tikz-timing}
\usepackage[normalem]{ulem}

\usetikzlibrary{shapes,calc,arrows.meta}
\usetikzlibrary{pgfplots.groupplots}
\pgfplotsset{compat=1.16}

\setminted{fontsize=\small}
\usemintedstyle{manni}

\newif\ifANONYMOUS
\ANONYMOUSfalse

\newif\ifCOMMENTS
\COMMENTSfalse
\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}}
\newcommand\JP[1]{\Comment{blue!50!black}{JP}{#1}}
\newcommand\NR[1]{\Comment{blue}{NR}{#1}}

\newcommand\JWcouldcut[1]{{\st{#1}}}
\newcommand\NRcouldcut[1]{{\st{#1}}}
\newcommand\NRreplace[2]{{\st{#1} \NR{#2}}}
\newcommand\JWreplace[2]{{\st{#1} \JW{#2}}}

\definecolor{compcert}{HTML}{66c2a5}
\definecolor{formalhls}{HTML}{fc8d62}
\definecolor{keywordcolour}{HTML}{8f0075}
\definecolor{functioncolour}{HTML}{721045}
\definecolor{constantcolour}{HTML}{0000bb}

\newcommand\yhkeywordsp[1]{\;\;\texttt{\textcolor{keywordcolour}{#1}}}
\newcommand\yhkeyword[1]{\texttt{\textcolor{keywordcolour}{#1}}}
\newcommand\yhfunctionsp[1]{\;\;\texttt{\textcolor{functioncolour}{#1}}}
\newcommand\yhfunction[1]{\texttt{\textcolor{functioncolour}{#1}}}
\newcommand\yhconstant[1]{\texttt{\textcolor{constantcolour}{#1}}}

\ifANONYMOUS
\newcommand{\vericert}{HLS\-Cert}
\else
\newcommand{\vericert}{Veri\-cert}
\fi
\newcommand{\compcert}{Comp\-Cert}
\newcommand{\legup}{Leg\-Up}

\newcommand{\slowdownOrig}{27}
\newcommand{\slowdownDiv}{2}
\newcommand{\areaIncr}{1.1}
\def\polybench{PolyBench/C}


\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem*{remark}{Remark}

\begin{document}

\title{Formal Verification of High-Level Synthesis}

%% Author with single affiliation.
\author{Yann Herklotz}
\orcid{0000-0002-2329-1029}
\affiliation{
  \institution{Imperial College London}
  \country{UK}
}
\email{yann.herklotz15@imperial.ac.uk}

\author{James D. Pollard}
\orcid{0000-0003-1404-1527}
\affiliation{
  \institution{Imperial College London}
  \country{UK}
}
\email{james.pollard16@imperial.ac.uk}

\author{Nadesh Ramanathan}
\orcid{0000-0001-9083-8349}
\affiliation{
  \institution{Imperial College London}
  \country{UK}
}
\email{n.ramanathan14@imperial.ac.uk}

\author{John Wickerson}
\orcid{0000-0001-6735-5533}
\affiliation{
  \institution{Imperial College London}
  \country{UK}
}
\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 such as 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.  Furthermore, 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 most C constructs, including all integer operations, function calls, local arrays, structs, unions, and general control-flow statements.  An evaluation on the \polybench{} benchmark suite indicates that \vericert{} generates hardware that is around an order of magnitude slower (only around 2$\times$ slower in the absence of division) and about the same size as hardware generated by an existing, optimising (but unverified) HLS tool.
\end{abstract}

\begin{CCSXML}
<ccs2012>
   <concept>
       <concept_id>10010583.10010682.10010684</concept_id>
       <concept_desc>Hardware~High-level and register-transfer level synthesis</concept_desc>
       <concept_significance>500</concept_significance>
       </concept>
   <concept>
       <concept_id>10010583.10010717.10010721</concept_id>
       <concept_desc>Hardware~Functional verification</concept_desc>
       <concept_significance>300</concept_significance>
       </concept>
   <concept>
       <concept_id>10002978.10002986.10002990</concept_id>
       <concept_desc>Security and privacy~Logic and verification</concept_desc>
       <concept_significance>500</concept_significance>
       </concept>
 </ccs2012>
\end{CCSXML}

\ccsdesc[500]{Hardware~High-level and register-transfer level synthesis}
\ccsdesc[300]{Hardware~Functional verification}
\ccsdesc[500]{Security and privacy~Logic and verification}


%% Keywords
%% comma separated list
\keywords{\compcert{}, Coq, high-level synthesis, C, Verilog}

\maketitle

\input{introduction}
\input{algorithm}
\input{verilog}
\input{proof}
\input{evaluation}
\input{related}
\input{limitations}
\input{conclusion}

\subsection*{Acknowledgements}
We'd like to thank Sandrine Blazy, Jianyi Cheng, Alastair Donaldson, Andreas Lööw, and the anonymous
reviewers for their helpful feedback.  This work was financially supported by the EPSRC via the
Research Institute for Verified Trustworthy Software Systems (VeTSS) and the IRIS Programme Grant
(EP/R006865/1).

%% Bibliography
\bibliography{references.bib}


%% Appendix
%\input{appendix}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% TeX-command-extra-options: "-shell-escape"
%%% End:
