Add new presentation

6 files changed, 273 insertions, 36 deletions

diff --git a/presentation/assets/fpga-flow.pdf b/presentation/assets/fpga-flow.pdf
index 5cbdf30..e5f41bf 100644
--- a/presentation/assets/fpga-flow.pdf
+++ b/presentation/assets/fpga-flow.pdf
diff --git a/presentation/assets/hls-flow.pdf b/presentation/assets/hls-flow.pdf
index 6a65045..f572a87 100644
--- a/presentation/assets/hls-flow.pdf
+++ b/presentation/assets/hls-flow.pdf
diff --git a/presentation/assets/verilog-flow.pdf b/presentation/assets/verilog-flow.pdf
index f62ef74..f7ce05e 100644
--- a/presentation/assets/verilog-flow.pdf
+++ b/presentation/assets/verilog-flow.pdf
diff --git a/presentation/presentation.org b/presentation/presentation.org
index 3ea79ba..2e8a18f 100644
--- a/presentation/presentation.org
+++ b/presentation/presentation.org
@@ -19,37 +19,126 @@ But:
 - Needs knowledge about hardware design.
 - *Less flexible*.
 
+** FPGA Layout
+
+#+begin_export latex
+\centering
+\includegraphics[width=7.5cm]{assets/fpga.pdf}
+#+end_export
+
 ** So How do we Program an FPGA?
 
 *** Code example :B_column:
 :PROPERTIES:
 :BEAMER_ENV: column
-:BEAMER_COL: 0.4
+:BEAMER_COL: 0.5
+:END:
+
+**** Top
+:PROPERTIES:
+:BEAMER_ENV: minipage
+:BEAMER_OPT: 4.5cm
+:END:
+
+#+attr_beamer: :overlay <+->
+- FPGAs contain *LUTs* and programmable interconnects.
+- Programmed using *hardware description languages*.
+- Simulation quite slow.
+- High-Level Synthesis is an alternative.
+- Faster testing through execution.
+
+**** Bottom
+:PROPERTIES:
+:BEAMER_ENV: minipage
+:BEAMER_OPT: 2.5cm
+:END:
+
+#+beamer: \vspace{1em}
+
+***** Only 2
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: <2-3>
 :END:
 
+#+begin_export latex
+\includegraphics[width=0.5cm]{assets/up-arrow.pdf} Fine control \hspace{1em}
+\includegraphics[width=0.5cm]{assets/down-arrow.pdf} Long to design
+#+end_export
+
+***** Only 3
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: <4-5>
+:END:
+
+#+begin_export latex
+\includegraphics[width=0.5cm]{assets/up-arrow.pdf} Quick to design \hspace{1em}
+\includegraphics[width=0.5cm]{assets/down-arrow.pdf} Less control
+#+end_export
+
 *** Code example :B_column:
 :PROPERTIES:
 :BEAMER_ENV: column
-:BEAMER_COL: 0.6
+:BEAMER_COL: 0.5
 :END:
 
-**** FPGA
+**** Minipage
+:PROPERTIES:
+:BEAMER_ENV: minipage
+:BEAMER_OPT: 5cm
+:END:
+***** FPGA
 :PROPERTIES:
 :BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: <1>
 :END:
 
-**** Verilog
+#+begin_export latex
+\includegraphics[width=6.8cm]{assets/fpga-flow.pdf}
+#+end_export
+
+***** Verilog
 :PROPERTIES:
 :BEAMER_ENV: onlyenvNH
-:BEAMER_ACT: <3>
+:BEAMER_ACT: <2>
 :END:
-**** HLS
+
+#+begin_export latex
+\includegraphics[width=6.8cm]{assets/verilog-flow.pdf}
+#+end_export
+
+***** Verilog Simulation
 :PROPERTIES:
 :BEAMER_ENV: onlyenvNH
 :BEAMER_ACT: <3>
 :END:
 
