diff options
| -rw-r--r-- | algorithm.tex | 10 | ||||
| -rw-r--r-- | evaluation.tex | 65 | ||||
| -rw-r--r-- | proof.tex | 4 | ||||
| -rw-r--r-- | verilog.tex | 2 |
4 files changed, 41 insertions, 40 deletions
diff --git a/algorithm.tex b/algorithm.tex index fbf8df1..6ab06c4 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -72,7 +72,7 @@ It has an unlimited number of pseudo-registers, and is represented as a control \begin{figure} \centering - \begin{subfigure}[b]{0.49\linewidth} + \begin{subfigure}[b]{0.24\linewidth} \begin{minted}{c} int main() { int x[3] = {1, 2, 3}; @@ -85,8 +85,8 @@ int main() { } \end{minted} \caption{Input C code.}\label{fig:accumulator_c} - \end{subfigure}\hspace*{-4mm} - \begin{subfigure}[b]{0.49\linewidth} + \end{subfigure} + \begin{subfigure}[b]{0.24\linewidth} \begin{minted}[fontsize=\footnotesize]{c} main() { 15: x8 = 1 @@ -107,8 +107,8 @@ main() { } \end{minted} \caption{3AC produced by \compcert{}.}\label{fig:accumulator_rtl} - \end{subfigure}\hfill% -\begin{subfigure}[b]{1\linewidth} + \end{subfigure} +\begin{subfigure}[b]{0.48\linewidth} \vspace{1em} \begin{minted}[fontsize=\tiny]{verilog} module main(reset, clk, finish, return_val); diff --git a/evaluation.tex b/evaluation.tex index 59fc7f9..1e02c84 100644 --- a/evaluation.tex +++ b/evaluation.tex @@ -25,14 +25,15 @@ We configured Polybench's parameters so that only integer types are used, since \subsection{RQ1: How fast is \vericert{}-generated hardware?} -\begin{figure} +\begin{figure}\centering +\begin{subfigure}[t]{0.48\textwidth} \definecolor{cyclecountcol}{HTML}{1b9e77} \begin{tikzpicture} \begin{axis}[ xmode=log, ymode=log, - height=80mm, - width=80mm, + height=1\textwidth, + width=1\textwidth, xlabel={\legup{} cycle count}, ylabel={\vericert{} cycle count}, xmin=1000, @@ -53,17 +54,16 @@ We configured Polybench's parameters so that only integer types are used, since \end{tikzpicture} \caption{A comparison of the cycle count of hardware designs generated by \vericert{} and by \legup{}.} \label{fig:comparison_cycles} -\end{figure} - -\begin{figure} +\end{subfigure}\hfill% +\begin{subfigure}[t]{0.48\textwidth} \definecolor{polycol}{HTML}{e6ab02} \definecolor{polywocol}{HTML}{7570b3} \begin{tikzpicture} \begin{axis}[ xmode=log, ymode=log, - height=80mm, - width=80mm, + height=1\textwidth, + width=1\textwidth, xlabel={\legup{} execution time (ms)}, ylabel={\vericert{} execution time (ms)}, xmin=10, @@ -73,8 +73,7 @@ We configured Polybench's parameters so that only integer types are used, since legend pos=south east, %log ticks with fixed point, ] - - + \addplot[draw=none, mark=*, draw opacity=0, fill opacity=0.8, polycol] table [x expr={\thisrow{legupcycles}/\thisrow{legupfreqMHz}}, y expr={\thisrow{vericertcycles}/\thisrow{vericertoldfreqMHz}}, col sep=comma] {results/poly.csv}; @@ -94,6 +93,7 @@ We configured Polybench's parameters so that only integer types are used, since \end{tikzpicture} \caption{A comparison of the execution time of hardware designs generated by \vericert{} and by \legup{}.} \label{fig:comparison_time} +\end{subfigure} \end{figure} %Firstly, before comparing any performance metrics, it is worth highlighting that any Verilog produced by \vericert{} is guaranteed to be \emph{correct}, whilst no such guarantee can be provided by \legup{}. @@ -115,11 +115,12 @@ Cycle count is one factor in calculating execution times; the other is the clock \subsection{RQ2: How area-efficient is \vericert{}-generated hardware?} \begin{figure} +\begin{subfigure}[t]{0.48\textwidth} \definecolor{resourceutilcol}{HTML}{e7298a} \begin{tikzpicture} \begin{axis}[ - height=80mm, - width=80mm, + height=1\textwidth, + width=1\textwidth, xlabel={\legup{} resource utilisation (\%)}, ylabel={\vericert{} resource utilisation (\%)}, xmin=0, ymin=0, @@ -136,27 +137,13 @@ Cycle count is one factor in calculating execution times; the other is the clock \end{tikzpicture} \caption{A comparison of the resource utilisation of designs generated by \vericert{} and by \legup{}.} \label{fig:comparison_area} -\end{figure} - -Figure~\ref{fig:comparison_area} compares the resource utilisation of the Polybench programs generated by \vericert{} and \legup{}. -On average, we see that \vericert{} produces hardware that is about $21\times$ larger than \legup{}. \vericert{} designs are filling up to 30\% of a (large) FPGA chip, while \legup{} uses no more than 1\% of the chip. -The main reason for this is that RAM is not inferred automatically for the Verilog that is generated by \vericert{}; instead, large arrays of registers are synthesised. -Synthesis tools such as Quartus generally require array accesses to be in a specific form in order for RAM inference to activate. -\legup{}'s Verilog generation is tailored to enable RAM inference by Quartus, while \vericert{} generates more generic array accesses. This may make \vericert{} more portable across different FPGA synthesis tools and vendors. -%For a fair comparison, we chose Quartus for these experiments because LegUp supports Quartus efficiently. -% Consequently, on average, \legup{} designs use $XX$ RAMs whereas \vericert{} use none. -Enabling RAM inference is part of our future plans. - -% We see that \vericert{} designs use between 1\% and 30\% of the available logic on the FPGA, averaging at around 10\%, whereas LegUp designs all use less than 1\% of the FPGA, averaging at around 0.45\%. The main reason for this is mainly because RAM is not inferred automatically for the Verilog that is generated by \vericert{}. Other synthesis tools can infer the RAM correctly for \vericert{} output, so this issue could be solved by either using a different synthesis tool and targeting a different FPGA, or by generating the correct template which allows Quartus to identify the RAM automatically. - -\subsection{RQ3: How long does \vericert{} take to produce hardware?} - -\begin{figure} +\end{subfigure}\hfill% +\begin{subfigure}[t]{0.48\textwidth} \definecolor{compiltimecol}{HTML}{66a61e} \begin{tikzpicture} \begin{axis}[ - height=80mm, - width=80mm, + height=1\textwidth, + width=1\textwidth, xlabel={\legup{} compilation time (s)}, ylabel={\vericert{} compilation time (s)}, yticklabel style={ @@ -167,8 +154,8 @@ Enabling RAM inference is part of our future plans. ymin=0.06, ymax=0.20, ] - -\addplot[draw=none, mark=*, draw opacity=0, fill opacity=0.6,compiltimecol] + +\addplot[draw=none, mark=*, draw opacity=0, fill opacity=0.6,compiltimecol] table [x=legupcomptime, y=vericertcomptime, col sep=comma] {results/poly.csv}; @@ -178,8 +165,22 @@ Enabling RAM inference is part of our future plans. \end{tikzpicture} \caption{A comparison of compilation time for \vericert{} and for \legup{}} \label{fig:comparison_comptime} +\end{subfigure} \end{figure} +Figure~\ref{fig:comparison_area} compares the resource utilisation of the Polybench programs generated by \vericert{} and \legup{}. +On average, we see that \vericert{} produces hardware that is about $21\times$ larger than \legup{}. \vericert{} designs are filling up to 30\% of a (large) FPGA chip, while \legup{} uses no more than 1\% of the chip. +The main reason for this is that RAM is not inferred automatically for the Verilog that is generated by \vericert{}; instead, large arrays of registers are synthesised. +Synthesis tools such as Quartus generally require array accesses to be in a specific form in order for RAM inference to activate. +\legup{}'s Verilog generation is tailored to enable RAM inference by Quartus, while \vericert{} generates more generic array accesses. This may make \vericert{} more portable across different FPGA synthesis tools and vendors. +%For a fair comparison, we chose Quartus for these experiments because LegUp supports Quartus efficiently. +% Consequently, on average, \legup{} designs use $XX$ RAMs whereas \vericert{} use none. +Enabling RAM inference is part of our future plans. + +% We see that \vericert{} designs use between 1\% and 30\% of the available logic on the FPGA, averaging at around 10\%, whereas LegUp designs all use less than 1\% of the FPGA, averaging at around 0.45\%. The main reason for this is mainly because RAM is not inferred automatically for the Verilog that is generated by \vericert{}. Other synthesis tools can infer the RAM correctly for \vericert{} output, so this issue could be solved by either using a different synthesis tool and targeting a different FPGA, or by generating the correct template which allows Quartus to identify the RAM automatically. + +\subsection{RQ3: How long does \vericert{} take to produce hardware?} + Figure~\ref{fig:comparison_comptime} compares the compilation times of \vericert{} and of \legup{}, with each data point corresponding to one of the PolyBench/C benchmarks. On average, \vericert{} compilation is about $47\times$ faster than \legup{} compilation. \vericert{} is much faster because it omits many of the time-consuming HLS optimisations performed by \legup{}, such as scheduling and memory analysis. This comparison also demonstrates that our fully verified approach does not add substantial overheads in compilation time, since we do not invoke verification for every compilation instance, unlike the approaches based on translation validation that we mentioned in Section~\ref{sec:intro}. %\NR{Do we want to finish the section off with some highlights or a summary?} @@ -156,7 +156,7 @@ The final lemma we need is that the Verilog we generate is deterministic. This r \centering \begin{tabular}{lrrrrr} \toprule - & \textbf{Coq code} & \textbf{OCaml code} & \textbf{Specifications} & \textbf{Theorems \& Proofs} & \textbf{Total}\\ + & \textbf{Coq code} & \multicolumn{1}{p{1cm}}{\centering\textbf{OCaml code}} & \textbf{Spec} & \multicolumn{1}{p{2cm}}{\centering\textbf{Theorems \& Proofs}} & \textbf{Total}\\ \midrule {Data structures and libraries} & 274 & --- & --- & 654 & 928 \\ {Integers and values} & 98 & --- & 15 & 744 & 857 \\ @@ -166,7 +166,7 @@ The final lemma we need is that the Verilog we generate is deterministic. This r {Verilog generation} & 68 & --- & --- & 396 & 464 \\ {Top-level driver, pretty printers} & 89 & 747 & --- & 209 & 1045 \\ \midrule - \textbf{Total} & 1184 & 747 & 1007 & 5526 & 8464 \\ + \textbf{Total} & 1184 & 747 & 1007 & 5526 & 8464 \\ \bottomrule \end{tabular} \caption{Statistics about the numbers of lines of code in the proof and implementation of \vericert{}.} diff --git a/verilog.tex b/verilog.tex index 0caf06c..cf5b455 100644 --- a/verilog.tex +++ b/verilog.tex @@ -103,7 +103,7 @@ Note that there is no step from \texttt{State} to \texttt{Callstate}; this is be Therefore, in addition to the rules shown in Figure~\ref{fig:inferrence_module}, an initial state and final state need to be defined: \begin{gather*} - \inferrule[Initial]{\yhfunction{is\_internal}\ (P.\texttt{main})}{\yhfunction{initial\_state}\ (\yhconstant{Callstate } []\ (P.\texttt{main})\ [])}\\ + \inferrule[Initial]{\yhfunction{is\_internal}\ (P.\texttt{main})}{\yhfunction{initial\_state}\ (\yhconstant{Callstate } []\ (P.\texttt{main})\ [])}\qquad \inferrule[Final]{ }{\yhfunction{final\_state}\ (\yhconstant{Returnstate } []\ n)\ n} \end{gather*} |