diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-09-08 19:24:11 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-09-08 19:24:11 +0100 |
| commit | 7bbb64542b8897ae82f83b947a05d772579d06a3 (patch) | |
| tree | 8109eab2eff8c462df026836e63877ed47474c63 | |
| parent | a68d9b19756801fb1633edd17aec2ac9c22d8444 (diff) | |
| download | oopsla21_fvhls-7bbb64542b8897ae82f83b947a05d772579d06a3.tar.gz oopsla21_fvhls-7bbb64542b8897ae82f83b947a05d772579d06a3.zip | |
Add the correct concepts
| -rw-r--r-- | main.tex | 40 |
1 files changed, 22 insertions, 18 deletions
@@ -1,5 +1,6 @@ -%% For double-blind review submission, w/o CCS and ACM Reference (max submission space) -\documentclass[acmsmall,10pt,review,pagebackref=true]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false} +\documentclass[acmsmall,screen]{acmart} + +\settopmatter{} %\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} @@ -166,26 +167,29 @@ 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. \vericert{} supports most C constructs, including all integer operations, function calls, local arrays, structs, unions, and general control-flow statements. An evaluation on the \polybench{} 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 -%% 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> + <concept> + <concept_id>10010583.10010682.10010684</concept_id> + <concept_desc>Hardware~High-level and register-transfer level synthesis</concept_desc> + <concept_significance>500</concept_significance> + </concept> + <concept> + <concept_id>10010583.10010717.10010721</concept_id> + <concept_desc>Hardware~Functional verification</concept_desc> + <concept_significance>300</concept_significance> + </concept> + <concept> + <concept_id>10002978.10002986.10002990</concept_id> + <concept_desc>Security and privacy~Logic and verification</concept_desc> + <concept_significance>500</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 +\ccsdesc[500]{Hardware~High-level and register-transfer level synthesis} +\ccsdesc[300]{Hardware~Functional verification} +\ccsdesc[500]{Security and privacy~Logic and verification} %% Keywords |