summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-09-06 13:52:07 +0200
committerYann Herklotz <git@yannherklotz.com>2021-09-06 13:52:07 +0200
commite88842877a7083ad0e2db2b0fa10c99c8035683b (patch)
tree5308e4d3c9bdbb6e1876ad2e048b8ffd36389afe
parent5fdbf56a8b427dd592cf0d68633bd910f39cd792 (diff)
downloadoopsla21_fvhls-e88842877a7083ad0e2db2b0fa10c99c8035683b.tar.gz
oopsla21_fvhls-e88842877a7083ad0e2db2b0fa10c99c8035683b.zip
Move and add to the acknowledgements
-rw-r--r--conclusion.tex5
-rw-r--r--main.tex6
2 files changed, 6 insertions, 5 deletions
diff --git a/conclusion.tex b/conclusion.tex
index a967e59..21c4831 100644
--- a/conclusion.tex
+++ b/conclusion.tex
@@ -21,11 +21,6 @@ Other optimisations include resource sharing to reduce the circuit area, and usi
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:
%%% mode: latex
%%% TeX-master: "main"
diff --git a/main.tex b/main.tex
index 8b81f03..0bca3ca 100644
--- a/main.tex
+++ b/main.tex
@@ -182,6 +182,12 @@
\input{limitations}
\input{conclusion}
+\subsection*{Acknowledgements}
+We'd like to thank Sandrine Blazy, Jianyi Cheng, Alastair Donaldson, Andreas Lööw, and the anonymous
+reviewers for their helpful feedback. 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).
+
%% Bibliography
\bibliography{references.bib}