From 12cf73bfe39d00fea73b17b831e09d419df0e121 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 13 Apr 2021 17:08:31 +0100 Subject: More changes --- conclusion.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'conclusion.tex') 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. -- cgit