#+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