From bb505be23ef07e2b3e47e268513a6f4f1b33f66b Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 12 Aug 2021 11:28:30 +0200
Subject: Fix many of the comments

---
 evaluation.tex | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'evaluation.tex')

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"
-- 
cgit 

