From 7afe2de9abfdbf6045863a9a31dec51b62b896a7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 27 Sep 2021 17:01:34 +0100 Subject: Add presentation --- presentation/.gitignore | 15 + presentation/assets/oopsla21.png | Bin 0 -> 63401 bytes presentation/beamercolorthemeauriga.sty | 35 + presentation/beamerthemeauriga.sty | 128 ++ presentation/outline.org | 9 + presentation/presentation.org | 2075 +++++++++++++++++++++++++++++++ presentation/setup.org | 25 + 7 files changed, 2287 insertions(+) create mode 100644 presentation/.gitignore create mode 100644 presentation/assets/oopsla21.png create mode 100644 presentation/beamercolorthemeauriga.sty create mode 100644 presentation/beamerthemeauriga.sty create mode 100644 presentation/outline.org create mode 100644 presentation/presentation.org create mode 100644 presentation/setup.org diff --git a/presentation/.gitignore b/presentation/.gitignore new file mode 100644 index 0000000..347c527 --- /dev/null +++ b/presentation/.gitignore @@ -0,0 +1,15 @@ +.DS_Store +.auctex-auto/ +_minted-*/ + +*.aux +*.vrb +*.log +*.nav +*.out +*.snm +*.synctex.gz +*.tex +*.toc +*.fdb_latexmk +*.fls diff --git a/presentation/assets/oopsla21.png b/presentation/assets/oopsla21.png new file mode 100644 index 0000000..15393a3 Binary files /dev/null and b/presentation/assets/oopsla21.png differ diff --git a/presentation/beamercolorthemeauriga.sty b/presentation/beamercolorthemeauriga.sty new file mode 100644 index 0000000..6c9cf63 --- /dev/null +++ b/presentation/beamercolorthemeauriga.sty @@ -0,0 +1,35 @@ +% Auriga theme +% https://github.com/anishathalye/auriga + +% ==================== +% Definitions +% ==================== + +\definecolor{lightgray}{RGB}{245, 246, 250} +\definecolor{darkgray}{RGB}{79,79,79} +\definecolor{lightgreen}{HTML}{003E74} +\definecolor{purple}{HTML}{751E66} +\definecolor{brown}{HTML}{0F8291} + +% ==================== +% Theme +% ==================== + +% Basic colors +\setbeamercolor{palette primary}{fg=black,bg=white} +\setbeamercolor{palette secondary}{fg=black,bg=white} +\setbeamercolor{palette tertiary}{bg=black,fg=white} +\setbeamercolor{palette quaternary}{fg=black,bg=white} +\setbeamercolor{structure}{fg=brown} + +\setbeamercolor{emph}{fg=lightgreen} +\setbeamercolor{alerted text}{fg=purple} + +% Itemize +\setbeamercolor{item}{fg=black} + +% Page numbering +\setbeamercolor{page number in head/foot}{fg=lightgreen} + +% Frame titles +\setbeamercolor{frametitle}{fg=black} diff --git a/presentation/beamerthemeauriga.sty b/presentation/beamerthemeauriga.sty new file mode 100644 index 0000000..5ecc877 --- /dev/null +++ b/presentation/beamerthemeauriga.sty @@ -0,0 +1,128 @@ +% Auriga theme +% https://github.com/anishathalye/auriga + +% ==================== +% Dependencies +% ==================== + +\RequirePackage{exscale} +\RequirePackage{ragged2e} +\RequirePackage{changepage} +\RequirePackage{fontspec} +\RequirePackage{xpatch} +\RequirePackage{microtype} +\RequirePackage{xparse} +\RequirePackage{xspace} +\RequirePackage{graphicx} + +% ==================== +% Fonts +% ==================== + +\newfontfamily\Raleway[Ligatures=TeX]{Raleway} +\newfontfamily\Lato[Ligatures=TeX]{Lato} +\newfontfamily\HKGrotesk[Ligatures=TeX]{HK Grotesk} + +\usefonttheme{professionalfonts} + +\setsansfont{HKGrotesk}[ + UprightFont=*-Regular, + ItalicFont=*-Italic, + BoldFont=*-Bold, + BoldItalicFont=*-BoldItalic +] + +\defaultfontfeatures{Ligatures=NoCommon} +\setmonofont[Renderer=Basic]{Iosevka} + +\setbeamerfont{title page}{family=\Raleway} +\setbeamerfont{title page title}{size=\LARGE,series=\bfseries} +\setbeamerfont{title page subtitle}{size=\small} +\setbeamerfont{title page author}{size=\footnotesize} +\setbeamerfont{title page institute}{size=\scriptsize} +\setbeamerfont{frametitle}{family=\Raleway,size=\large,series=\bfseries} +\setbeamerfont{caption}{size=\Macros} + +% ==================== +% footnotesizeb +% ==================== + +\newcommand{\samelineand}{\qquad} + +% ==================== +% Elements +% ==================== + +% Itemize + +\setbeamertemplate{itemize item}[circle] +\setbeamertemplate{itemize subitem}[circle] +\setbeamertemplate{itemize subsubitem}[circle] +%\xpatchcmd{\itemize} +% {\def\makelabel} +% {\ifnum\@itemdepth=1\relax +% \setlength\itemsep{3ex}% separation for first level +% \else +% \ifnum\@itemdepth=2\relax +% \setlength\itemsep{0.5ex}% separation for second level +% \else +% \ifnum\@itemdepth=3\relax +% \setlength\itemsep{0.5ex}% separation for third level +% \fi\fi\fi\def\makelabel +% } +% {} +% {} + +% Equation +\setlength\belowdisplayshortskip{2ex} + +% Caption +\setlength{\abovecaptionskip}{2ex} +\setlength{\belowcaptionskip}{1ex} +\setbeamertemplate{caption} +{ + {\usebeamerfont{caption}\insertcaption} +} + +% Navigation +\beamertemplatenavigationsymbolsempty + +% ==================== +% Components +% ==================== + +% Title page +\setbeamertemplate{title page} +{ + \begin{centering} + \vskip5ex plus 1filll + {\usebeamerfont{title page title}\usebeamercolor[fg]{title page}\inserttitle\\[0.5ex]} + {\usebeamerfont{title page subtitle}\usebeamercolor[fg]{title page}\insertsubtitle\\[3ex]} + {\par\noindent\centering\color{lightgreen}\rule{350pt}{2pt}\\[3ex]} + {\usebeamerfont{title page author}\usebeamercolor[fg]{title page}\insertauthor\\[2ex]} + {\usebeamerfont{title page institute}\usebeamercolor[fg]{title page}\insertinstitute\\[1ex]} + \vskip0pt plus 1filll + \end{centering} + {\hfill\includegraphics[height=1cm]{./assets/oopsla21.png}} +} + +% Footer +\setbeamertemplate{footline}{ + \hspace{2em}\includegraphics[height=1cm]{./assets/imperial_logo.pdf}% + \hfill% + \usebeamercolor[fg]{page number in head/foot}% + \usebeamerfont{page number in head/foot}% + \hspace{2em}% + \insertframenumber\kern1em\vskip2ex% +} + +% Frame title +\setbeamertemplate{frametitle}{ + \nointerlineskip + \vskip2ex + {\usebeamerfont{frametitle}\usebeamercolor[fg]{frametitle}\insertframetitle\\[-2.5ex]} + {\par\color{lightgreen}\rule{390pt}{2pt}} +} + +% Alert +\setbeamerfont{alerted text}{series=\bfseries} diff --git a/presentation/outline.org b/presentation/outline.org new file mode 100644 index 0000000..3d7470e --- /dev/null +++ b/presentation/outline.org @@ -0,0 +1,9 @@ +#+title: Outline + +For the presentation at chalmers, I will in general want the following outline: + +* Background + +The background that I need to introduce is: What is HLS, and what is CompCert. + +* diff --git a/presentation/presentation.org b/presentation/presentation.org new file mode 100644 index 0000000..3902b42 --- /dev/null +++ b/presentation/presentation.org @@ -0,0 +1,2075 @@ +#+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 <+-> +- When fuzzing OpenCL tools (Lidbury et al.), Intel's OpenCL could not be fuzzed because of *too many issues*. +- 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: + +Debugging HLS tools when they go wrong is difficult: + +#+attr_beamer: :overlay <+-> +- It is not clear what part of the input caused the bug. +- Only testing the input specification is not enough. + +** 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 + +** 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}~ + +** Memory Inferrence Pass + +- An HTL $\rightarrow$ HTL translation removes loads and stores. +- Replaced by accesses to a proper *RAM*. + +#+beamer: \vspace{1em} + +~stack[{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}]~ + +#+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 + +*** 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, \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 + +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: + +- We have an *algorithm* describing the *translation*. +- Have to *prove* that it does not change *behaviour* with respect to our language semantics. + +#+beamer: \vspace{1em} + +*** 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 + +* 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: + +- ~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 + +** 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*. + +** 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 + +** Conclusion + +Written a formally verified high-level synthesis tool in *Coq* based on *CompCert*. + +#+attr_beamer: :overlay <+-> +- Base translation *proven correct*. +- Some optimisations *implemented*, proofs being worked on. +- Small issues such as *unsigned comparisons* not working. + +** 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 +** 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 +: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 +: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 +: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 +: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 +: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 +: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 +: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 +:BEAMER_env: onlyenvNH +:END: + +#+begin_src C +for (int i = 1; i < N; i++) { + x = A[i]; + sum = sum + x; + A[i] = sum; +} +#+end_src + +*** Transformed loop :B_column: +:PROPERTIES: +:BEAMER_ENV: column +:BEAMER_COL: 0.45 +:END: + +**** Code :B_onlyenvNH: +:PROPERTIES: +:BEAMER_ACT: <1> +:BEAMER_env: onlyenvNH +:END: + +#+begin_src C +x = A[0]; +sum = sum + x; +x = A[1]; +for (int i = 0; i < N - 2; i++) { + A[i] = sum; + sum = sum + x; + x = A[i + 2]; +} +A[N-2] = sum; +sum = sum + x; +A[N-1] = sum; +#+end_src +** Example of Iterative Modulo Scheduling + +*** Initial loop :B_column: +:PROPERTIES: +:BEAMER_ENV: column +:BEAMER_COL: 0.45 +:END: + +**** Code :B_onlyenvNH: +:PROPERTIES: +:BEAMER_ACT: <1> +:BEAMER_env: onlyenvNH +:END: + +#+begin_src C +for (int i = 1; i < N; i++) { + c1 = acc[i-1] * c; + c2 = x[i] * y[i]; + acc[i] = c1 + c2; +} +#+end_src + +*** Transformed loop :B_column: +:PROPERTIES: +:BEAMER_ENV: column +:BEAMER_COL: 0.45 +:END: + +**** Code :B_onlyenvNH: +:PROPERTIES: +:BEAMER_ACT: <1> +:BEAMER_env: onlyenvNH +:END: + +#+begin_src C +c1 = acc[0] * c; +c2 = x[1] * y[1]; +for (int i = 1; i < N - 1; i++) { + acc[i] = c1 + c2; + c2 = x[i+1] * y[i+1]; + c1 = acc[i+1] * c; +} +acc[i] = c1 + c2; +#+end_src + diff --git a/presentation/setup.org b/presentation/setup.org new file mode 100644 index 0000000..99d8006 --- /dev/null +++ b/presentation/setup.org @@ -0,0 +1,25 @@ +#+latex_compiler: lualatex +#+latex_class_options: [12pt,aspectratio=169] +#+latex_header: \usepackage{tikz} +#+latex_header: \usepackage{amsmath} +#+latex_header: \usepackage{mathpartir} +#+latex_header: \usepackage{booktabs} +#+latex_header:\usepackage{microtype} +#+latex_header:\usepackage{mathtools} +#+latex_header_extra: \DisableLigatures{encoding=T1, family=tt*} +#+latex_header_extra: \usemintedstyle{manni} +#+latex_header_extra: \setminted{fontsize=\small} +#+latex_header_extra: \institute[shortinst]{Imperial College London} +#+latex_header_extra: \AtBeginSection[]{\begin{frame}\frametitle{Outline}\tableofcontents[currentsection]\end{frame}} +#+latex_header_extra: \usetikzlibrary{shapes,calc,arrows.meta} +#+latex_header_extra: \definecolor{keywordcolour}{HTML}{8f0075} +#+latex_header_extra: \definecolor{functioncolour}{HTML}{721045} +#+latex_header_extra: \definecolor{constantcolour}{HTML}{0000bb} +#+latex_header_extra: \newcommand\yhkeywordsp[1]{\;\;\texttt{\textcolor{keywordcolour}{#1}}} +#+latex_header_extra: \newcommand\yhkeyword[1]{\texttt{\textcolor{keywordcolour}{#1}}} +#+latex_header_extra: \newcommand\yhfunctionsp[1]{\;\;\texttt{\textcolor{functioncolour}{#1}}} +#+latex_header_extra: \newcommand\yhfunction[1]{\texttt{\textcolor{functioncolour}{#1}}} +#+latex_header_extra: \newcommand\yhconstant[1]{\texttt{\textcolor{constantcolour}{#1}}} + +#+beamer_theme: auriga +#+beamer_color_theme: auriga -- cgit