-** What is High-Level Synthesis
+#+begin_export latex
+\includegraphics[width=6.8cm]{assets/verilog-flow-testing.pdf}
+#+end_export
+
+***** HLS
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: <4>
+:END:
+
+#+begin_export latex
+\includegraphics[width=6.8cm]{assets/hls-flow.pdf}
+#+end_export
+
+***** HLS Testing
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: <5>
+:END:
+
+#+begin_export latex
+\includegraphics[width=6.8cm]{assets/hls-flow-testing.pdf}
+#+end_export
+
+** What is High-Level Synthesis :noexport:
 
 *** High-Level Synthesis (HLS)
 :PROPERTIES:
@@ -76,30 +165,28 @@ Translation of a high-level programming language such as C/C++ into a hardware d
 - *Performance*: Requires automatic parallelisation.
 - *Correctness*: Hard to verify generated HDL.
 
-** Motivation
+** Motivation for Formal Verification
 
-*** HLS Unreliable :B_blockNH:
+*** HLS Difficulties :B_blockNH:
 :PROPERTIES:
 :BEAMER_env: blockNH
 :END:
 
-High-level synthesis is often quite unreliable:
+Difficult to debug HLS tools:
 
-#+attr_beamer: :overlay <+->
-- Intel's OpenCL could not be fuzzed because of too many issues (cite:lidbury15_many_core_compil_fuzzin).
-- We fuzzed HLS tools and found they failed on *2.5%* of simple random test cases.
+- Simulation can take a long time.
+- Correctness is important in hardware, testing is done at every level.
 
-*** HLS Difficulties :B_blockNH:
+*** HLS Unreliable :B_blockNH:
 :PROPERTIES:
 :BEAMER_env: blockNH
-:BEAMER_ACT: <3->
+:BEAMER_ACT: <2>
 :END:
 
-Difficult to debug HLS tools:
+High-level synthesis is often quite unreliable:
 
-#+attr_beamer: :overlay <+->
-- Simulation can take a long time.
-- Correctness is important in hardware, testing is done at every level.
+- Intel's OpenCL could not be fuzzed because of too many issues (cite:lidbury15_many_core_compil_fuzzin).
+- We fuzzed HLS tools and found they failed on *2.5%* of simple random test cases.
 
 ** Solution :B_frame:
 :PROPERTIES:
@@ -569,16 +656,39 @@ endmodule
 - Always block run in parallel
 ** Verilog Semantics (Adapted from Lööw et al. (2019))
 
+#+attr_beamer: :overlay <+->
+- Top-level semantics are *small-step operational semantics*.
+- Within each small step, a Verilog module is executed in one big step.
+
+*** Minipage
+:PROPERTIES:
+:BEAMER_ENV: minipage
+:BEAMER_OPT: 5cm
+:END:
+
+#+beamer: \vspace{1em}
+#+beamer: \centering
+
+**** Only 1
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: <1>
+:END:
+
 #+begin_export latex
