path: root/main.tex

%% For double-blind review submission, w/o CCS and ACM Reference (max submission space)
\documentclass[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{} % \acmDOI{10.1145/nnnnnnn.nnnnnnn};'--
\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}           %% If different from \acmYear

%% Bibliography style
\bibliographystyle{ACM-Reference-Format}
%% Citation style
%% Note: author/year citations are required for papers published as an
%% issue of PACMPL.
\citestyle{acmauthoryear}   %% For author/year citations


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Note: Authors migrating a paper from PACMPL format to traditional
%% SIGPLAN proceedings format must update the '\documentclass' and
%% topmatter commands above; see 'acmart-sigplanproc-template.tex'.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


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

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

\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}
%\authornote{with author1 note}          %% \authornote is optional;
                                        %% can be repeated if necessary
\orcid{0000-0002-2329-1029}             %% \orcid is optional
\affiliation{
%  \position{PhD Student}
%  \department{Electrical and Electronic Engineering} %% \department is recommended
  \institution{Imperial College London} %% \institution is required
%  \streetaddress{South Kensington Campus}
%  \city{London}
  \state{}
%  \postcode{SW7 2AZ}
  \country{UK}                    %% \country is recommended
}
\email{yann.herklotz15@imperial.ac.uk}          %% \email is recommended

\author{James Pollard}
%\authornote{with author1 note}          %% \authornote is optional;
                                        %% can be repeated if necessary
\orcid{0000-0003-1404-1527}             %% \orcid is optional
\affiliation{
%  \position{PhD Student}
%  \department{Electrical and Electronic Engineering} %% \department is recommended
  \institution{Imperial College London} %% \institution is required
%  \streetaddress{South Kensington Campus}
%  \city{London}
  \state{}
%  \postcode{SW7 2AZ}
  \country{UK}                    %% \country is recommended
}
\email{james.pollard16@imperial.ac.uk}          %% \email is recommended

\author{Nadesh Ramanathan}
%\authornote{with author1 note}          %% \authornote is optional;
                                        %% can be repeated if necessary
\orcid{0000-0000-0000-0000}             %% \orcid is optional
\affiliation{
%  \position{PhD Student}
%  \department{Electrical and Electronic Engineering} %% \department is recommended
  \institution{Imperial College London} %% \institution is required
%  \streetaddress{South Kensington Campus}
%  \city{London}
  \state{}
%  \postcode{SW7 2AZ}
  \country{UK}                    %% \country is recommended
}
\email{n.ramanathan14@imperial.ac.uk}          %% \email is recommended

\author{John Wickerson}
%\authornote{with author1 note}          %% \authornote is optional;
                                        %% can be repeated if necessary
\orcid{0000-0000-0000-0000}             %% \orcid is optional
\affiliation{
%  \position{PhD Student}
%  \department{Electrical and Electronic Engineering} %% \department is recommended
  \institution{Imperial College London} %% \institution is required
%  \streetaddress{South Kensington Campus}
%  \city{London}
  \state{}
%  \postcode{SW7 2AZ}
  \country{UK}                    %% \country is recommended
}
\email{j.wickerson@imperial.ac.uk}          %% \email is recommended


%% Abstract
%% Note: \begin{abstract}...\end{abstract} environment must come
%% before \maketitle command
\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 as well as simpler behavioural verification, as all the software tools can be used.  The HLS process has to be trusted though to be sure that .  C constructs are also often not supported in various combinations, which make existing tools quite brittle.  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.
\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}  %% \keywords are mandatory in final camera-ready submission


%% \maketitle
%% Note: \maketitle command must come after title commands, author
%% commands, abstract environment, Computing Classification System
%% environment and commands, and keywords command.
\maketitle


\section{Introduction}

\section{Background}

\subsection{Verilog}

\subsection{CompCert / Coq / Proof by simulation}

\subsection{HLS}

\section{Verilog Semantics}

Definition of state.

\begin{equation}
  \label{eq:10}
  s = (\Gamma, \Delta)
\end{equation}

