Add some more updates to presentation

6 files changed, 181 insertions, 39 deletions

diff --git a/presentation/assets/database-asic.pdf b/presentation/assets/database-asic.pdf
new file mode 100644
index 0000000..4a16fff
--- /dev/null
+++ b/presentation/assets/database-asic.pdf
diff --git a/presentation/assets/fpga-expl2.pdf b/presentation/assets/fpga-expl2.pdf
index 97a5f12..34c6df4 100644
--- a/presentation/assets/fpga-expl2.pdf
+++ b/presentation/assets/fpga-expl2.pdf
diff --git a/presentation/beamerthemeauriga.sty b/presentation/beamerthemeauriga.sty
index 5ecc877..e4b18e4 100644
--- a/presentation/beamerthemeauriga.sty
+++ b/presentation/beamerthemeauriga.sty
@@ -103,12 +103,11 @@
     {\usebeamerfont{title page institute}\usebeamercolor[fg]{title page}\insertinstitute\\[1ex]}
     \vskip0pt plus 1filll
   \end{centering}
-  {\hfill\includegraphics[height=1cm]{./assets/oopsla21.png}}
+  {\includegraphics[height=1cm]{./assets/imperial_logo.pdf}\hfill\includegraphics[height=1cm]{./assets/oopsla21.png}}
 }
 
 % Footer
