From ea7be8d5217ee7d028f1cd4e2a8e2948fd248db7 Mon Sep 17 00:00:00 2001 From: John Wickerson Date: Wed, 1 Sep 2021 14:42:17 +0000 Subject: Update on Overleaf. --- conclusion.tex | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'conclusion.tex') diff --git a/conclusion.tex b/conclusion.tex index b7daf71..a967e59 100644 --- a/conclusion.tex +++ b/conclusion.tex @@ -16,10 +16,14 @@ Beyond this, we plan to implement scheduling and loop pipelining, since this all % 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. +Other optimisations include resource sharing to reduce the circuit area, and using tailored hardware operators that exploit the hard IP blocks of the 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. That concern may be allayed in the future thanks to recent work by~\citet{10.1145/3437992.3439916} to produce a verified logic synthesis tool. +Finally, it's worth considering how trustworthy \vericert{} is compared to other HLS tools. The guarantee of full functional equivalence between input and output has been both proven and fuzz-tested; the semantics for the source and target languages are both well established; and Coq is a mature and thoroughly tested system. Nonetheless, \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. That concern may be allayed in the future thanks to recent work by~\citet{10.1145/3437992.3439916} to produce a verified logic synthesis tool. + +\subsection*{Acknowledgements} +We'd like to thank Sandrine Blazy, Jianyi Cheng, Alastair Donaldson, and the anonymous reviewers for their helpful feedback. \JW{Might need adding to.} +This work was financially supported by the EPSRC via the Research Institute for Verified Trustworthy Software Systems (VeTSS) and the IRIS Programme Grant (EP/R006865/1). %%% Local Variables: -- cgit