Update on Overleaf.

1 files changed, 16 insertions, 4 deletions

diff --git a/conclusion.tex b/conclusion.tex
index a53c268..755dedc 100644
--- a/conclusion.tex
+++ b/conclusion.tex
@@ -1,11 +1,23 @@
 \section{Conclusion}
+\label{sec:conclusion}
 
-\vericert{} is the first fully mechanised proof of correctness for HLS in Coq, translating C into Verilog.  
+We have presented \vericert{}, the first mechanically verified HLS tool for translating software in C into hardware in Verilog.
+%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.
+%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.
 
-However, to make the tool more usable there are many more optimisations that could be implemented to get the performance closer to \legup{}.  The main optimisation that should be performed is scheduling operations into the same clock cycle, so that these can run in parallel.  In addition to that, another issue that \vericert{} faces is that \compcert{}'s 3AC uses many different registers, even if these are not used anymore later on.  It would therefore be useful to have a register allocation algorithm that could ensure that registers could be reused appropriately, where the register allocation algorithm would find the minimum number of registers needed.  Finally, another optimisation would be to support resource sharing to reduce the area that the final design uses, this could include multi-cycle operations and pipelining optimisations so that division and multiplication operators also become more efficient.
-
-Finally, it's worth considering how trustworthy \vericert{} is compared to other HLS tools.  A formally verified tool does not guarantee an output for every input and it is therefore allowed to fail.  However, the subset of C that will compile is well-described and the tool should therefore not fail in surprising ways.  However, the guarantee that the output behaves the same as the input is strong, as it uses well-known C and existing Verilog semantics to prove the equivalence.
+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$. 
+%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.
+%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.
 
+Finally, it's worth considering how trustworthy \vericert{} is compared to other HLS tools. The guarantee of full functional equivalence between input and output that $\vericert$ provides is a strong one, the semantics for the source and target languages are both well-established, and Coq is a mature and thoroughly tested system. However, \vericert{} cannot guarantee to provide an output for every valid input -- for instance, as remarked in Section~\ref{sec:proof:htl_verilog}, \vericert{} will error out if given a program with more than about four million instructions! -- but our evaluation indicates that it does not seem to error out too frequently. And of course, \vericert{} cannot guarantee that the final hardware produced will be correct, because the Verilog it generates must pass through a series of unverified tools along the way. This concern may be allayed in the future by ongoing work we are aware of to produce a verified hardware synthesis tool.
 
 
 %%% Local Variables: