Fix many of the comments

1 files changed, 10 insertions, 4 deletions

diff --git a/evaluation.tex b/evaluation.tex
index e1719e3..0f18db9 100644
--- a/evaluation.tex
+++ b/evaluation.tex
@@ -1,10 +1,11 @@
 \section{Evaluation}\label{sec:evaluation}
 
-Our evaluation is designed to answer the following three research questions.
+Our evaluation is designed to answer the following four research questions.
 \begin{description}
-\item[RQ1] How fast is the hardware generated by \vericert{}?
-\item[RQ2] How area-efficient is the hardware generated by \vericert{}?
-\item[RQ3] How quickly does \vericert{} translate the C into Verilog?
+  \item[RQ1] How fast is the hardware generated by \vericert{}?
+  \item[RQ2] How area-efficient is the hardware generated by \vericert{}?
+  \item[RQ3] How quickly does \vericert{} translate the C into Verilog?
+  \item[RQ4] How effective is the correctness theorem in \vericert{}?
 \end{description}
 
 \subsection{Experimental Setup}
@@ -174,6 +175,11 @@ By looking at the median, when division/modulo operations are enabled, we see th
 
 \legup{} takes around 10$\times$ as long as \vericert{} to perform the translation from C into Verilog, showing at least that verification does not have a substantial effect on the run-time of the HLS tool.  However, this is a meaningless victory, as a lot of the extra time that \legup{} uses is on performing computationally heavy optimisations such as loop pipelining and scheduling.
 
+\subsection{RQ4: How effective is the correctness theorem in \vericert{}?}
+
+
+To check that the Verilog designs generated by \vericert{} are actually correct, and that the correctness theorem is indeed effective, \vericert{} was fuzzed using Csmith~\cite{yang11_findin_under_bugs_c_compil}, with a similar configuration used by \citet{du21_fuzzin_high_level_synth_tools} when other HLS tools were fuzzed, including \legup{}.
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "main"