summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-09-08 18:55:41 +0100
committerYann Herklotz <git@yannherklotz.com>2021-09-08 18:55:41 +0100
commita68d9b19756801fb1633edd17aec2ac9c22d8444 (patch)
tree5deb0f398621309decd0c106ef7b9b67eb06b0dc
parentaf5b7dd0370e7f0087b5bc58042baa71288c59bb (diff)
downloadoopsla21_fvhls-a68d9b19756801fb1633edd17aec2ac9c22d8444.tar.gz
oopsla21_fvhls-a68d9b19756801fb1633edd17aec2ac9c22d8444.zip
Some initial changes towards the final submission
-rw-r--r--ACM-Reference-Format.bst112
-rw-r--r--acmart.cls180
-rw-r--r--algorithm.tex36
-rw-r--r--main.tex59
-rw-r--r--verilog.tex2
5 files changed, 306 insertions, 83 deletions
diff --git a/ACM-Reference-Format.bst b/ACM-Reference-Format.bst
index 18bf3b8..c16e6f3 100644
--- a/ACM-Reference-Format.bst
+++ b/ACM-Reference-Format.bst
@@ -435,19 +435,19 @@ FUNCTION { output.coden } % UTAH
FUNCTION { strip.articleno.or.eid }
{
't :=
- t #1 #7 substring$ "Article" =
+ t #1 #7 substring$ "Article" =
{t #8 t text.length$ substring$ 't :=}
{ }
if$
- t #1 #7 substring$ "article" =
+ t #1 #7 substring$ "article" =
{t #8 t text.length$ substring$ 't :=}
{ }
if$
- t #1 #5 substring$ "Paper" =
+ t #1 #5 substring$ "Paper" =
{t #6 t text.length$ substring$ 't :=}
{ }
if$
- t #1 #5 substring$ "paper" =
+ t #1 #5 substring$ "paper" =
{t #6 t text.length$ substring$ 't :=}
{ }
if$
@@ -455,12 +455,12 @@ FUNCTION { strip.articleno.or.eid }
t #1 #1 substring$ " " =
{t #2 t text.length$ substring$ 't :=}
{ }
- if$
+ if$
t #1 #1 substring$ "~" =
{t #2 t text.length$ substring$ 't :=}
{ }
if$
- t
+ t
}
@@ -1454,7 +1454,12 @@ FUNCTION { format.pages.check.without.articleno }
articleno empty.or.unknown eid empty.or.unknown and
{
pages missing$
- { numpages }
+ {
+ numpages empty.or.unknown
+ {""}
+ { "\bibinfo{numpages}{" numpages * "}~pages" * }
+ if$
+ }
{ format.pages }
if$
}
@@ -2607,6 +2612,99 @@ MACRO {nov} {"Nov."}
MACRO {dec} {"Dec."}
+%%% ACM journal names
+
+MACRO {cie} {"ACM Computers in Entertainment"}
+MACRO {csur} {"ACM Computing Surveys"}
+MACRO {dgov} {"Digital Government: Research and Practice"}
+MACRO {dtrap} {"Digital Threats: Research and Practice"}
+MACRO {health} {"ACM Transactions on Computing for Healthcare"}
+MACRO {imwut} {"PACM on Interactive, Mobile, Wearable and Ubiquitous Technologies"}
+MACRO {jacm} {"Journal of the ACM"}
+MACRO {jdiq} {"ACM Journal of Data and Information Quality"}
+MACRO {jea} {"ACM Journal of Experimental Algorithmics"}
+MACRO {jeric} {"ACM Journal of Educational Resources in Computing"}
+MACRO {jetc} {"ACM Journal on Emerging Technologies in Computing Systems"}
+MACRO {jocch} {"ACM Journal on Computing and Cultural Heritage"}
+MACRO {pacmcgit} {"Proceedings of the ACM on Computer Graphics and Interactive Techniques"}
+MACRO {pacmhci} {"PACM on Human-Computer Interaction"}
+MACRO {pacmpl} {"PACM on Programming Languages"}
+MACRO {pomacs} {"PACM on Measurement and Analysis of Computing Systems"}
+MACRO {taas} {"ACM Transactions on Autonomous and Adaptive Systems"}
+MACRO {taccess} {"ACM Transactions on Accessible Computing"}
+MACRO {taco} {"ACM Transactions on Architecture and Code Optimization"}
+MACRO {talg} {"ACM Transactions on Algorithms"}
+MACRO {tallip} {"ACM Transactions on Asian and Low-Resource Language Information Processing"}
+MACRO {tap} {"ACM Transactions on Applied Perception"}
+MACRO {tcps} {"ACM Transactions on Cyber-Physical Systems"}
+MACRO {tds} {"ACM/IMS Transactions on Data Science"}
+MACRO {teac} {"ACM Transactions on Economics and Computation"}
+MACRO {tecs} {"ACM Transactions on Embedded Computing Systems"}
+MACRO {telo} {"ACM Transactions on Evolutionary Learning"}
+MACRO {thri} {"ACM Transactions on Human-Robot Interaction"}
+MACRO {tiis} {"ACM Transactions on Interactive Intelligent Systems"}
+MACRO {tiot} {"ACM Transactions on Internet of Things"}
+MACRO {tissec} {"ACM Transactions on Information and System Security"}
+MACRO {tist} {"ACM Transactions on Intelligent Systems and Technology"}
+MACRO {tkdd} {"ACM Transactions on Knowledge Discovery from Data"}
+MACRO {tmis} {"ACM Transactions on Management Information Systems"}
+MACRO {toce} {"ACM Transactions on Computing Education"}
+MACRO {tochi} {"ACM Transactions on Computer-Human Interaction"}
+MACRO {tocl} {"ACM Transactions on Computational Logic"}
+MACRO {tocs} {"ACM Transactions on Computer Systems"}
+MACRO {toct} {"ACM Transactions on Computation Theory"}
+MACRO {todaes} {"ACM Transactions on Design Automation of Electronic Systems"}
+MACRO {tods} {"ACM Transactions on Database Systems"}
+MACRO {tog} {"ACM Transactions on Graphics"}
+MACRO {tois} {"ACM Transactions on Information Systems"}
+MACRO {toit} {"ACM Transactions on Internet Technology"}
+MACRO {tomacs} {"ACM Transactions on Modeling and Computer Simulation"}
+MACRO {tomm} {"ACM Transactions on Multimedia Computing, Communications and Applications"}
+MACRO {tompecs} {"ACM Transactions on Modeling and Performance Evaluation of Computing Systems"}
+MACRO {toms} {"ACM Transactions on Mathematical Software"}
+MACRO {topc} {"ACM Transactions on Parallel Computing"}
+MACRO {toplas} {"ACM Transactions on Programming Languages and Systems"}
+MACRO {tops} {"ACM Transactions on Privacy and Security"}
+MACRO {tos} {"ACM Transactions on Storage"}
+MACRO {tosem} {"ACM Transactions on Software Engineering and Methodology"}
+MACRO {tosn} {"ACM Transactions on Sensor Networks"}
+MACRO {tqc} {"ACM Transactions on Quantum Computing"}
+MACRO {trets} {"ACM Transactions on Reconfigurable Technology and Systems"}
+MACRO {tsas} {"ACM Transactions on Spatial Algorithms and Systems"}
+MACRO {tsc} {"ACM Transactions on Social Computing"}
+MACRO {tslp} {"ACM Transactions on Speech and Language Processing"}
+MACRO {tweb} {"ACM Transactions on the Web"}
+
+%%% Some traditional macros
+MACRO {acmcs} {"ACM Computing Surveys"}
+
+MACRO {acta} {"Acta Informatica"}
+
+MACRO {cacm} {"Communications of the ACM"}
+
+MACRO {ibmjrd} {"IBM Journal of Research and Development"}
+
+MACRO {ibmsj} {"IBM Systems Journal"}
+
+MACRO {ieeese} {"IEEE Transactions on Software Engineering"}
+
+MACRO {ieeetc} {"IEEE Transactions on Computers"}
+
+MACRO {ieeetcad}
+ {"IEEE Transactions on Computer-Aided Design of Integrated Circuits"}
+
+MACRO {ipl} {"Information Processing Letters"}
+
+MACRO {jcss} {"Journal of Computer and System Sciences"}
+
+MACRO {scp} {"Science of Computer Programming"}
+
+MACRO {sicomp} {"SIAM Journal on Computing"}
+
+MACRO {toois} {"ACM Transactions on Office Information Systems"}
+
+MACRO {tcs} {"Theoretical Computer Science"}
+
READ
diff --git a/acmart.cls b/acmart.cls
index 239698b..393d65a 100644
--- a/acmart.cls
+++ b/acmart.cls
@@ -37,7 +37,7 @@
%% Right brace \} Tilde \~}
\NeedsTeXFormat{LaTeX2e}
\ProvidesClass{acmart}
-[2020/04/30 v1.71 Typesetting articles for the Association for Computing Machinery]
+[2021/04/16 v1.77 Typesetting articles for the Association for Computing Machinery]
\def\@classname{acmart}
\InputIfFileExists{acmart-preload-hook.tex}{%
\ClassWarning{\@classname}{%
@@ -120,6 +120,10 @@
\PackageError{\@classname}{The option balance can be either true or
false}}
\ExecuteOptionsX{balance}
+\define@boolkey+{acmart.cls}[@ACM@]{pbalance}[true]{}{%
+ \PackageError{\@classname}{The option pbalance can be either true or
+ false}}
+\ExecuteOptionsX{pbalance=false}
\define@boolkey+{acmart.cls}[@ACM@]{natbib}[true]{%
\if@ACM@natbib
\PackageInfo{\@classname}{Explicitly selecting natbib mode}%
@@ -487,6 +491,7 @@
\rule\z@\footnotesep\ignorespaces#1\@finalstrut\strutbox}%
\color@endgroup}}
\def\@makefnmark{\hbox{\@textsuperscript{\normalfont\@thefnmark}}}
+\RequirePackage{hyperxmp}
\let\@footnotemark@nolink\@footnotemark
\let\@footnotetext@nolink\@footnotetext
\RequirePackage[bookmarksnumbered,unicode]{hyperref}
@@ -698,7 +703,6 @@
\flushbottom
\or % sigchi-a
\fi
-\RequirePackage{iftex}
\ifPDFTeX
\input{glyphtounicode}
\pdfglyphtounicode{f_f}{FB00}
@@ -709,34 +713,40 @@
\pdfglyphtounicode{f_t}{0066 0074}
\pdfglyphtounicode{T_h}{0054 0068}
\pdfgentounicode=1
-\fi
\RequirePackage{cmap}
+\fi
\newif\if@ACM@newfonts
\@ACM@newfontstrue
\IfFileExists{libertine.sty}{}{\ClassWarning{\@classname}{You do not
have the libertine package installed. Please upgrade your
TeX}\@ACM@newfontsfalse}
\IfFileExists{zi4.sty}{}{\ClassWarning{\@classname}{You do not
- have the zi4 package installed. Please upgrade your
+ have the inconsolata (zi4.sty) package installed. Please upgrade your
TeX}\@ACM@newfontsfalse}
\IfFileExists{newtxmath.sty}{}{\ClassWarning{\@classname}{You do not
have the newtxmath package installed. Please upgrade your
TeX}\@ACM@newfontsfalse}
\if@ACM@newfonts
\RequirePackage[T1]{fontenc}
+ % Note that the order in which packages are loaded matters,
+ % and the correct order depends on the LaTeX engine used.
+ % See https://github.com/borisveytsman/acmart/issues/402
+ % and https://github.com/borisveytsman/acmart/issues/410
\ifxetex
+ \RequirePackage[libertine]{newtxmath}
\RequirePackage[tt=false]{libertine}
\setmonofont[StylisticSet=3]{inconsolata}
\else
\ifluatex
+ \RequirePackage[libertine]{newtxmath}
\RequirePackage[tt=false]{libertine}
\setmonofont[StylisticSet=3]{inconsolata}
\else
\RequirePackage[tt=false, type1=true]{libertine}
\RequirePackage[varqu]{zi4}
+ \RequirePackage[libertine]{newtxmath}
\fi
\fi
- \RequirePackage[libertine]{newtxmath}
\fi
\let\liningnums\@undefined
\AtEndPreamble{%
@@ -775,6 +785,14 @@
\let\@vspacer\@vspacer@orig}
\AtBeginEnvironment{lstlisting*}{\let\@vspace\@vspace@orig
\let\@vspacer\@vspacer@orig}
+\AtBeginEnvironment{minted}{\let\@vspace\@vspace@orig
+ \let\@vspacer\@vspacer@orig}
+\AtBeginEnvironment{minted*}{\let\@vspace\@vspace@orig
+ \let\@vspacer\@vspacer@orig}
+\AtBeginEnvironment{listing}{\let\@vspace\@vspace@orig
+ \let\@vspacer\@vspacer@orig}
+\AtBeginEnvironment{listing*}{\let\@vspace\@vspace@orig
+ \let\@vspacer\@vspacer@orig}
\RequirePackage{caption, float}
\captionsetup[table]{position=top}
@@ -1254,9 +1272,12 @@
DC, USA}%
\fi
\def\acmBooktitle#1{\gdef\@acmBooktitle{#1}}
+\acmBooktitle{}
+\ifx\acmConference@name\@undefined\else
\acmBooktitle{Proceedings of \acmConference@name
\ifx\acmConference@name\acmConference@shortname\else
- \ (\acmConference@shortname)\fi}
+ \ (\acmConference@shortname)\fi}
+\fi
\def\@editorsAbbrev{(Ed.)}
\def\@acmEditors{}
\def\editor#1{\ifx\@acmEditors\@empty
@@ -1274,7 +1295,7 @@
\newif\if@insideauthorgroup
\@insideauthorgroupfalse
\renewcommand\author[2][]{%
- \IfSubStr{#2}{,}{\ClassWarning{\@classname}{Do not put several
+ \IfSubStr{\detokenize{#2}}{,}{\ClassWarning{\@classname}{Do not put several
authors in the same \string\author\space macro!}}{}%
\global\advance\num@authors by 1\relax
\if@insideauthorgroup\else
@@ -1288,12 +1309,16 @@
\@acmSubmissionID\fi}}%
\gdef\authors{Anonymous Author(s)}%
\else
- \gdef\addresses{\@author{#2}}%
+ \expandafter\gdef\expandafter\addresses\expandafter{%
+ \expandafter\@author\expandafter{%
+ \csname typeset@author\the\num@authors\endcsname{#2}}}%
\gdef\authors{#2}%
\fi
\else
\if@ACM@anonymous\else
- \g@addto@macro\addresses{\and\@author{#2}}%
+ \expandafter\g@addto@macro\expandafter\addresses\expandafter{%
+ \expandafter\and\expandafter\@author\expandafter{%
+ \csname typeset@author\the\num@authors\endcsname{#2}}}%
\g@addto@macro\authors{\and#2}%
\fi
\fi
@@ -1344,7 +1369,14 @@
\if@ACM@anonymous\else
\g@addto@macro\addresses{\email{#1}{#2}}%
\fi}
-\def\orcid#1{\unskip\ignorespaces}
+\def\orcid#1{\unskip\ignorespaces%
+ \IfBeginWith{#1}{http}{%
+ \expandafter\gdef\csname
+ typeset@author\the\num@authors\endcsname##1{%
+ \href{#1}{##1}}}{%
+ \expandafter\gdef\csname
+ typeset@author\the\num@authors\endcsname##1{%
+ \href{https://orcid.org/#1}{##1}}}}
\def\authorsaddresses#1{\def\@authorsaddresses{#1}}
\authorsaddresses{\@mkauthorsaddresses}
\def\@titlenotes{}
@@ -1764,8 +1796,12 @@
\else
\g@addto@macro\thankses{\thanks{#1}}%
\fi}}
+\ifx\@beginmaketitlehook\@undefined
+ \let\@beginmaketitlehook\@empty
+\fi
+\def\AtBeginMaketitle{\g@addto@macro\@beginmaketitlehook}
\newbox\mktitle@bx
-\def\maketitle{%
+\def\maketitle{\@beginmaketitlehook
\@ACM@maketitle@typesettrue
\if@ACM@anonymous
% Anonymize omission of \author-s
@@ -1869,17 +1905,13 @@
\else
\@specialsection{Keywords}%
\fi
- \noindent\@keywords}\par\egroup
+ \noindent\@keywords\par}\egroup
\fi
- \andify\authors
- \andify\shortauthors
- \global\let\authors=\authors
- \global\let\shortauthors=\shortauthors
- \if@ACM@printacmref
- \@mkbibcitation
- \fi
+ \let\metadata@authors=\authors
+ \nxandlist{, }{, }{, }\metadata@authors
+ \def\@ACM@checkaffil{}%
\hypersetup{%
- pdfauthor={\authors},
+ pdfauthor={\metadata@authors},
pdftitle={\@title},
pdfsubject={\@concepts},
pdfkeywords={\@keywords},
@@ -1887,6 +1919,13 @@
\csname ver@acmart.cls\endcsname\space
and hyperref
\csname ver@hyperref.sty\endcsname}}%
+ \andify\authors
+ \andify\shortauthors
+ \global\let\authors=\authors
+ \global\let\shortauthors=\shortauthors
+ \if@ACM@printacmref
+ \@mkbibcitation
+ \fi
\global\@topnum\z@ % this prevents floats from falling
% at the top of page 1
\global\@botnum\z@ % we do not want them to be on the bottom either
@@ -2097,19 +2136,22 @@
\def\postcode#1{\unskip\ignorespaces}
\if@ACM@journal
\def\position#1{\unskip\ignorespaces}
- \def\institution#1{\unskip~#1\ignorespaces}
- \def\city#1{\unskip\ignorespaces}
+ \def\institution#1{\global\@ACM@instpresenttrue
+ \unskip~#1\ignorespaces}
+ \def\city#1{\global\@ACM@citypresenttrue\unskip\ignorespaces}
\def\state#1{\unskip\ignorespaces}
\newcommand\department[2][0]{\unskip\ignorespaces}
- \def\country#1{\if@ACM@affiliation@obeypunctuation\else, \fi#1\ignorespaces}
+ \def\country#1{\global\@ACM@countrypresenttrue
+ \if@ACM@affiliation@obeypunctuation\else, \fi#1\ignorespaces}
\else
\def\position#1{\if@ACM@affiliation@obeypunctuation#1\else#1\par\fi}%
- \def\institution#1{\if@ACM@affiliation@obeypunctuation#1\else#1\par\fi}%
+ \def\institution#1{\global\@ACM@instpresenttrue
+ \if@ACM@affiliation@obeypunctuation#1\else#1\par\fi}%
\newcommand\department[2][0]{\if@ACM@affiliation@obeypunctuation
#2\else#2\par\fi}%
- \let\city\@ACM@addtoaddress
+ \def\city#1{\global\@ACM@citypresenttrue\@ACM@addtoaddress{#1}}%
\let\state\@ACM@addtoaddress
- \let\country\@ACM@addtoaddress
+ \def\country#1{\global\@ACM@countrypresenttrue\@ACM@addtoaddress{#1}}%
\fi
\def\@mkauthors{\begingroup
\hsize=\textwidth
@@ -2170,6 +2212,29 @@
\unskip, {\@currentaffiliations}\par
\fi
\def\@currentaffiliations{}}
+\newif\if@ACM@instpresent
+\@ACM@instpresenttrue
+\newif\if@ACM@citypresent
+\@ACM@citypresenttrue
+\newif\if@ACM@countrypresent
+\@ACM@countrypresenttrue
+\def\@ACM@resetaffil{%
+ \global\@ACM@instpresentfalse
+ \global\@ACM@citypresentfalse
+ \global\@ACM@countrypresentfalse
+}
+\def\@ACM@checkaffil{%
+ \if@ACM@instpresent\else
+ \ClassWarningNoLine{\@classname}{No institution present for an affiliation}%
+ \fi
+ \if@ACM@citypresent\else
+ \ClassWarningNoLine{\@classname}{No city present for an affiliation}%
+ \fi
+ \if@ACM@countrypresent\else
+ \ClassError{\@classname}{No country present for an affiliation}{ACM
+ requires each author to indicate their country using country macro.}%
+ \fi
+}
\def\@mkauthors@i{%
\def\@currentauthors{}%
\def\@currentaffiliations{}%
@@ -2188,11 +2253,13 @@
\gdef\@currentaffiliations{%
\setkeys{@ACM@affiliation@}{obeypunctuation=false}%
\setkeys{@ACM@affiliation@}{##1}%
- \@affiliationfont##2}%
+ \@ACM@resetaffil
+ \@affiliationfont##2\@ACM@checkaffil}%
\else
\g@addto@macro{\@currentaffiliations}{\and
\setkeys{@ACM@affiliation@}{obeypunctuation=false}%
- \setkeys{@ACM@affiliation@}{##1}##2}%
+ \setkeys{@ACM@affiliation@}{##1}\@ACM@resetaffil
+ ##2\@ACM@checkaffil}%
\fi
\fi
\global\let\and\@typeset@author@line}%
@@ -2250,11 +2317,13 @@
\def\affiliation##1##2{\ifx\@currentaffiliation\@empty
\gdef\@currentaffiliation{%
\setkeys{@ACM@affiliation@}{obeypunctuation=false}%
- \setkeys{@ACM@affiliation@}{##1}##2}%
+ \setkeys{@ACM@affiliation@}{##1}\@ACM@resetaffil
+ ##2\@ACM@checkaffil}%
\else
\g@addto@macro\@currentaffiliation{\par
\setkeys{@ACM@affiliation@}{obeypunctuation=false}%
- \setkeys{@ACM@affiliation@}{##1}##2}%
+ \setkeys{@ACM@affiliation@}{##1}\@ACM@resetaffil
+ ##2\@ACM@checkaffil}%
\fi
\global\let\and\@typeset@author@bx
}%
@@ -2293,11 +2362,13 @@
\def\affiliation##1##2{\ifx\@currentaffiliation\@empty
\gdef\@currentaffiliation{%
\setkeys{@ACM@affiliation@}{obeypunctuation=false}%
- \setkeys{@ACM@affiliation@}{##1}##2}%
+ \setkeys{@ACM@affiliation@}{##1}\@ACM@resetaffil
+ ##2\@ACM@checkaffil}%
\else
\g@addto@macro\@currentaffiliation{\par
\setkeys{@ACM@affiliation@}{obeypunctuation=false}%
- \setkeys{@ACM@affiliation@}{##1}##2}%
+ \setkeys{@ACM@affiliation@}{##1}\@ACM@resetaffil
+ ##2\@ACM@checkaffil}%
\fi
\global\let\and\@typeset@author@bx}%
\bgroup\hsize=\columnwidth
@@ -2313,12 +2384,13 @@
\def\streetaddress##1{\unskip, ##1}%
\def\postcode##1{\unskip, ##1}%
\def\position##1{\unskip\ignorespaces}%
- \def\institution##1{\unskip, ##1}%
+ \gdef\@ACM@institution@separator{, }%
+ \def\institution##1{\unskip\@ACM@institution@separator ##1\gdef\@ACM@institution@separator{ and }}%
\def\city##1{\unskip, ##1}%
\def\state##1{\unskip, ##1}%
\renewcommand\department[2][0]{\unskip\@addpunct, ##2}%
\def\country##1{\unskip, ##1}%
- \def\and{\unskip; }%
+ \def\and{\unskip; \gdef\@ACM@institution@separator{, }}%
\def\@author##1{##1}%
\def\email##1##2{\unskip, \nolinkurl{##2}}%
\addresses
@@ -2534,7 +2606,10 @@
\fancyfoot[C]{\if@ACM@printfolios\footnotesize\thepage\fi}%
\fancyhead[LO]{\ACM@linecountL\@headfootfont\shorttitle}%
\fancyhead[RE]{\@headfootfont\@shortauthors\ACM@linecountR}%
- \if@ACM@nonacm\else%
+ \if@ACM@nonacm
+ \fancyhead[LE]{\ACM@linecountL}%
+ \fancyhead[RO]{\ACM@linecountR}%
+ \else%
\fancyhead[LE]{\ACM@linecountL\@headfootfont\footnotesize
\acmConference@shortname,
\acmConference@date, \acmConference@venue}%
@@ -2547,7 +2622,10 @@
\fancyfoot[C]{\if@ACM@printfolios\footnotesize\thepage\fi}%
\fancyhead[LO]{\ACM@linecountL\@headfootfont\shorttitle}%
\fancyhead[RE]{\@headfootfont\@shortauthors\ACM@linecountR}%
- \if@ACM@nonacm\else%
+ \if@ACM@nonacm
+ \fancyhead[LE]{\ACM@linecountL}%
+ \fancyhead[RO]{\ACM@linecountR}%
+ \else%
\fancyhead[LE]{\ACM@linecountL\@headfootfont
\acmConference@shortname,
\acmConference@date, \acmConference@venue}%
@@ -2878,6 +2956,25 @@
\popQED\endtrivlist\@endpefalse
}
\AtEndPreamble{%
+ \if@ACM@pbalance
+ \global\@ACM@balancefalse
+ \ifcase\ACM@format@nr
+ \relax % manuscript
+ \or % acmsmall
+ \or % acmlarge
+ \or % acmtog
+ \RequirePackage{pbalance}%
+ \or % sigconf
+ \RequirePackage{pbalance}%
+ \or % siggraph
+ \RequirePackage{pbalance}%
+ \or % sigplan
+ \RequirePackage{pbalance}%
+ \or % sigchi
+ \RequirePackage{pbalance}%
+ \or % sigchi-a
+ \fi
+ \fi
\if@ACM@balance
\ifcase\ACM@format@nr
\relax % manuscript
@@ -2935,8 +3032,15 @@
\def\@tempa{#1}%
\ifx\@tempa\@empty\def\@tempa{arxiv}\fi
\def\@tempb{arxiv}%
- \ifx\@tempa\@tempb
- arXiv:\href{https://arxiv.org/abs/#2}{#2}\else arXiv:#2%
+ \ifx\@tempa\@tempb\relax
+ arXiv:\href{https://arxiv.org/abs/#2}{#2}%
+ \else
+ \def\@tempb{arXiv}%
+ \ifx\@tempa\@tempb\relax
+ arXiv:\href{https://arxiv.org/abs/#2}{#2}%
+ \else
+ arXiv:#2%
+ \fi
\fi}
\let\@vspace@orig=\@vspace
\let\@vspacer@orig=\@vspacer
diff --git a/algorithm.tex b/algorithm.tex
index c3b2153..06cf110 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -34,26 +34,26 @@ The .NET framework has been used as a basis for other HLS tools, such as Kiwi~\c
[language/.style={fill=white,rounded corners=3pt,minimum height=7mm},
continuation/.style={},
linecount/.style={rounded corners=3pt,dashed}]
- \fill[compcert,rounded corners=3pt] (-1,-0.5) rectangle (11.4,2);
- \fill[formalhls,rounded corners=3pt] (-1,-1) rectangle (11.4,-2);
- \draw[linecount] (-0.95,-0.45) rectangle (3.6,1);
- \draw[linecount] (4,-0.45) rectangle (7.5,1);
+ \fill[compcert,rounded corners=3pt] (-1,-0.5) rectangle (9.9,2);
+ \fill[formalhls,rounded corners=3pt] (-1,-1) rectangle (9.9,-2);
+ %\draw[linecount] (-0.95,-0.45) rectangle (3.6,1);
+ %\draw[linecount] (4,-0.45) rectangle (7.5,1);
\node[language] at (-0.3,0) (clight) {Clight};
\node[continuation] at (1,0) (conta) {$\cdots$};
\node[language] at (2.7,0) (cminor) {CminorSel};
\node[language] at (4.7,0) (rtl) {3AC};
\node[language] at (6.2,0) (ltl) {LTL};
- \node[language,anchor=west] at (8.4,0) (aarch) {aarch64 \small ($\sim$ 12 kloc)};
- \node[language,anchor=west] at (8.4,0.8) (x86) {x86 \small ($\sim$ 14 kloc)};
+ \node[language,anchor=west] at (8.4,0) (aarch) {aarch64};
+ \node[language,anchor=west] at (8.4,0.8) (x86) {x86};
\node[continuation,anchor=west] at (8.4,1.4) (backs) {$\cdots$};
\node[continuation] at (7.3,0) (contb) {$\cdots$};
\node[language] at (4.7,-1.5) (htl) {HTL};
\node[language] at (6.7,-1.5) (verilog) {Verilog};
\node at (0,1.5) {\bf\compcert{}};
\node at (0,-1.5) {\bf\vericert{}};
- \node[anchor=west] at (-0.9,0.7) {\small $\sim$ 27 kloc};
- \node[anchor=west] at (4.1,0.7) {\small $\sim$ 46 kloc};
- \node[anchor=west] at (2,-1.5) {\small $\sim$ 17 kloc};
+ %%\node[anchor=west] at (-0.9,0.7) {\small $\sim$ 27 kloc};
+ %%\node[anchor=west] at (4.1,0.7) {\small $\sim$ 46 kloc};
+ %%\node[anchor=west] at (2,-1.5) {\small $\sim$ 17 kloc};
\node[align=center] at (3.5,-2.4) {\footnotesize RAM\\[-0.5em]\footnotesize insertion};
\draw[->,thick] (clight) -- (conta);
\draw[->,thick] (conta) -- (cminor);
@@ -67,7 +67,7 @@ The .NET framework has been used as a basis for other HLS tools, such as Kiwi~\c
\draw[->,thick] (htl) -- (verilog);
\draw[->,thick] (htl.west) to [out=180,in=150] (4,-2.2) to [out=330,in=270] (htl.south);
\end{tikzpicture}%}
- \caption{\vericert{} as a Verilog back end to \compcert{}. For scale, the approximate lines of code (kloc) are shown for \vericert{}, as well as for the front end and back end of \compcert{}, including any comments and whitespace.}%
+ \caption{\vericert{} as a Verilog back end to \compcert{}.}%
\label{fig:rtlbranch}
\end{figure}
@@ -115,9 +115,9 @@ endmodule
\begin{subfigure}{0.45\linewidth}
\centering
\begin{tikzpicture}
- \node[draw,circle,inner sep=8pt] (s0) at (0,0) {$S_{0}$};
- \node[draw,circle,inner sep=8pt] (s1) at (1.5,-3) {$S_{1}$};
- \node[draw,circle,inner sep=8pt] (s2) at (3,0) {$S_{2}$};
+ \node[draw,circle,inner sep=6pt] (s0) at (0,0) {$S_{\mathit{start}}$};
+ \node[draw,circle,inner sep=8pt] (s1) at (1.5,-3) {$S_{0}$};
+ \node[draw,circle,inner sep=8pt] (s2) at (3,0) {$S_{1}$};
\node (s2s) at ($(s2.west) + (-0.3,1)$) {\texttt{x0/1}};
\node (s2ss) at ($(s2.east) + (0.3,1)$) {\texttt{1x/1}};
\draw[-{Latex[length=2mm,width=1.4mm]}] ($(s0.west) + (-0.3,1)$) to [out=0,in=120] (s0);
@@ -250,8 +250,8 @@ This involves going from a CFG representation of the computation to a finite sta
Hence, an HTL program consists of two maps from states to Verilog statements: the \emph{control logic} map, which expresses state transitions, and the \emph{data-path} map, which expresses computations.
Figure~\ref{fig:accumulator_diagram} shows the resulting FSMD architecture. The right-hand block is the control logic that computes the next state, while the left-hand block updates all the registers and RAM based on the current program state.
-The HTL language was mainly introduced to make it easier to prove the translation from 3AC to Verilog, as these languages have very different semantics.
-It serves as an intermediate language with similar semantics to 3AC at the top level, using maps to represents what to execute at every state, and similar semantics to Verilog at the low level by already using Verilog statements instead of more abstract instructions.
+The HTL language was mainly introduced to simplify the proof of translation from 3AC to Verilog, as these languages have very different semantics.
+It serves as an intermediate language with similar semantics to 3AC at the top level, using maps to represents what to execute at every state, and similar semantics to Verilog at the lower level by already using Verilog statements instead of more abstract instructions.
Compared to plain Verilog, HTL is simpler to manipulate and analyse, thereby making it easier to prove optimisations like proper RAM insertion.
\begin{figure*}
@@ -375,7 +375,7 @@ Most 3AC instructions correspond to hardware constructs.
% JW: Thanks; please check proposed new text.
For example, line 2 in Figure~\ref{fig:accumulator_rtl} shows a 32-bit register \texttt{x5} being initialised to 3, after which the control flow moves execution to line 3. This initialisation is also encoded in the Verilog generated from HTL at state 8 in both the control logic and data-path always-blocks, shown at lines 33 and 16 respectively in Figure~\ref{fig:accumulator_v}. Simple operator instructions are translated in a similar way. For example, the add instruction is just translated to the built-in add operator, similarly for the multiply operator. All 32-bit instructions can be translated in this way, but some special instructions require extra care. One such is the \texttt{Oshrximm} instruction, which is discussed further in Section~\ref{sec:algorithm:optimisation:oshrximm}. Another is the \texttt{Oshldimm} instruction, which is a left rotate instruction that has no Verilog equivalent and therefore has to be implemented in terms of other operations and proven to be equivalent.
% In addition to any non-32-bit operations, the remaining
-The only 32-bit instructions that we do not translate are those related to function calls (\texttt{Icall}, \texttt{Ibuiltin}, and \texttt{Itailcall}), because we enable inlining by default.
+The only 32-bit instructions that we do not translate are case-statements (\texttt{Ijumptable}) and those instructions related to function calls (\texttt{Icall}, \texttt{Ibuiltin}, and \texttt{Itailcall}), because we enable inlining by default.
\subsubsection{Translating HTL to Verilog}
@@ -398,9 +398,9 @@ Although we would not claim that \vericert{} is a proper `optimising' HLS compil
\subsubsection{Byte- and word-addressable memories}
One big difference between C and Verilog is how memory is represented. Although Verilog arrays use similar syntax to C arrays, they must be treated quite differently. To make loads and stores as efficient as possible, the RAM needs to be word-addressable, which means that an entire integer can be loaded or stored in one clock cycle.
-However, the memory model that \compcert{} uses for its intermediate languages is byte-addre\-ssa\-ble~\cite{blazy05_formal_verif_memor_model_c}. If a byte-addressable memory was used in the target hardware, which is closer to \compcert{}'s memory model, then a load and store would instead take four clock cycles, because a RAM can only perform one read and write per clock cycle. It therefore has to be proven that the byte-addressable memory behaves in the same way as the word-addressable memory in hardware. Any modifications of the bytes in the \compcert{} memory model also have to be shown to modify the word-addressable memory in the same way. Since only integer loads and stores are currently supported in \vericert{}, it follows that the addresses given to the loads and stores will be multiples of four. If that is the case, then the translation from byte-addressed memory to word-addressed memory can be done by dividing the address by four.
+However, the memory model that \compcert{} uses for its intermediate languages is byte-addre\-ssa\-ble~\cite{blazy05_formal_verif_memor_model_c}. If a byte-addressable memory was used in the target hardware, which is closer to \compcert{}'s memory model, then a load and store would instead take four clock cycles, because a RAM can only perform one read and write per clock cycle. It therefore has to be proven that the byte-addressable memory behaves in the same way as the word-addressable memory in hardware. Any modifications of the bytes in the \compcert{} memory model also have to be shown to modify the word-addressable memory in the same way. Since only integer loads and stores are currently supported in \vericert{}, it follows that the addresses given to the loads and stores will be multiples of four. Translating from byte-addressed memory to word-addressed memory can then be done by dividing the address by four.
-\subsubsection{Implementation of RAM interface}
+\subsubsection{Implementation of RAM interface}\label{sec:algorithm:optimisation:ram}
The simplest way to implement loads and stores in \vericert{} would be to access the Verilog array directly from within the data-path (i.e., inside the always-block on lines 16--32 of Figure~\ref{fig:accumulator_v}). This would be correct, but when a Verilog array is accessed at several program points, the synthesis tool is unlikely to detect that it can be implemented as a RAM block, and will resort to using lots of registers instead, ruining the circuit's area and performance. To avert this, we arrange that the data-path does not access memory directly, but simply sets the address it wishes to access and then toggles the \texttt{u\_en} flag. This activates the RAM interface (lines 9--15 of Figure~\ref{fig:accumulator_v}) on the next falling clock edge, which performs the requested load or store. By factoring all the memory accesses out into a separate interface like this, we ensure that the underlying array is only accessed from a single program point in the Verilog code, and thus ensure that the synthesis tool will correctly infer a RAM block.\footnote{Interestingly, the Verilog code shown for the RAM interface must not be modified, because the synthesis tool will only generate a RAM when the code matches a small set of specific patterns.}
%\JW{I tweaked this slightly in an attempt to clarify; please check.} %\NR{Bring forward this sentence to help with flow.}
diff --git a/main.tex b/main.tex
index d0fb3fc..84bddd0 100644
--- a/main.tex
+++ b/main.tex
@@ -13,19 +13,18 @@
%% 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}
+%%\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}
@@ -36,6 +35,28 @@
%% 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}
@@ -104,38 +125,38 @@
\begin{document}
-\title[Formal Verification of HLS]{Formal Verification of High-Level Synthesis}
+\title{Formal Verification of High-Level Synthesis}
%% Author with single affiliation.
\author{Yann Herklotz}
\orcid{0000-0002-2329-1029}
\affiliation{
- \institution{Imperial College London, UK}
- %\country{UK}
+ \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, UK}
- %\country{UK}
+ \institution{Imperial College London}
+ \country{UK}
}
\email{james.pollard16@imperial.ac.uk}
\author{Nadesh Ramanathan}
-\orcid{0000-0000-0000-0000}
+\orcid{0000-0001-9083-8349}
\affiliation{
- \institution{Imperial College London, UK}
- %\country{UK}
+ \institution{Imperial College London}
+ \country{UK}
}
\email{n.ramanathan14@imperial.ac.uk}
\author{John Wickerson}
-\orcid{0000-0000-0000-0000}
+\orcid{0000-0001-6735-5533}
\affiliation{
- \institution{Imperial College London, UK}
- %\country{UK}
+ \institution{Imperial College London}
+ \country{UK}
}
\email{j.wickerson@imperial.ac.uk}
diff --git a/verilog.tex b/verilog.tex
index 1a1ac2f..c0eced8 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -63,7 +63,7 @@ The main execution of the module $\downarrow_{\text{module}}$ is split into $\do
\paragraph{Removing support for external inputs to modules} Support for receiving external inputs was removed from the semantics for simplicity, as these are not needed for an HLS target. The main module in Verilog models the main function in C, and since the inputs to a C function should not change during its execution, there is no need for external inputs for Verilog modules.
-\paragraph{Simplifying representation of bitvectors} Finally, we use 32-bit integers to represent bitvectors rather than arrays of Booleans. This is because \vericert{} (currently) only supports types represented by 32 bits.
+\paragraph{Simplifying representation of bitvectors} Finally, we use 32-bit integers to represent bitvectors rather than arrays of booleans. This is because \vericert{} (currently) only supports types represented by 32 bits.
\subsection{Integrating the Verilog Semantics into \compcert{}'s Model}
\label{sec:verilog:integrating}