%% For double-blind review submission, w/o CCS and ACM Reference (max submission space)
\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{none}
%\setcopyright{acmcopyright}
%\setcopyright{acmlicensed}
%\setcopyright{rightsretained}
%\copyrightyear{2018}

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

\renewcommand*{\backrefalt}[4]{%
    \ifcase #1%
          \or [Page~#2.]%
          \else [Pages~#2.]%
    \fi%
    }

\usepackage{amsmath}
\usepackage{booktabs}
\usepackage{mathpartir}
\usepackage{subcaption}
\usepackage{tikz}

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

\definecolor{compcert}{HTML}{66c2a5}
\definecolor{formalhls}{HTML}{fc8d62}

\begin{document}

%% Title information
\title[Formally Verified HLS]{Formally Verified High-Level Synthesis}         %% [Short Title] is optional;
                                        %% when present, will be used in
                                        %% header instead of Full Title.
%\titlenote{with title note}             %% \titlenote is optional;
                                        %% can be repeated if necessary;
                                        %% contents suppressed with 'anonymous'
%\subtitle{Subtitle}                     %% \subtitle is optional
%\subtitlenote{with subtitle note}       %% \subtitlenote is optional;
                                        %% can be repeated if necessary;
                                        %% contents suppressed with 'anonymous'


%% Author information
%% Contents and number of authors suppressed with 'anonymous'.
%% Each author should be introduced by \author, followed by
%% \authornote (optional), \orcid (optional), \affiliation, and
%% \email.
%% An author may have multiple affiliations and/or emails; repeat the
%% appropriate command.
%% Many elements are not rendered, but should be provided for metadata
%% extraction tools.

%% Author with single affiliation.
\author{Yann Herklotz}
\orcid{0000-0002-2329-1029}
\affiliation{
%  \position{PhD Student}
%  \department{EEE}
  \institution{Imperial College London}
%  \streetaddress{South Kensington Campus}
%  \city{London}
%  \state{}
%  \postcode{SW7 2AZ}
  \country{UK}
}
\email{yann.herklotz15@imperial.ac.uk}

\author{James Pollard}
\orcid{0000-0003-1404-1527}
\affiliation{
%  \position{}
%  \department{EEE}
  \institution{Imperial College London}
%  \streetaddress{South Kensington Campus}
%  \city{London}
%  \state{}
%  \postcode{SW7 2AZ}
  \country{UK}
}
\email{james.pollard16@imperial.ac.uk}

\author{Nadesh Ramanathan}
\orcid{0000-0000-0000-0000}
\affiliation{
%  \position{}
%  \department{EEE}
  \institution{Imperial College London}
%  \streetaddress{South Kensington Campus}
%  \city{London}
%  \state{}
%  \postcode{SW7 2AZ}
  \country{UK}
}
\email{n.ramanathan14@imperial.ac.uk}

\author{John Wickerson}
\orcid{0000-0000-0000-0000}
\affiliation{
%  \position{}
%  \department{EEE}
  \institution{Imperial College London}
%  \streetaddress{South Kensington Campus}
%  \city{London}
%  \state{}
%  \postcode{SW7 2AZ}
  \country{UK}
}
\email{j.wickerson@imperial.ac.uk}


%% Abstract
\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}


%% 2012 ACM Computing Classification System (CSS) concepts
%% Generate at 'http://dl.acm.org/ccs/ccs.cfm'.
\begin{CCSXML}
<ccs2012>
<concept>
<concept_id>10011007.10011006.10011008</concept_id>
<concept_desc>Software and its engineering~General programming languages</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003456.10003457.10003521.10003525</concept_id>
<concept_desc>Social and professional topics~History of programming languages</concept_desc>
<concept_significance>300</concept_significance>
</concept>
</ccs2012>
\end{CCSXML}

\ccsdesc[500]{Software and its engineering~General programming languages}
\ccsdesc[300]{Social and professional topics~History of programming languages}
%% End of generated code


%% Keywords
%% comma separated list
\keywords{CompCert, Coq, high-level synthesis}

\maketitle

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

%% Acknowledgments
\begin{acks}                            %% acks environment is optional
                                        %% contents suppressed with 'anonymous'
  %% Commands \grantsponsor{<sponsorID>}{<name>}{<url>} and
  %% \grantnum[<url>]{<sponsorID>}{<number>} should be used to
  %% acknowledge financial support and will be used by metadata
  %% extraction tools.
  This material is based upon work supported by the
  \grantsponsor{GS100000001}{National Science
    Foundation}{http://dx.doi.org/10.13039/100000001} under Grant
  No.~\grantnum{GS100000001}{nnnnnnn} and Grant
  No.~\grantnum{GS100000001}{mmmmmmm}.  Any opinions, findings, and
  conclusions or recommendations expressed in this material are those
  of the author and do not necessarily reflect the views of the
  National Science Foundation.
\end{acks}


%% Bibliography
\bibliography{references.bib}


%% Appendix
\appendix
\section{Appendix}

Text of appendix \ldots

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: