Update the presentation

2 files changed, 90 insertions, 74 deletions

diff --git a/presentation/presentation.org b/presentation/presentation.org
index 3786da0..9465196 100644
--- a/presentation/presentation.org
+++ b/presentation/presentation.org
@@ -300,8 +300,6 @@ Use CompCert, a fully verified C compiler, and add an HLS backend.
 :BEAMER_ACT: <2>
 :END:
 
-Current progress: fully verified HLS tool for a subset of C.
-
 Support for: all *control flow*, *fixedpoint*, *non-recursive functions* and *local arrays/structs/unions*.
 
 * Example
@@ -370,7 +368,7 @@ main() {
 }
 #+end_src
 
-** Example: HTL Overview :noexport:
+** Example: HTL Overview
 
 The representation of the *finite state-machine with datapath (FSMD)* is abstract and called **HTL**.
 
@@ -411,8 +409,8 @@ Translation from *control-flow graph (CFG)* into a *finite state-machine with da
 #+attr_beamer: :overlay <+->
 - *Control-flow* is translated into a *finite state-machine*.
 - Each *3AC instructions* translated into equivalent *Verilog statements*.
-- Function *stack* implemented as *RAM*.
-- Pointers for loads and stores translated to RAM addresses.
+- Function *stack* implemented as *Verilog array*.
+- Pointers for loads and stores translated to array addresses.
   - *Byte* addressed to *word* addressed.
 
 #+beamer: \vspace{1em}
@@ -429,7 +427,7 @@ Translation from *control-flow graph (CFG)* into a *finite state-machine with da
 :BEAMER_ACT: 3
 :END:
 
-~x3 = x3 + x5 + 0~ $\quad\longrightarrow\quad$ ~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 + 32'd0}}}
 
 **** Only 2 :B_onlyenvNH:
 :PROPERTIES:
@@ -437,18 +435,16 @@ Translation from *control-flow graph (CFG)* into a *finite state-machine with da
 :BEAMER_ACT: 5-6
 :END:
 
-~x5 + x1 * 4 + 0~
-
-$\quad\longrightarrow\quad$ ~{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}~
+~x5 + x1 * 4 + 0~ $\quad\longrightarrow\quad$ src_verilog[:exports code]{{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}}
 
-** Example: Memory Inference Pass :noexport:
+** Example: Memory Inference Pass
 
 - An HTL $\rightarrow$ HTL translation removes loads and stores.
 - Replaced by accesses to a proper *RAM*.
 
 #+beamer: \vspace{1em}
 
-~stack[{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}]~
+src_verilog[:exports code]{stack[{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}]}
 
 #+beamer: \vspace{1em}
 
