summaryrefslogtreecommitdiffstats
path: root/conclusion.tex
diff options
context:
space:
mode:
Diffstat (limited to 'conclusion.tex')
-rw-r--r--conclusion.tex4
1 files changed, 3 insertions, 1 deletions
diff --git a/conclusion.tex b/conclusion.tex
index d45485e..cf83a6d 100644
--- a/conclusion.tex
+++ b/conclusion.tex
@@ -12,7 +12,9 @@ Currently, our hardware is \slowdownOrig$\times$ slower and \areaIncr$\times$ la
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.
+Beyond this, we plan to implement scheduling and loop pipelining, since this allows more operations to be packed into fewer clock cycles.
+% JW: I chopped the following because we mentioned Six et al already.
+%recent work by \citet{six+20} indicates how these scheduling algorithms can be implemented in \compcert.
%Another possibility is re-using registers, since \compcert{}'s 3AC does not include register allocation.
Other optimisations include resource sharing to reduce the circuit area, and using tailored hardware operators that use hard IP blocks on chip and can be pipelined.
% this could include multi-cycle operations and pipelining optimisations so that division and multiplication operators also become more efficient.