Some more slight changes

4 files changed, 49 insertions, 36 deletions

diff --git a/evaluation.tex b/evaluation.tex
index 0077246..76460c5 100644
--- a/evaluation.tex
+++ b/evaluation.tex
@@ -205,7 +205,7 @@ By looking at the median, when division/modulo operations are enabled, we see th
 {\it ``Beware of bugs in the above code; I have only proved it correct, not tried it.''} \par\hfill -- D. E. Knuth (1977)
 \end{quotation}
 
-To gain further confidence that the Verilog designs generated by \vericert{} are actually correct, and that the correctness theorem is indeed effective, we fuzzed \vericert{} using Csmith~\cite{yang11_findin_under_bugs_c_compil}. \citeauthor{yang11_findin_under_bugs_c_compil} previously used Csmith in an extensive fuzzing campaign on CompCert and found a handful of bugs in the unverified parts of that compiler, so it is natural to explore whether it can find bugs in \vericert{} too. \citet{du21_fuzzin_high_level_synth_tools} have recently used Csmith to fuzz other HLS tools including \legup{}, so we configured Csmith in a similar way. In addition to the features turned off by \citeauthor{du21_fuzzin_high_level_synth_tools}, we turned off the generation of global variables and non-32-bit operations. The generated designs were tested by simulating them and comparing the output value to the results of compiling the test-cases with GCC 10.3.0.
+To gain further confidence that the Verilog designs generated by \vericert{} are actually correct, and that the correctness theorem is indeed effective, we fuzzed \vericert{} using Csmith~\cite{yang11_findin_under_bugs_c_compil}. \citeauthor{yang11_findin_under_bugs_c_compil} previously used Csmith in an extensive fuzzing campaign on CompCert and found a handful of bugs in the unverified parts of that compiler, so it is natural to explore whether it can find bugs in \vericert{} too. \citet{herklotz21_empir_study_reliab_high_level_synth_tools} have recently used Csmith to fuzz other HLS tools including \legup{}, so we configured Csmith in a similar way. In addition to the features turned off by \citeauthor{du21_fuzzin_high_level_synth_tools}, we turned off the generation of global variables and non-32-bit operations. The generated designs were tested by simulating them and comparing the output value to the results of compiling the test-cases with GCC 10.3.0.
 
 The results of the fuzzing run are shown in Figure~\ref{tab:fuzzing}.  Out of 155267 test-cases generated by Csmith, 26\% of them passed, meaning they compiled without error and resulted in the same final value as GCC. Most of the test-cases, 73.97\%, failed at compile time.  The most common reasons for this were unsigned comparisons between integers (\vericert{} requires them to be signed), and the presence of 8-bit operations (which \vericert{} does not support, and which we could not turn off due to a limitation in Csmith). % The latter programs are present because of a slight limitation with how Csmith can be configured, as it does not allow 8-bit operations to be turned off completely, and will get stuck when it generates the C code.  
 Because the test-cases generated by Csmith could not be tailored exactly to the C fragment that \vericert{} supports, such a high compile-time failure rate is not unexpected. Finally, and most interestingly, there were a total of 39 run-time failures, which the correctness theorem should be proving impossible.  However, all 39 of these failures are due to a bug in the pretty-printing of the final Verilog code, where a logical negation (\texttt{!}) was accidentally used instead of a bitwise negation (\verb|~|).  Once this bug was fixed, all test-cases passed.
