Add more diagrams and content

7 files changed, 59 insertions, 29 deletions

diff --git a/presentation/assets/big-step.pdf b/presentation/assets/big-step.pdf
new file mode 100644
index 0000000..f6f5c8b
--- /dev/null
+++ b/presentation/assets/big-step.pdf
diff --git a/presentation/assets/clk.pdf b/presentation/assets/clk.pdf
new file mode 100644
index 0000000..82226f8
--- /dev/null
+++ b/presentation/assets/clk.pdf
diff --git a/presentation/assets/fpga-expl.pdf b/presentation/assets/fpga-expl.pdf
new file mode 100644
index 0000000..8b914c4
--- /dev/null
+++ b/presentation/assets/fpga-expl.pdf
diff --git a/presentation/assets/fpga-expl2.pdf b/presentation/assets/fpga-expl2.pdf
new file mode 100644
index 0000000..97a5f12
--- /dev/null
+++ b/presentation/assets/fpga-expl2.pdf
diff --git a/presentation/assets/fpga.pdf b/presentation/assets/fpga.pdf
index 9e56964..e6af8e2 100644
--- a/presentation/assets/fpga.pdf
+++ b/presentation/assets/fpga.pdf
diff --git a/presentation/presentation.org b/presentation/presentation.org
index 2e8a18f..97d7baa 100644
--- a/presentation/presentation.org
+++ b/presentation/presentation.org
@@ -21,9 +21,49 @@ But:
 
 ** FPGA Layout
 
+#+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.
+
+*** Minipage
+:PROPERTIES:
+:BEAMER_ENV: minipage
+:BEAMER_OPT: 5cm
+:END:
+
+#+beamer: \centering
+#+beamer: \vspace{0.2em}
+
+**** Only 1
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: <1>
+:END:
+
+#+begin_export latex
+\includegraphics[width=8cm]{assets/fpga.pdf}
+#+end_export
+
+**** Only 2
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: <2>
+:END:
+
+#+begin_export latex
+\includegraphics[width=8cm]{assets/fpga-expl.pdf}
+#+end_export
+
+**** Only 3
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: <3>
+:END:
+
 #+begin_export latex
 \centering
-\includegraphics[width=7.5cm]{assets/fpga.pdf}
+\includegraphics[width=8cm]{assets/fpga-expl2.pdf}
 #+end_export
 
 ** So How do we Program an FPGA?
@@ -339,11 +379,9 @@ The representation of the *finite state-machine with datapath (FSMD)* is abstrac
 :BEAMER_env: blockNH
 :END:
 
-#+attr_latex: :options fontsize=\footnotesize
-#+begin_src coq
-Definition datapath := PTree.t Verilog.stmnt.
-Definition controllogic := PTree.t Verilog.stmnt.
-#+end_src
+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}$
 
 *** Module definition :B_blockNH:
 :PROPERTIES:
@@ -355,9 +393,8 @@ Definition controllogic := PTree.t Verilog.stmnt.
 #+attr_latex: :options fontsize=\footnotesize
 #+begin_src coq
 Record module: Type := mkmodule {
-    mod_datapath: datapath; mod_controllogic: controllogic;
-    mod_wf: map_well_formed mod_controllogic
-             /\ map_well_formed mod_datapath;
+    mod_datapath: datapath;
+    mod_controllogic: controllogic;
     mod_reset: reg;
     mod_ram: ram_spec;
     ...
@@ -654,42 +691,33 @@ endmodule
 #+attr_beamer: :overlay <+->
 - Verilog example for a simple shift register.
 - 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
+*** Only 1
 :PROPERTIES:
-:BEAMER_ENV: onlyenvNH
-:BEAMER_ACT: <1>
+:BEAMER_ENV: blockNH
+:BEAMER_ACT: <1->
 :END:
 
 #+begin_export latex
-\includegraphics[width=8cm]{assets/semantics_clk.pdf}
+{\centering\includegraphics[width=8cm]{assets/clk.pdf}\par}
 #+end_export
 
-**** Only 2
+*** Only 2
 :PROPERTIES:
-:BEAMER_ENV: onlyenvNH
+:BEAMER_ENV: blockNH
 :BEAMER_ACT: <2>
 :END:
 
+- At each clock tick, the *whole module* is executed using *big-step semantics*.
+
 #+begin_export latex
-\includegraphics[width=8cm]{assets/semantics.pdf}
+{\centering\includegraphics[width=6cm]{assets/big-step.pdf}\par}
 #+end_export
 
-
 ** How the Verilog semantics changed :noexport:
 
 Changed the semantics in *5* minor ways to make it a better HLS target.
@@ -802,7 +830,7 @@ This describes the main proof that is needed to show that the HLS tool is correc
 | Wrong      | Such as undefined behaviour, no guarantees need to be shown.     |
 |------------+------------------------------------------------------------------|
 
-**** Theorem :B_onlyenvNH:
+**** Theorem :B_onlyenvNH:noexport:
 :PROPERTIES:
 :BEAMER_env: onlyenvNH
 :BEAMER_ACT: <3>
@@ -928,6 +956,8 @@ 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
diff --git a/presentation/presentation.pdf b/presentation/presentation.pdf
index 0a3e687..a402eb5 100644
--- a/presentation/presentation.pdf
+++ b/presentation/presentation.pdf