diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-04-13 17:08:31 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-04-13 17:08:45 +0100 |
| commit | 12cf73bfe39d00fea73b17b831e09d419df0e121 (patch) | |
| tree | c6b263879550f89d8e21da99fd8cbec66b3c4e94 /conclusion.tex | |
| parent | b6e4d6c2a90d89d3ab56110e3f621fd92408eae7 (diff) | |
| download | oopsla21_fvhls-12cf73bfe39d00fea73b17b831e09d419df0e121.tar.gz oopsla21_fvhls-12cf73bfe39d00fea73b17b831e09d419df0e121.zip | |
More changes
Diffstat (limited to 'conclusion.tex')
| -rw-r--r-- | conclusion.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/conclusion.tex b/conclusion.tex index 755dedc..9a4bcfa 100644 --- a/conclusion.tex +++ b/conclusion.tex @@ -5,7 +5,7 @@ We have presented \vericert{}, the first mechanically verified HLS tool for tran %In this article, we present \vericert{}, the first fully mechanised proof of correctness for HLS in Coq, translating C into Verilog. We built \vericert{} by extending \compcert{} with a new hardware-specific intermediate language and a Verilog back end, and we verified it with respect to a semantics for Verilog due to \citet{loow19_proof_trans_veril_devel_hol}. %The behaviour of any C program compiled via \vericert{} is guaranteed to be translated correctly to Verilog. -We evaluated \vericert{} against the existing \legup{} HLS tool on the Polybench/C benchmark suite. +We evaluated \vericert{} against the existing \legup{} HLS tool on the \polybench{} benchmark suite. %Our Polybench hardware is guaranteed to preserve the C behaviour, whilst \legup{} cannot provide any such guarantee about its generated hardware. Currently, our hardware is \slowdownOrig$\times$ slower and \areaIncr$\times$ larger compared to \legup{}, though it is only \slowdownDiv$\times$ slower if inefficient divisions are removed. |