Fix more capitalisation

1 files changed, 4 insertions, 4 deletions

diff --git a/evaluation.tex b/evaluation.tex
index 76460c5..f5deff8 100644
--- a/evaluation.tex
+++ b/evaluation.tex
@@ -29,7 +29,7 @@ We configured \polybench{}'s parameters so that only integer types are used.  We
 
 \paragraph{Synthesis setup} The Verilog that is generated by \vericert{} or \legup{} is provided to Xilinx Vivado v2017.1~\cite{xilinx_vivad_desig_suite}, which synthesises it to a netlist, before placing-and-routing this netlist onto a Xilinx XC7Z020 FPGA device that contains approximately 85000 LUTs.
 
-\subsection{RQ1: How fast is \vericert{}-generated hardware?}
+\subsection{RQ1: How Fast is \vericert{}-Generated Hardware?}
 
 \pgfplotstableread[col sep=comma]{results/rel-time-div.csv}{\divtimingtable}
 \pgfplotstableread[col sep=comma]{results/rel-size-div.csv}{\divslicetable}
@@ -166,16 +166,16 @@ Secondly, looking at the maximum clock frequency that each design can achieve, \
 
 Looking at a few benchmarks in particular in Figure~\ref{fig:polybench-nodiv} for some interesting cases.  For the \texttt{trmm} benchmark, \vericert{} produces hardware that executes with the same cycle count as \legup{}, and manages to create hardware that achieves twice the frequency compared to \legup{}, thereby actually producing a design that executes twice as fast as \legup{}.  Another interesting benchmark is \texttt{doitgen}, where \vericert{} is comparable to \legup{} without LLVM optimisations, however, LLVM optimisations seem to have a large effect on the cycle count.
 
-\subsection{RQ2: How area-efficient is \vericert{}-generated hardware?}
+\subsection{RQ2: How Area-Efficient is \vericert{}-Generated Hardware?}
 
 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?}
+\subsection{RQ3: How Quickly does \vericert{} Translate the C into Verilog?}
 
 \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{}?}
+\subsection{RQ4: How Effective is the Correctness Theorem in \vericert{}?}
 
 \definecolor{fuzzred}{HTML}{f8514f}
 \definecolor{fuzzyellow}{HTML}{fee4bf}