summaryrefslogtreecommitdiffstats
path: root/conclusion.tex
diff options
context:
space:
mode:
authorYann Herklotz <ymh15@ic.ac.uk>2021-04-04 20:12:20 +0000
committeroverleaf <overleaf@localhost>2021-04-04 20:18:08 +0000
commit62a127dfb009b8ffe94ac348ecafb7f596406cbd (patch)
tree7dbee2f45b6baa1edc4054d32610ff2b1fad6b5b /conclusion.tex
parentadc0afcec6fe025f85fbfdfdfc5ef522fa760d98 (diff)
downloadfccm21_esrhls-62a127dfb009b8ffe94ac348ecafb7f596406cbd.tar.gz
fccm21_esrhls-62a127dfb009b8ffe94ac348ecafb7f596406cbd.zip
Update on Overleaf.
Diffstat (limited to 'conclusion.tex')
-rw-r--r--conclusion.tex10
1 files changed, 8 insertions, 2 deletions
diff --git a/conclusion.tex b/conclusion.tex
index d081b09..c5f1f6a 100644
--- a/conclusion.tex
+++ b/conclusion.tex
@@ -1,11 +1,17 @@
\section{Conclusion}
-We have shown how an existing fuzzing tool can be modified so that its output is suitable for HLS, and then used it in a campaign to test the reliability of three modern HLS tools. In total, we found at least \numuniquebugs{} unique bugs across all the tools, including both crashes and miscompilations.
-Further work could be done on supporting more HLS tools, especially ones that claim to prove that their output is correct before terminating, such as Catapult-C~\cite{mentor20_catap_high_level_synth}. % This could give an indication of how effective these proofs are, and how often they are actually able to complete their equivalence proofs during compilation in a feasible timescale.
+We have shown how an existing fuzzing tool can be modified so that its output is suitable for HLS, and then used it in a campaign to test the reliability of four modern HLS tools. In total, we found at least \numuniquebugs{} unique bugs across all the tools, including both crashes and miscompilations.
+Further work could be done on supporting more HLS tools, especially those that claim to prove that their output is correct before terminating, such as Catapult-C~\cite{mentor20_catap_high_level_synth}. % This could give an indication of how effective these proofs are, and how often they are actually able to complete their equivalence proofs during compilation in a feasible timescale.
Conventional compilers have become quite resilient to fuzzing over the last decade, so recent work on fuzzing compilers has had to employ increasingly imaginative techniques to keep finding new bugs~\cite{karine+20}. In contrast, we have found that HLS tools -- at least, as they currently stand -- can be made to exhibit bugs even using the relatively basic fuzzing techniques that we employed in this project.
As HLS is becoming increasingly relied upon, it is important to make sure that HLS tools are also reliable. We hope that this work further motivates the need for rigorous engineering of HLS tools, whether that is by validating that each output the tool produces is correct or by proving the HLS tool itself correct once and for all.
+\section*{Acknowledgements}
+
+We thank Alastair F. Donaldson for helpful feedback.
+We acknowledge financial support from the Research Institute on Verified Trustworthy Software Systems (VeTSS), which is funded by the UK National Cyber Security Centre (NCSC).
+
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"