From 2db9260b7ed82e4e097185a3334ae1f4c14a365d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 17 Apr 2021 12:12:47 +0100 Subject: Add --- conclusion.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/conclusion.tex b/conclusion.tex index 5029bae..23476da 100644 --- a/conclusion.tex +++ b/conclusion.tex @@ -9,7 +9,7 @@ We evaluated \vericert{} against the existing \legup{} HLS tool on the \polybenc %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. -There are abundant opportunities for improving \vericert{}'s performance. For instance, as discussed in Section~\ref{sec:evaluation}, simply replacing the na\"ive single-cycle division and modulo operations with C implementations increases clock frequency by $5.6\times$. +There are abundant opportunities for improving \vericert{}'s performance. For instance, as discussed in Section~\ref{sec:evaluation}, simply replacing the na\"ive single-cycle division and modulo operations with C implementations increases clock frequency by $8.2\times$. %Going forward, we envision introducing HLS-specific optimisations that are intended to improve the hardware quality of \vericert{}, whilst maintaining correctness. % However, to make the tool more usable there are many more optimisations that could be implemented to get the performance closer to \legup{}. Beyond this, we plan to implement scheduling and loop pipelining, since this allows more operations to be packed into fewer clock cycles; recent work by \citet{six+20} indicates how these scheduling algorithms can be implemented in \compcert. -- cgit