From 12cf73bfe39d00fea73b17b831e09d419df0e121 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
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 