@@ -463,6 +459,69 @@ u_en <= ( ~ u_en); wr_en <= 32'd0;
 addr <= {{{reg_3 + 32'd0} + {reg_1 * 32'd4}} / 32'd4};
 #+end_src
 
+** Verilog Syntax
+
+*** Column 1 :B_column:
+:PROPERTIES:
+:BEAMER_COL: 0.45
+:END:
+
+**** No highlight :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <1>
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize
+#+begin_src verilog
+module top(input clk, input [31:0] in1,
+           output reg [31:0] out1);
+   reg [31:0] reg_1, tmp;
+
+   always @(posedge clk) begin
+      reg1 <= in1;
+   end
+
+   always @(posedge clk) begin
+      tmp = reg1;
+      out1 <= tmp;
+   end
+endmodule
+#+end_src
+
+**** Highlight :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <2>
+:END:
+
+#+attr_latex: :options highlightlines={5-7,9-12},fontsize=\footnotesize
+#+begin_src verilog
+module top(input clk, input [31:0] in1,
+           output reg [31:0] out1);
+   reg [31:0] reg_1, tmp;
+
+   always @(posedge clk) begin
+      reg1 <= in1;
+   end
+
+   always @(posedge clk) begin
+      tmp = reg1;
+      out1 <= tmp;
+   end
+endmodule
+#+end_src
+
+*** Column 2
+:PROPERTIES:
+:BEAMER_COL: 0.55
+:END:
+
+#+attr_beamer: :overlay <+->
+- Verilog example for a simple shift register.
+- Always block run in parallel
+
+
 ** Example: Translation (HTL $\rightarrow$ Verilog) :B_frame:
 
 *** Column
@@ -630,68 +689,6 @@ endmodule
 - Control logic is translated into another case statement with a reset.
 
 * Verification
-** Verilog Syntax
-
-*** Column 1 :B_column:
-:PROPERTIES:
-:BEAMER_COL: 0.45
-:END:
-
-**** No highlight :B_onlyenvNH:
-:PROPERTIES:
-:BEAMER_env: onlyenvNH
-:BEAMER_ACT: <1>
-:END:
-
-#+attr_latex: :options fontsize=\small
-#+begin_src verilog
-module top(input clk, input [31:0] in1,
-           output reg [31:0] out1);
-   reg [31:0] reg_1, tmp;
-
-   always @(posedge clk) begin
-      reg1 <= in1;
-   end
-
-   always @(posedge clk) begin
-      tmp = reg1;
-      out1 <= tmp;
-   end
-endmodule
-#+end_src
-
-**** Highlight :B_onlyenvNH:
-:PROPERTIES:
-:BEAMER_env: onlyenvNH
-:BEAMER_ACT: <2>
-:END:
-
-#+attr_latex: :options highlightlines={5-7,9-12},fontsize=\small
-#+begin_src verilog
-module top(input clk, input [31:0] in1,
-           output reg [31:0] out1);
-   reg [31:0] reg_1, tmp;
-
-   always @(posedge clk) begin
-      reg1 <= in1;
-   end
-
-   always @(posedge clk) begin
-      tmp = reg1;
-      out1 <= tmp;
-   end
-endmodule
-#+end_src
-
-*** Column 2
-:PROPERTIES:
-:BEAMER_COL: 0.55
-:END:
-
-#+attr_beamer: :overlay <+->
-- Verilog example for a simple shift register.
-- Always block run in parallel
-
 ** Verilog Semantics (Adapted from Lööw et al. (2019))
 
 - Top-level semantics are *small-step operational semantics*.
@@ -956,6 +953,25 @@ Prove the simulation diagram correct:
 - there exists 1 or more steps in Verilog,
 - such that after 1 step in 3AC, the resulting states match.
 
+** Main Challenges in Proof
+
+*** Translation of memory model
+:PROPERTIES:
+:BEAMER_ENV: block
+:BEAMER_ACT: <1->
+:END:
+
+*Abstract/infinite memory model* translated into *concrete/finite RAM*.
+
+*** Integration of Verilog Semantics
+:PROPERTIES:
+:BEAMER_ENV: block
+:BEAMER_ACT: <2->
+:END:
+
+- *Verilog semantics* differs from CompCert's main assumptions of intermediate language semantics.
+- Abstract values like the *program counter* now correspond to *values in registers*.
+
 * Results
 
 ** With Division approximately 27$\times$ slower
@@ -1117,7 +1133,7 @@ Fuzzed Vericert with Csmith to check correctness theorem.
 Written a formally verified high-level synthesis tool in *Coq* based on *CompCert*.
 
 #+attr_beamer: :overlay <+->
-- Base translation *proven correct* by proving translation of CFG into FSMD.
+- HLS tool *proven correct in Coq* by proving translation of CFG into FSMD.
 - Small optimisations implemented such as *Ram Inference*.
 - Performance without divisions comparable to LegUp without optimisations.
 
diff --git a/presentation/presentation.pdf b/presentation/presentation.pdf
index 74f3beb..b491429 100644
--- a/presentation/presentation.pdf
+++ b/presentation/presentation.pdf