Definition of stmntrun. \JW{stmtntrun has four parameters, and if I read the rules correctly, it looks like the fourth parameter is uniquely determined by the first three. So, you could consider presenting stmntrun simply as a recursive definition, e.g. `stmntrun f s Vskip = s', `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2', and so on. That might (\emph{might}) be easier to read than the inference rule format.}

\YH{It works well for Seq and Skip, but I think that CaseMatch and CaseNoMatch, or even if statements will be a bit clunky? We would have to use case statements in the function to do different things
based on what they evaluate to. For case I think that would end up being a three way choice. I'll try it out though and see how nice it is.}

\JP{I suppose this would essentially be an ``interpreter'' style semantics but we can prove equivalence pretty easily.}

\YH{To add to that, I used to have both in the Coq code, but commented the recursive definition out, and now only have the inductive definition, which is basically what I copy pasted here.} \JW{Fair enough. Whatever you think ends up being the easiest to read and understand, really. There's something to be said for staying close to the Coq definitions anyway.}

\begin{align}
    \text{stmntrun}\ f\ s\ \mathtt{Vskip} &= s \\
    \text{stmntrun}\ f\ s_0\ (\mathtt{Vseq}\ \mathit{st}_1\ \mathit{st}_2) &= \text{stmntrun}\ f\
    (\text{stmntrun}\ f\ s_0\ \mathit{st}_1)\ \mathit{st}_2
\end{align}

\begin{equation}
  \label{eq:1}
  \inferrule[Skip]{ }{\text{stmntrun}\ f\ s\ \mathtt{Vskip} = s}
\end{equation}

\begin{equation}
  \label{eq:4}
  \inferrule[Seq]{\text{stmntrun}\ f\ s_{0}\ \mathit{st}_{1}\ s_{1} \\ \text{stmntrun}\ f\ s_{1}\ \mathit{st}_{2}\ s_{2}}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vseq}\ \mathit{st}_{1}\ \mathit{st}_{2})\ s_{2}}
\end{equation}

\begin{equation}
  \label{eq:2}
  \inferrule[CondTrue]{\text{exprrun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \text{valToB}\ v_{c} = \mathtt{true} \\ \text{stmntrun}\ f\ s_{0}\ \mathit{stt}\ s_{1}}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf})\ s_{1}}
\end{equation}

\begin{equation}
  \label{eq:3}
  \inferrule[CondFalse]{\text{exprrun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \text{valToB}\ v_{c} = \mathtt{false} \\ \text{stmntrun}\ f\ s_{0}\ \mathit{stf}\ s_{1}}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf})\ s_{1}}
\end{equation}

\begin{equation}
  \label{eq:5}
  \inferrule[CaseNoMatch]{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ cs\ def)\ s_{1} \\ \text{exprrun}\ f\ \Gamma_{0}\ me\ mve \\ \text{exprrun}\ f\ \Gamma_{0}\ e\ ve \\ mve \neq ve}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ def)\ s_{1}}
\end{equation}

\begin{equation}
  \label{eq:6}
  \inferrule[CaseMatch]{\text{stmntrun}\ f\ s_{0}\ sc\ s_{1} \\ \text{exprrun}\ f\ \Gamma_{0}\ e\ ve \\ \text{exprrun}\ f\ \Gamma_{0}\ me\ mve \\ mve = ve}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ def)\ s_{1}}
\end{equation}

\begin{equation}
  \label{eq:7}
  \inferrule[CaseDefault]{\text{stmntrun}\ f\ s_{0}\ st\ s_{1}}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ []\ (\mathtt{Some}\ st))\ s_{1}}
\end{equation}

\begin{equation}
  \label{eq:8}
  \inferrule[Blocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{exprrun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{stmntrun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vblock}\ \mathit{lhs}\ \mathit{rhs})\ (\Gamma ! n \rightarrow v_{\mathit{rhs}}, \Delta)}
\end{equation}

\begin{equation}
  \label{eq:9}
  \inferrule[Nonblocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{exprrun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{stmntrun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vnonblock}\ \mathit{lhs}\ \mathit{rhs}) = (\Gamma, \Delta ! n \rightarrow v_{\mathit{rhs}})}
\end{equation}

\section{Proof}

\section{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}