Add initial files

10 files changed, 2927 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..347c527
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,15 @@
+.DS_Store
+.auctex-auto/
+_minted-*/
+
+*.aux
+*.vrb
+*.log
+*.nav
+*.out
+*.snm
+*.synctex.gz
+*.tex
+*.toc
+*.fdb_latexmk
+*.fls
diff --git a/beamercolorthemeauriga.sty b/beamercolorthemeauriga.sty
new file mode 100644
index 0000000..6c9cf63
--- /dev/null
+++ b/beamercolorthemeauriga.sty
@@ -0,0 +1,35 @@
+% Auriga theme
+% https://github.com/anishathalye/auriga
+
+% ====================
+% Definitions
+% ====================
+
+\definecolor{lightgray}{RGB}{245, 246, 250}
+\definecolor{darkgray}{RGB}{79,79,79}
+\definecolor{lightgreen}{HTML}{003E74}
+\definecolor{purple}{HTML}{751E66}
+\definecolor{brown}{HTML}{0F8291}
+
+% ====================
+% Theme
+% ====================
+
+% Basic colors
+\setbeamercolor{palette primary}{fg=black,bg=white}
+\setbeamercolor{palette secondary}{fg=black,bg=white}
+\setbeamercolor{palette tertiary}{bg=black,fg=white}
+\setbeamercolor{palette quaternary}{fg=black,bg=white}
+\setbeamercolor{structure}{fg=brown}
+
+\setbeamercolor{emph}{fg=lightgreen}
+\setbeamercolor{alerted text}{fg=purple}
+
+% Itemize
+\setbeamercolor{item}{fg=black}
+
+% Page numbering
+\setbeamercolor{page number in head/foot}{fg=lightgreen}
+
+% Frame titles
+\setbeamercolor{frametitle}{fg=black}
diff --git a/beamerthemeauriga.sty b/beamerthemeauriga.sty
new file mode 100644
index 0000000..e4b18e4
--- /dev/null
+++ b/beamerthemeauriga.sty
@@ -0,0 +1,127 @@
+% Auriga theme
+% https://github.com/anishathalye/auriga
+
+% ====================
+% Dependencies
+% ====================
+
+\RequirePackage{exscale}
+\RequirePackage{ragged2e}
+\RequirePackage{changepage}
+\RequirePackage{fontspec}
+\RequirePackage{xpatch}
+\RequirePackage{microtype}
+\RequirePackage{xparse}
+\RequirePackage{xspace}
+\RequirePackage{graphicx}
+
+% ====================
+% Fonts
+% ====================
+
+\newfontfamily\Raleway[Ligatures=TeX]{Raleway}
+\newfontfamily\Lato[Ligatures=TeX]{Lato}
+\newfontfamily\HKGrotesk[Ligatures=TeX]{HK Grotesk}
+
+\usefonttheme{professionalfonts}
+
+\setsansfont{HKGrotesk}[
+  UprightFont=*-Regular,
+  ItalicFont=*-Italic,
+  BoldFont=*-Bold,
+  BoldItalicFont=*-BoldItalic
+]
+
+\defaultfontfeatures{Ligatures=NoCommon}
+\setmonofont[Renderer=Basic]{Iosevka}
+
+\setbeamerfont{title page}{family=\Raleway}
+\setbeamerfont{title page title}{size=\LARGE,series=\bfseries}
+\setbeamerfont{title page subtitle}{size=\small}
+\setbeamerfont{title page author}{size=\footnotesize}
+\setbeamerfont{title page institute}{size=\scriptsize}
+\setbeamerfont{frametitle}{family=\Raleway,size=\large,series=\bfseries}
+\setbeamerfont{caption}{size=\Macros}
+
+% ====================
+% footnotesizeb
+% ====================
+
+\newcommand{\samelineand}{\qquad}
+
+% ====================
+% Elements
+% ====================
+
+% Itemize
+
+\setbeamertemplate{itemize item}[circle]
+\setbeamertemplate{itemize subitem}[circle]
+\setbeamertemplate{itemize subsubitem}[circle]
+%\xpatchcmd{\itemize}
+%  {\def\makelabel}
+%  {\ifnum\@itemdepth=1\relax
+%     \setlength\itemsep{3ex}% separation for first level
+%   \else
+%     \ifnum\@itemdepth=2\relax
+%       \setlength\itemsep{0.5ex}% separation for second level
+%     \else
+%       \ifnum\@itemdepth=3\relax
+%         \setlength\itemsep{0.5ex}% separation for third level
+%   \fi\fi\fi\def\makelabel
+%  }
+% {}
+% {}
+
+% Equation
+\setlength\belowdisplayshortskip{2ex}
+
+% Caption
+\setlength{\abovecaptionskip}{2ex}
+\setlength{\belowcaptionskip}{1ex}
+\setbeamertemplate{caption}
+{
+    {\usebeamerfont{caption}\insertcaption}
+}
+
+% Navigation
+\beamertemplatenavigationsymbolsempty
+
+% ====================
+% Components
+% ====================
+
+% Title page
+\setbeamertemplate{title page}
+{
+  \begin{centering}
+    \vskip5ex plus 1filll
+    {\usebeamerfont{title page title}\usebeamercolor[fg]{title page}\inserttitle\\[0.5ex]}
+    {\usebeamerfont{title page subtitle}\usebeamercolor[fg]{title page}\insertsubtitle\\[3ex]}
+    {\par\noindent\centering\color{lightgreen}\rule{350pt}{2pt}\\[3ex]}
+    {\usebeamerfont{title page author}\usebeamercolor[fg]{title page}\insertauthor\\[2ex]}
+    {\usebeamerfont{title page institute}\usebeamercolor[fg]{title page}\insertinstitute\\[1ex]}
+    \vskip0pt plus 1filll
+  \end{centering}
+  {\includegraphics[height=1cm]{./assets/imperial_logo.pdf}\hfill\includegraphics[height=1cm]{./assets/oopsla21.png}}
+}
+
+% Footer
+\setbeamertemplate{footline}{%
+    \hfill%
+    \usebeamercolor[fg]{page number in head/foot}%
+    \usebeamerfont{page number in head/foot}%
+    \hspace{2em}%
+    \insertframenumber\kern1em\vskip2ex%
+}
+
+% Frame title
+\setbeamertemplate{frametitle}{%
+    \nointerlineskip%
+    \vskip2ex%
+    {\usebeamerfont{frametitle}\usebeamercolor[fg]{frametitle}\insertframetitle\\[-2.5ex]}%
+    {\par\color{lightgreen}\rule{390pt}{2pt}}%
+}
+
+% Alert
+\setbeamerfont{alerted text}{series=\bfseries}
diff --git a/flashlight22.bib b/flashlight22.bib
new file mode 100644
index 0000000..11e20ad
--- /dev/null
+++ b/flashlight22.bib
@@ -0,0 +1,9 @@
+@inproceedings{9444067,
+  author={Herklotz, Yann and Du, Zewei and Ramanathan, Nadesh and Wickerson, John},
+  booktitle={2021 IEEE 29th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM)},
+  title={An Empirical Study of the Reliability of High-Level Synthesis Tools},
+  year={2021},
+  volume={},
+  number={},
+  pages={219-223},
+  doi={10.1109/FCCM51124.2021.00034}}
diff --git a/flashlight22.org b/flashlight22.org
new file mode 100644
index 0000000..ae68e33
--- /dev/null
+++ b/flashlight22.org
@@ -0,0 +1,185 @@
+#+title: Formal Verification of High-Level Synthesis
+#+author: \underline{Yann Herklotz}, John Wickerson
+#+options: H:2 toc:nil
+#+columns: %45ITEM %10BEAMER_ENV(Env) %10BEAMER_ACT(Act) %4BEAMER_COL(Col)
+#+setupfile: setup.org
+
+** Why HLS is unreliable
+** Small Introduction to Coq
+** Solution: Formally Verify HLS
+*** Vericert
+** Current Status of Vericert
+* Loop Pipelining
+** The Need for Loop Pipelining
+
+# - really useful, or you might say necessary optimisation that HLS performs.
+
+- Main difficulty with having hardware as a target is the need to pipeline loops.
+
+*** Column left
+:PROPERTIES:
+:BEAMER_COL: 0.45
+:END:
+
+#+attr_latex: :options fontsize=\small,escapeinside=||
+#+begin_src c
+for (int i = 0; i < N; i++) {
+|\sA{1}| x18 = i - 1
+|\sR{1}| x16 = load[1, x18 * 4]
+|\sM{1}| x8 = x16 * x1
+|\sR{2}| x12 = load[3, i * 4]
+|\sR{3}| x13 = load[2, i * 4]
+|\sM{2}| x7 = x12 * x13
+|\sA{2}| x11 = x8 + x7
+|\sW{1}| store[1, i * 4] = x11
+   i = i + 1
+}
+#+end_src
+
+*** Column right
+:PROPERTIES:
+:BEAMER_COL: 0.45
+:END:
+
+#+begin_export latex
+\begin{tikzpicture}[lnode/.style={circle,draw=black,minimum size=4mm,scale=0.8},nlabel/.style={midway,right
+,font=\tiny},node distance=1.3cm,shorten >=1pt]
+  \node[lnode,fill=s1col] (A1) {1};
+  \node[lnode,fill=s2col,below of=A1] (R1) {1};
+  \node[lnode,fill=s3col,below of=R1] (M1) {1};
+  \node[lnode,fill=s2col,right of=A1] (R2) {2};
+  \node[lnode,fill=s2col,right of=R2] (R3) {3};
+  \node[lnode,fill=s3col,below of=R2,xshift=0.7cm] (M2) {2};
+  \node[lnode,fill=s1col,below right of=M1,xshift=0.4cm] (A2) {2};
+  \node[lnode,fill=s4col,below of=A2] (W1) {1};
+
+  \draw[->,thick] (A1) -- (R1);
+  \draw[->,thick] (R1) -- node[nlabel] {2} (M1);
+  \draw[->,thick] (R2) -- node[nlabel] {2} (M2);
+  \draw[->,thick] (R3) -- node[nlabel] {2} (M2);
+  \draw[->,thick] (M1) -- (A2);
+  \draw[->,thick] (M2) -- (A2);
+  \draw[->,thick] (A2) -- (W1);
+  \draw[->,thick] (R1) to [out=220,in=180,loop,looseness=2] (W1);
+\end{tikzpicture}
+#+end_export
+
+** Ideas Behind Static Hardware Loop Pipelining
+
+*** One Possible Workflow
+
+- Generate scheduling constraints for linear code as well as loops.
+- Solve for a scheduling using an ILP solver.
+- Place the instructions into the cycle that it was assigned to.
+
+#+begin_export latex
+\begin{center}
+  \begin{tikzpicture}[lnode/.style={circle,draw=black,minimum size=4mm,scale=0.8},node
+    distance=1.3cm,shorten >=1pt]
+    \node[lnode,fill=s1col] (A1) {1}; \node[lnode,fill=s2col,below of=A1] (R2) {2};
+    \node[lnode,fill=s2col,below of=R2] (R3) {3}; \node[lnode,fill=s2col,right of=A1] (R1) {1};
+    \node[lnode,fill=s3col,right of=R1] (M2) {2}; \node[lnode,fill=s3col,right of=M2] (M1) {1};
+    \node[lnode,fill=s1col,right of=M1] (A2) {2}; \node[lnode,right of=A2] (E1) {};
+    \node[lnode,fill=s4col,right of=E1] (W1) {1}; \node[lnode,right of=W1] (E2) {}; \node[above
+    right of=R1,xshift=-0.35cm] (S1T) {}; \node[below of=S1T,yshift=-2.5cm] (S1B) {}; \draw[very
+    thick] (S1T) -- (S1B); \node[above right of=M1,xshift=-0.35cm] (S2T) {}; \node[below
+    of=S2T,yshift=-2.5cm] (S2B) {}; \draw[very thick] (S2T) -- (S2B); \node[above right
+    of=E1,xshift=-0.35cm] (S3T) {}; \node[below of=S3T,yshift=-2.5cm] (S3B) {}; \draw[very thick]
+    (S3T) -- (S3B);
+  \end{tikzpicture}
+\end{center}
+#+end_export
+
+** Verifying Hardware Pipelining is Difficult
+
+- Normally part of the scheduling step.
+- Lose control about how the loops are translated, the fundamental structure of the loop could
+  change and would be difficult to identify again.
+
+* Verifying Loop Pipelining
+** Ideas Behind Software Loop Pipelining
+
+*** Main Idea
+
+Can perform a source-to-source transformation which generates a pipeline purely in software.
+
+*** Column left
+:PROPERTIES:
+:BEAMER_COL: 0.45
+:END:
+
+#+attr_latex: :options fontsize=\small,escapeinside=||
+#+begin_src c
+for (int i = 0; i < N; i++) {
+|\sA{1}| x18 = i - 1
+|\sR{1}| x16 = load[1, x18 * 4]
+|\sM{1}| x8 = x16 * x1
+|\sR{2}| x12 = load[3, i * 4]
+|\sR{3}| x13 = load[2, i * 4]
+|\sM{2}| x7 = x12 * x13
+|\sA{2}| x11 = x8 + x7
+|\sW{1}| store[1, i * 4] = x11
+   i = i + 1
+}
+#+end_src
+
+*** Column right
+:PROPERTIES:
+:BEAMER_COL: 0.45
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,escapeinside=||
+#+begin_src c
+for (int i = 0; i < N; i++) {
+|\sA{1}| x18[i] = i - 1
+|\sR{2}| x12[i] = load[3, i * 4]
+|\sR{3}| x13[i] = load[2, i * 4]
+|\sM{2}| x7[i-1] = x12[i-1] * x13[i-1]
+|\sA{2}| x11[i-2] = x8[i-2] + x7[i-2]
+|\sW{1}| store[1, (i-3) * 4] = x11[i-3]
+
+|\sR{1}| x16[i] = load[1, x18[i] * 4]
+|\sM{1}| x8[i-1] = x16[i-1] * x1
+   i = i + 1
+}
+#+end_src
+
+** Verifying Software Loop Pipelining
+
+*** Symbolic Execution
+
+Define an $\alpha$, such that $\alpha(\mathcal{C})$ evaluates some code $\mathcal{C}$ and returns
+*symbolic states* for all registers.
+
+*** Example
+
+Executing the following code will evaluate to the following symbolic code:
+
+*** Column left
+:PROPERTIES:
+:BEAMER_COL: 0.45
+:END:
+
+
+
+*** Column right
+:PROPERTIES:
+:BEAMER_COL: 0.45
+:END:
+
+* Comparing Software and Hardware Loop Pipelining
+** Comparing Pipelines in Hardware and Software
+
+*** Pipelines can be identical
+
+- In terms of expressivity, both hardware and software pipelining can express the same loop
+  pipelines.
+
+** Resource Usage of Pipelines
+
+Naively, They will both contain
+
+* Wrapping up
+** Conclusion
+
+- To verify loop pipelines, it seems easier
diff --git a/notes.org b/notes.org
new file mode 100644
index 0000000..39e93f8
--- /dev/null
+++ b/notes.org
@@ -0,0 +1,52 @@
+Yes! It's loads better! I'm glad I made a fuss! :)
+
+Ok, lots of feedback below, but it's mostly low-level details now. Here goes...
+
+TALK 1: You say "formally verified" but the slide says "formal verification of" which is a bit jarring.
+
+TALK 3: Don't start with "So...". Just launch straight in with "The need for...". (I'm getting such deja
+vu from 2012-ish when I was given exactly the same advice when giving a practice talk for a
+fellowship interview. I started with "So..." and was immediately heckled for it!)
+
+TALK 3: I like the SSD/SSD/HDD example. It's nifty. And perfectly understandable too. I think there
+are one or two bits that could still be slightly optimised, for instance, you say "It will always
+perform the same task" and then "which would always do the same task" a few moments later.
+
+TALK 5: The .v -> FPGA diagram is very good -- I would just change your words from "use logic synthesis"
+to "use a logic synthesis tool" to emphasise that it's not a manual process.
+
+6: The text about "difficult to debug" appears too soon. I found myself reading the text and being a
+bit confused because it didn't match what you were saying. Only introduce the text at the moment you
+talk about it. Same happens on slide 16 -- the diagram appears a few seconds too soon and it
+distracts me from what you're saying.
+
+TALK 7: "we're gonna call 3AC [because RTL is already an established abbreviation in hardware design]"
+
+TALK 14: I still think there's an opportunity for a little bit of humour/showmanship when you make the
+point about the RAM interface. For instance, you could say something like "Actually here is a mildly
+terrifying example of quite how fragile the logic synthesis tools are -- if the RAM interface
+doesn't use this _exact_ Verilog syntax, then the tool won't know to use RAM and will synthesise
+thousands of registers instead, and the circuit will be disastrously inefficient."
+
+TODO 17: Similar comment as before: I recommend making sure that each piece of text only appears at
+the instant you talk about it. Currently I'm reading about "Wrong" while you're talking about
+"Converging" and that's not ideal :)
+
+TALK 20: I like the addition of "bad news" -- that's really helpful for telling the audience how to
+interpret this slide. I suggest beginning this slide by saying which benchmarks you use (and why)
+and emphasise that you can compile almost all of them. And then, when you show the graphs, you need
+to give a bit of time for them to be digested. You were talking about interpreting the results, but
+I was still trying to read the labels on the y-axes. You need to say what the top and bottom graphs
+are showing, say what the three colours of bar mean, whether higher bars are good or bad (and say
+things like "we see that the green bars really high, and way higher than the others"), and say that
+the x-axis shows all 27 benchmarks plus the median. I think you need to spend a good 2 minutes on
+this slide alone.
+
+TALK 22: Rather than "0% (0.03%)", I suggest showing "0.03%" first, explaining what's going on, and
+then striking it out and writing "0%", so the end result looks like ^0.03%^ 0%. (As for Bambu, I'd
+be tempted to drop the 13.7% point altogether, as it's an unnecessary detail. (Let's just be kind to
+them!)) And I'd encourage a little bit of showmanship here -- you could put the "Vericert" text in
+first, leaving the number blank, and then say something "and of course, since this is all proven in
+Coq we'd expect a nice 'zero percent' here...[then introduce the 0.03%]...well ok, that's not quite
+how it worked out at first...but what happened was...". And I'd mention that this is exactly what
+happened when the Csmith people fuzzed CompCert for the first time.
diff --git a/outline.org b/outline.org
new file mode 100644
index 0000000..3d7470e
--- /dev/null
+++ b/outline.org
@@ -0,0 +1,9 @@
+#+title: Outline
+
+For the presentation at chalmers, I will in general want the following outline:
+
+* Background
+
+The background that I need to introduce is: What is HLS, and what is CompCert.
+
+*
diff --git a/pipeline.sv b/pipeline.sv
new file mode 100644
index 0000000..7c7c27c
--- /dev/null
+++ b/pipeline.sv
@@ -0,0 +1,68 @@
+module ram(clk, addr, idata, wr_en, odata);
+   input logic         clk;
+   input logic [31:0]  addr;
+   input logic [31:0]  idata;
+   input logic         wr_en;
+
+   output logic [31:0] odata;
+
+   logic [31:0]        ram [9:0];
+
+   always @(posedge clk) begin
+      if (wr_en) begin
+         ram[addr] <= idata;
+      end
+   end
+
+   assign odata = ram[addr];
+endmodule
+
+module pipeline(valid, clk, x1, x6, fin, val);
+   input logic         start;
+   input logic         clk;
+   input logic [31:0]  x1;
+   input logic [31:0]  x6;
+
+   output logic        fin;
+   output logic [31:0] val;
+
+   logic [31:0]        x18, x16, x8, x12, x13, x7, x11;
+
+   logic [1:0]         state;
+
+   logic [31:0]        ram1 [9:0];
+   logic [31:0]        ram2 [9:0];
+   logic [31:0]        ram3 [9:0];
+
+   parameter           IDLE   = 0;
+   parameter           STATE1 = 1;
+   parameter           STATE2 = 2;
+
+   initial begin
+      state = IDLE;
+   end
+
+   always @(posedge clk) begin
+      case(state)
+        IDLE: begin
+           if (start) state <= STATE1;
+        end
+        STATE1: state <= STATE2;
+        STATE2: state <= STATE1;
+      endcase
+   end
+
+   always @(posedge clk) begin
+      if (state == STATE1) begin
+         x18 <= x6 - 1;
+         x12 <= ram2[x6];
+         x13 <= ram3[x6];
+      end
+   end
+
+   always @(posedge clk) begin
+      if (state == STATE2) begin
+         x16 <= ram1[x18];
+      end
+   end
+endmodule
diff --git a/presentation.org b/presentation.org
new file mode 100644
index 0000000..2f383c0
--- /dev/null
+++ b/presentation.org
@@ -0,0 +1,2373 @@
+#+title: Formal Verification of High-Level Synthesis
+#+author: \underline{Yann Herklotz}, John Wickerson
+#+options: H:2 toc:nil
+#+columns: %45ITEM %10BEAMER_ENV(Env) %10BEAMER_ACT(Act) %4BEAMER_COL(Col)
+#+setupfile: setup.org
+
+** Script for start :noexport:
+
+Hi, I'm Yann and I will be presenting our work on formal verification of high-level synthesis.
+
+Hardware accelerators are becoming increasingly more popular in many industries, because using a CPU
+for those tasks is often unnecessary.  For example, a datacenter might have a CPU organising
+accesses to various SSDs or harddrives.  However, this does not benefit from the flexibility of the
+CPU, and would therefore result in increased latency for requests, as well as increased power
+consumption.  Instead, one would ideally like to have a application-specific integrated circuit that
+only does one task, thereby using up less power and probably being more performant at that task.
+However, until recently, designing a special chip for each application is expensive.  This is where
+FPGAs come in, whose main benefit is that their circuit can be reprogrammed at any time.
+
+** The Need to Design Hardware Accelerators
+
+Application-specific hardware accelerators are increasingly being needed in industries.
+
+*** Column 1
+:PROPERTIES:
+:BEAMER_ENV: column
+:BEAMER_COL: 0.5
+:END:
+
+#+attr_beamer: :overlay <+->
+- Using a *CPU* everywhere not always the best choice.
+- *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:
+:BEAMER_ENV: column
+:BEAMER_COL: 0.5
+:END:
+
+**** Minipage
+:PROPERTIES:
+:BEAMER_ENV: minipage
+:BEAMER_OPT: 5cm
+:END:
+
+#+beamer: \vspace{2em}
+
+***** Only 1
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: 1
+:END:
+
+#+begin_export latex
+\includegraphics[width=6cm]{assets/database-cpu.pdf}
+#+end_export
+
+***** Only 2
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+: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
+\includegraphics[width=6cm]{assets/database-fpga.pdf}
+#+end_export
+
+** Where does the flexibility of FPGAs come from?
+
+#+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*.
+- *RAMs* 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=8cm]{assets/fpga-expl2.pdf}
+#+end_export
+
+** So How do we Program an FPGA?
+
+*** Code example :B_column:
+:PROPERTIES:
+:BEAMER_ENV: column
+: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>
+: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>
+: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.5
+:END:
+
+**** Minipage
+:PROPERTIES:
+:BEAMER_ENV: minipage
+:BEAMER_OPT: 5cm
+:END:
+***** FPGA
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: <1>
+:END:
+
+#+begin_export latex
+\includegraphics[width=6.8cm]{assets/fpga-flow.pdf}
+#+end_export
+
+***** Verilog
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: <2>
+:END:
+
+#+begin_export latex
+\includegraphics[width=6.8cm]{assets/verilog-flow.pdf}
+#+end_export
+
+***** Verilog Simulation
+:PROPERTIES:
+:BEAMER_ENV: onlyenvNH
+:BEAMER_ACT: <3>
+:END:
+
+#+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:
+:BEAMER_ENV: definition
+:END:
+
+Translation of a high-level programming language such as C/C++ into a hardware description language (HDL) such as Verilog.
+
+*** Benefits of HLS :B_blockNH:
+:PROPERTIES:
+:BEAMER_env: block
+:BEAMER_ACT: <2->
+:END:
+
+- *Usability*: Use software ecosystem.
+- *Speed*: Quickly design hardware.
+
+*** Trade-offs of HLS
+:PROPERTIES:
+:BEAMER_ENV: block
+:BEAMER_ACT: <3->
+:END:
+
+- *Performance*: Requires automatic parallelisation.
+- *Correctness*: Hard to verify generated HDL.
+
+** Motivation for Formal Verification
+
+*** HLS Unreliable :B_blockNH:
+:PROPERTIES:
+:BEAMER_env: blockNH
+:END:
+
+High-level synthesis is often quite unreliable:
+
+- We fuzzed HLS tools (Herklotz et al. [2021]) and found they failed on simple random test cases.
+
+#+beamer: \vspace{2em}
+
+#+attr_latex: :booktabs t
+|-----------------+-----------------|
+| Tool            | Run-time errors |
+|-----------------+-----------------|
+| Vivado HLS      |           1.23% |
+| Intel i++       |            0.4% |
+| Bambu 0.9.7-dev |            0.3% |
+| LegUp 4.0       |            0.1% |
+|-----------------+-----------------|
+
+** Solution :B_frame:
+:PROPERTIES:
+:BEAMER_env: frame
+:BEAMER_OPT: t
+:END:
+
+#+begin_export latex
+\definecolor{compcert}{HTML}{bebada}
+\definecolor{formalhls}{HTML}{8dd3c7}
+\begin{center}
+  \begin{tikzpicture}
+    [language/.style={fill=white,rounded corners=3pt,minimum height=7mm},
+    continuation/.style={},
+    linecount/.style={rounded corners=3pt,dashed},scale=0.8]
+    \fill[compcert,rounded corners=3pt] (-1.2,-0.5) rectangle (14,2);
+    \fill[formalhls,rounded corners=3pt] (-1.2,-1) rectangle (14,-2.4);
+    %\draw[linecount] (-0.95,-0.45) rectangle (3.6,1);
+    %\draw[linecount] (4,-0.45) rectangle (7.5,1);
+    \node[language] at (-0.3,0) (clight) {Clight};
+    \node[continuation] at (1.5,0) (conta) {$\cdots$};
+    \node[language] at (3.5,0) (cminor) {CminorSel};
+    \node[language] at (6,0) (rtl) {3AC};
+    \node[language] at (8,0) (ltl) {LTL};
+    \node[language,anchor=west] at (11.5,0) (aarch) {aarch64};
+    \node[language,anchor=west] at (11.5,0.8) (x86) {x86};
+    \node[continuation,anchor=west] at (11.5,1.4) (backs) {$\cdots$};
+    \node[continuation] at (10,0) (contb) {$\cdots$};
+    \node[language] at (6,-1.5) (htl) {HTL};
+    \node[language] at (9,-1.5) (verilog) {Verilog};
+    \node[anchor=west] at (-0.9,1.6) {\bf CompCert};
+    \node[anchor=west] at (-0.9,-1.4) {\bf Vericert};
+    %%\node[anchor=west] at (-0.9,0.7) {\small $\sim$ 27 kloc};
+    %%\node[anchor=west] at (4.1,0.7) {\small $\sim$ 46 kloc};
+    %%\node[anchor=west] at (2,-1.5) {\small $\sim$ 17 kloc};
+    \node[align=center] at (4,-2) {\footnotesize RAM\\[-0.5em]\footnotesize insertion};
+    \draw[->,thick] (clight) -- (conta);
+    \draw[->,thick] (conta) -- (cminor);
+    \draw[->,thick] (cminor) -- (rtl);
+    \draw[->,thick] (rtl) -- (ltl);
+    \draw[->,thick] (ltl) -- (contb);
+    \draw[->,thick] (contb) -- (aarch);
+    \draw[->,thick] (contb) to [out=0,in=200] (x86.west);
+    \draw[->,thick] (contb) to [out=0,in=190] (backs.west);
+    \draw[->,thick] (rtl) -- (htl);
+    \draw[->,thick] (htl) -- (verilog);
+    \draw[->,thick] (htl.west) to [out=180,in=150] (5,-2.2) to [out=330,in=270] (htl.south);
+  \end{tikzpicture}%}
+\end{center}
+#+end_export
+
+#+beamer: \vspace{1em}
+
+*** Minipage
+:PROPERTIES:
+:BEAMER_ENV: minipage
+:BEAMER_OPT: 5cm
+:END:
+
+**** Block 1 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <1>
+:END:
+
+Use CompCert, a fully verified C compiler, and add an HLS backend.
+
+**** Block 2 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <2>
+:END:
+
+Support for: all *control flow*, *fixedpoint*, *non-recursive functions* and *local arrays/structs/unions*.
+
+* Example
+** Example: 3AC :B_frame:
+
+*** Code example :B_column:
+:PROPERTIES:
+:BEAMER_ENV: column
+:BEAMER_COL: 0.45
+:END:
+
+**** Code 1 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_ACT: <1>
+:BEAMER_env: onlyenvNH
+:END:
+
+#+begin_src C
+int main() {
+    int x[2] = {3, 6};
+    int i = 1;
+    return x[i];
+}
+#+end_src
+
+**** Explanation 5 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <2>
+:END:
+
+- *Three address code (3AC)* instructions are represented as a control-flow graph (CFG).
+- Each instruction links to the next one.
+
+*** Text :B_column:
+:PROPERTIES:
+:BEAMER_ENV: column
+:BEAMER_COL: 0.45
+:END:
+
+**** Text 1 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_ACT: <1>
+:BEAMER_ENV: onlyenvNH
+:END:
+
+- Example of a very simple program performing loads and stores.
+
+**** 3AC Code 5 :B_onlyenv:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <2>
+:END:
+
+#+attr_latex: :options fontsize=\small
+#+begin_src C
+main() {
+    x5 = 3
+    int32[stack(0)] = x5
+    x4 = 6
+    int32[stack(4)] = x4
+    x1 = 1
+    x3 = stack(0) (int)
+    x2 = int32[x3 + x1 * 4 + 0]
+    return x2
+}
+#+end_src
+
+** HTL Overview
+
+The representation of the *finite state-machine with datapath* is abstract and called **HTL**.
+
+*** Datapath and control logic :B_blockNH:
+:PROPERTIES:
+:BEAMER_env: blockNH
+:END:
+
+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}$
+
+*** Minipage
+:PROPERTIES:
+:BEAMER_ENV: minipage
+:BEAMER_OPT: 5cm
+:END:
+
+**** Module definition :B_blockNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 2
+:END:
+
+#+beamer: \vspace{0.25em}
+
+#+attr_latex: :options fontsize=\footnotesize
+#+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: 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*.
+
+#+beamer: \pause
+#+beamer: \vspace{1em}
+
+#+attr_beamer: :overlay <+->
+- *Control-flow* is translated into a *finite state-machine*.
+- Each *3AC instructions* translated into equivalent *Verilog statements*.
+- Call *stack* implemented as *Verilog array*.
+- Pointers for loads and stores translated to array addresses.
+  - *Byte* addressed to *word* addressed.
+
+#+beamer: \vspace{1em}
+
+*** Minipage :B_minipage:noexport:
+:PROPERTIES:
+:BEAMER_env: minipage
+:BEAMER_OPT: 5cm
+:END:
+
+**** Only 1 :B_onlyenvNH:noexport:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 3
+:END:
+
+~x3 = x3 + x5 + 0~ $\quad\longrightarrow\quad$ src_verilog[:exports code]{reg_3 <= {reg_3 + {reg_5 + 0}}}
+
+**** Only 2 :B_onlyenvNH:noexport:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 5-6
+:END:
+
+~x5 + x1 * 4 + 0~ $\quad\longrightarrow\quad$ src_verilog[:exports code]{{{{reg_5 + 0} + {reg_1 * 4}} / 4}}
+
+** 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 / 4]}
+
+#+beamer: \vspace{1em}
+
+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 <= 0;
+addr <= reg_5 / 4;
+#+end_src
+
+***** 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:
+: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
+
+
+** Translation (HTL $\rightarrow$ Verilog) :B_frame:
+
+*** Column
+:PROPERTIES:
+:BEAMER_COL: 0.45
+:END:
+
+**** Code 1 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <1>
+:END:
+
+#+attr_latex: :options fontsize=\tiny
+#+begin_src verilog
+module main(reset, clk, finish, return_val);
+  input [0:0] reset, clk;
+  output reg [0:0] finish = 0;
+  output reg [31:0] return_val = 0;
+  reg [31:0] reg_3 = 0, addr = 0, d_in = 0,
+             reg_5 = 0, wr_en = 0,
+             state = 0, reg_2 = 0,
+             reg_4 = 0, d_out = 0, reg_1 = 0;
+  reg [0:0] en = 0, u_en = 0;
+  reg [31:0] stack [1:0];
+  // RAM interface
+  always @(negedge clk)
+    if ({u_en != en}) begin
+      if (wr_en) stack[addr] <= d_in;
+      else d_out <= stack[addr];
+      en <= u_en;
+    end
+#+end_src
+
+**** Code 2 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <2>
+:END:
+
+#+attr_latex: :options fontsize=\tiny,highlightlines={11-17}
+#+begin_src verilog
+module main(reset, clk, finish, return_val);
+  input [0:0] reset, clk;
+  output reg [0:0] finish = 0;
+  output reg [31:0] return_val = 0;
+  reg [31:0] reg_3 = 0, addr = 0, d_in = 0,
+             reg_5 = 0, wr_en = 0,
+             state = 0, reg_2 = 0,
+             reg_4 = 0, d_out = 0, reg_1 = 0;
+  reg [0:0] en = 0, u_en = 0;
+  reg [31:0] stack [1:0];
+  // RAM interface
+  always @(negedge clk)
+    if ({u_en != en}) begin
+      if (wr_en) stack[addr] <= d_in;
+      else d_out <= stack[addr];
+      en <= u_en;
+    end
+#+end_src
+
+**** Code 3 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <3>
+:END:
+
+#+attr_latex: :options fontsize=\tiny
+#+begin_src verilog
+  // Data-path
+  always @(posedge clk)
+    case (state)
+      32'd11: reg_2 <= d_out;
+      32'd8: reg_5 <= 32'd3;
+      32'd7: begin
+        u_en <= ( ~ u_en); wr_en <= 32'd1;
+        d_in <= reg_5; addr <= 32'd0;
+      end
+      32'd6: reg_4 <= 32'd6;
+      32'd5: begin
+        u_en <= ( ~ u_en); wr_en <= 32'd1;
+        d_in <= reg_4; addr <= 32'd1;
+      end
+      32'd4: reg_1 <= 32'd1;
+      32'd3: reg_3 <= 32'd0;
+      32'd2: begin
+        u_en <= ( ~ u_en); wr_en <= 32'd0;
+        addr <= {{{reg_3 + 32'd0} + {reg_1 * 32'd4}} / 32'd4};
+      end
+      32'd1: begin finish = 32'd1; return_val = reg_2; end
+      default: ;
+    endcase
+#+end_src
+
+**** Code 4 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <4>
+:END:
+
+#+attr_latex: :options fontsize=\tiny,highlightlines={7,8,12,13,18,19}
+#+begin_src verilog
+  // Data-path
+  always @(posedge clk)
+    case (state)
+      32'd11: reg_2 <= d_out;
+      32'd8: reg_5 <= 32'd3;
+      32'd7: begin
+        u_en <= ( ~ u_en); wr_en <= 32'd1;
+        d_in <= reg_5; addr <= 32'd0;
+      end
+      32'd6: reg_4 <= 32'd6;
+      32'd5: begin
+        u_en <= ( ~ u_en); wr_en <= 32'd1;
+        d_in <= reg_4; addr <= 32'd1;
+      end
+      32'd4: reg_1 <= 32'd1;
+      32'd3: reg_3 <= 32'd0;
+      32'd2: begin
+        u_en <= ( ~ u_en); wr_en <= 32'd0;
+        addr <= {{{reg_3 + 32'd0} + {reg_1 * 32'd4}} / 32'd4};
+      end
+      32'd1: begin finish = 32'd1; return_val = reg_2; end
+      default: ;
+    endcase
+#+end_src
+
+**** Code 5 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <5>
+:END:
+
+#+attr_latex: :options fontsize=\tiny
+#+begin_src verilog
+  // Control logic
+  always @(posedge clk)
+    if ({reset == 32'd1}) state <= 32'd8;
+    else case (state)
+           32'd11: state <= 32'd1;        32'd4: state <= 32'd3;
+           32'd8: state <= 32'd7;         32'd3: state <= 32'd2;
+           32'd7: state <= 32'd6;         32'd2: state <= 32'd11;
+           32'd6: state <= 32'd5;         32'd1: ;
+           32'd5: state <= 32'd4;         default: ;
+         endcase
+endmodule
+#+end_src
+
+*** Text
+:PROPERTIES:
+:BEAMER_COL: 0.45
+:END:
+
+**** Text 1 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_ACT: <1-5>
+:BEAMER_env: onlyenvNH
+:END:
+
+#+attr_beamer: :overlay <+->
+- 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.
+- Control logic is translated into another case statement with a reset.
+
+* Verification
+** Verilog Semantics (Adapted from Lööw et al. (2019))
+
+- Top-level semantics are *small-step operational semantics*.
+
+*** Only 1
+:PROPERTIES:
+:BEAMER_ENV: blockNH
+:BEAMER_ACT: <1->
+:END:
+
+#+begin_export latex
+{\centering\includegraphics[width=8cm]{assets/clk.pdf}\par}
+#+end_export
+
+*** Only 2
+:PROPERTIES:
+:BEAMER_ENV: blockNH
+:BEAMER_ACT: <2>
+:END:
+
+- At each clock tick, the *whole module* is executed using *big-step semantics*.
+
+#+begin_export latex
+{\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.
+
+#+attr_beamer: :overlay <+->
+- Verilog *2D array support*,
+- add *negative edge* support,
+- add support for *declarations*,
+- *removed* support for *external IO*, and
+- *simplifying* support for *bitvectors*.
+
+#+beamer: \vspace{1em}
+
+*** Minipage :B_minipage:
+:PROPERTIES:
+:BEAMER_env: minipage
+:BEAMER_OPT: 5cm
+:END:
+
+**** Only 1 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 1
+:END:
+
+#+attr_latex: :options fontsize=\small
+#+begin_src verilog
+reg [31:0] x[1:0];
+always @(posedge clk) begin x[0] = 1; x[1] <= 1; end
+#+end_src
+
+**** Only 2 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 2
+:END:
+
+#+begin_export latex
+\begin{equation*}
+\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{equation*}
+#+end_export
+
+**** Only 3 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 3
+:END:
+
+Have an association map for each register to declaration.
+
+- Information about input or output.
+- Information about size.
+
+**** Only 4 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 4
+:END:
+
+Constant inputs and outputs modelling the HLS interface.
+
+**** Only 5 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 5
+:END:
+
+Use integers modulo $2^n$.
+
+Those are the only types needed for HLS.
+
+** How do we prove the HLS tool correct? :noexport:
+
+*** Notes
+:PROPERTIES:
+:BEAMER_ENV: note
+:END:
+
+This describes the main proof that is needed to show that the HLS tool is correct.  I should probably be spending most of my time on this section, as that is what George will be most unfamiliar with.
+
+*** Text 1 :B_blockNH:
+:PROPERTIES:
+:BEAMER_env: blockNH
+:END:
+
+#+beamer: \vspace{-1.5em}
+
+- We have an *algorithm* describing the *translation*.
+- Have to *prove* that it does not change *behaviour* with respect to our language semantics.
+
+*** Minipage :B_minipage:
+:PROPERTIES:
+:BEAMER_env: minipage
+:BEAMER_OPT: 5cm
+:END:
+
+**** Table :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <2>
+:END:
+
+#+attr_latex: :booktabs t :align cp{10cm}
+|------------+------------------------------------------------------------------|
+| Behaviour  | Guarantee                                                        |
+|------------+------------------------------------------------------------------|
+| Converging | Means a result is obtained, Verilog and C results must be equal. |
+| Diverging  | C is in an infinite loop, Verilog must execute indefinitely.     |
+| Wrong      | Such as undefined behaviour, no guarantees need to be shown.     |
+|------------+------------------------------------------------------------------|
+
+**** Theorem :B_onlyenvNH:noexport:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <3>
+:END:
+
+***** Main Backward Simulation :B_theorem:
+:PROPERTIES:
+:BEAMER_env: theorem
+:END:
+
+#+begin_export latex
+\begin{equation*}
+  \forall C, V, B,\quad \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land \mathit{Safe}(C) \implies (V \Downarrow B \implies C \Downarrow B).
+\end{equation*}
+#+end_export
+
+where
+
+#+begin_export latex
+\begin{equation*}
+  \mathit{Safe}(C):\ \forall B,\ C \Downarrow B \implies B \in \texttt{Safe}
+\end{equation*}
+#+end_export
+
+**** Theorem :B_onlyenvNH:noexport:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <4->
+:END:
+
+***** Forward Simulation :B_theorem:
+:PROPERTIES:
+:BEAMER_env: theorem
+:END:
+
+#+begin_export latex
+\begin{align*}
+  &(\forall C, V, B \in \texttt{Safe},\quad \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land C \Downarrow B \implies V \Downarrow B)\\
+&\land (\forall V, B_1, B_2,\quad V \Downarrow B_1 \land V \Downarrow B_2 \implies B_1 = B_2).
+\end{align*}
+#+end_export
+
+** 3AC $\to$ HTL: Build a Specification :noexport:
+
+Assuming $\yhfunction{HLS} (C) = \yhconstant{OK} (V)$ requires reasoning about implementation details.
+
+#+beamer: \pause
+#+beamer: \vspace{1em}
+
+Instead we build a model of the translation which we can use.
+
+#+begin_export latex
+\begin{equation*}
+  \forall C, V,\quad \yhfunction{HLS} (C) = \yhconstant{OK} (V) \rightarrow \yhfunction{tr\_hls}\ \ C\ \ V.
+\end{equation*}
+#+end_export
+
+#+beamer: \pause
+
+*** 3AC to HTL operator conversion :B_example:
+:PROPERTIES:
+:BEAMER_env: example
+:BEAMER_ACT: <2->
+:END:
+
+#+begin_export latex
+\begin{equation*}
+  \inferrule[Iop]{\yhfunction{tr\_op } \mathit{op}\ \vec{a} = \yhconstant{OK } e}{\yhfunction{tr\_instr}\ \mathit{fin}\ \mathit{rtrn}\ \sigma\ \mathit{stk}\ (\yhconstant{Iop}\ \mathit{op}\ \vec{a}\ d\ n)\ (d \Leftarrow e)\ (\sigma \Leftarrow n)}
+\end{equation*}
+#+end_export
+
+** 3AC $\to$ HTL: Prove Forward Simulation :noexport:
+
+*** Column 1
+:PROPERTIES:
+:BEAMER_COL: 0.35
+:END:
+
+#+begin_export latex
+\definecolor{highlightcol}{HTML}{db6060}
+\begin{center}
+  \begin{tikzpicture}
+    \begin{scope}
+      \node[circle,minimum size=2] (s1) at (0,3) {$S_{1}$};%
+      \only<2>{\node[circle,minimum size=2] (s1) at (0,3) {\textcolor{highlightcol}{$S_{1}$}};}
+      \node[circle,minimum size=2] (r1) at (4,3) {$R_{1}$};%
+      \only<2-3>{\node[circle,minimum size=2] (r1) at (4,3) {\textcolor{highlightcol}{$R_{1}$}};}
+      \node[circle,minimum size=2] (s2) at (0,0) {$S_{2}$};%
+      \only<4>{\node[circle,minimum size=2] (s2) at (0,0) {\textcolor{highlightcol}{$S_{2}$}};}
+      \node[circle,minimum size=2] (r2) at (4,0) {$R_{2}$};%
+      \only<3-4>{\node[circle,minimum size=2] (r2) at (4,0) {\textcolor{highlightcol}{$R_{2}$}};}
+      \draw (s1) -- node[above] {\textasciitilde{}} node[below] {\small\texttt{match\_states}} ++ (r1);
+      \only<2>{\draw[highlightcol] (s1) -- node[above] {\textasciitilde{}} node[below] {\small\texttt{match\_states}} ++ (r1);}
+      \draw[-{Latex[length=3mm]}] (s1) -- (s2);
+      \draw[dashed] (s2) -- node[above] {\textasciitilde{}} node[below] {\small\texttt{match\_states}} ++ (r2);%
+      \only<4>{\draw[highlightcol,dashed] (s2) -- node[above] {\textasciitilde{}} node[below] {\small\textcolor{highlightcol}{\texttt{match\_states}}} ++ (r2);}
+      \draw[-{Latex[length=3mm]},dashed] (r1) -- node[left] {+} ++ (r2);%
+      \only<3>{\draw[highlightcol,-{Latex[length=3mm]},dashed] (r1) -- node[left] {+} ++ (r2);}
+    \end{scope}
+  \end{tikzpicture}
+\end{center}
+#+end_export
+
+*** Column 2
+:PROPERTIES:
+:BEAMER_COL: 0.6
+:END:
+
+\texttt{match\_states} defined as:
+
+#+begin_export latex
+\begin{equation*}
+  \mathcal{I} \land R \le \Gamma \land M \le \Gamma ! \mathit{stk} \land \mathit{pc} = \Gamma ! \sigma
+\end{equation*}
+#+end_export
+
+Prove the simulation diagram correct:
+
+#+beamer: \pause
+
+#+attr_beamer: :overlay <+->
+- Assuming an initial match between the 3AC state $S_1$ and Verilog state $R_1$,
+- 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*.
+
+* Extensions
+** Current work
+
+Many optimisations missing:
+
+- *scheduling*
+- *if-conversion*
+- memory partitioning
+- *loop pipelining*
+- polyhedral analysis
+- operation chaining
+- register allocation
+
+** New languages for scheduling
+
+Currently implemented two new languages for it:
+
+- ~3ACBlock~ :: 3AC with basic blocks.
+- ~3ACPar~ :: 3AC with basic blocks made up of parallel constructs.
+
+#+beamer: \vspace{1.5em}
+
+*** Minipage :B_minipage:
+:PROPERTIES:
+:BEAMER_env: minipage
+:BEAMER_OPT: 10cm
+:END:
+
+**** 3ACBlock Basic Block
+:PROPERTIES:
+:BEAMER_ACT: 2
+:BEAMER_env: onlyenv
+:END:
+
+#+begin_src coq
+Record bblock: Type := mk_bblock {
+  bb_body: list instr;
+  bb_exit: cf_instr
+}.
+#+end_src
+
+**** Instructions :B_onlyenv:
+:PROPERTIES:
+:BEAMER_ACT: 3
+:BEAMER_env: onlyenv
+:END:
+
+#+begin_src coq
+Inductive instr: Type :=
+| RBnop: instr
+| RBop: option pred_op -> operation -> list reg -> reg -> instr
+| RBload: option pred_op -> memory_chunk -> addressing
+           -> list reg -> reg -> instr
+| RBstore: option pred_op -> memory_chunk -> addressing
+            -> list reg -> reg -> instr
+| RBsetpred: condition -> list reg -> predicate -> instr.
+#+end_src
+
+** More details of transformations
+
+#+begin_export latex
+\scalebox{0.8}{\begin{tikzpicture}
+  \begin{scope}
+    \node[draw,minimum width=3cm,minimum height=1cm,align=center] (imstranslation) at (1.5,2) {\small\texttt{\textcolor{functioncolour}{Iterative Modulo}}\\\small\texttt{\textcolor{functioncolour}{Scheduling}}};
+    \node[draw,ellipse] (input) at (-1.5,2) {\small\texttt{3ACBlock}};
+    \node[draw,ellipse] (output) at (5,2) {\small\texttt{3ACBlock}};
+    \draw[->] (input) -- (imstranslation);
+    \draw[->] (imstranslation) -- (output);
+      \visible<2->{\node[draw,minimum width=3cm,minimum height=1cm,align=center] (verification) at (1.5,0.5) {\small Equivalence\\\small Check};%
+      \draw[->] (input) |- (verification);%
+      \draw[->] (output) |- (verification);%
+      \node[draw,ellipse] (error) at ($(verification.south) - (0.5,1.5)$) {\small\texttt{\textcolor{constantcolour}{Error}}};%
+      \draw[->] ($(verification.south) - (0.5,0)$) -- (error);%
+      \node at (0.3,-0.5) {\footnotesize\texttt{\textcolor{keywordcolour}{false}}};%
+      \node at (2,-0.3) {\footnotesize\texttt{\textcolor{keywordcolour}{true}}};%
+      \node[draw,ellipse] (ok) at (5,-0.5) {\small\texttt{\textcolor{constantcolour}{OK}(3ACBlock)}};%
+      \draw[->] (verification) |- (ok);}
+
+      \visible<3->{\node[draw,minimum width=3cm,minimum height=1cm,align=center] (schedtranslation) at (9.5,-0.5) {\small\texttt{\textcolor{functioncolour}{Resource Constrained}}\\\small\texttt{\textcolor{functioncolour}{Scheduling}}};%
+    \node[draw,ellipse] (schedoutput) at (13,-0.5) {\small\texttt{3ACPar}};%
+    \draw[->] (ok) -- (schedtranslation);%
+    \draw[->] (schedtranslation) -- (schedoutput);%
+      \node[draw,minimum width=3cm,minimum height=1cm,align=center] (schedverification) at (9.5,-2) {\small Equivalence\\\small Check};%
+      \draw[->] (ok) |- (schedverification);%
+      \draw[->] (schedoutput) |- (schedverification);%
+      \node[draw,ellipse] (schederror) at ($(schedverification.south) - (0.5,1.5)$) {\small\texttt{\textcolor{constantcolour}{Error}}};%
+      \draw[->] ($(schedverification.south) - (0.5,0)$) -- (schederror);%
+      \node at (8.3,-3) {\footnotesize\texttt{\textcolor{keywordcolour}{false}}};%
+      \node at (10,-2.8) {\footnotesize\texttt{\textcolor{keywordcolour}{true}}};%
+      \node[draw,ellipse] (ok) at (13,-3) {\small\texttt{\textcolor{constantcolour}{OK}(3ACPar)}};%
+      \draw[->] (schedverification) |- (ok);}
+  \end{scope}
+\end{tikzpicture}}
+#+end_export
+
+** Scheduling example
+
+#+beamer: \vspace{0.5em}
+
+*** Column 1
+:PROPERTIES:
+:BEAMER_COL: 0.40
+:END:
+
+**** Minipage :B_minipage:
+:PROPERTIES:
+:BEAMER_env: minipage
+:BEAMER_OPT: 10cm
+:END:
+
+***** Code 1 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 1
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize
+#+begin_src C
+p1 = r3 == 0
+r1 = r3 + r4
+(p1) r2 = r3 + r1
+(~ p1) r2 = r4 + r1
+stk[r5] = r2
+r6 = stk[r5+1]
+#+end_src
+
+***** Code 2 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 2
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize
+#+begin_src C
+p1 = r3 == 0
+r1 = r3 + r4
+(p1) r2 = r3 + r1
+(~ p1) r2 = r4 + r1
+stk[r5] = r2
+r6 = stk[r5+1]
+#+end_src
+
+***** Code 3 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 3
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={5,6}
+#+begin_src C
+p1 = r3 == 0
+r1 = r3 + r4
+(p1) r2 = r3 + r1
+(~ p1) r2 = r4 + r1
+stk[r5] = r2
+r6 = stk[r5+1]
+#+end_src
+
+***** Code 4 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 4
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={1}
+#+begin_src C
+p1 = r3 == 0
+r1 = r3 + r4
+(p1) r2 = r3 + r1
+(~ p1) r2 = r4 + r1
+stk[r5] = r2
+r6 = stk[r5+1]
+#+end_src
+
+#+beamer: \vspace{-2em}
+
+#+begin_export latex
+\begin{align*}
+  &p_{1} \mapsto r_{3}^{0} = 0
+\end{align*}
+#+end_export
+
+***** Code 5 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 5
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={2}
+#+begin_src C
+p1 = r3 == 0
+r1 = r3 + r4
+(p1) r2 = r3 + r1
+(~ p1) r2 = r4 + r1
+stk[r5] = r2
+r6 = stk[r5+1]
+#+end_src
+
+#+beamer: \vspace{-2em}
+
+#+begin_export latex
+\begin{align*}
+  &p_{1} \mapsto r_{3}^{0} = 0\\
+  &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}
+\end{align*}
+#+end_export
+
+***** Code 6 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 6
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={3}
+#+begin_src C
+p1 = r3 == 0
+r1 = r3 + r4
+(p1) r2 = r3 + r1
+(~ p1) r2 = r4 + r1
+stk[r5] = r2
+r6 = stk[r5+1]
+#+end_src
+
+#+beamer: \vspace{-2em}
+
+#+begin_export latex
+\begin{align*}
+  &p_{1} \mapsto r_{3}^{0} = 0\\
+  &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\
+  &r_{2} \mapsto \begin{cases}
+    r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}
+    \end{cases}
+\end{align*}
+#+end_export
+
+***** Code 7 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 7
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={4}
+#+begin_src C
+p1 = r3 == 0
+r1 = r3 + r4
+(p1) r2 = r3 + r1
+(~ p1) r2 = r4 + r1
+stk[r5] = r2
+r6 = stk[r5+1]
+#+end_src
+
+#+beamer: \vspace{-2em}
+
+#+begin_export latex
+\begin{align*}
+  &p_{1} \mapsto r_{3}^{0} = 0\\
+  &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\
+  &r_{2} \mapsto \begin{cases}
+    r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\
+    r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\
+  \end{cases}
+\end{align*}
+#+end_export
+
+***** Code 8 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 8
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={5}
+#+begin_src C
+p1 = r3 == 0
+r1 = r3 + r4
+(p1) r2 = r3 + r1
+(~ p1) r2 = r4 + r1
+stk[r5] = r2
+r6 = stk[r5+1]
+#+end_src
+
+#+beamer: \vspace{-2em}
+
+#+begin_export latex
+\begin{align*}
+  &p_{1} \mapsto r_{3}^{0} = 0\\
+  &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\
+  &r_{2} \mapsto \begin{cases}
+    r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\
+    r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\
+  \end{cases}\\
+  &\mathit{Mem} \mapsto \mathit{Mem}^0 \cup \{r_{5}^{0} \mapsto r_{1}^{0} + r_{2}^{0}\}
+\end{align*}
+#+end_export
+
+***** Code 9 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 9
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={6}
+#+begin_src C
+p1 = r3 == 0
+r1 = r3 + r4
+(p1) r2 = r3 + r1
+(~ p1) r2 = r4 + r1
+stk[r5] = r2
+r6 = stk[r5+1]
+#+end_src
+
+#+beamer: \vspace{-2em}
+
+#+begin_export latex
+\begin{align*}
+  &p_{1} \mapsto r_{3}^{0} = 0\\
+  &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\
+  &r_{2} \mapsto \begin{cases}
+    r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\
+    r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\
+  \end{cases}\\
+  &\mathit{Mem} \mapsto \mathit{Mem}^0 \cup \{r_{5}^{0} \mapsto r_{1}^{0} + r_{2}^{0}\}\\
+  &r_{6} \mapsto (\mathit{Mem}^0 \cup \{r_{5}^{0} \mapsto r_{1}^{0} + r_{2}^{0}\})[r_{5}^0 + 1]
+\end{align*}
+#+end_export
+***** Code 10 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 10
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={6}
+#+begin_src C
+p1 = r3 == 0
+r1 = r3 + r4
+(p1) r2 = r3 + r1
+(~ p1) r2 = r4 + r1
+stk[r5] = r2
+r6 = stk[r5+1]
+#+end_src
+
+#+beamer: \vspace{-2em}
+
+#+begin_export latex
+\begin{align*}
+  &p_{1} \mapsto r_{3}^{0} = 0\\
+  &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\
+  &r_{2} \mapsto \begin{cases}
+    r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\
+    r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\
+  \end{cases}\\
+  &\mathit{Mem} \mapsto \mathit{Mem}^0 \cup \{r_{5}^{0} \mapsto r_{1}^{0} + r_{2}^{0}\}\\
+  &r_{6} \mapsto \mathit{Mem}^0[r_{5}^0 + 1]
+\end{align*}
+#+end_export
+
+*** Column 2
+:PROPERTIES:
+:BEAMER_COL: 0.55
+:END:
+
+**** Minipage :B_minipage:
+:PROPERTIES:
+:BEAMER_env: minipage
+:BEAMER_OPT: 10cm
+:END:
+
+***** Code 2 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 2
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize
+#+begin_src C
+p1 = r3 == 0 || r1 = r3 + r4
+     || r6 = stk[r5+1]
+(p1) r2 = r3 + r1
+     || (~ p1) r2 = r4 + r1
+stk[r5] = r1 + r2
+#+end_src
+
+***** Code 3 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 3
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={2,5}
+#+begin_src C
+p1 = r3 == 0 || r1 = r3 + r4
+     || r6 = stk[r5+1]
+(p1) r2 = r3 + r1
+     || (~ p1) r2 = r4 + r1
+stk[r5] = r1 + r2
+#+end_src
+
+***** Code 4 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 4
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={1,2}
+#+begin_src C
+p1 = r3 == 0 || r1 = r3 + r4
+     || r6 = stk[r5+1]
+(p1) r2 = r3 + r1
+     || (~ p1) r2 = r4 + r1
+stk[r5] = r1 + r2
+#+end_src
+
+#+beamer: \vspace{-2em}
+
+#+begin_export latex
+\begin{align*}
+  &p_{1} \mapsto r_{3}^{0} = 0\\
+  &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\
+  &r_{6} \mapsto \mathit{Mem}^0[r_{5}^{0} + 1]
+\end{align*}
+#+end_export
+
+***** Code 5 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 5
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={3,4}
+#+begin_src C
+p1 = r3 == 0 || r1 = r3 + r4
+     || r6 = stk[r5+1]
+(p1) r2 = r3 + r1
+     || (~ p1) r2 = r4 + r1
+stk[r5] = r1 + r2
+#+end_src
+
+#+beamer: \vspace{-2em}
+
+#+begin_export latex
+\begin{align*}
+  &p_{1} \mapsto r_{3}^{0} = 0\\
+  &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\
+  &r_{2} \mapsto \begin{cases}
+    r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\
+    r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\
+  \end{cases}\\
+  &r_{6} \mapsto \mathit{Mem}^0[r_{5}^{0} + 1]
+\end{align*}
+#+end_export
+
+***** Code 6 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 6-
+:END:
+
+#+attr_latex: :options fontsize=\footnotesize,highlightlines={5}
+#+begin_src C
+p1 = r3 == 0 || r1 = r3 + r4
+     || r6 = stk[r5+1]
+(p1) r2 = r3 + r1
+     || (~ p1) r2 = r4 + r1
+stk[r5] = r1 + r2
+#+end_src
+
+#+beamer: \vspace{-2em}
+
+#+begin_export latex
+\begin{align*}
+  &p_{1} \mapsto r_{3}^{0} = 0\\
+  &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\
+  &r_{2} \mapsto \begin{cases}
+    r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\
+    r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\
+  \end{cases}\\
+  &\mathit{Mem} \mapsto \mathit{Mem}^0 \cup \{r_{5}^{0} \mapsto r_{1}^{0} + r_{2}^{0}\} \\
+  &r_{6} \mapsto \mathit{Mem}^0[r_{5}^{0} + 1]
+\end{align*}
+#+end_export
+
+** One more complication
+
+How to prove equality of *conditional expressions*?
+
+#+begin_export latex
+\begin{equation*}
+  \begin{drcases}
+    r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1} \lor (p_{2} \land \neg p_{2}) \\
+    r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\
+    r_{4}^{0}, &p_{3} \land \neg p_{3}\\
+  \end{drcases} = \begin{cases}
+  r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\
+    r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\
+  \end{cases}
+\end{equation*}
+#+end_export
+
+#+attr_beamer: :overlay <+->
+- They can be *reordered* in any way.
+- Some expressions *not present anymore* (when predicate is provably false).
+- Predicates *simplified* by scheduling.
+
+** Solution to proving conditional functions
+
+#+attr_beamer: :overlay <+->
+1. Use a *formally verified SAT solver*.
+2. Show that predicates are *independent*.
+3. Reorder the list of predicates in a more useful order.
+4. Use SAT solver to go through list and find equivalent pairings.
+5. Show that attached expressions are equal.
+
+*** Minipage :B_minipage:
+:PROPERTIES:
+:BEAMER_env: minipage
+:BEAMER_OPT: 5cm
+:END:
+
+**** Only 1 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 2
+:END:
+
+#+begin_export latex
+\begin{equation*}
+  \text{unsat}\quad (p_1 \land \neg p_1) \lor (p_1 \land (p_{3} \land \neg p_{3})) \lor (\neg p_1 \land (p_{3} \land \neg p_{3}))
+\end{equation*}
+#+end_export
+
+**** Only 2 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 3
+:END:
+
+#+begin_export latex
+\begin{equation*}
+  \begin{drcases}
+    r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1} \lor (p_{2} \land \neg p_{2}) \\
+    r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\
+    r_{4}^{0}, &p_{3} \land \neg p_{3}\\
+  \end{drcases} = \begin{cases}
+    r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\
+      r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\
+  \end{cases}
+\end{equation*}
+#+end_export
+
+**** Only 3 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 4
+:END:
+
+#+begin_export latex
+\begin{equation*}
+  \begin{drcases}
+    r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1} \lor (p_{2} \land \neg p_{2}) \\
+    r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\
+    r_{4}^{0}, &p_{3} \land \neg p_{3}\\
+  \end{drcases} = \begin{cases}
+    r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\
+      r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\
+  \end{cases}
+\end{equation*}
+#+end_export
+
+#+begin_export latex
+\begin{equation*}
+\text{unsat}\quad \neg (p_{1} \lor (p_{2} \land \neg p_{2}) \Longleftrightarrow p_1)
+\end{equation*}
+#+end_export
+
+**** Only 4 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: 5
+:END:
+
+#+begin_export latex
+\begin{equation*}
+  \begin{drcases}
+    r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1} \lor (p_{2} \land \neg p_{2}) \\
+    r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\
+    r_{4}^{0}, &p_{3} \land \neg p_{3}\\
+  \end{drcases} = \begin{cases}
+    r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\
+      r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\
+  \end{cases}
+\end{equation*}
+#+end_export
+
+#+begin_export latex
+\begin{equation*}
+\text{unsat}\quad \neg (p_{1} \lor (p_{2} \land \neg p_{2}) \Longleftrightarrow p_1)
+\end{equation*}
+#+end_export
+
+#+begin_export latex
+\begin{equation*}
+r_{3}^{0} + r_{3}^{0} + r_{4}^{0} \stackrel{?}{=} r_{3}^{0} + r_{3}^{0} + r_{4}^{0}
+\end{equation*}
+#+end_export
+
+** New passes
+
+#+begin_export latex
+\definecolor{compcert}{HTML}{66c2a5}
+\definecolor{formalhls}{HTML}{fc8d62}
+\begin{center}\scalebox{0.8}{\begin{tikzpicture}[language/.style={fill=white,rounded corners=2pt}]
+    \fill[compcert,rounded corners=3pt] (-1,-1) rectangle (9,1.5);
+    \fill[formalhls,rounded corners=3pt] (-1,-1.5) rectangle (9,-2.5);
+    \node[language] at (0,0) (clight) {Clight};
+    \node[language] at (2,0) (cminor) {C\#minor};
+    \node[language] at (4,0) (rtl) {3AC};
+    \node[language] at (6,0) (ltl) {LTL};
+    \node[language] at (8,0) (ppc) {PPC};
+    \node[language] at (2,-2) (acblock) {\small 3ACBlock};
+    \node[language] at (4,-2) (acpar) {\small 3ACPar};
+    \node[language] at (6,-2) (dfgstmd) {HTL};
+    \node[language] at (8,-2) (verilog) {Verilog};
+    \node at (0,1) {CompCert};
+    \node at (0,-2) {Vericert};
+    \draw[->] (clight) -- (cminor);
+    \draw[->,dashed] (cminor) -- (rtl);
+    \draw[->] (rtl) -- (ltl);
+    \draw[->,dashed] (ltl) -- (ppc);
+    \draw[->] (rtl) |- (2,-1.3) -- (acblock);
+    \draw[->] (acblock) -- (acpar);
+    \draw[->] (acpar) -- (dfgstmd);
+    \draw[->] (dfgstmd) -- (verilog);
+    \draw[->] ($(acblock.south) - (0.1,0)$) to [out=270,in=180] (2,-3) to [out=0,in=270] ($(acblock.south) + (0.1,0)$);
+\end{tikzpicture}}\end{center}
+#+end_export
+
+#+beamer: \vspace{1em}
+
+Add two more passes, from *3ACBlock* $\rightarrow$ *3ACBlock* and from *3ACBlock* to *3ACPar*.
+
+** About Iterative Modulo Scheduling
+
+#+attr_beamer: :overlay <+->
+- Algorithm used to approximate an optimal schedule for a loop.
+- Performs code transformations from one loop iteration into other loop iterations.
+- Allows for more parallelism between instructions.
+
+** Example of proof by translation validation
+
+*** Diagram
+:PROPERTIES:
+:BEAMER_COL: 0.45
+:END:
+
+#+begin_export latex
+\scalebox{0.8}{
+  \begin{tikzpicture}
+    \begin{scope}
+      \node[draw,minimum width=3cm,minimum height=1cm] (translation) at (1.5,2) {\texttt{\textcolor{functioncolour}{HLS}}};
+      \node[draw,ellipse] (input) at (-1.5,2) {\texttt{C}};
+      \node[draw,ellipse] (output) at (5,2) {\texttt{Verilog}};
+      \draw[->] (input) -- (translation);
+      \draw[->] (translation) -- (output);
+      \visible<2->{%
+        \node[draw,minimum width=3cm,minimum height=1cm,align=center] (verification) at (1.5,0.5) {Equivalence\\Check};
+        \draw[->] (input) |- (verification);
+        \draw[->] (output) |- (verification);}
+      \visible<3->{%
+        \node[draw,ellipse] (error) at ($(verification.south) - (0.5,1.5)$) {\texttt{\textcolor{constantcolour}{Error}}};
+        \draw[->] ($(verification.south) - (0.5,0)$) -- (error);
+        \node at (0.3,-0.5) {\footnotesize\texttt{\textcolor{keywordcolour}{false}}};}
+      \visible<4->{%
+        \node at (2,-0.3) {\footnotesize\texttt{\textcolor{keywordcolour}{true}}};
+        \node[draw,ellipse] (ok) at (5,-0.5) {\texttt{\textcolor{constantcolour}{OK}(Verilog)}};
+        \draw[->] (verification) |- (ok);}
+    \end{scope}
+  \end{tikzpicture}}
+#+end_export
+
+*** Text
+:PROPERTIES:
+:BEAMER_COL: 0.45
+:END:
+
+#+attr_beamer: :overlay <+->
+- Prove correctness of an existing translation from ~C~ to ~Verilog~.
+- Add equivalence check.
+- Error out if it fails.
+- Succeed if the equivalence check passes.
+
+** How is the Equivalence Check Performed? :B_frame:
+
+*** Code example :B_column:
+:PROPERTIES:
+:BEAMER_ENV: column
+:BEAMER_COL: 0.45
+:END:
+
+**** Code 1 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_ACT: <1>
+:BEAMER_env: onlyenvNH
+:END:
+
+#+begin_src C
+int main() {
+    int x[3] = {1, 2, 3};
+    int sum = 0;
+    for (int i = 0; i < 3; i++)
+        sum += x[i];
+    return sum;
+}
+#+end_src
+
+**** Code 2 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <2>
+:END:
+
+#+attr_latex: :options highlightlines={2}
+#+begin_src C
+int main() {
+    int x[3] = {1, 2, 3};
+    int sum = 0;
+    for (int i = 0; i < 3; i++)
+        sum += x[i];
+    return sum;
+}
+#+end_src
+
+#+begin_export latex
+\begin{align*}
+\text{Mem} \{0 \rightarrow 1, 4 \rightarrow 2, 8 \rightarrow 3\} =\\ \text{Mem} \{0 \rightarrow 1\} \land\\
+  \texttt{x8} \rightarrow 1
+\end{align*}
+#+end_export
+
+**** Code 3 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <3>
+:END:
+
+#+attr_latex: :options highlightlines={2}
+#+begin_src C
+int main() {
+    int x[3] = {1, 2, 3};
+    int sum = 0;
+    for (int i = 0; i < 3; i++)
+        sum += x[i];
+    return sum;
+}
+#+end_src
+
+#+begin_export latex
+\begin{align*}
+  \text{Mem} \{0 \rightarrow 1, 4 \rightarrow 2, 8 \rightarrow 3\} =\\ \text{Mem} \{0 \rightarrow 1, 4 \rightarrow 2\} \land\\
+  \texttt{x8} \rightarrow 1 \cup \texttt{x7} \rightarrow 2
+\end{align*}
+#+end_export
+
+**** Code 4 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <4>
+:END:
+
+#+attr_latex: :options highlightlines={2}
+#+begin_src C
+int main() {
+    int x[3] = {1, 2, 3};
+    int sum = 0;
+    for (int i = 0; i < 3; i++)
+        sum += x[i];
+    return sum;
+}
+#+end_src
+
+#+begin_export latex
+\begin{align*}
+  \text{Mem} \{0 \rightarrow 1, 4 \rightarrow 2, 8 \rightarrow 3\} =\\ \text{Mem} \{0 \rightarrow 1, 4 \rightarrow 2, 8 \rightarrow 3\} \land\\
+  \texttt{x8} \rightarrow 1 \cup \texttt{x7} \rightarrow 2 \cup \texttt{x6} \rightarrow 3
+\end{align*}
+#+end_export
+
+**** Code 5 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <5>
+:END:
+
+#+attr_latex: :options highlightlines={3}
+#+begin_src C
+int main() {
+    int x[3] = {1, 2, 3};
+    int sum = 0;
+    for (int i = 0; i < 3; i++)
+        sum += x[i];
+    return sum;
+}
+#+end_src
+
+Here we also need a mapping for variable names: $\texttt{sum} \rightarrow \texttt{x2}$.
+
+#+begin_export latex
+\begin{align*}
+  \texttt{sum} \rightarrow 0 = \texttt{x2} \rightarrow 0
+\end{align*}
+#+end_export
+
+**** Code 6 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <6>
+:END:
+
+#+attr_latex: :options highlightlines={4}
+#+begin_src C
+int main() {
+    int x[3] = {1, 2, 3};
+    int sum = 0;
+    for (int i = 0; i < 3; i++)
+        sum += x[i];
+    return sum;
+}
+#+end_src
+
+#+beamer: \vspace{2em}
+
+For loops can just be identified using a template.
+
+**** Code 7 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <7>
+:END:
+
+#+attr_latex: :options highlightlines={5}
+#+begin_src C
+int main() {
+    int x[3] = {1, 2, 3};
+    int sum = 0;
+    for (int i = 0; i < 3; i++)
+        sum += x[i];
+    return sum;
+}
+#+end_src
+
+#+begin_export latex
+\begin{align*}
+  \texttt{sum} \rightarrow \texttt{sum}^{0} + \text{Mem}[i^{0} * 4] =\\ \texttt{x5} \rightarrow 0
+\end{align*}
+#+end_export
+
+**** Code 8 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <8>
+:END:
+
+#+attr_latex: :options highlightlines={5}
+#+begin_src C
+int main() {
+    int x[3] = {1, 2, 3};
+    int sum = 0;
+    for (int i = 0; i < 3; i++)
+        sum += x[i];
+    return sum;
+}
+#+end_src
+
+#+begin_export latex
+\begin{align*}
+  \texttt{sum} \rightarrow \texttt{sum}^{0} + \text{Mem}[i^{0} * 4] =\\ \texttt{x5} \rightarrow 0 \cup \texttt{x4} \rightarrow \text{Mem}[\texttt{x1} * 4]
+\end{align*}
+#+end_export
+
+**** Code 9 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <9>
+:END:
+
+#+attr_latex: :options highlightlines={5}
+#+begin_src C
+int main() {
+    int x[3] = {1, 2, 3};
+    int sum = 0;
+    for (int i = 0; i < 3; i++)
+        sum += x[i];
+    return sum;
+}
+#+end_src
+
+#+begin_export latex
+\begin{align*}
+  \texttt{sum} \rightarrow \texttt{sum}^{0} + \text{Mem}[i^{0} * 4] =\\ \texttt{x5} \rightarrow 0 \cup \texttt{x4} \rightarrow \text{Mem}[\texttt{x1}^{0} * 4]\\ \cup\ \texttt{x2} \rightarrow \texttt{x2}^{0} + \text{Mem}[\texttt{x1}^{0} * 4]
+\end{align*}
+#+end_export
+
+*** Text :B_column:
+:PROPERTIES:
+:BEAMER_ENV: column
+:BEAMER_COL: 0.45
+:END:
+
+**** Text 1 :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_ACT: <1>
+:BEAMER_env: onlyenvNH
+:END:
+
+Example of simple loop accumulating values in array.
+
+**** 3AC Code 2 :B_onlyenv:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <2>
+:END:
+
+#+attr_latex: :options fontsize=\scriptsize,highlightlines={2-3}
+#+begin_src C
+main() {
+   15:  x8 = 1
+   14:  int32[stack(0)] = x8
+   13:  x7 = 2
+   12:  int32[stack(4)] = x7
+   11:  x6 = 3
+   10:  int32[stack(8)] = x6
+    9:  x2 = 0
+    8:  x1 = 0
+    7:  x5 = stack(0) (int)
+    6:  x4 = int32[x5 + x1 * 4 + 0]
+    5:  x2 = x2 + x4 + 0 (int)
+    4:  x1 = x1 + 1 (int)
+    3:  if (x1 <s 3) goto 7 else goto 2
+    2:  x3 = x2
+    1:  return x3
+}
+#+end_src
+
+**** 3AC Code 3 :B_onlyenv:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <3>
+:END:
+
+#+attr_latex: :options fontsize=\scriptsize,highlightlines={2-5}
+#+begin_src C
+main() {
+   15:  x8 = 1
+   14:  int32[stack(0)] = x8
+   13:  x7 = 2
+   12:  int32[stack(4)] = x7
+   11:  x6 = 3
+   10:  int32[stack(8)] = x6
+    9:  x2 = 0
+    8:  x1 = 0
+    7:  x5 = stack(0) (int)
+    6:  x4 = int32[x5 + x1 * 4 + 0]
+    5:  x2 = x2 + x4 + 0 (int)
+    4:  x1 = x1 + 1 (int)
+    3:  if (x1 <s 3) goto 7 else goto 2
+    2:  x3 = x2
+    1:  return x3
+}
+#+end_src
+
+**** 3AC Code 4 :B_onlyenv:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <4>
+:END:
+
+#+attr_latex: :options fontsize=\scriptsize,highlightlines={2-7}
+#+begin_src C
+main() {
+   15:  x8 = 1
+   14:  int32[stack(0)] = x8
+   13:  x7 = 2
+   12:  int32[stack(4)] = x7
+   11:  x6 = 3
+   10:  int32[stack(8)] = x6
+    9:  x2 = 0
+    8:  x1 = 0
+    7:  x5 = stack(0) (int)
+    6:  x4 = int32[x5 + x1 * 4 + 0]
+    5:  x2 = x2 + x4 + 0 (int)
+    4:  x1 = x1 + 1 (int)
+    3:  if (x1 <s 3) goto 7 else goto 2
+    2:  x3 = x2
+    1:  return x3
+}
+#+end_src
+
+**** 3AC Code 5 :B_onlyenv:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <5>
+:END:
+
+#+attr_latex: :options fontsize=\scriptsize,highlightlines={8}
+#+begin_src C
+main() {
+   15:  x8 = 1
+   14:  int32[stack(0)] = x8
+   13:  x7 = 2
+   12:  int32[stack(4)] = x7
+   11:  x6 = 3
+   10:  int32[stack(8)] = x6
+    9:  x2 = 0
+    8:  x1 = 0
+    7:  x5 = stack(0) (int)
+    6:  x4 = int32[x5 + x1 * 4 + 0]
+    5:  x2 = x2 + x4 + 0 (int)
+    4:  x1 = x1 + 1 (int)
+    3:  if (x1 <s 3) goto 7 else goto 2
+    2:  x3 = x2
+    1:  return x3
+}
+#+end_src
+
+**** 3AC Code 6 :B_onlyenv:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <6>
+:END:
+
+#+attr_latex: :options fontsize=\scriptsize,highlightlines={9,13-14}
+#+begin_src C
+main() {
+   15:  x8 = 1
+   14:  int32[stack(0)] = x8
+   13:  x7 = 2
+   12:  int32[stack(4)] = x7
+   11:  x6 = 3
+   10:  int32[stack(8)] = x6
+    9:  x2 = 0
+    8:  x1 = 0
+    7:  x5 = stack(0) (int)
+    6:  x4 = int32[x5 + x1 * 4 + 0]
+    5:  x2 = x2 + x4 + 0 (int)
+    4:  x1 = x1 + 1 (int)
+    3:  if (x1 <s 3) goto 7 else goto 2
+    2:  x3 = x2
+    1:  return x3
+}
+#+end_src
+
+**** 3AC Code 7 :B_onlyenv:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <7>
+:END:
+
+#+attr_latex: :options fontsize=\scriptsize,highlightlines={10}
+#+begin_src C
+main() {
+   15:  x8 = 1
+   14:  int32[stack(0)] = x8
+   13:  x7 = 2
+   12:  int32[stack(4)] = x7
+   11:  x6 = 3
+   10:  int32[stack(8)] = x6
+    9:  x2 = 0
+    8:  x1 = 0
+    7:  x5 = stack(0) (int)
+    6:  x4 = int32[x5 + x1 * 4 + 0]
+    5:  x2 = x2 + x4 + 0 (int)
+    4:  x1 = x1 + 1 (int)
+    3:  if (x1 <s 3) goto 7 else goto 2
+    2:  x3 = x2
+    1:  return x3
+}
+#+end_src
+
+**** 3AC Code 8 :B_onlyenv:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <8>
+:END:
+
+#+attr_latex: :options fontsize=\scriptsize,highlightlines={11}
+#+begin_src C
+main() {
+   15:  x8 = 1
+   14:  int32[stack(0)] = x8
+   13:  x7 = 2
+   12:  int32[stack(4)] = x7
+   11:  x6 = 3
+   10:  int32[stack(8)] = x6
+    9:  x2 = 0
+    8:  x1 = 0
+    7:  x5 = stack(0) (int)
+    6:  x4 = int32[x5 + x1 * 4 + 0]
+    5:  x2 = x2 + x4 + 0 (int)
+    4:  x1 = x1 + 1 (int)
+    3:  if (x1 <s 3) goto 7 else goto 2
+    2:  x3 = x2
+    1:  return x3
+}
+#+end_src
+
+**** 3AC Code 9 :B_onlyenv:
+:PROPERTIES:
+:BEAMER_env: onlyenvNH
+:BEAMER_ACT: <9>
+:END:
+
+#+attr_latex: :options fontsize=\scriptsize,highlightlines={12}
+#+begin_src C
+main() {
+   15:  x8 = 1
+   14:  int32[stack(0)] = x8
+   13:  x7 = 2
+   12:  int32[stack(4)] = x7
+   11:  x6 = 3
+   10:  int32[stack(8)] = x6
+    9:  x2 = 0
+    8:  x1 = 0
+    7:  x5 = stack(0) (int)
+    6:  x4 = int32[x5 + x1 * 4 + 0]
+    5:  x2 = x2 + x4 + 0 (int)
+    4:  x1 = x1 + 1 (int)
+    3:  if (x1 <s 3) goto 7 else goto 2
+    2:  x3 = x2
+    1:  return x3
+}
+#+end_src
+
+** Example of Iterative Modulo Scheduling
+
+*** Initial loop :B_column:
+:PROPERTIES:
+:BEAMER_ENV: column
+:BEAMER_COL: 0.45
+:END:
+
+**** Code :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_ACT: <1>
+:BEAMER_env: onlyenvNH
+:END:
+
+#+begin_src C
+for (int i = 1; i < N; i++) {
+    x = A[i];
+    sum = sum + x;
+    A[i] = sum;
+}
+#+end_src
+
+*** Transformed loop :B_column:
+:PROPERTIES:
+:BEAMER_ENV: column
+:BEAMER_COL: 0.45
+:END:
+
+**** Code :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_ACT: <1>
+:BEAMER_env: onlyenvNH
+:END:
+
+#+begin_src C
+x = A[0];
+sum = sum + x;
+x = A[1];
+for (int i = 0; i < N - 2; i++) {
+    A[i] = sum;
+    sum = sum + x;
+    x = A[i + 2];
+}
+A[N-2] = sum;
+sum = sum + x;
+A[N-1] = sum;
+#+end_src
+** Example of Iterative Modulo Scheduling
+
+*** Initial loop :B_column:
+:PROPERTIES:
+:BEAMER_ENV: column
+:BEAMER_COL: 0.45
+:END:
+
+**** Code :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_ACT: <1>
+:BEAMER_env: onlyenvNH
+:END:
+
+#+begin_src C
+for (int i = 1; i < N; i++) {
+    c1 = acc[i-1] * c;
+    c2 = x[i] * y[i];
+    acc[i] = c1 + c2;
+}
+#+end_src
+
+*** Transformed loop :B_column:
+:PROPERTIES:
+:BEAMER_ENV: column
+:BEAMER_COL: 0.45
+:END:
+
+**** Code :B_onlyenvNH:
+:PROPERTIES:
+:BEAMER_ACT: <1>
+:BEAMER_env: onlyenvNH
+:END:
+
+#+begin_src C
+c1 = acc[0] * c;
+c2 = x[1] * y[1];
+for (int i = 1; i < N - 1; i++) {
+    acc[i] = c1 + c2;
+    c2 = x[i+1] * y[i+1];
+    c1 = acc[i+1] * c;
+}
+acc[i] = c1 + c2;
+#+end_src
diff --git a/setup.org b/setup.org
new file mode 100644
index 0000000..67e3696
--- /dev/null
+++ b/setup.org
@@ -0,0 +1,54 @@
+#+latex_compiler: lualatex
+#+latex_class_options: [12pt,aspectratio=169]
+#+latex_header: \usepackage{tikz}
+#+latex_header: \usepackage{amsmath}
+#+latex_header: \usepackage{mathpartir}
+#+latex_header: \usepackage{booktabs}
+#+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}
+#+latex_header_extra: \setminted{fontsize=\small}
+# #+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}
+#+latex_header_extra: \definecolor{functioncolour}{HTML}{721045}
+#+latex_header_extra: \definecolor{constantcolour}{HTML}{0000bb}
+#+latex_header_extra: \newcommand\yhkeywordsp[1]{\;\;\texttt{\textcolor{keywordcolour}{#1}}}
+#+latex_header_extra: \newcommand\yhkeyword[1]{\texttt{\textcolor{keywordcolour}{#1}}}
+#+latex_header_extra: \newcommand\yhfunctionsp[1]{\;\;\texttt{\textcolor{functioncolour}{#1}}}
+#+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: \tikzexternalize
+
+#+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}
+
+#+latex_header_extra: \definecolor{s1col}{HTML}{7fc97f}
+#+latex_header_extra: \definecolor{s2col}{HTML}{beaed4}
+#+latex_header_extra: \definecolor{s3col}{HTML}{fdc086}
+#+latex_header_extra: \definecolor{s4col}{HTML}{ffff99}
+#+latex_header_extra: \definecolor{s5col}{HTML}{386cb0}
+
+#+latex_header_extra: \newcommand*{\makedfgstate}[2]{\raisebox{-2pt}{\tikz{\node[circle,draw=black,minimum
+#+latex_header_extra:       size=4mm,fill=#1,scale=0.5](#1#2){#2};}}}
+#+latex_header_extra: \newcommand*{\sA}[1]{\makedfgstate{s1col}{#1}}
+#+latex_header_extra: \newcommand*{\sR}[1]{\makedfgstate{s2col}{#1}}
+#+latex_header_extra: \newcommand*{\sM}[1]{\makedfgstate{s3col}{#1}}
+#+latex_header_extra: \newcommand*{\sW}[1]{\makedfgstate{s4col}{#1}}
+
+#+exclude_tags: noexport
+
+#+beamer_theme: auriga
+#+beamer_color_theme: auriga