Add text for evaluation

1 files changed, 11 insertions, 1 deletions

diff --git a/evaluation.tex b/evaluation.tex
index 0f18db9..7afe23f 100644
--- a/evaluation.tex
+++ b/evaluation.tex
@@ -177,8 +177,18 @@ By looking at the median, when division/modulo operations are enabled, we see th
 
 \subsection{RQ4: How effective is the correctness theorem in \vericert{}?}
 
+\begin{figure}
+  \centering
+  \begin{tabular}{cccc}\toprule
+    \textbf{Passing} & \textbf{Compile time errors} & \textbf{Runtime errors} & \textbf{Total}\\\midrule
+    40379 (26.00\%) & 114849 (73.97\%) & 39 (0.03\%) & 155267\\\bottomrule
+  \end{tabular}
+  \caption{Results of fuzzing \vericert{} using random C files generated by Csmith.}\label{tab:fuzzing}
+\end{figure}
+
+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{}.  The main features that were turned off in addition to the ones turned off by \citet{du21_fuzzin_high_level_synth_tools} were generation of global variables, as well as generation of operations other than 32-bits. 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 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{}.
+The results of the fuzzing run are shown in Table~\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.  Then, because of some small limitations in the programs accepted by \vericert{}, most of the test-cases, 73.97\%, failed at compile time.  The most common reasons for this were unsigned comparisons between integers, which needed to be signed for \vericert{} instead, and no support for 8-bit operations.  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 C code could not be tailored exactly to the supported subset of inputs \vericert{} accepts, such a high compile time failure rate is expected.  Finally, and more interestingly, there were a total of 39 runtime failures, which the correctness theorem should be proving could not be possible.  However, these 39 failures are all because of a bug in the pretty printing of the final Verilog code, where a single bit not operation (\texttt{!}) was used instead of the proper 32-bit not operation modelled in the semantics (\verb|~|).  Once this bug was fixed, all test-cases passed.
 
 %%% Local Variables:
 %%% mode: latex