diff options
| -rw-r--r-- | evaluation.tex | 45 | ||||
| -rw-r--r-- | main.tex | 2 | ||||
| -rw-r--r-- | related.tex | 10 |
3 files changed, 42 insertions, 15 deletions
diff --git a/evaluation.tex b/evaluation.tex index 8c74a2e..9236c98 100644 --- a/evaluation.tex +++ b/evaluation.tex @@ -33,7 +33,7 @@ We configured \polybench{}'s parameters so that only integer types are used, sin \begin{figure}\centering \begin{tikzpicture} - \newcommand\backgroundbar[1]{\draw[draw=none, fill=black!10] (axis cs:#1,0.8) rectangle (axis cs:1+#1,300);} + \newcommand\backgroundbar[2][5]{\draw[draw=none, fill=black!#1] (axis cs:#2,0.1) rectangle (axis cs:1+#2,300);} \begin{groupplot}[ group style={ @@ -45,8 +45,6 @@ We configured \polybench{}'s parameters so that only integer types are used, sin }, ymode=log, ybar=0pt, - %ymode=log, %JW: normalised data ==> log scale - %log ticks with fixed point, width=1\textwidth, height=0.4\textwidth, /pgf/bar width=3pt, @@ -54,7 +52,7 @@ We configured \polybench{}'s parameters so that only integer types are used, sin log ticks with fixed point, xticklabels from table={\divtimingtable}{benchmark}, legend style={nodes={scale=0.7, transform shape}}, - x tick label style={rotate=60,anchor=east,font=\footnotesize}, + x tick label style={rotate=90,anchor=east,font=\footnotesize}, legend columns=-1, xtick=data, enlarge x limits={abs=0.5}, @@ -62,24 +60,49 @@ We configured \polybench{}'s parameters so that only integer types are used, sin xtick style={draw=none}, ] - \nextgroupplot[ymin=0.8,ylabel={Relative execution time to \legup{}}] - \backgroundbar{0.5} + \nextgroupplot[ymin=0.8,ymax=300,ylabel={Execution time relative to \legup{}}] + % JW: sorry about the lack of loop below. \pgfplotsinvokeforeach is supposed to work but overleaf compilation hangs. + % oh, I had actually just tried to solve it, and this worked on mine: \pgfplotsinvokeforeach{0,...,13}{\draw[draw=none, fill=black!10] (axis cs:#1*2+0.5,0.01) rectangle (axis cs:#1*2+1.5,300);} (Locally though) + \backgroundbar{0.5} \backgroundbar{2.5} \backgroundbar{4.5} \backgroundbar{6.5} \backgroundbar{8.5} + \backgroundbar{10.5} + \backgroundbar{12.5} + \backgroundbar{14.5} + \backgroundbar{16.5} + \backgroundbar{18.5} + \backgroundbar{20.5} + \backgroundbar{22.5} + \backgroundbar[10]{24.5} \addplot+[vericertcol] table [x expr=\coordindex,y=vericert,col sep=comma] from \divtimingtable; \addplot+[legupnooptcol] table [x expr=\coordindex,y=legup noopt nochain,col sep=comma] from \divtimingtable; \addplot+[legupnooptnochaincol] table [x expr=\coordindex,y=legup noopt,col sep=comma] from \divtimingtable; \draw (axis cs:-1,1) -- (axis cs:26,1); + % JW: redraw axis border which has been partially covered by the grey bars + \draw (axis cs:-0.5,0.8) rectangle (axis cs:25.5,300); - - - \nextgroupplot[ymin=0.3,ylabel={Relative area to \legup{}}] + \nextgroupplot[ymin=0.3,ymax=10,ylabel={Area relative to \legup{}}] + \backgroundbar{0.5} + \backgroundbar{2.5} + \backgroundbar{4.5} + \backgroundbar{6.5} + \backgroundbar{8.5} + \backgroundbar{10.5} + \backgroundbar{12.5} + \backgroundbar{14.5} + \backgroundbar{16.5} + \backgroundbar{18.5} + \backgroundbar{20.5} + \backgroundbar{22.5} + \backgroundbar[10]{24.5} \addplot+[vericertcol] table [x expr=\coordindex,y=vericert,col sep=comma] from \divslicetable; \addplot+[legupnooptcol] table [x expr=\coordindex,y=legup noopt nochain,col sep=comma] from \divslicetable; \addplot+[legupnooptnochaincol] table [x expr=\coordindex,y=legup noopt,col sep=comma] from \divslicetable; \draw (axis cs:-1,1) -- (axis cs:26,1); + % JW: redraw axis border which has been partially covered by the grey bars + \draw (axis cs:-0.5,0.3) rectangle (axis cs:25.5,10); \legend{\vericert{},\legup{} w/o opt/chain,\legup{} w/o opt}; \end{groupplot} @@ -119,16 +142,20 @@ We configured \polybench{}'s parameters so that only integer types are used, sin ] \nextgroupplot[ylabel={Relative execution time to \legup{}}] + \pgfplotsinvokeforeach{0,...,13}{\draw[draw=none, fill=black!10] (axis cs:#1*2+0.5,0.01) rectangle (axis cs:#1*2+1.5,300);} \addplot+[vericertcol] table [x expr=\coordindex,y=vericert,col sep=comma] from \nodivtimingtable; \addplot+[legupnooptcol] table [x expr=\coordindex,y=legup noopt nochain,col sep=comma] from \nodivtimingtable; \addplot+[legupnooptnochaincol] table [x expr=\coordindex,y=legup noopt,col sep=comma] from \nodivtimingtable; \draw (axis cs:-1,1) -- (axis cs:26,1); + \draw (axis cs:-0.5,0.3) rectangle (axis cs:26.5,10); \nextgroupplot[ylabel={Relative area to \legup{}}] + \pgfplotsinvokeforeach{0,...,13}{\draw[draw=none, fill=black!10] (axis cs:#1*2+0.5,0.01) rectangle (axis cs:#1*2+1.5,300);} \addplot+[vericertcol] table [x expr=\coordindex,y=vericert,col sep=comma] from \nodivslicetable; \addplot+[legupnooptcol] table [x expr=\coordindex,y=legup noopt nochain,col sep=comma] from \nodivslicetable; \addplot+[legupnooptnochaincol] table [x expr=\coordindex,y=legup noopt,col sep=comma] from \nodivslicetable; \draw (axis cs:-1,1) -- (axis cs:26,1); + \draw (axis cs:-0.5,0.3) rectangle (axis cs:26.5,10); \legend{\vericert{},\legup{} w/o opt/chain,\legup{} w/o opt}; \end{groupplot} @@ -140,7 +140,7 @@ \begin{abstract} High-level synthesis (HLS), which refers to the automatic compilation of software into hardware, is rapidly gaining popularity. In a world increasingly reliant on application-specific hardware accelerators, HLS promises hardware designs of comparable performance and energy efficiency to those coded by hand in a hardware description language like Verilog, while maintaining the convenience and the rich ecosystem of software development. However, current HLS tools cannot always guarantee that the hardware designs they produce are equivalent to the software they were given, thus undermining any reasoning conducted at the software level. Worse, there is mounting evidence that existing HLS tools are quite unreliable, sometimes generating wrong hardware or crashing when given valid inputs. - To address this problem, we present the first HLS tool that is mechanically verified to preserve the behaviour of its input software. Our tool, called \vericert{}, extends the \compcert{} verified C compiler with a new hardware-oriented intermediate language and a Verilog back end, and has been proven correct in Coq. \JW{Could maybe drop the following sentence from the abstract?}\YH{Hmm, I don't know actually, I feel like as we don't support all of the C features one might want to know what features are supported.} \vericert{} supports all C constructs except for case statements, function pointers, recursive function calls, integers larger than 32 bits, floats, and global variables. An evaluation on the PolyBench/C benchmark suite indicates that \vericert{} generates hardware that is around an order of magnitude slower but about the same size as hardware generated by an existing, optimising (but unverified) HLS tool.\YH{Technically this is right, but we might want to add the division values.} + To address this problem, we present the first HLS tool that is mechanically verified to preserve the behaviour of its input software. Our tool, called \vericert{}, extends the \compcert{} verified C compiler with a new hardware-oriented intermediate language and a Verilog back end, and has been proven correct in Coq. \JW{Could maybe drop the following sentence from the abstract?}\YH{Hmm, I don't know actually, I feel like as we don't support all of the C features one might want to know what features are supported.} \JW{What would the list look like if you phrased it has the features that \emph{are} supported? (Following Ally's suggestion.)} \vericert{} supports all C constructs except for case statements, function pointers, recursive function calls, integers larger than 32 bits, floats, and global variables. An evaluation on the PolyBench/C benchmark suite indicates that \vericert{} generates hardware that is around an order of magnitude slower but about the same size as hardware generated by an existing, optimising (but unverified) HLS tool.\YH{Technically this is right, but we might want to add the division values.} \JW{What would it look like if you add those?} \end{abstract} %% 2012 ACM Computing Classification System (CSS) concepts diff --git a/related.tex b/related.tex index 633fe6f..584653a 100644 --- a/related.tex +++ b/related.tex @@ -25,12 +25,12 @@ \node[align=center] at (0,2.8) {Standard HLS tools \\ \footnotesize\cite{canis11_legup,intel20_sdk_openc_applic} \\ \footnotesize\cite{nigam20_predic_accel_desig_time_sensit_affin_types,xilinx20_vivad_high_synth}}; \node[align=center] at (0,1.5) {Translation validation approaches \\ \footnotesize\cite{mentor20_catap_high_level_synth,kundu08_valid_high_level_synth,clarke03_behav_c_veril}}; \node at (0,0.5) {\bf \vericert{}}; - \node[align=left] at (-1.8,0.32) {K\^oika {\footnotesize\cite{bourgeat20_essen_blues}}}; - \node[align=left] at (-1.8,0.0) {L\"o\"ow et al. {\footnotesize\cite{loow19_verif_compil_verif_proces}}}; + \node[align=left] at (-1.8,0.0) {\footnotesize K\^oika \cite{bourgeat20_essen_blues}}; + \node[align=left] at (-1.8,0.32) { \footnotesize\citet{loow19_verif_compil_verif_proces}}; - \node at (2.2,0.2) {Ellis {\footnotesize\cite{ellis08}}}; - \node at (-1.3,-0.32) {Perna et al. {\footnotesize\cite{perna12_mechan_wire_wise_verif_handel_c_synth}}}; - \node at (0,-1.3) {BEDROC {\footnotesize\cite{chapman92_verif_bedroc}}}; + \node at (2.2,0.2) {\footnotesize\citet{ellis08}}; + \node at (-1.3,-0.32) { {\footnotesize\citet{perna12_mechan_wire_wise_verif_handel_c_synth}}}; + \node at (0,-1.3) {\footnotesize BEDROC \cite{chapman92_verif_bedroc}}; \node[align=left] at (-2.9,-1.7) {\color{colorproof}Correctness \\ \color{colorproof}proof}; \draw[myoutline] (1.2,-0.9) to (2.6,-1.7); |