#+title: Formal Verification of High-Level Synthesis
#+author: \underline{Yann Herklotz}, James D. Pollard, Nadesh Ramanathan, John Wickerson
#+options: H:2
#+columns: %45ITEM %10BEAMER_ENV(Env) %10BEAMER_ACT(Act) %4BEAMER_COL(Col)
#+setupfile: setup.org

** What is High-Level Synthesis

*** 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

*** HLS Unreliable :B_blockNH:
:PROPERTIES:
:BEAMER_env: blockNH
:END:

High-level synthesis is often quite unreliable:

#+attr_beamer: :overlay <+->
- Intel's OpenCL could not be fuzzed because of too many issues (cite:lidbury15_many_core_compil_fuzzin).
- We fuzzed HLS tools and found they failed on *2.5%* of simple random test cases.

*** HLS Difficulties :B_blockNH:
:PROPERTIES:
:BEAMER_env: blockNH
:BEAMER_ACT: <3->
:END:

Difficult to debug HLS tools:

#+attr_beamer: :overlay <+->
- Simulation can take a long time.
- Correctness is important in hardware, testing is done at every level.

** 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:

Current progress: fully verified HLS tool for a subset of C.

Support for: all *control flow*, *fixedpoint*, *non-recursive functions* and *local arrays/structs/unions*.

* Example
** Example: RTL :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 (RTL)* 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.

**** RTL 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

** Example: HTL Overview

The representation of the *finite state-machine with datapath (FSMD)* is abstract and called **HTL**.

*** Datapath and control logic :B_blockNH:
:PROPERTIES:
:BEAMER_env: blockNH
:END:

#+attr_latex: :options fontsize=\footnotesize
#+begin_src coq
Definition datapath := PTree.t Verilog.stmnt.
Definition controllogic := PTree.t Verilog.stmnt.
#+end_src

*** Module definition :B_blockNH:
:PROPERTIES:
:BEAMER_env: blockNH
:BEAMER_ACT: 2
:END:

#+beamer: \vspace{-1.5em}
#+attr_latex: :options fontsize=\footnotesize
#+begin_src coq
Record module: Type := mkmodule {
    mod_datapath: datapath; mod_controllogic: controllogic;
    mod_wf: map_well_formed mod_controllogic
             /\ map_well_formed mod_datapath;
    mod_reset: reg;
    mod_ram: ram_spec;
    ...
  }.
#+end_src

** Example: Translation (RTL $\rightarrow$ HTL)

Translation from *control-flow graph (CFG)* into a *finite state-machine with datapath (FSMD)*.

#+beamer: \pause
#+beamer: \vspace{1em}

#+attr_beamer: :overlay <+->
- *Control-flow* is translated into a *finite state-machine*.
- Each *RTL instructions* translated into equivalent *Verilog statements*.
- Function *stack* implemented as *RAM*.
- Pointers for loads and stores translated to RAM addresses.
  - *Byte* addressed to *word* addressed.

#+beamer: \vspace{1em}

*** Minipage :B_minipage:
:PROPERTIES:
:BEAMER_env: minipage
:BEAMER_OPT: 5cm
:END:

**** Only 1 :B_onlyenvNH:
:PROPERTIES:
:BEAMER_env: onlyenvNH
:BEAMER_ACT: 3
:END:

~x3 = x3 + x5 + 0~ $\quad\longrightarrow\quad$ ~reg_3 <= {reg_3 + {reg_5 + 32'd0}}~

**** Only 2 :B_onlyenvNH:
:PROPERTIES:
:BEAMER_env: onlyenvNH
:BEAMER_ACT: 5-6
:END:

~x5 + x1 * 4 + 0~

$\quad\longrightarrow\quad$ ~{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}~

** Example: Memory Inference Pass :noexport:

- An HTL $\rightarrow$ HTL translation removes loads and stores.
- Replaced by accesses to a proper *RAM*.

#+beamer: \vspace{1em}

~stack[{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}]~

#+beamer: \vspace{1em}

becomes

#+beamer: \vspace{1em}

#+attr_latex: :options fontsize=\footnotesize

#+begin_src verilog
u_en <= ( ~ u_en); wr_en <= 32'd0;
addr <= {{{reg_3 + 32'd0} + {reg_1 * 32'd4}} / 32'd4};
#+end_src

** Example: 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 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=\small
#+begin_src verilog
module top(input clk, input [31:0] in1,
           output reg [31:0] out1);
   reg [31:0] reg_1, tmp;

   always @(posedge clk) begin
      reg1 <= in1;
   end

   always @(posedge clk) begin
      tmp = reg1;
      out1 <= tmp;
   end
endmodule
#+end_src

**** Highlight :B_onlyenvNH:
:PROPERTIES:
:BEAMER_env: onlyenvNH
:BEAMER_ACT: <2>
:END:

#+attr_latex: :options highlightlines={5-7,9-12},fontsize=\small
#+begin_src verilog
module top(input clk, input [31:0] in1,
           output reg [31:0] out1);
   reg [31:0] reg_1, tmp;

   always @(posedge clk) begin
      reg1 <= in1;
   end

   always @(posedge clk) begin
      tmp = reg1;
      out1 <= tmp;
   end
endmodule
#+end_src

*** Column 2
:PROPERTIES:
:BEAMER_COL: 0.55
:END:

#+attr_beamer: :overlay <+->
- Verilog example for a simple shift register.
- Always block run in parallel
** Verilog Semantics (Adapted from Lööw et al. (2019))

#+begin_export latex
\begin{gather*}
%\inferrule[Nonblocking]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \downarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ <= } e) \downarrow_{\text{stmnt}} (\Gamma, \Delta [n \mapsto v])} \quad \inferrule[Blocking]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \downarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ = } e) \downarrow_{\text{stmnt}} (\Gamma [n \mapsto v], \Delta)} \\
\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{gather*}
#+end_export

