Update on Overleaf.

1 files changed, 5 insertions, 0 deletions

diff --git a/evaluation.tex b/evaluation.tex
index 5dcd49c..1d800e4 100644
--- a/evaluation.tex
+++ b/evaluation.tex
@@ -5,6 +5,7 @@ Our evaluation is designed to answer the following two 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?
 \end{description}
 
 \subsection{Experimental Setup}
@@ -163,6 +164,10 @@ Looking at a few benchmarks in particular in Figure~\ref{fig:polybench-nodiv} fo
 The bottom graphs in both Figure~\ref{fig:polybench-div} and Figure~\ref{fig:polybench-nodiv} compare the resource utilisation of the \polybench{} programs generated by \vericert{} and \legup{} at various optimisation levels.
 By looking at the median, when division/modulo operations are enabled, we see that \vericert{} produces hardware that is about the same size as optimised \legup{}, whereas the unoptimised versions of \legup{} actually produce slightly smaller hardware.  This is because optimisations can often increase the size of the hardware to make it faster.  Especially in Figure~\ref{fig:polybench-div}, there are a few benchmarks where the size of the \legup{} design is much smaller than that produced by \vericert{}.  This can mostly be explained because of resource sharing in LegUp.  Division/modulo operations need large circuits, and it is therefore usual to only have one circuit per design.  As \vericert{} uses the na\"ive implementation of division/modulo, there will be multiple circuits present in the design, which blows up the size.  Looking at Figure~\ref{fig:polybench-nodiv}, one can see that without division, the size of \vericert{} designs are almost always around the same size as \legup{} designs, never being more than 2$\times$ larger, and sometimes even being smaller.  The similarity in area also shows that RAM is correctly being inferred by the synthesis tool, and is therefore not implemented as registers.
 
+\subsection{RQ3: How quickly does \vericert{} translate the C into Verilog?}
+
+\vericert{} takes around 0.1$\times$ as long as \legup{} 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.
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "main"