From bb505be23ef07e2b3e47e268513a6f4f1b33f66b Mon Sep 17 00:00:00 2001 From: Yann Herklotz 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