-\begin{gather*}
-%\inferrule[Nonblocking]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \downarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ <= } e) \downarrow_{\text{stmnt}} (\Gamma, \Delta [n \mapsto v])} \quad \inferrule[Blocking]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \downarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ = } e) \downarrow_{\text{stmnt}} (\Gamma [n \mapsto v], \Delta)} \\
-\inferrule[Module]{(\Gamma, \epsilon, \vec{m})\ \downarrow_{\text{module}^{+}} (\Gamma', \Delta') \\ (\Gamma'\ //\ \Delta', \epsilon, \vec{m}) \downarrow_{\text{module}^{-}} (\Gamma'', \Delta'')}{(\Gamma, \yhkeyword{module}\ \yhconstant{main} \yhkeyword{(...);}\ \vec{m}\ \yhkeyword{endmodule}) \downarrow_{\text{program}} (\Gamma''\ //\ \Delta'')}
-\end{gather*}
+\includegraphics[width=8cm]{assets/semantics_clk.pdf}
+#+end_export
+
+**** Only 2
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: <2>
+:END:
+
+#+begin_export latex
+\includegraphics[width=8cm]{assets/semantics.pdf}
 #+end_export
 
-#+attr_beamer: :overlay <+->
-- Two separate association maps: current ($\Gamma$) and next ($\Delta$).
-- Maps are merged at the end of the clock cycle.
 
 ** How the Verilog semantics changed :noexport:
 
@@ -717,7 +827,7 @@ where
 \end{equation*}
 #+end_export
 
-**** Theorem :B_onlyenvNH:
+**** Theorem :B_onlyenvNH:noexport:
 :PROPERTIES:
 :BEAMER_env: onlyenvNH
 :BEAMER_ACT: <4->
@@ -735,7 +845,7 @@ where
 \end{align*}
 #+end_export
 
-** RTL $\to$ HTL: Build a Specification
+** RTL $\to$ HTL: Build a Specification :noexport:
 
 Assuming $\yhfunction{HLS} (C) = \yhconstant{OK} (V)$ requires reasoning about implementation details.
 
@@ -764,7 +874,7 @@ Instead we build a model of the translation which we can use.
 \end{equation*}
 #+end_export
 
-** RTL $\to$ HTL: Prove Forward Simulation
+** RTL $\to$ HTL: Prove Forward Simulation :noexport:
 
 *** Column 1
 :PROPERTIES:
@@ -818,15 +928,132 @@ Prove the simulation diagram correct:
 - there exists 1 or more steps in Verilog,
 - such that after 1 step in RTL, the resulting states match.
 
-** Results
+** With Division approximately 27$\times$ slower
+
+#+begin_export latex
+\pgfplotstableread[col sep=comma]{../results/rel-time-div.csv}{\divtimingtable}
+\pgfplotstableread[col sep=comma]{../results/rel-size-div.csv}{\divslicetable}
+\definecolor{vericertcol}{HTML}{66C2A5}
+\definecolor{legupnooptcol}{HTML}{FC8D62}
+\definecolor{legupnooptnochaincol}{HTML}{8DA0CB}
+\newcommand\backgroundbar[2][5]{\draw[draw=none, fill=black!#1] (axis cs:#2*2+0.5,0.1) rectangle (axis cs:1+#2*2+0.5,300);}
+
+\centering
+\begin{tikzpicture}[scale=0.65]
+  
+  \begin{groupplot}[
+    group style={
+      group name=my plots,
+      group size=1 by 2,
+      xlabels at=edge bottom,
+      xticklabels at=edge bottom,
+      vertical sep=5pt,
+    },
+    ymode=log,
+    ybar=0.4pt,
+    width=1\textwidth,
+    height=0.4\textwidth,
+    /pgf/bar width=3pt,
+    legend pos=south east,
+    log ticks with fixed point,
+    xticklabels from table={\divtimingtable}{benchmark},
+    legend style={nodes={scale=0.7, transform shape}},
+    x tick label style={rotate=90,anchor=east,font=\footnotesize},
+    legend columns=-1,
+    xtick=data,
+    enlarge x limits={abs=0.5},
+    ylabel style={font=\footnotesize},
+    xtick style={draw=none},
+    ]
+
+    \nextgroupplot[ymin=0.8,ymax=300,ylabel={Execution time relative to \legup{}}]
+    \pgfplotsinvokeforeach{0,...,12}{%
+      \backgroundbar{#1}}
+    \backgroundbar[10]{13}
+    \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:28,1);
+    % JW: redraw axis border which has been partially covered by the grey bars
+    \draw (axis cs:-0.5,0.8) rectangle (axis cs:27.5,300);
+    
+    \nextgroupplot[ymin=0.3,ymax=10,ylabel={Area relative to \legup{}}]
+    \pgfplotsinvokeforeach{0,...,12}{%
+      \backgroundbar{#1}}
+    \backgroundbar[10]{13}
+    \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:28,1);
+    % JW: redraw axis border which has been partially covered by the grey bars
+    \draw (axis cs:-0.5,0.3) rectangle (axis cs:27.5,10);
+
+    \legend{\vericert{},\legupnooptchain{},\legupnoopt{}};
+  \end{groupplot}
+\end{tikzpicture}
+#+end_export
 
-*** Performance Results
+** Without Division about 2$\times$ slower
 
-#+attr_beamer: :overlay <+->
-- Ran on 27/30 PolyBench/C benchmarks and compared to LegUp.
-- 27$\times$ slower and 1.1$\times$ larger.
-- Ran on PolyBench/C with divisions replaced by iterative shifting.
-- 2$\times$ slower (on par with unoptimised LegUp).
+#+begin_export latex
+\pgfplotstableread[col sep=comma]{../results/rel-time-nodiv.csv}{\nodivtimingtable}
+\pgfplotstableread[col sep=comma]{../results/rel-size-nodiv.csv}{\nodivslicetable}
+\definecolor{vericertcol}{HTML}{66C2A5}
+\definecolor{legupnooptcol}{HTML}{FC8D62}
+\definecolor{legupnooptnochaincol}{HTML}{8DA0CB}
+\centering
+\begin{tikzpicture}[scale=0.65]
+  \begin{groupplot}[
+    group style={
+      group name=my plots,
+      group size=1 by 2,
+      xlabels at=edge bottom,
+      xticklabels at=edge bottom,
+      vertical sep=5pt,
+    },
+    ymode=log,
+    ybar=0.4pt,
+    ytick={0.5,1,2,4,8},
+    width=1\textwidth,
+    height=0.4\textwidth,
+    /pgf/bar width=3pt,
+    legend pos=south east,
+    log ticks with fixed point,
+    xticklabels from table={\nodivtimingtable}{benchmark},
+    legend style={nodes={scale=0.7, transform shape}},
+    x tick label style={rotate=90,anchor=east,font=\footnotesize},
+    legend columns=-1,
+    xtick=data,
+    enlarge x limits={abs=0.5},
+    ylabel style={font=\footnotesize},
+    ymin=0.3,
+    xtick style={draw=none},
+    ]
+
+    \nextgroupplot[ymin=0.3,ymax=10,ylabel={Execution time relative to \legup{}}]
+    \pgfplotsinvokeforeach{0,...,12}{%
+      \backgroundbar{#1}}
+    \backgroundbar[10]{13}
+    \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:28,1);
+    \draw (axis cs:-0.5,0.3) rectangle (axis cs:27.5,10);
+
+    \nextgroupplot[ymin=0.3,ymax=4,ylabel={Area relative to \legup{}}]
+    \pgfplotsinvokeforeach{0,...,12}{%
+      \backgroundbar{#1}}
+    \backgroundbar[10]{13}
+    \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:28,1);
+    \draw (axis cs:-0.5,0.3) rectangle (axis cs:27.5,4);
+
+    \legend{\vericert{},\legupnooptchain{},\legupnoopt{}};
+  \end{groupplot}
+\end{tikzpicture}
+#+end_export
 
 ** Fuzzing Vericert with Csmith
 
diff --git a/presentation/presentation.pdf b/presentation/presentation.pdf
index b28b731..0a3e687 100644
--- a/presentation/presentation.pdf
+++ b/presentation/presentation.pdf
diff --git a/presentation/setup.org b/presentation/setup.org
index 8585178..8fd866f 100644
--- a/presentation/setup.org
+++ b/presentation/setup.org
@@ -7,6 +7,9 @@
 #+latex_header: \usepackage{microtype}
 #+latex_header: \usepackage{mathtools}
 #+latex_header: \usepackage{natbib}
+#+latex_header: \usepackage{graphicx}
+#+latex_header: \usepackage{pgfplots}
+#+latex_header: \usepackage{pgfplotstable}
 
 #+latex_header_extra: \DisableLigatures{encoding=T1, family=tt*}
 #+latex_header_extra: \usemintedstyle{manni}
@@ -23,6 +26,13 @@
 #+latex_header_extra: \newcommand\yhfunction[1]{\texttt{\textcolor{functioncolour}{#1}}}
 #+latex_header_extra: \newcommand\yhconstant[1]{\texttt{\textcolor{constantcolour}{#1}}}
 #+latex_header_extra: \bibliographystyle{plainnat}
+#+latex_header_extra: \pgfplotsset{compat=1.16}
+#+latex_header_extra: \usetikzlibrary{pgfplots.groupplots}
+
+#+latex_header_extra: \newcommand\legup{Leg\-Up}
+#+latex_header_extra: \newcommand\legupnoopt{\legup{} no-opt}
+#+latex_header_extra: \newcommand\legupnooptchain{\legup{} no-opt no-chaining}
+#+latex_header_extra: \newcommand\vericert{Veri\-cert}
 
 #+exclude_tags: noexport