diff --git a/introduction.tex b/introduction.tex
index 104cf7f..abf6271 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -21,7 +21,7 @@ Indeed, there are reasons to doubt that HLS tools actually \emph{do} always pres
 %Other reasons are more specific: 
 For instance, Vivado HLS has been shown to apply pipelining optimisations incorrectly\footnote{\url{https://bit.ly/vivado-hls-pipeline-bug}} or to silently generate wrong code should the programmer stray outside the fragment of C that it supports.\footnote{\url{https://bit.ly/vivado-hls-pointer-bug}} 
 Meanwhile, \citet{lidbury15_many_core_compil_fuzzin} had to abandon their attempt to fuzz-test Altera's (now Intel's) OpenCL compiler since it ``either crashed or emitted an internal compiler error'' on so many of their test inputs.  
-More recently, \citet{du21_fuzzin_high_level_synth_tools} fuzz-tested three commercial HLS tools using Csmith~\cite{yang11_findin_under_bugs_c_compil}, and despite restricting the generated programs to the C fragment explicitly supported by all the tools, they still found that on average 2.5\% of test cases were compiled to designs that behaved incorrectly. %\NR{The word `input' here made me think of I/Os. `input software' or just `software' is better. I think it is worth being consistent across the article on the word used to describe the software description provided to the HLS tool. Actually, we can even signpost it like: `From here on we used the word bla to refer to the input software that is provided to a HLS tool.'} %JW: thanks, done.
+More recently, \citet{herklotz21_empir_study_reliab_high_level_synth_tools} fuzz-tested three commercial HLS tools using Csmith~\cite{yang11_findin_under_bugs_c_compil}, and despite restricting the generated programs to the C fragment explicitly supported by all the tools, they still found that on average 2.5\% of test cases were compiled to designs that behaved incorrectly. %\NR{The word `input' here made me think of I/Os. `input software' or just `software' is better. I think it is worth being consistent across the article on the word used to describe the software description provided to the HLS tool. Actually, we can even signpost it like: `From here on we used the word bla to refer to the input software that is provided to a HLS tool.'} %JW: thanks, done.
 
 \paragraph{Existing workarounds}
 
@@ -51,7 +51,7 @@ The contributions of this paper are as follows:
   \item In Section~\ref{sec:evaluation}, we evaluate \vericert{} on the \polybench{} benchmark suite~\cite{polybench}, and compare the performance of our generated hardware against an existing, unverified HLS tool called \legup{}~\cite{canis11_legup}. We show that \vericert{} generates hardware that is \slowdownOrig$\times$ slower (\slowdownDiv$\times$ slower in the absence of division) and \areaIncr$\times$ larger than that generated by \legup{}. This performance gap can be largely attributed to \vericert{}'s current lack of support for instruction-level parallelism and the absence of an efficient, pipelined division operator. We intend to close this gap in the future by introducing (and verifying) HLS optimisations of our own, such as scheduling and memory analysis.  This section also reports on our campaign to fuzz-test \vericert{} using over a hundred thousand random C programs generated by Csmith~\cite{yang11_findin_under_bugs_c_compil} in order to confirm that its correctness theorem is watertight. %\NR{Question rather than comment: Will there be verification issues to add support for hard IPs like division blocks?}\YH{Not really any issues, just many different levels of reliability.  You don't have to prove IP correct, but theoretically could.}
 \end{itemize}
 %\JW{This sentence seems pretty good to me; is it up-to-date with the latest `challenges' you've faced?}
-\vericert{} is fully open source and available online.
+\vericert{} is fully open source and available online~\cite{yann_herklotz_2021_5093839}.
 
 \begin{center}
 \ifANONYMOUS
diff --git a/main.tex b/main.tex
index 187761e..110d901 100644
--- a/main.tex
+++ b/main.tex
@@ -180,16 +180,21 @@
        <concept_significance>300</concept_significance>
        </concept>
    <concept>
-       <concept_id>10002978.10002986.10002990</concept_id>
-       <concept_desc>Security and privacy~Logic and verification</concept_desc>
+       <concept_id>10011007.10011074.10011099.10011692</concept_id>
+       <concept_desc>Software and its engineering~Formal software verification</concept_desc>
        <concept_significance>500</concept_significance>
        </concept>
- </ccs2012>
+   <concept>
+       <concept_id>10003752.10010124.10010138.10010142</concept_id>
+       <concept_desc>Theory of computation~Program verification</concept_desc>
+       <concept_significance>500</concept_significance>
+       </concept>
+</ccs2012>
 \end{CCSXML}
 
 \ccsdesc[500]{Hardware~High-level and register-transfer level synthesis}
-\ccsdesc[300]{Hardware~Functional verification}
-\ccsdesc[500]{Security and privacy~Logic and verification}
+\ccsdesc[500]{Software and its engineering~Formal software verification}
+\ccsdesc[500]{Theory of computation~Program verification}
 
 
 %% Keywords
diff --git a/references.bib b/references.bib
index 0065756..b183298 100644
--- a/references.bib
+++ b/references.bib
@@ -123,13 +123,14 @@ year = {2020},
   year      = {2018},
   doi       = {https://doi.org/10.1145/3192366.3192379}
 }
-  
-@article{greaves_note,
-  author    = {David J. Greaves},
-  title     = {Research Note: An Open Source Bluespec Compiler},
-  journal   = {CoRR},
-  volume    = {abs/1905.03746},
-  year      = {2019}
+
+@misc{greaves_note,
+      title={Research Note: An Open Source Bluespec Compiler},
+      author={David J. Greaves},
+      year={2019},
+      eprint={1905.03746},
+      archivePrefix={arXiv},
+      primaryClass={cs.PL}
 }
 
 @article{takach16_high_level_synth,
@@ -579,11 +580,9 @@ year = {2020},
 
 @misc{silexicahlshdl,
 author = {Gauthier, Stephane and Wadood, Zubair},
-title = {High-Level Synthesis:
-Can it outperform
-hand-coded HDL?},
+title = {High-Level Synthesis: Can it outperform hand-coded {HDL}?},
 note = {White paper},
-url = {https://bit.ly/2IDhKBR},
+url = {https://info.silexica.com/high-level-synthesis/1},
 year = {2020},
 }
 
@@ -835,14 +834,7 @@ year = {2020},
   doi={https://doi.org/10.1109/CODES-ISSS.2013.6659002}
 }
 
-@inproceedings{poly_hls_zhao2017,
-  title={COMBA: A comprehensive model-based analysis framework for high level synthesis of real applications},
-  author={Zhao, Jieru and Feng, Liang and Sinha, Sharad and Zhang, Wei and Liang, Yun and He, Bingsheng},
-  booktitle={2017 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)},
-  pages={430--437},
-  year={2017},
-  organization={IEEE}
-}
+@INPROCEEDINGS{poly_hls_zhao2017,  author={Zhao, Jieru and Feng, Liang and Sinha, Sharad and Zhang, Wei and Liang, Yun and He, Bingsheng},  booktitle={2017 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)},   title={COMBA: A comprehensive model-based analysis framework for high level synthesis of real applications},   year={2017},  volume={},  number={},  pages={430-437},  doi={10.1109/ICCAD.2017.8203809}}
 
 @inproceedings{poly_hls_pouchet2013polyhedral,
   title={Polyhedral-based data reuse optimization for configurable computing},
@@ -869,15 +861,6 @@ year = {2020},
   year = 2019,
 }
 
-@inproceedings{du21_fuzzin_high_level_synth_tools,
-  author          = {Herklotz, Yann and Du, Zewei and Ramanathan, Nadesh and Wickerson, John},
-  note            = {(to appear)},
-  year            = 2021,
-  url             = {https://yannherklotz.com/docs/drafts/fuzzing_hls.pdf},
-  title           = {An Empirical Study of the Reliability of High-Level Synthesis Tools},
-  booktitle       = {29th IEEE International Symposium on Field-Programmable Custom Computing Machines},
-}
-
 @inproceedings{chisel,
   title={{Chisel: Constructing hardware in a Scala embedded language}},
   author={Bachrach, Jonathan and Vo, Huy and Richards, Brian and Lee, Yunsup and Waterman, Andrew and Avi{\v{z}}ienis, Rimas and Wawrzynek, John and Asanovi{\'c}, Krste},
@@ -1015,3 +998,28 @@ series = {CPP 2021}
 	pages = {1-6},
 	doi = {10.1109/RECONFIG.2017.8279807}
 }
+
+@software{yann_herklotz_2021_5093839,
+  author       = {Yann Herklotz and
+                  James D. Pollard and
+                  Nadesh Ramanathan and
+                  John Wickerson},
+  title        = {ymherklotz/vericert: Vericert v1.2.1},
+  month        = jul,
+  year         = 2021,
+  publisher    = {Zenodo},
+  version      = {v1.2.1},
+  doi          = {10.5281/zenodo.5093839},
+  url          = {https://doi.org/10.5281/zenodo.5093839}
+}
+
+@INPROCEEDINGS{herklotz21_empir_study_reliab_high_level_synth_tools,
+	author = {Herklotz, Yann and Du, Zewei and Ramanathan, Nadesh and Wickerson, John},
+	booktitle = {2021 IEEE 29th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM)},
+	title = {An Empirical Study of the Reliability of High-Level Synthesis Tools},
+	year = {2021},
+	volume = {},
+	number = {},
+	pages = {219-223},
+	doi = {10.1109/FCCM51124.2021.00034}
+}