diff options
Diffstat (limited to 'main.tex')
| -rw-r--r-- | main.tex | 43 |
1 files changed, 3 insertions, 40 deletions
@@ -1,5 +1,6 @@ %% 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} +\documentclass[sigplan,10pt,pagebackref=true,review,anonymous]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false} +%\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) @@ -35,13 +36,6 @@ %% Citation style \citestyle{acmauthoryear} -\renewcommand*{\backrefalt}[4]{% - \ifcase #1% - \or [Page~#2.]% - \else [Pages~#2.]% - \fi% - } - \usepackage{amsmath} \usepackage{booktabs} \usepackage{mathpartir} @@ -67,7 +61,7 @@ \definecolor{constantcolour}{HTML}{0000bb} \newcommand\yhkeywordsp[1]{\;\;\texttt{\textcolor{keywordcolour}{#1}}} -\newcommand\yhkeyword[1]{\texttt{\textcolor{keywordcolour}{#1}}}4 +\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}}} @@ -101,13 +95,7 @@ \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} @@ -115,13 +103,7 @@ \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} @@ -129,13 +111,7 @@ \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} @@ -143,30 +119,17 @@ \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} -% High-level synthesis (HLS) refers to the automatic compilation of software into hardware. In a world increasingly reliant on application-specific hardware accelerators, HLS allows developers to enjoy the high-level abstractions and mature tooling associated with software development, while still benefitting from the performance and energy-efficiency of custom hardware. However, its adoption in safety-critical contexts is limited because no existing HLS tool guarantees that the output hardware is behaviourally equivalent to the input software. Indeed, there is empirical evidence that existing HLS tools, being complex pieces of software that implement delicate algorithms, are quite buggy. This undermines any assurance provided by software-level analysis. - -% Aiming to rectify that shortcoming, we present the first HLS tool that is mechanically verified to be semantics-preserving. Our tool, called CoqUp, is realised as an extension to the CompCert verified C compiler. It consists of a new hardware-oriented intermediate language and a new Verilog-producing back-end, all proven correct in Coq. CoqUp supports the full C language as input, except recursion and non-integer datatypes. An evaluation on the standard CHStone benchmark indicates that CoqUp generates hardware that is slower than, but has a comparable area to, that generated by two existing (unverified) HLS tools. - - -%% Abstract \begin{abstract} High-level synthesis (HLS) refers to automatically compiling software into hardware. In a world increasingly reliant on application-specific hardware accelerators, HLS provides a higher-level of abstraction for hardware designers, while also benefitting from the rich software ecosystem to verify the functionality of their designs. However, adoption of HLS in safety-critical applications is still limited, because current tools cannot verify that the hardware implements the same behaviour as the software it was generated from, eliminating the benefits that software verification may provide. There is even evidence that HLS tools tend to be quite unreliable instead, either generating wrong hardware or sometimes not generating any hardware at all. We present the first mechanically verified HLS tool that preserves the behaviour of the software according to our semantics. Our tool, called VeriCert, extends the CompCert verified C compiler and consists of a new hardware specific intermediate language and a Verilog back end, which has been proven correct in Coq. VeriCert supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables. It has been evaluated on all suitable PolyBench benchmarks, which indicates that it generates hardware with area and cycle count around a magnitude larger than an existing, unverified HLS tool. \end{abstract} - %% 2012 ACM Computing Classification System (CSS) concepts %% Generate at 'http://dl.acm.org/ccs/ccs.cfm'. \begin{CCSXML} |