summaryrefslogtreecommitdiffstats
path: root/main.tex
diff options
context:
space:
mode:
authorn.ramanathan14 <n.ramanathan14@imperial.ac.uk>2020-11-20 10:25:10 +0000
committeroverleaf <overleaf@localhost>2020-11-20 10:33:05 +0000
commitf15f47310bb4ed375c9004509f13a352b5797062 (patch)
tree4476d23c25f97aa4c384b6f60b7d1b76c08bc6c0 /main.tex
parenta5c4157174c3eedd1e086825ff316ca9a42215c1 (diff)
downloadoopsla21_fvhls-f15f47310bb4ed375c9004509f13a352b5797062.tar.gz
oopsla21_fvhls-f15f47310bb4ed375c9004509f13a352b5797062.zip
Update on Overleaf.
Diffstat (limited to 'main.tex')
-rw-r--r--main.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/main.tex b/main.tex
index 512226e..81fed60 100644
--- a/main.tex
+++ b/main.tex
@@ -150,9 +150,9 @@
\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 like 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. Worse, there is mounting evidence that existing HLS tools are actually quite unreliable, sometimes generating wrong hardware or crashing when given valid inputs.
+ 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 like 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. Worse, 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-esque intermediate language and a Verilog back end, and has been proven correct in Coq. \vericert{} supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables. We evaluate \vericert{} on the PolyBench/C benchmark suite. We can generate Polybench hardware that is guaranteed to be translated correctly from C to Verilog. Our generated hardware is a magnitude slower and larger than hardware generated by an existing, optimised but unverified HLS tool.
+ 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-esque intermediate language and a Verilog back end, and has been proven correct in Coq. \vericert{} supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables. We evaluate \vericert{} on the PolyBench/C benchmark suite. We can generate Polybench hardware that is guaranteed to be translated correctly from C to Verilog. Our generated hardware is a magnitude slower and larger than hardware generated by an existing, optimised but unverified HLS tool.
\end{abstract}
%% 2012 ACM Computing Classification System (CSS) concepts