#+attr_beamer: :overlay <+->
- Two separate association maps: current ($\Gamma$) and next ($\Delta$).
- Maps are merged at the end of the clock cycle.

** 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?

*** 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:
: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:
: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

** RTL $\to$ HTL: Build a Specification

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

*** RTL 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

** RTL $\to$ HTL: Prove Forward Simulation

*** 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 RTL state $S_1$ and Verilog state $R_1$,
- there exists 1 or more steps in Verilog,
- such that after 1 step in RTL, the resulting states match.

** Results

*** Performance Results

#+attr_beamer: :overlay <+->
- Ran on 27/30 PolyBench/C benchmarks and compared to LegUp.
- 27$\times$ slower and 1.1$\times$ larger.
- Ran on PolyBench/C with divisions replaced by iterative shifting.
- 2$\times$ slower (on par with unoptimised LegUp).

** Fuzzing Vericert with Csmith

Fuzzed Vericert with Csmith to check correctness theorem.

- One bug was found in the pretty printing.
- Many compile-time errors are expected.
- Mainly rejected because of wrong size.

#+beamer: \vspace{1em}

#+begin_export latex
\definecolor{fuzzred}{HTML}{f8514f}
\definecolor{fuzzyellow}{HTML}{fee4bf}
\definecolor{fuzzgreen}{HTML}{b2df8a}
\begin{tikzpicture}[xscale=0.11]
  \draw[-latex] (13,0.5) to (13,0.25);
  \draw[-latex] (55,0.5) to (55,0.25);
  \draw[-latex] (99.85,0.5) to (99.85,0.25);
  \draw[fuzzgreen, line width=5mm] (0,0) to (26.0,0);
  \draw[fuzzyellow, line width=5mm] (26.0,0) to (99.7,0);
  \draw[fuzzred, line width=5mm] (99.7,0) to (100,0);
  \node[anchor=south] at (13,0.5) {\footnotesize passes (26.00\%)};
  \node[anchor=south] at (55,0.5) {\footnotesize compile-time errors (73.97\%)};
  \node[anchor=south] at (100,0.5) {\footnotesize run-time errors (0.03\%)};
\end{tikzpicture}
#+end_export

** Conclusion

Written a formally verified high-level synthesis tool in *Coq* based on *CompCert*.

#+attr_beamer: :overlay <+->
- Base translation *proven correct* by proving translation of CFG into FSMD.
- Small optimisations implemented such as *Ram Inference*.
- Performance without divisions comparable to LegUp without optimisations.

** Thank you :B_fullframe:
:PROPERTIES:
:BEAMER_env: fullframe
:END:

#+begin_export latex
\begin{center}
  {\usebeamerfont{frametitle}\Large Thank you\par}
  {\color{lightgreen}\rule{350pt}{2pt}\par}
  \vspace{1em}
  \begin{minipage}{5cm}
    \begin{center}
    Documentation\\
    \includegraphics[width=50pt]{assets/formal_hls_docs.pdf}\\
    \tiny\url{https://vericert.ymhg.org}
    \end{center}
  \end{minipage}
  \begin{minipage}{5cm}
  \begin{center}
  GitHub\\
  \includegraphics[width=50pt]{assets/formal_hls_github.pdf}\\
  \tiny\url{https://github.com/ymherklotz/vericert}
  \end{center}
  \end{minipage}\vspace{1em}
  \begin{minipage}{5cm}
  \begin{center}
  OOPSLA'21 Preprint\\
  \includegraphics[width=50pt]{assets/formal_hls_paper.pdf}\\
  \tiny\url{https://ymhg.org/papers/fvhls_oopsla21.pdf}
  \end{center}
  \end{minipage}
\end{center}
#+end_export
** References

bibliography:./references.bib


* Extensions :noexport:
** 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:

- ~RTLBlock~ :: RTL with basic blocks.
- ~RTLPar~ :: RTL with basic blocks made up of parallel constructs.

#+beamer: \vspace{1.5em}

*** Minipage :B_minipage:
:PROPERTIES:
:BEAMER_env: minipage
:BEAMER_OPT: 10cm
:END:

**** RTLBlock 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{RTLBlock}};
    \node[draw,ellipse] (output) at (5,2) {\small\texttt{RTLBlock}};
    \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}(RTLBlock)}};%
      \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{RTLPar}};%
    \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}(RTLPar)}};%
      \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) {RTL};
    \node[language] at (6,0) (ltl) {LTL};
    \node[language] at (8,0) (ppc) {PPC};
    \node[language] at (2,-2) (acblock) {\small RTLBlock};
    \node[language] at (4,-2) (acpar) {\small RTLPar};
    \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 *RTLBlock* $\rightarrow$ *RTLBlock* and from *RTLBlock* to *RTLPar*.

** 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.

**** RTL 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

**** RTL 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

**** RTL 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

**** RTL 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

**** RTL 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

**** RTL 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

**** RTL 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

**** RTL 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