summaryrefslogtreecommitdiffstats
path: root/main.tex
diff options
context:
space:
mode:
authorJohn Wickerson <j.wickerson@imperial.ac.uk>2021-04-14 13:58:04 +0000
committeroverleaf <overleaf@localhost>2021-04-14 19:52:44 +0000
commit826f861788376d5867a3fe4bec0ab8d8d54545db (patch)
tree7e9f9b5eb5b34d51e5d709af868b11e122fb73d7 /main.tex
parentccc1cd93aa993302b55e6e073cdca9a16c2fa478 (diff)
downloadoopsla21_fvhls-826f861788376d5867a3fe4bec0ab8d8d54545db.tar.gz
oopsla21_fvhls-826f861788376d5867a3fe4bec0ab8d8d54545db.zip
Update on Overleaf.
Diffstat (limited to 'main.tex')
-rw-r--r--main.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/main.tex b/main.tex
index 04ce858..07c754a 100644
--- a/main.tex
+++ b/main.tex
@@ -140,7 +140,7 @@
\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 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-oriented intermediate language and a Verilog back end, and has been proven correct in Coq. \JW{Could maybe drop the following sentence from the abstract?}\YH{Hmm, I don't know actually, I feel like as we don't support all of the C features one might want to know what features are supported.} \JW{What would the list look like if you phrased it has the features that \emph{are} supported? (Following Ally's suggestion.)}\YH{``\vericert{} supports most C constructs, including all integer operations, function calls, local arrays, structs and unions and general control-flow statements.''} \vericert{} supports all C constructs except for case statements, function pointers, recursive function calls, integers larger than 32 bits, floats, and global variables. An evaluation on the PolyBench/C benchmark suite indicates that \vericert{} generates hardware that is around an order of magnitude slower but about the same size as hardware generated by an existing, optimising (but unverified) HLS tool.\YH{Technically this is right, but we might want to add the division values.} \JW{What would it look like if you add those?}\YH{``If divisions are replaced by an iterative algorithm, then \vericert{} is only $2\times$ slower.''}
+ 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-oriented intermediate language and a Verilog back end, and has been proven correct in Coq. \JW{Could maybe drop the following sentence from the abstract?}\YH{Hmm, I don't know actually, I feel like as we don't support all of the C features one might want to know what features are supported.} \JW{What would the list look like if you phrased it has the features that \emph{are} supported? (Following Ally's suggestion.)}\YH{``\vericert{} supports most C constructs, including all integer operations, function calls, local arrays, structs and unions and general control-flow statements.''} \JW{What do you think? I quite like the positive phrasing.} \vericert{} supports all C constructs except for case statements, function pointers, recursive function calls, integers larger than 32 bits, floats, and global variables. An evaluation on the PolyBench/C benchmark suite indicates that \vericert{} generates hardware that is around an order of magnitude slower but about the same size as hardware generated by an existing, optimising (but unverified) HLS tool.\YH{Technically this is right, but we might want to add the division values.} \JW{What would it look like if you add those?}\YH{``If divisions are replaced by an iterative algorithm, then \vericert{} is only $2\times$ slower.''} \JW{Mm. So you could say something like ``An evaluation on the PolyBench/C benchmark suite indicates that \vericert{} generates hardware that is around an order of magnitude slower (only around 2$\times$ slower in the absence of division) and about the same size as hardware generated by an existing, optimising (but unverified) HLS tool.''}
\end{abstract}
%% 2012 ACM Computing Classification System (CSS) concepts