-\setbeamertemplate{footline}{
-  \hspace{2em}\includegraphics[height=1cm]{./assets/imperial_logo.pdf}%
+\setbeamertemplate{footline}{%
     \hfill%
     \usebeamercolor[fg]{page number in head/foot}%
     \usebeamerfont{page number in head/foot}%
@@ -117,11 +116,11 @@
 }
 
 % Frame title
-\setbeamertemplate{frametitle}{
-    \nointerlineskip
-    \vskip2ex
-    {\usebeamerfont{frametitle}\usebeamercolor[fg]{frametitle}\insertframetitle\\[-2.5ex]}
-    {\par\color{lightgreen}\rule{390pt}{2pt}}
+\setbeamertemplate{frametitle}{%
+    \nointerlineskip%
+    \vskip2ex%
+    {\usebeamerfont{frametitle}\usebeamercolor[fg]{frametitle}\insertframetitle\\[-2.5ex]}%
+    {\par\color{lightgreen}\rule{390pt}{2pt}}%
 }
 
 % Alert
diff --git a/presentation/presentation.org b/presentation/presentation.org
index bc580ab..106232e 100644
--- a/presentation/presentation.org
+++ b/presentation/presentation.org
@@ -1,12 +1,12 @@
 #+title: Formal Verification of High-Level Synthesis
 #+author: \underline{Yann Herklotz}, James D. Pollard, Nadesh Ramanathan, John Wickerson
-#+options: H:2
+#+options: H:2 toc:nil
 #+columns: %45ITEM %10BEAMER_ENV(Env) %10BEAMER_ACT(Act) %4BEAMER_COL(Col)
 #+setupfile: setup.org
 
 ** The Need to Design Hardware Accelerators
 
-Hardware accelerators are needed more and more industries.
+Application-specific hardware accelerators are increasingly being needed in industries.
 
 *** Column 1
 :PROPERTIES:
@@ -16,8 +16,10 @@ Hardware accelerators are needed more and more industries.
 
 #+attr_beamer: :overlay <+->
 - Using a *CPU* everywhere not always the best choice.
-- *Field-Programmable Gate Arrays (FPGA)* provide a good alternative.
-- FPGAs act as *reprogrammable hardware*, therefore can be made application specific.
+- *Application-specific integrated circuits (ASIC)* are the ideal choice, but very expensive to
+  create.
+- *Field-programmable gate arrays (FPGA)* act as *reprogrammable hardware*, therefore can be made
+  application-specific.
 
 *** Column 2
 :PROPERTIES:
@@ -46,7 +48,17 @@ Hardware accelerators are needed more and more industries.
 ***** Only 2
 :PROPERTIES:
 :BEAMER_ENV: onlyenvNH
-:BEAMER_ACT: 2-
+:BEAMER_ACT: 2
+:END:
+
+#+begin_export latex
+\includegraphics[width=6cm]{assets/database-asic.pdf}
+#+end_export
+
+***** Only 3
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: 3-
 :END:
 
 #+begin_export latex
@@ -58,7 +70,7 @@ Hardware accelerators are needed more and more industries.
 #+attr_beamer: :overlay <+->
 - FPGA's are programmable circuits with two main components.
 - *Look up tables (LUTs)* provide flexible logic gates.  They are connected by *configurable switches*.
-- *BRAMs* provide accessible storage.
+- *RAMs* provide accessible storage.
 
 *** Minipage
 :PROPERTIES:
@@ -132,7 +144,7 @@ Hardware accelerators are needed more and more industries.
 ***** Only 2
 :PROPERTIES:
 :BEAMER_ENV: onlyenvNH
-:BEAMER_ACT: <2-3>
+:BEAMER_ACT: <2>
 :END:
 
 #+begin_export latex
@@ -143,7 +155,7 @@ Hardware accelerators are needed more and more industries.
 ***** Only 3
 :PROPERTIES:
 :BEAMER_ENV: onlyenvNH
-:BEAMER_ACT: <4-5>
+:BEAMER_ACT: <4>
 :END:
 
 #+begin_export latex
@@ -259,7 +271,6 @@ Difficult to debug HLS tools:
 
 High-level synthesis is often quite unreliable:
 
-- Intel's OpenCL could not be fuzzed because of too many issues (cite:lidbury15_many_core_compil_fuzzin).
 - We fuzzed HLS tools (cite:9444067) and found they failed on *2.5%* of simple random test cases.
 
 ** Solution :B_frame:
@@ -365,7 +376,7 @@ int main() {
 :BEAMER_ACT: <2>
 :END:
 
-- *three address code (3AC)* instructions are represented as a control-flow graph (CFG).
+- *Three address code (3AC)* instructions are represented as a control-flow graph (CFG).
 - Each instruction links to the next one.
 
 *** Text :B_column:
@@ -377,10 +388,10 @@ int main() {
 **** Text 1 :B_onlyenvNH:
 :PROPERTIES:
 :BEAMER_ACT: <1>
-:BEAMER_env: onlyenvNH
+:BEAMER_ENV: onlyenvNH
 :END:
 
-Example of a very simple program performing loads and stores.
+- Example of a very simple program performing loads and stores.
 
 **** 3AC Code 5 :B_onlyenv:
 :PROPERTIES:
@@ -402,7 +413,7 @@ main() {
 }
 #+end_src
 
-** Example: HTL Overview
+** HTL Overview
 
 The representation of the *finite state-machine with datapath* is abstract and called **HTL**.
 
@@ -413,15 +424,23 @@ The representation of the *finite state-machine with datapath* is abstract and c
 
 src_coq[:exports code]{Definition datapath := } $\mathbb{Z}^+ \mapsto \texttt{\small Verilog.stmnt}$
 
-src_coq[:exports code]{Definition controllogic := } $\mathbb{Z}^+ \mapsto \texttt{\small Verilog.stmnt}$
+src_coq[:exports code]{Definition controllogic := } $\mathbb{Z}^+ \mapsto \texttt{\small
+Verilog.stmnt}$
 
-*** Module definition :B_blockNH:
+*** Minipage
 :PROPERTIES:
-:BEAMER_env: blockNH
+:BEAMER_ENV: minipage
+:BEAMER_OPT: 5cm
+:END:
+
+**** Module definition :B_blockNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
 :BEAMER_ACT: 2
 :END:
 
-#+beamer: \vspace{-1.5em}
+#+beamer: \vspace{0.25em}
+
 #+attr_latex: :options fontsize=\footnotesize
 #+begin_src coq
 Record module: Type := mkmodule {
@@ -433,7 +452,58 @@ Record module: Type := mkmodule {
   }.
 #+end_src
 
-** Example: Translation (3AC $\rightarrow$ HTL)
+**** Module definition :B_blockNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 3
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={2-3}
+#+begin_src coq
+Record module: Type := mkmodule {
+    mod_datapath: datapath;
+    mod_controllogic: controllogic;
+    mod_reset: reg;
+    mod_ram: ram_spec;
+    ...
+  }.
+#+end_src
+
+**** Module definition :B_blockNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 4
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={4}
+#+begin_src coq
+Record module: Type := mkmodule {
+    mod_datapath: datapath;
+    mod_controllogic: controllogic;
+    mod_reset: reg;
+    mod_ram: ram_spec;
+    ...
+  }.
+#+end_src
+
+**** Module definition :B_blockNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 5
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={5}
+#+begin_src coq
+Record module: Type := mkmodule {
+    mod_datapath: datapath;
+    mod_controllogic: controllogic;
+    mod_reset: reg;
+    mod_ram: ram_spec;
+    ...
+  }.
+#+end_src
+
+** Translation (3AC $\rightarrow$ HTL)
 
 Translation from *control-flow graph* into a *finite state-machine with datapath*.
 
@@ -443,7 +513,7 @@ Translation from *control-flow graph* into a *finite state-machine with datapath
 #+attr_beamer: :overlay <+->
 - *Control-flow* is translated into a *finite state-machine*.
 - Each *3AC instructions* translated into equivalent *Verilog statements*.
-- Function *stack* implemented as *Verilog array*.
+- Call *stack* implemented as *Verilog array*.
 - Pointers for loads and stores translated to array addresses.
   - *Byte* addressed to *word* addressed.
 
@@ -461,7 +531,7 @@ Translation from *control-flow graph* into a *finite state-machine with datapath
 :BEAMER_ACT: 3
 :END:
 
-~x3 = x3 + x5 + 0~ $\quad\longrightarrow\quad$ src_verilog[:exports code]{reg_3 <= {reg_3 + {reg_5 + 32'd0}}}
+~x3 = x3 + x5 + 0~ $\quad\longrightarrow\quad$ src_verilog[:exports code]{reg_3 <= {reg_3 + {reg_5 + 0}}}
 
 **** Only 2 :B_onlyenvNH:noexport:
 :PROPERTIES:
@@ -469,16 +539,22 @@ Translation from *control-flow graph* into a *finite state-machine with datapath
 :BEAMER_ACT: 5-6
 :END:
 
-~x5 + x1 * 4 + 0~ $\quad\longrightarrow\quad$ src_verilog[:exports code]{{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}}
+~x5 + x1 * 4 + 0~ $\quad\longrightarrow\quad$ src_verilog[:exports code]{{{{reg_5 + 0} + {reg_1 * 4}} / 4}}
 
-** Example: Memory Inference Pass
+** Memory Inference Pass
 
 - An HTL $\rightarrow$ HTL translation removes loads and stores.
 - Replaced by accesses to a proper *RAM*.
 
+*** Minipage
+:PROPERTIES:
+:BEAMER_COL: 0.5
+:END:
+
+
 #+beamer: \vspace{1em}
 
-src_verilog[:exports code]{stack[{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}]}
+src_verilog[:exports code]{stack[reg_5 / 4]}
 
 #+beamer: \vspace{1em}
 
@@ -486,14 +562,68 @@ becomes
 
 #+beamer: \vspace{1em}
 
+**** Minipage
+:PROPERTIES:
+:BEAMER_ENV: minipage
+:BEAMER_OPT: 5cm
+:END:
+
+***** Only 1
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: 1
+:END:
+
+#+beamer: \vspace{0.25em}
+
 #+attr_latex: :options fontsize=\footnotesize
+#+begin_src verilog
+u_en <= ( ~ u_en);
+wr_en <= 0;
+addr <= reg_5 / 4;
+#+end_src
+
+***** Only 2
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: 2
+:END:
 
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={1}
 #+begin_src verilog
-u_en <= ( ~ u_en); wr_en <= 32'd0;
-addr <= {{{reg_3 + 32'd0} + {reg_1 * 32'd4}} / 32'd4};
+u_en <= ( ~ u_en);
+wr_en <= 0;
+addr <= reg_5 / 4;
 #+end_src
 
-** Verilog Syntax
+***** Only 3
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: 3
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={2}
+#+begin_src verilog
+u_en <= ( ~ u_en);
+wr_en <= 0;
+addr <= reg_5 / 4;
+#+end_src
+
+***** Only 4
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: 4
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={3}
+#+begin_src verilog
+u_en <= ( ~ u_en);
+wr_en <= 0;
+addr <= reg_5 / 4;
+#+end_src
+
+
+** Verilog Syntax :noexport:
 
 *** Column 1 :B_column:
 :PROPERTIES:
@@ -556,7 +686,7 @@ endmodule
 - Always block run in parallel
 
 
-** Example: Translation (HTL $\rightarrow$ Verilog) :B_frame:
+** Translation (HTL $\rightarrow$ Verilog) :B_frame:
 
 *** Column
 :PROPERTIES:
@@ -719,7 +849,7 @@ endmodule
 - Finally, translate the FSMD into Verilog.
 - This includes a RAM interface.
 - Data path is translated into a case statement.
-- Ram loads and stores automatically turn off RAM.
+- RAM loads and stores automatically turn off RAM.
 - Control logic is translated into another case statement with a reset.
 
 * Verification
@@ -821,7 +951,7 @@ Use integers modulo $2^n$.
 
 Those are the only types needed for HLS.
 
-** How do we prove the HLS tool correct?
+** How do we prove the HLS tool correct? :noexport:
 
 *** Notes
 :PROPERTIES:
@@ -1193,9 +1323,22 @@ Written a formally verified high-level synthesis tool in *Coq* based on *CompCer
 
 #+attr_beamer: :overlay <+->
 - HLS tool *proven correct in Coq* by proving translation of CFG into FSMD.
-- Small optimisations implemented such as *Ram Inference*.
+- Small optimisations implemented such as *RAM Inference*.
 - Performance without divisions comparable to LegUp without optimisations.
 
+*** Future Work
+:PROPERTIES:
+:BEAMER_ENV: block
+:BEAMER_ACT: <4->
+:END:
+
+Make Vericert not only *correct*, but *competitive*.
+
+#+attr_beamer: :overlay +-
+- Implement *scheduling* and *resource sharing*.
+- Add *external module* support.
+- Add *global variable* support.
+
 ** Thank you :B_fullframe:
 :PROPERTIES:
 :BEAMER_env: fullframe
diff --git a/presentation/presentation.pdf b/presentation/presentation.pdf
index 22e9e58..0842f3b 100644
--- a/presentation/presentation.pdf
+++ b/presentation/presentation.pdf
diff --git a/presentation/setup.org b/presentation/setup.org
index 8fd866f..0b35a82 100644
--- a/presentation/setup.org
+++ b/presentation/setup.org
@@ -14,7 +14,7 @@
 #+latex_header_extra: \DisableLigatures{encoding=T1, family=tt*}
 #+latex_header_extra: \usemintedstyle{manni}
 #+latex_header_extra: \setminted{fontsize=\small}
-#+latex_header_extra: \institute[shortinst]{Imperial College London}
+# #+latex_header_extra: \institute[shortinst]{Imperial College London}
 #+latex_header_extra: \AtBeginSection[]{\begin{frame}\frametitle{Outline}\tableofcontents[currentsection]\end{frame}}
 #+latex_header_extra: \usetikzlibrary{shapes,calc,arrows.meta}
 #+latex_header_extra: \definecolor{keywordcolour}{HTML}{8f0075}