diff options
Diffstat (limited to 'presentation.org')
| -rw-r--r-- | presentation.org | 2373 |
1 files changed, 2373 insertions, 0 deletions
diff --git a/presentation.org b/presentation.org new file mode 100644 index 0000000..2f383c0 --- /dev/null +++ b/presentation.org @@ -0,0 +1,2373 @@ +#+title: Formal Verification of High-Level Synthesis +#+author: \underline{Yann Herklotz}, John Wickerson +#+options: H:2 toc:nil +#+columns: %45ITEM %10BEAMER_ENV(Env) %10BEAMER_ACT(Act) %4BEAMER_COL(Col) +#+setupfile: setup.org + +** Script for start :noexport: + +Hi, I'm Yann and I will be presenting our work on formal verification of high-level synthesis. + +Hardware accelerators are becoming increasingly more popular in many industries, because using a CPU +for those tasks is often unnecessary. For example, a datacenter might have a CPU organising +accesses to various SSDs or harddrives. However, this does not benefit from the flexibility of the +CPU, and would therefore result in increased latency for requests, as well as increased power +consumption. Instead, one would ideally like to have a application-specific integrated circuit that +only does one task, thereby using up less power and probably being more performant at that task. +However, until recently, designing a special chip for each application is expensive. This is where +FPGAs come in, whose main benefit is that their circuit can be reprogrammed at any time. + +** The Need to Design Hardware Accelerators + +Application-specific hardware accelerators are increasingly being needed in industries. + +*** Column 1 +:PROPERTIES: +:BEAMER_ENV: column +:BEAMER_COL: 0.5 +:END: + +#+attr_beamer: :overlay <+-> +- Using a *CPU* everywhere not always the best choice. +- *Application-specific integrated circuits (ASIC)* are the ideal choice, but very expensive to + create. +- *Field-programmable gate arrays (FPGA)* act as *reprogrammable hardware*, therefore can be made + application-specific. + +*** Column 2 +:PROPERTIES: +:BEAMER_ENV: column +:BEAMER_COL: 0.5 +:END: + +**** Minipage +:PROPERTIES: +:BEAMER_ENV: minipage +:BEAMER_OPT: 5cm +:END: + +#+beamer: \vspace{2em} + +***** Only 1 +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: 1 +:END: + +#+begin_export latex +\includegraphics[width=6cm]{assets/database-cpu.pdf} +#+end_export + +***** Only 2 +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: 2 +:END: + +#+begin_export latex +\includegraphics[width=6cm]{assets/database-asic.pdf} +#+end_export + +***** Only 3 +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: 3- +:END: + +#+begin_export latex +\includegraphics[width=6cm]{assets/database-fpga.pdf} +#+end_export + +** Where does the flexibility of FPGAs come from? + +#+attr_beamer: :overlay <+-> +- FPGA's are programmable circuits with two main components. +- *Look up tables (LUTs)* provide flexible logic gates. They are connected by *configurable switches*. +- *RAMs* provide accessible storage. + +*** Minipage +:PROPERTIES: +:BEAMER_ENV: minipage +:BEAMER_OPT: 5cm +:END: + +#+beamer: \centering +#+beamer: \vspace{0.2em} + +**** Only 1 +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: <1> +:END: + +#+begin_export latex +\includegraphics[width=8cm]{assets/fpga.pdf} +#+end_export + +**** Only 2 +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: <2> +:END: + +#+begin_export latex +\includegraphics[width=8cm]{assets/fpga-expl.pdf} +#+end_export + +**** Only 3 +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: <3> +:END: + +#+begin_export latex +\centering +\includegraphics[width=8cm]{assets/fpga-expl2.pdf} +#+end_export + +** So How do we Program an FPGA? + +*** Code example :B_column: +:PROPERTIES: +:BEAMER_ENV: column +:BEAMER_COL: 0.5 +:END: + +**** Top +:PROPERTIES: +:BEAMER_ENV: minipage +:BEAMER_OPT: 4.5cm +:END: + +#+attr_beamer: :overlay <+-> +- FPGAs contain *LUTs* and programmable interconnects. +- Programmed using *hardware description languages*. +- Simulation quite slow. +- High-Level Synthesis is an alternative. +- Faster testing through execution. + +**** Bottom +:PROPERTIES: +:BEAMER_ENV: minipage +:BEAMER_OPT: 2.5cm +:END: + +#+beamer: \vspace{1em} + +***** Only 2 +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: <2> +:END: + +#+begin_export latex +\includegraphics[width=0.5cm]{assets/up-arrow.pdf} Fine control \hspace{1em} +\includegraphics[width=0.5cm]{assets/down-arrow.pdf} Long to design +#+end_export + +***** Only 3 +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: <4> +:END: + +#+begin_export latex +\includegraphics[width=0.5cm]{assets/up-arrow.pdf} Quick to design \hspace{1em} +\includegraphics[width=0.5cm]{assets/down-arrow.pdf} Less control +#+end_export + +*** Code example :B_column: +:PROPERTIES: +:BEAMER_ENV: column +:BEAMER_COL: 0.5 +:END: + +**** Minipage +:PROPERTIES: +:BEAMER_ENV: minipage +:BEAMER_OPT: 5cm +:END: +***** FPGA +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: <1> +:END: + +#+begin_export latex +\includegraphics[width=6.8cm]{assets/fpga-flow.pdf} +#+end_export + +***** Verilog +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: <2> +:END: + +#+begin_export latex +\includegraphics[width=6.8cm]{assets/verilog-flow.pdf} +#+end_export + +***** Verilog Simulation +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: <3> +:END: + +#+begin_export latex +\includegraphics[width=6.8cm]{assets/verilog-flow-testing.pdf} +#+end_export + +***** HLS +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: <4> +:END: + +#+begin_export latex +\includegraphics[width=6.8cm]{assets/hls-flow.pdf} +#+end_export + +***** HLS Testing +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: <5> +:END: + +#+begin_export latex +\includegraphics[width=6.8cm]{assets/hls-flow-testing.pdf} +#+end_export + +** What is High-Level Synthesis :noexport: + +*** High-Level Synthesis (HLS) +:PROPERTIES: +:BEAMER_ENV: definition +:END: + +Translation of a high-level programming language such as C/C++ into a hardware description language (HDL) such as Verilog. + +*** Benefits of HLS :B_blockNH: +:PROPERTIES: +:BEAMER_env: block +:BEAMER_ACT: <2-> +:END: + +- *Usability*: Use software ecosystem. +- *Speed*: Quickly design hardware. + +*** Trade-offs of HLS +:PROPERTIES: +:BEAMER_ENV: block +:BEAMER_ACT: <3-> +:END: + +- *Performance*: Requires automatic parallelisation. +- *Correctness*: Hard to verify generated HDL. + +** Motivation for Formal Verification + +*** HLS Unreliable :B_blockNH: +:PROPERTIES: +:BEAMER_env: blockNH +:END: + +High-level synthesis is often quite unreliable: + +- We fuzzed HLS tools (Herklotz et al. [2021]) and found they failed on simple random test cases. + +#+beamer: \vspace{2em} + +#+attr_latex: :booktabs t +|-----------------+-----------------| +| Tool | Run-time errors | +|-----------------+-----------------| +| Vivado HLS | 1.23% | +| Intel i++ | 0.4% | +| Bambu 0.9.7-dev | 0.3% | +| LegUp 4.0 | 0.1% | +|-----------------+-----------------| + +** Solution :B_frame: +:PROPERTIES: +:BEAMER_env: frame +:BEAMER_OPT: t +:END: + +#+begin_export latex +\definecolor{compcert}{HTML}{bebada} +\definecolor{formalhls}{HTML}{8dd3c7} +\begin{center} + \begin{tikzpicture} + [language/.style={fill=white,rounded corners=3pt,minimum height=7mm}, + continuation/.style={}, + linecount/.style={rounded corners=3pt,dashed},scale=0.8] + \fill[compcert,rounded corners=3pt] (-1.2,-0.5) rectangle (14,2); + \fill[formalhls,rounded corners=3pt] (-1.2,-1) rectangle (14,-2.4); + %\draw[linecount] (-0.95,-0.45) rectangle (3.6,1); + %\draw[linecount] (4,-0.45) rectangle (7.5,1); + \node[language] at (-0.3,0) (clight) {Clight}; + \node[continuation] at (1.5,0) (conta) {$\cdots$}; + \node[language] at (3.5,0) (cminor) {CminorSel}; + \node[language] at (6,0) (rtl) {3AC}; + \node[language] at (8,0) (ltl) {LTL}; + \node[language,anchor=west] at (11.5,0) (aarch) {aarch64}; + \node[language,anchor=west] at (11.5,0.8) (x86) {x86}; + \node[continuation,anchor=west] at (11.5,1.4) (backs) {$\cdots$}; + \node[continuation] at (10,0) (contb) {$\cdots$}; + \node[language] at (6,-1.5) (htl) {HTL}; + \node[language] at (9,-1.5) (verilog) {Verilog}; + \node[anchor=west] at (-0.9,1.6) {\bf CompCert}; + \node[anchor=west] at (-0.9,-1.4) {\bf Vericert}; + %%\node[anchor=west] at (-0.9,0.7) {\small $\sim$ 27 kloc}; + %%\node[anchor=west] at (4.1,0.7) {\small $\sim$ 46 kloc}; + %%\node[anchor=west] at (2,-1.5) {\small $\sim$ 17 kloc}; + \node[align=center] at (4,-2) {\footnotesize RAM\\[-0.5em]\footnotesize insertion}; + \draw[->,thick] (clight) -- (conta); + \draw[->,thick] (conta) -- (cminor); + \draw[->,thick] (cminor) -- (rtl); + \draw[->,thick] (rtl) -- (ltl); + \draw[->,thick] (ltl) -- (contb); + \draw[->,thick] (contb) -- (aarch); + \draw[->,thick] (contb) to [out=0,in=200] (x86.west); + \draw[->,thick] (contb) to [out=0,in=190] (backs.west); + \draw[->,thick] (rtl) -- (htl); + \draw[->,thick] (htl) -- (verilog); + \draw[->,thick] (htl.west) to [out=180,in=150] (5,-2.2) to [out=330,in=270] (htl.south); + \end{tikzpicture}%} +\end{center} +#+end_export + +#+beamer: \vspace{1em} + +*** Minipage +:PROPERTIES: +:BEAMER_ENV: minipage +:BEAMER_OPT: 5cm +:END: + +**** Block 1 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <1> +:END: + +Use CompCert, a fully verified C compiler, and add an HLS backend. + +**** Block 2 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <2> +:END: + +Support for: all *control flow*, *fixedpoint*, *non-recursive functions* and *local arrays/structs/unions*. + +* Example +** Example: 3AC :B_frame: + +*** Code example :B_column: +:PROPERTIES: +:BEAMER_ENV: column +:BEAMER_COL: 0.45 +:END: + +**** Code 1 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_ACT: <1> +:BEAMER_env: onlyenvNH +:END: + +#+begin_src C +int main() { + int x[2] = {3, 6}; + int i = 1; + return x[i]; +} +#+end_src + +**** Explanation 5 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <2> +:END: + +- *Three address code (3AC)* instructions are represented as a control-flow graph (CFG). +- Each instruction links to the next one. + +*** Text :B_column: +:PROPERTIES: +:BEAMER_ENV: column +:BEAMER_COL: 0.45 +:END: + +**** Text 1 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_ACT: <1> +:BEAMER_ENV: onlyenvNH +:END: + +- Example of a very simple program performing loads and stores. + +**** 3AC Code 5 :B_onlyenv: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <2> +:END: + +#+attr_latex: :options fontsize=\small +#+begin_src C +main() { + x5 = 3 + int32[stack(0)] = x5 + x4 = 6 + int32[stack(4)] = x4 + x1 = 1 + x3 = stack(0) (int) + x2 = int32[x3 + x1 * 4 + 0] + return x2 +} +#+end_src + +** HTL Overview + +The representation of the *finite state-machine with datapath* is abstract and called **HTL**. + +*** Datapath and control logic :B_blockNH: +:PROPERTIES: +:BEAMER_env: blockNH +:END: + +src_coq[:exports code]{Definition datapath := } $\mathbb{Z}^+ \mapsto \texttt{\small Verilog.stmnt}$ + +src_coq[:exports code]{Definition controllogic := } $\mathbb{Z}^+ \mapsto \texttt{\small +Verilog.stmnt}$ + +*** Minipage +:PROPERTIES: +:BEAMER_ENV: minipage +:BEAMER_OPT: 5cm +:END: + +**** Module definition :B_blockNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 2 +:END: + +#+beamer: \vspace{0.25em} + +#+attr_latex: :options fontsize=\footnotesize +#+begin_src coq +Record module: Type := mkmodule { + mod_datapath: datapath; + mod_controllogic: controllogic; + mod_reset: reg; + mod_ram: ram_spec; + ... + }. +#+end_src + +**** Module definition :B_blockNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 3 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={2-3} +#+begin_src coq +Record module: Type := mkmodule { + mod_datapath: datapath; + mod_controllogic: controllogic; + mod_reset: reg; + mod_ram: ram_spec; + ... + }. +#+end_src + +**** Module definition :B_blockNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 4 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={4} +#+begin_src coq +Record module: Type := mkmodule { + mod_datapath: datapath; + mod_controllogic: controllogic; + mod_reset: reg; + mod_ram: ram_spec; + ... + }. +#+end_src + +**** Module definition :B_blockNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 5 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={5} +#+begin_src coq +Record module: Type := mkmodule { + mod_datapath: datapath; + mod_controllogic: controllogic; + mod_reset: reg; + mod_ram: ram_spec; + ... + }. +#+end_src + +** Translation (3AC $\rightarrow$ HTL) + +Translation from *control-flow graph* into a *finite state-machine with datapath*. + +#+beamer: \pause +#+beamer: \vspace{1em} + +#+attr_beamer: :overlay <+-> +- *Control-flow* is translated into a *finite state-machine*. +- Each *3AC instructions* translated into equivalent *Verilog statements*. +- Call *stack* implemented as *Verilog array*. +- Pointers for loads and stores translated to array addresses. + - *Byte* addressed to *word* addressed. + +#+beamer: \vspace{1em} + +*** Minipage :B_minipage:noexport: +:PROPERTIES: +:BEAMER_env: minipage +:BEAMER_OPT: 5cm +:END: + +**** Only 1 :B_onlyenvNH:noexport: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 3 +:END: + +~x3 = x3 + x5 + 0~ $\quad\longrightarrow\quad$ src_verilog[:exports code]{reg_3 <= {reg_3 + {reg_5 + 0}}} + +**** Only 2 :B_onlyenvNH:noexport: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 5-6 +:END: + +~x5 + x1 * 4 + 0~ $\quad\longrightarrow\quad$ src_verilog[:exports code]{{{{reg_5 + 0} + {reg_1 * 4}} / 4}} + +** Memory Inference Pass + +- An HTL $\rightarrow$ HTL translation removes loads and stores. +- Replaced by accesses to a proper *RAM*. + +*** Minipage +:PROPERTIES: +:BEAMER_COL: 0.5 +:END: + + +#+beamer: \vspace{1em} + +src_verilog[:exports code]{stack[reg_5 / 4]} + +#+beamer: \vspace{1em} + +becomes + +#+beamer: \vspace{1em} + +**** Minipage +:PROPERTIES: +:BEAMER_ENV: minipage +:BEAMER_OPT: 5cm +:END: + +***** Only 1 +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: 1 +:END: + +#+beamer: \vspace{0.25em} + +#+attr_latex: :options fontsize=\footnotesize +#+begin_src verilog +u_en <= ( ~ u_en); +wr_en <= 0; +addr <= reg_5 / 4; +#+end_src + +***** Only 2 +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: 2 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={1} +#+begin_src verilog +u_en <= ( ~ u_en); +wr_en <= 0; +addr <= reg_5 / 4; +#+end_src + +***** Only 3 +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: 3 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={2} +#+begin_src verilog +u_en <= ( ~ u_en); +wr_en <= 0; +addr <= reg_5 / 4; +#+end_src + +***** Only 4 +:PROPERTIES: +:BEAMER_ENV: onlyenvNH +:BEAMER_ACT: 4 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={3} +#+begin_src verilog +u_en <= ( ~ u_en); +wr_en <= 0; +addr <= reg_5 / 4; +#+end_src + + +** Verilog Syntax :noexport: + +*** Column 1 :B_column: +:PROPERTIES: +:BEAMER_COL: 0.45 +:END: + +**** No highlight :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <1> +:END: + +#+attr_latex: :options fontsize=\footnotesize +#+begin_src verilog +module top(input clk, input [31:0] in1, + output reg [31:0] out1); + reg [31:0] reg_1, tmp; + + always @(posedge clk) begin + reg1 <= in1; + end + + always @(posedge clk) begin + tmp = reg1; + out1 <= tmp; + end +endmodule +#+end_src + +**** Highlight :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <2> +:END: + +#+attr_latex: :options highlightlines={5-7,9-12},fontsize=\footnotesize +#+begin_src verilog +module top(input clk, input [31:0] in1, + output reg [31:0] out1); + reg [31:0] reg_1, tmp; + + always @(posedge clk) begin + reg1 <= in1; + end + + always @(posedge clk) begin + tmp = reg1; + out1 <= tmp; + end +endmodule +#+end_src + +*** Column 2 +:PROPERTIES: +:BEAMER_COL: 0.55 +:END: + +#+attr_beamer: :overlay <+-> +- Verilog example for a simple shift register. +- Always block run in parallel + + +** Translation (HTL $\rightarrow$ Verilog) :B_frame: + +*** Column +:PROPERTIES: +:BEAMER_COL: 0.45 +:END: + +**** Code 1 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <1> +:END: + +#+attr_latex: :options fontsize=\tiny +#+begin_src verilog +module main(reset, clk, finish, return_val); + input [0:0] reset, clk; + output reg [0:0] finish = 0; + output reg [31:0] return_val = 0; + reg [31:0] reg_3 = 0, addr = 0, d_in = 0, + reg_5 = 0, wr_en = 0, + state = 0, reg_2 = 0, + reg_4 = 0, d_out = 0, reg_1 = 0; + reg [0:0] en = 0, u_en = 0; + reg [31:0] stack [1:0]; + // RAM interface + always @(negedge clk) + if ({u_en != en}) begin + if (wr_en) stack[addr] <= d_in; + else d_out <= stack[addr]; + en <= u_en; + end +#+end_src + +**** Code 2 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <2> +:END: + +#+attr_latex: :options fontsize=\tiny,highlightlines={11-17} +#+begin_src verilog +module main(reset, clk, finish, return_val); + input [0:0] reset, clk; + output reg [0:0] finish = 0; + output reg [31:0] return_val = 0; + reg [31:0] reg_3 = 0, addr = 0, d_in = 0, + reg_5 = 0, wr_en = 0, + state = 0, reg_2 = 0, + reg_4 = 0, d_out = 0, reg_1 = 0; + reg [0:0] en = 0, u_en = 0; + reg [31:0] stack [1:0]; + // RAM interface + always @(negedge clk) + if ({u_en != en}) begin + if (wr_en) stack[addr] <= d_in; + else d_out <= stack[addr]; + en <= u_en; + end +#+end_src + +**** Code 3 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <3> +:END: + +#+attr_latex: :options fontsize=\tiny +#+begin_src verilog + // Data-path + always @(posedge clk) + case (state) + 32'd11: reg_2 <= d_out; + 32'd8: reg_5 <= 32'd3; + 32'd7: begin + u_en <= ( ~ u_en); wr_en <= 32'd1; + d_in <= reg_5; addr <= 32'd0; + end + 32'd6: reg_4 <= 32'd6; + 32'd5: begin + u_en <= ( ~ u_en); wr_en <= 32'd1; + d_in <= reg_4; addr <= 32'd1; + end + 32'd4: reg_1 <= 32'd1; + 32'd3: reg_3 <= 32'd0; + 32'd2: begin + u_en <= ( ~ u_en); wr_en <= 32'd0; + addr <= {{{reg_3 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}; + end + 32'd1: begin finish = 32'd1; return_val = reg_2; end + default: ; + endcase +#+end_src + +**** Code 4 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <4> +:END: + +#+attr_latex: :options fontsize=\tiny,highlightlines={7,8,12,13,18,19} +#+begin_src verilog + // Data-path + always @(posedge clk) + case (state) + 32'd11: reg_2 <= d_out; + 32'd8: reg_5 <= 32'd3; + 32'd7: begin + u_en <= ( ~ u_en); wr_en <= 32'd1; + d_in <= reg_5; addr <= 32'd0; + end + 32'd6: reg_4 <= 32'd6; + 32'd5: begin + u_en <= ( ~ u_en); wr_en <= 32'd1; + d_in <= reg_4; addr <= 32'd1; + end + 32'd4: reg_1 <= 32'd1; + 32'd3: reg_3 <= 32'd0; + 32'd2: begin + u_en <= ( ~ u_en); wr_en <= 32'd0; + addr <= {{{reg_3 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}; + end + 32'd1: begin finish = 32'd1; return_val = reg_2; end + default: ; + endcase +#+end_src + +**** Code 5 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <5> +:END: + +#+attr_latex: :options fontsize=\tiny +#+begin_src verilog + // Control logic + always @(posedge clk) + if ({reset == 32'd1}) state <= 32'd8; + else case (state) + 32'd11: state <= 32'd1; 32'd4: state <= 32'd3; + 32'd8: state <= 32'd7; 32'd3: state <= 32'd2; + 32'd7: state <= 32'd6; 32'd2: state <= 32'd11; + 32'd6: state <= 32'd5; 32'd1: ; + 32'd5: state <= 32'd4; default: ; + endcase +endmodule +#+end_src + +*** Text +:PROPERTIES: +:BEAMER_COL: 0.45 +:END: + +**** Text 1 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_ACT: <1-5> +:BEAMER_env: onlyenvNH +:END: + +#+attr_beamer: :overlay <+-> +- Finally, translate the FSMD into Verilog. +- This includes a RAM interface. +- Data path is translated into a case statement. +- RAM loads and stores automatically turn off RAM. +- Control logic is translated into another case statement with a reset. + +* Verification +** Verilog Semantics (Adapted from Lööw et al. (2019)) + +- Top-level semantics are *small-step operational semantics*. + +*** Only 1 +:PROPERTIES: +:BEAMER_ENV: blockNH +:BEAMER_ACT: <1-> +:END: + +#+begin_export latex +{\centering\includegraphics[width=8cm]{assets/clk.pdf}\par} +#+end_export + +*** Only 2 +:PROPERTIES: +:BEAMER_ENV: blockNH +:BEAMER_ACT: <2> +:END: + +- At each clock tick, the *whole module* is executed using *big-step semantics*. + +#+begin_export latex +{\centering\includegraphics[width=6cm]{assets/big-step.pdf}\par} +#+end_export + +** How the Verilog semantics changed :noexport: + +Changed the semantics in *5* minor ways to make it a better HLS target. + +#+attr_beamer: :overlay <+-> +- Verilog *2D array support*, +- add *negative edge* support, +- add support for *declarations*, +- *removed* support for *external IO*, and +- *simplifying* support for *bitvectors*. + +#+beamer: \vspace{1em} + +*** Minipage :B_minipage: +:PROPERTIES: +:BEAMER_env: minipage +:BEAMER_OPT: 5cm +:END: + +**** Only 1 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 1 +:END: + +#+attr_latex: :options fontsize=\small +#+begin_src verilog +reg [31:0] x[1:0]; +always @(posedge clk) begin x[0] = 1; x[1] <= 1; end +#+end_src + +**** Only 2 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 2 +:END: + +#+begin_export latex +\begin{equation*} +\inferrule[Module]{(\Gamma, \epsilon, \vec{m})\ \downarrow_{\text{module}^{+}} (\Gamma', \Delta') \\ (\Gamma'\ //\ \Delta', \epsilon, \vec{m}) \downarrow_{\text{module}^{-}} (\Gamma'', \Delta'')}{(\Gamma, \yhkeyword{module}\ \yhconstant{main} \yhkeyword{(...);}\ \vec{m}\ \yhkeyword{endmodule}) \downarrow_{\text{program}} (\Gamma''\ //\ \Delta'')} +\end{equation*} +#+end_export + +**** Only 3 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 3 +:END: + +Have an association map for each register to declaration. + +- Information about input or output. +- Information about size. + +**** Only 4 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 4 +:END: + +Constant inputs and outputs modelling the HLS interface. + +**** Only 5 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 5 +:END: + +Use integers modulo $2^n$. + +Those are the only types needed for HLS. + +** How do we prove the HLS tool correct? :noexport: + +*** Notes +:PROPERTIES: +:BEAMER_ENV: note +:END: + +This describes the main proof that is needed to show that the HLS tool is correct. I should probably be spending most of my time on this section, as that is what George will be most unfamiliar with. + +*** Text 1 :B_blockNH: +:PROPERTIES: +:BEAMER_env: blockNH +:END: + +#+beamer: \vspace{-1.5em} + +- We have an *algorithm* describing the *translation*. +- Have to *prove* that it does not change *behaviour* with respect to our language semantics. + +*** Minipage :B_minipage: +:PROPERTIES: +:BEAMER_env: minipage +:BEAMER_OPT: 5cm +:END: + +**** Table :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <2> +:END: + +#+attr_latex: :booktabs t :align cp{10cm} +|------------+------------------------------------------------------------------| +| Behaviour | Guarantee | +|------------+------------------------------------------------------------------| +| Converging | Means a result is obtained, Verilog and C results must be equal. | +| Diverging | C is in an infinite loop, Verilog must execute indefinitely. | +| Wrong | Such as undefined behaviour, no guarantees need to be shown. | +|------------+------------------------------------------------------------------| + +**** Theorem :B_onlyenvNH:noexport: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <3> +:END: + +***** Main Backward Simulation :B_theorem: +:PROPERTIES: +:BEAMER_env: theorem +:END: + +#+begin_export latex +\begin{equation*} + \forall C, V, B,\quad \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land \mathit{Safe}(C) \implies (V \Downarrow B \implies C \Downarrow B). +\end{equation*} +#+end_export + +where + +#+begin_export latex +\begin{equation*} + \mathit{Safe}(C):\ \forall B,\ C \Downarrow B \implies B \in \texttt{Safe} +\end{equation*} +#+end_export + +**** Theorem :B_onlyenvNH:noexport: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <4-> +:END: + +***** Forward Simulation :B_theorem: +:PROPERTIES: +:BEAMER_env: theorem +:END: + +#+begin_export latex +\begin{align*} + &(\forall C, V, B \in \texttt{Safe},\quad \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land C \Downarrow B \implies V \Downarrow B)\\ +&\land (\forall V, B_1, B_2,\quad V \Downarrow B_1 \land V \Downarrow B_2 \implies B_1 = B_2). +\end{align*} +#+end_export + +** 3AC $\to$ HTL: Build a Specification :noexport: + +Assuming $\yhfunction{HLS} (C) = \yhconstant{OK} (V)$ requires reasoning about implementation details. + +#+beamer: \pause +#+beamer: \vspace{1em} + +Instead we build a model of the translation which we can use. + +#+begin_export latex +\begin{equation*} + \forall C, V,\quad \yhfunction{HLS} (C) = \yhconstant{OK} (V) \rightarrow \yhfunction{tr\_hls}\ \ C\ \ V. +\end{equation*} +#+end_export + +#+beamer: \pause + +*** 3AC to HTL operator conversion :B_example: +:PROPERTIES: +:BEAMER_env: example +:BEAMER_ACT: <2-> +:END: + +#+begin_export latex +\begin{equation*} + \inferrule[Iop]{\yhfunction{tr\_op } \mathit{op}\ \vec{a} = \yhconstant{OK } e}{\yhfunction{tr\_instr}\ \mathit{fin}\ \mathit{rtrn}\ \sigma\ \mathit{stk}\ (\yhconstant{Iop}\ \mathit{op}\ \vec{a}\ d\ n)\ (d \Leftarrow e)\ (\sigma \Leftarrow n)} +\end{equation*} +#+end_export + +** 3AC $\to$ HTL: Prove Forward Simulation :noexport: + +*** Column 1 +:PROPERTIES: +:BEAMER_COL: 0.35 +:END: + +#+begin_export latex +\definecolor{highlightcol}{HTML}{db6060} +\begin{center} + \begin{tikzpicture} + \begin{scope} + \node[circle,minimum size=2] (s1) at (0,3) {$S_{1}$};% + \only<2>{\node[circle,minimum size=2] (s1) at (0,3) {\textcolor{highlightcol}{$S_{1}$}};} + \node[circle,minimum size=2] (r1) at (4,3) {$R_{1}$};% + \only<2-3>{\node[circle,minimum size=2] (r1) at (4,3) {\textcolor{highlightcol}{$R_{1}$}};} + \node[circle,minimum size=2] (s2) at (0,0) {$S_{2}$};% + \only<4>{\node[circle,minimum size=2] (s2) at (0,0) {\textcolor{highlightcol}{$S_{2}$}};} + \node[circle,minimum size=2] (r2) at (4,0) {$R_{2}$};% + \only<3-4>{\node[circle,minimum size=2] (r2) at (4,0) {\textcolor{highlightcol}{$R_{2}$}};} + \draw (s1) -- node[above] {\textasciitilde{}} node[below] {\small\texttt{match\_states}} ++ (r1); + \only<2>{\draw[highlightcol] (s1) -- node[above] {\textasciitilde{}} node[below] {\small\texttt{match\_states}} ++ (r1);} + \draw[-{Latex[length=3mm]}] (s1) -- (s2); + \draw[dashed] (s2) -- node[above] {\textasciitilde{}} node[below] {\small\texttt{match\_states}} ++ (r2);% + \only<4>{\draw[highlightcol,dashed] (s2) -- node[above] {\textasciitilde{}} node[below] {\small\textcolor{highlightcol}{\texttt{match\_states}}} ++ (r2);} + \draw[-{Latex[length=3mm]},dashed] (r1) -- node[left] {+} ++ (r2);% + \only<3>{\draw[highlightcol,-{Latex[length=3mm]},dashed] (r1) -- node[left] {+} ++ (r2);} + \end{scope} + \end{tikzpicture} +\end{center} +#+end_export + +*** Column 2 +:PROPERTIES: +:BEAMER_COL: 0.6 +:END: + +\texttt{match\_states} defined as: + +#+begin_export latex +\begin{equation*} + \mathcal{I} \land R \le \Gamma \land M \le \Gamma ! \mathit{stk} \land \mathit{pc} = \Gamma ! \sigma +\end{equation*} +#+end_export + +Prove the simulation diagram correct: + +#+beamer: \pause + +#+attr_beamer: :overlay <+-> +- Assuming an initial match between the 3AC state $S_1$ and Verilog state $R_1$, +- there exists 1 or more steps in Verilog, +- such that after 1 step in 3AC, the resulting states match. + +** Main Challenges in Proof + +*** Translation of memory model +:PROPERTIES: +:BEAMER_ENV: block +:BEAMER_ACT: <1-> +:END: + +*Abstract/infinite memory model* translated into *concrete/finite RAM*. + +*** Integration of Verilog Semantics +:PROPERTIES: +:BEAMER_ENV: block +:BEAMER_ACT: <2-> +:END: + +- *Verilog semantics* differs from CompCert's main assumptions of intermediate language semantics. +- Abstract values like the *program counter* now correspond to *values in registers*. + +* Extensions +** Current work + +Many optimisations missing: + +- *scheduling* +- *if-conversion* +- memory partitioning +- *loop pipelining* +- polyhedral analysis +- operation chaining +- register allocation + +** New languages for scheduling + +Currently implemented two new languages for it: + +- ~3ACBlock~ :: 3AC with basic blocks. +- ~3ACPar~ :: 3AC with basic blocks made up of parallel constructs. + +#+beamer: \vspace{1.5em} + +*** Minipage :B_minipage: +:PROPERTIES: +:BEAMER_env: minipage +:BEAMER_OPT: 10cm +:END: + +**** 3ACBlock Basic Block +:PROPERTIES: +:BEAMER_ACT: 2 +:BEAMER_env: onlyenv +:END: + +#+begin_src coq +Record bblock: Type := mk_bblock { + bb_body: list instr; + bb_exit: cf_instr +}. +#+end_src + +**** Instructions :B_onlyenv: +:PROPERTIES: +:BEAMER_ACT: 3 +:BEAMER_env: onlyenv +:END: + +#+begin_src coq +Inductive instr: Type := +| RBnop: instr +| RBop: option pred_op -> operation -> list reg -> reg -> instr +| RBload: option pred_op -> memory_chunk -> addressing + -> list reg -> reg -> instr +| RBstore: option pred_op -> memory_chunk -> addressing + -> list reg -> reg -> instr +| RBsetpred: condition -> list reg -> predicate -> instr. +#+end_src + +** More details of transformations + +#+begin_export latex +\scalebox{0.8}{\begin{tikzpicture} + \begin{scope} + \node[draw,minimum width=3cm,minimum height=1cm,align=center] (imstranslation) at (1.5,2) {\small\texttt{\textcolor{functioncolour}{Iterative Modulo}}\\\small\texttt{\textcolor{functioncolour}{Scheduling}}}; + \node[draw,ellipse] (input) at (-1.5,2) {\small\texttt{3ACBlock}}; + \node[draw,ellipse] (output) at (5,2) {\small\texttt{3ACBlock}}; + \draw[->] (input) -- (imstranslation); + \draw[->] (imstranslation) -- (output); + \visible<2->{\node[draw,minimum width=3cm,minimum height=1cm,align=center] (verification) at (1.5,0.5) {\small Equivalence\\\small Check};% + \draw[->] (input) |- (verification);% + \draw[->] (output) |- (verification);% + \node[draw,ellipse] (error) at ($(verification.south) - (0.5,1.5)$) {\small\texttt{\textcolor{constantcolour}{Error}}};% + \draw[->] ($(verification.south) - (0.5,0)$) -- (error);% + \node at (0.3,-0.5) {\footnotesize\texttt{\textcolor{keywordcolour}{false}}};% + \node at (2,-0.3) {\footnotesize\texttt{\textcolor{keywordcolour}{true}}};% + \node[draw,ellipse] (ok) at (5,-0.5) {\small\texttt{\textcolor{constantcolour}{OK}(3ACBlock)}};% + \draw[->] (verification) |- (ok);} + + \visible<3->{\node[draw,minimum width=3cm,minimum height=1cm,align=center] (schedtranslation) at (9.5,-0.5) {\small\texttt{\textcolor{functioncolour}{Resource Constrained}}\\\small\texttt{\textcolor{functioncolour}{Scheduling}}};% + \node[draw,ellipse] (schedoutput) at (13,-0.5) {\small\texttt{3ACPar}};% + \draw[->] (ok) -- (schedtranslation);% + \draw[->] (schedtranslation) -- (schedoutput);% + \node[draw,minimum width=3cm,minimum height=1cm,align=center] (schedverification) at (9.5,-2) {\small Equivalence\\\small Check};% + \draw[->] (ok) |- (schedverification);% + \draw[->] (schedoutput) |- (schedverification);% + \node[draw,ellipse] (schederror) at ($(schedverification.south) - (0.5,1.5)$) {\small\texttt{\textcolor{constantcolour}{Error}}};% + \draw[->] ($(schedverification.south) - (0.5,0)$) -- (schederror);% + \node at (8.3,-3) {\footnotesize\texttt{\textcolor{keywordcolour}{false}}};% + \node at (10,-2.8) {\footnotesize\texttt{\textcolor{keywordcolour}{true}}};% + \node[draw,ellipse] (ok) at (13,-3) {\small\texttt{\textcolor{constantcolour}{OK}(3ACPar)}};% + \draw[->] (schedverification) |- (ok);} + \end{scope} +\end{tikzpicture}} +#+end_export + +** Scheduling example + +#+beamer: \vspace{0.5em} + +*** Column 1 +:PROPERTIES: +:BEAMER_COL: 0.40 +:END: + +**** Minipage :B_minipage: +:PROPERTIES: +:BEAMER_env: minipage +:BEAMER_OPT: 10cm +:END: + +***** Code 1 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 1 +:END: + +#+attr_latex: :options fontsize=\footnotesize +#+begin_src C +p1 = r3 == 0 +r1 = r3 + r4 +(p1) r2 = r3 + r1 +(~ p1) r2 = r4 + r1 +stk[r5] = r2 +r6 = stk[r5+1] +#+end_src + +***** Code 2 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 2 +:END: + +#+attr_latex: :options fontsize=\footnotesize +#+begin_src C +p1 = r3 == 0 +r1 = r3 + r4 +(p1) r2 = r3 + r1 +(~ p1) r2 = r4 + r1 +stk[r5] = r2 +r6 = stk[r5+1] +#+end_src + +***** Code 3 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 3 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={5,6} +#+begin_src C +p1 = r3 == 0 +r1 = r3 + r4 +(p1) r2 = r3 + r1 +(~ p1) r2 = r4 + r1 +stk[r5] = r2 +r6 = stk[r5+1] +#+end_src + +***** Code 4 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 4 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={1} +#+begin_src C +p1 = r3 == 0 +r1 = r3 + r4 +(p1) r2 = r3 + r1 +(~ p1) r2 = r4 + r1 +stk[r5] = r2 +r6 = stk[r5+1] +#+end_src + +#+beamer: \vspace{-2em} + +#+begin_export latex +\begin{align*} + &p_{1} \mapsto r_{3}^{0} = 0 +\end{align*} +#+end_export + +***** Code 5 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 5 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={2} +#+begin_src C +p1 = r3 == 0 +r1 = r3 + r4 +(p1) r2 = r3 + r1 +(~ p1) r2 = r4 + r1 +stk[r5] = r2 +r6 = stk[r5+1] +#+end_src + +#+beamer: \vspace{-2em} + +#+begin_export latex +\begin{align*} + &p_{1} \mapsto r_{3}^{0} = 0\\ + &r_{1} \mapsto r_{3}^{0} + r_{4}^{0} +\end{align*} +#+end_export + +***** Code 6 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 6 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={3} +#+begin_src C +p1 = r3 == 0 +r1 = r3 + r4 +(p1) r2 = r3 + r1 +(~ p1) r2 = r4 + r1 +stk[r5] = r2 +r6 = stk[r5+1] +#+end_src + +#+beamer: \vspace{-2em} + +#+begin_export latex +\begin{align*} + &p_{1} \mapsto r_{3}^{0} = 0\\ + &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\ + &r_{2} \mapsto \begin{cases} + r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1} + \end{cases} +\end{align*} +#+end_export + +***** Code 7 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 7 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={4} +#+begin_src C +p1 = r3 == 0 +r1 = r3 + r4 +(p1) r2 = r3 + r1 +(~ p1) r2 = r4 + r1 +stk[r5] = r2 +r6 = stk[r5+1] +#+end_src + +#+beamer: \vspace{-2em} + +#+begin_export latex +\begin{align*} + &p_{1} \mapsto r_{3}^{0} = 0\\ + &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\ + &r_{2} \mapsto \begin{cases} + r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\ + r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\ + \end{cases} +\end{align*} +#+end_export + +***** Code 8 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 8 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={5} +#+begin_src C +p1 = r3 == 0 +r1 = r3 + r4 +(p1) r2 = r3 + r1 +(~ p1) r2 = r4 + r1 +stk[r5] = r2 +r6 = stk[r5+1] +#+end_src + +#+beamer: \vspace{-2em} + +#+begin_export latex +\begin{align*} + &p_{1} \mapsto r_{3}^{0} = 0\\ + &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\ + &r_{2} \mapsto \begin{cases} + r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\ + r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\ + \end{cases}\\ + &\mathit{Mem} \mapsto \mathit{Mem}^0 \cup \{r_{5}^{0} \mapsto r_{1}^{0} + r_{2}^{0}\} +\end{align*} +#+end_export + +***** Code 9 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 9 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={6} +#+begin_src C +p1 = r3 == 0 +r1 = r3 + r4 +(p1) r2 = r3 + r1 +(~ p1) r2 = r4 + r1 +stk[r5] = r2 +r6 = stk[r5+1] +#+end_src + +#+beamer: \vspace{-2em} + +#+begin_export latex +\begin{align*} + &p_{1} \mapsto r_{3}^{0} = 0\\ + &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\ + &r_{2} \mapsto \begin{cases} + r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\ + r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\ + \end{cases}\\ + &\mathit{Mem} \mapsto \mathit{Mem}^0 \cup \{r_{5}^{0} \mapsto r_{1}^{0} + r_{2}^{0}\}\\ + &r_{6} \mapsto (\mathit{Mem}^0 \cup \{r_{5}^{0} \mapsto r_{1}^{0} + r_{2}^{0}\})[r_{5}^0 + 1] +\end{align*} +#+end_export +***** Code 10 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 10 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={6} +#+begin_src C +p1 = r3 == 0 +r1 = r3 + r4 +(p1) r2 = r3 + r1 +(~ p1) r2 = r4 + r1 +stk[r5] = r2 +r6 = stk[r5+1] +#+end_src + +#+beamer: \vspace{-2em} + +#+begin_export latex +\begin{align*} + &p_{1} \mapsto r_{3}^{0} = 0\\ + &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\ + &r_{2} \mapsto \begin{cases} + r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\ + r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\ + \end{cases}\\ + &\mathit{Mem} \mapsto \mathit{Mem}^0 \cup \{r_{5}^{0} \mapsto r_{1}^{0} + r_{2}^{0}\}\\ + &r_{6} \mapsto \mathit{Mem}^0[r_{5}^0 + 1] +\end{align*} +#+end_export + +*** Column 2 +:PROPERTIES: +:BEAMER_COL: 0.55 +:END: + +**** Minipage :B_minipage: +:PROPERTIES: +:BEAMER_env: minipage +:BEAMER_OPT: 10cm +:END: + +***** Code 2 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 2 +:END: + +#+attr_latex: :options fontsize=\footnotesize +#+begin_src C +p1 = r3 == 0 || r1 = r3 + r4 + || r6 = stk[r5+1] +(p1) r2 = r3 + r1 + || (~ p1) r2 = r4 + r1 +stk[r5] = r1 + r2 +#+end_src + +***** Code 3 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 3 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={2,5} +#+begin_src C +p1 = r3 == 0 || r1 = r3 + r4 + || r6 = stk[r5+1] +(p1) r2 = r3 + r1 + || (~ p1) r2 = r4 + r1 +stk[r5] = r1 + r2 +#+end_src + +***** Code 4 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 4 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={1,2} +#+begin_src C +p1 = r3 == 0 || r1 = r3 + r4 + || r6 = stk[r5+1] +(p1) r2 = r3 + r1 + || (~ p1) r2 = r4 + r1 +stk[r5] = r1 + r2 +#+end_src + +#+beamer: \vspace{-2em} + +#+begin_export latex +\begin{align*} + &p_{1} \mapsto r_{3}^{0} = 0\\ + &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\ + &r_{6} \mapsto \mathit{Mem}^0[r_{5}^{0} + 1] +\end{align*} +#+end_export + +***** Code 5 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 5 +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={3,4} +#+begin_src C +p1 = r3 == 0 || r1 = r3 + r4 + || r6 = stk[r5+1] +(p1) r2 = r3 + r1 + || (~ p1) r2 = r4 + r1 +stk[r5] = r1 + r2 +#+end_src + +#+beamer: \vspace{-2em} + +#+begin_export latex +\begin{align*} + &p_{1} \mapsto r_{3}^{0} = 0\\ + &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\ + &r_{2} \mapsto \begin{cases} + r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\ + r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\ + \end{cases}\\ + &r_{6} \mapsto \mathit{Mem}^0[r_{5}^{0} + 1] +\end{align*} +#+end_export + +***** Code 6 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 6- +:END: + +#+attr_latex: :options fontsize=\footnotesize,highlightlines={5} +#+begin_src C +p1 = r3 == 0 || r1 = r3 + r4 + || r6 = stk[r5+1] +(p1) r2 = r3 + r1 + || (~ p1) r2 = r4 + r1 +stk[r5] = r1 + r2 +#+end_src + +#+beamer: \vspace{-2em} + +#+begin_export latex +\begin{align*} + &p_{1} \mapsto r_{3}^{0} = 0\\ + &r_{1} \mapsto r_{3}^{0} + r_{4}^{0}\\ + &r_{2} \mapsto \begin{cases} + r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\ + r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\ + \end{cases}\\ + &\mathit{Mem} \mapsto \mathit{Mem}^0 \cup \{r_{5}^{0} \mapsto r_{1}^{0} + r_{2}^{0}\} \\ + &r_{6} \mapsto \mathit{Mem}^0[r_{5}^{0} + 1] +\end{align*} +#+end_export + +** One more complication + +How to prove equality of *conditional expressions*? + +#+begin_export latex +\begin{equation*} + \begin{drcases} + r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1} \lor (p_{2} \land \neg p_{2}) \\ + r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\ + r_{4}^{0}, &p_{3} \land \neg p_{3}\\ + \end{drcases} = \begin{cases} + r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\ + r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\ + \end{cases} +\end{equation*} +#+end_export + +#+attr_beamer: :overlay <+-> +- They can be *reordered* in any way. +- Some expressions *not present anymore* (when predicate is provably false). +- Predicates *simplified* by scheduling. + +** Solution to proving conditional functions + +#+attr_beamer: :overlay <+-> +1. Use a *formally verified SAT solver*. +2. Show that predicates are *independent*. +3. Reorder the list of predicates in a more useful order. +4. Use SAT solver to go through list and find equivalent pairings. +5. Show that attached expressions are equal. + +*** Minipage :B_minipage: +:PROPERTIES: +:BEAMER_env: minipage +:BEAMER_OPT: 5cm +:END: + +**** Only 1 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 2 +:END: + +#+begin_export latex +\begin{equation*} + \text{unsat}\quad (p_1 \land \neg p_1) \lor (p_1 \land (p_{3} \land \neg p_{3})) \lor (\neg p_1 \land (p_{3} \land \neg p_{3})) +\end{equation*} +#+end_export + +**** Only 2 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 3 +:END: + +#+begin_export latex +\begin{equation*} + \begin{drcases} + r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1} \lor (p_{2} \land \neg p_{2}) \\ + r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\ + r_{4}^{0}, &p_{3} \land \neg p_{3}\\ + \end{drcases} = \begin{cases} + r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\ + r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\ + \end{cases} +\end{equation*} +#+end_export + +**** Only 3 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 4 +:END: + +#+begin_export latex +\begin{equation*} + \begin{drcases} + r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1} \lor (p_{2} \land \neg p_{2}) \\ + r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\ + r_{4}^{0}, &p_{3} \land \neg p_{3}\\ + \end{drcases} = \begin{cases} + r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\ + r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\ + \end{cases} +\end{equation*} +#+end_export + +#+begin_export latex +\begin{equation*} +\text{unsat}\quad \neg (p_{1} \lor (p_{2} \land \neg p_{2}) \Longleftrightarrow p_1) +\end{equation*} +#+end_export + +**** Only 4 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: 5 +:END: + +#+begin_export latex +\begin{equation*} + \begin{drcases} + r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1} \lor (p_{2} \land \neg p_{2}) \\ + r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\ + r_{4}^{0}, &p_{3} \land \neg p_{3}\\ + \end{drcases} = \begin{cases} + r_{3}^{0} + r_{3}^{0} + r_{4}^{0}, &p_{1}\\ + r_{4}^{0} + r_{3}^{0} + r_{4}^{0}, &\neg p_{1}\\ + \end{cases} +\end{equation*} +#+end_export + +#+begin_export latex +\begin{equation*} +\text{unsat}\quad \neg (p_{1} \lor (p_{2} \land \neg p_{2}) \Longleftrightarrow p_1) +\end{equation*} +#+end_export + +#+begin_export latex +\begin{equation*} +r_{3}^{0} + r_{3}^{0} + r_{4}^{0} \stackrel{?}{=} r_{3}^{0} + r_{3}^{0} + r_{4}^{0} +\end{equation*} +#+end_export + +** New passes + +#+begin_export latex +\definecolor{compcert}{HTML}{66c2a5} +\definecolor{formalhls}{HTML}{fc8d62} +\begin{center}\scalebox{0.8}{\begin{tikzpicture}[language/.style={fill=white,rounded corners=2pt}] + \fill[compcert,rounded corners=3pt] (-1,-1) rectangle (9,1.5); + \fill[formalhls,rounded corners=3pt] (-1,-1.5) rectangle (9,-2.5); + \node[language] at (0,0) (clight) {Clight}; + \node[language] at (2,0) (cminor) {C\#minor}; + \node[language] at (4,0) (rtl) {3AC}; + \node[language] at (6,0) (ltl) {LTL}; + \node[language] at (8,0) (ppc) {PPC}; + \node[language] at (2,-2) (acblock) {\small 3ACBlock}; + \node[language] at (4,-2) (acpar) {\small 3ACPar}; + \node[language] at (6,-2) (dfgstmd) {HTL}; + \node[language] at (8,-2) (verilog) {Verilog}; + \node at (0,1) {CompCert}; + \node at (0,-2) {Vericert}; + \draw[->] (clight) -- (cminor); + \draw[->,dashed] (cminor) -- (rtl); + \draw[->] (rtl) -- (ltl); + \draw[->,dashed] (ltl) -- (ppc); + \draw[->] (rtl) |- (2,-1.3) -- (acblock); + \draw[->] (acblock) -- (acpar); + \draw[->] (acpar) -- (dfgstmd); + \draw[->] (dfgstmd) -- (verilog); + \draw[->] ($(acblock.south) - (0.1,0)$) to [out=270,in=180] (2,-3) to [out=0,in=270] ($(acblock.south) + (0.1,0)$); +\end{tikzpicture}}\end{center} +#+end_export + +#+beamer: \vspace{1em} + +Add two more passes, from *3ACBlock* $\rightarrow$ *3ACBlock* and from *3ACBlock* to *3ACPar*. + +** About Iterative Modulo Scheduling + +#+attr_beamer: :overlay <+-> +- Algorithm used to approximate an optimal schedule for a loop. +- Performs code transformations from one loop iteration into other loop iterations. +- Allows for more parallelism between instructions. + +** Example of proof by translation validation + +*** Diagram +:PROPERTIES: +:BEAMER_COL: 0.45 +:END: + +#+begin_export latex +\scalebox{0.8}{ + \begin{tikzpicture} + \begin{scope} + \node[draw,minimum width=3cm,minimum height=1cm] (translation) at (1.5,2) {\texttt{\textcolor{functioncolour}{HLS}}}; + \node[draw,ellipse] (input) at (-1.5,2) {\texttt{C}}; + \node[draw,ellipse] (output) at (5,2) {\texttt{Verilog}}; + \draw[->] (input) -- (translation); + \draw[->] (translation) -- (output); + \visible<2->{% + \node[draw,minimum width=3cm,minimum height=1cm,align=center] (verification) at (1.5,0.5) {Equivalence\\Check}; + \draw[->] (input) |- (verification); + \draw[->] (output) |- (verification);} + \visible<3->{% + \node[draw,ellipse] (error) at ($(verification.south) - (0.5,1.5)$) {\texttt{\textcolor{constantcolour}{Error}}}; + \draw[->] ($(verification.south) - (0.5,0)$) -- (error); + \node at (0.3,-0.5) {\footnotesize\texttt{\textcolor{keywordcolour}{false}}};} + \visible<4->{% + \node at (2,-0.3) {\footnotesize\texttt{\textcolor{keywordcolour}{true}}}; + \node[draw,ellipse] (ok) at (5,-0.5) {\texttt{\textcolor{constantcolour}{OK}(Verilog)}}; + \draw[->] (verification) |- (ok);} + \end{scope} + \end{tikzpicture}} +#+end_export + +*** Text +:PROPERTIES: +:BEAMER_COL: 0.45 +:END: + +#+attr_beamer: :overlay <+-> +- Prove correctness of an existing translation from ~C~ to ~Verilog~. +- Add equivalence check. +- Error out if it fails. +- Succeed if the equivalence check passes. + +** How is the Equivalence Check Performed? :B_frame: + +*** Code example :B_column: +:PROPERTIES: +:BEAMER_ENV: column +:BEAMER_COL: 0.45 +:END: + +**** Code 1 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_ACT: <1> +:BEAMER_env: onlyenvNH +:END: + +#+begin_src C +int main() { + int x[3] = {1, 2, 3}; + int sum = 0; + for (int i = 0; i < 3; i++) + sum += x[i]; + return sum; +} +#+end_src + +**** Code 2 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <2> +:END: + +#+attr_latex: :options highlightlines={2} +#+begin_src C +int main() { + int x[3] = {1, 2, 3}; + int sum = 0; + for (int i = 0; i < 3; i++) + sum += x[i]; + return sum; +} +#+end_src + +#+begin_export latex +\begin{align*} +\text{Mem} \{0 \rightarrow 1, 4 \rightarrow 2, 8 \rightarrow 3\} =\\ \text{Mem} \{0 \rightarrow 1\} \land\\ + \texttt{x8} \rightarrow 1 +\end{align*} +#+end_export + +**** Code 3 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <3> +:END: + +#+attr_latex: :options highlightlines={2} +#+begin_src C +int main() { + int x[3] = {1, 2, 3}; + int sum = 0; + for (int i = 0; i < 3; i++) + sum += x[i]; + return sum; +} +#+end_src + +#+begin_export latex +\begin{align*} + \text{Mem} \{0 \rightarrow 1, 4 \rightarrow 2, 8 \rightarrow 3\} =\\ \text{Mem} \{0 \rightarrow 1, 4 \rightarrow 2\} \land\\ + \texttt{x8} \rightarrow 1 \cup \texttt{x7} \rightarrow 2 +\end{align*} +#+end_export + +**** Code 4 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <4> +:END: + +#+attr_latex: :options highlightlines={2} +#+begin_src C +int main() { + int x[3] = {1, 2, 3}; + int sum = 0; + for (int i = 0; i < 3; i++) + sum += x[i]; + return sum; +} +#+end_src + +#+begin_export latex +\begin{align*} + \text{Mem} \{0 \rightarrow 1, 4 \rightarrow 2, 8 \rightarrow 3\} =\\ \text{Mem} \{0 \rightarrow 1, 4 \rightarrow 2, 8 \rightarrow 3\} \land\\ + \texttt{x8} \rightarrow 1 \cup \texttt{x7} \rightarrow 2 \cup \texttt{x6} \rightarrow 3 +\end{align*} +#+end_export + +**** Code 5 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <5> +:END: + +#+attr_latex: :options highlightlines={3} +#+begin_src C +int main() { + int x[3] = {1, 2, 3}; + int sum = 0; + for (int i = 0; i < 3; i++) + sum += x[i]; + return sum; +} +#+end_src + +Here we also need a mapping for variable names: $\texttt{sum} \rightarrow \texttt{x2}$. + +#+begin_export latex +\begin{align*} + \texttt{sum} \rightarrow 0 = \texttt{x2} \rightarrow 0 +\end{align*} +#+end_export + +**** Code 6 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <6> +:END: + +#+attr_latex: :options highlightlines={4} +#+begin_src C +int main() { + int x[3] = {1, 2, 3}; + int sum = 0; + for (int i = 0; i < 3; i++) + sum += x[i]; + return sum; +} +#+end_src + +#+beamer: \vspace{2em} + +For loops can just be identified using a template. + +**** Code 7 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <7> +:END: + +#+attr_latex: :options highlightlines={5} +#+begin_src C +int main() { + int x[3] = {1, 2, 3}; + int sum = 0; + for (int i = 0; i < 3; i++) + sum += x[i]; + return sum; +} +#+end_src + +#+begin_export latex +\begin{align*} + \texttt{sum} \rightarrow \texttt{sum}^{0} + \text{Mem}[i^{0} * 4] =\\ \texttt{x5} \rightarrow 0 +\end{align*} +#+end_export + +**** Code 8 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <8> +:END: + +#+attr_latex: :options highlightlines={5} +#+begin_src C +int main() { + int x[3] = {1, 2, 3}; + int sum = 0; + for (int i = 0; i < 3; i++) + sum += x[i]; + return sum; +} +#+end_src + +#+begin_export latex +\begin{align*} + \texttt{sum} \rightarrow \texttt{sum}^{0} + \text{Mem}[i^{0} * 4] =\\ \texttt{x5} \rightarrow 0 \cup \texttt{x4} \rightarrow \text{Mem}[\texttt{x1} * 4] +\end{align*} +#+end_export + +**** Code 9 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <9> +:END: + +#+attr_latex: :options highlightlines={5} +#+begin_src C +int main() { + int x[3] = {1, 2, 3}; + int sum = 0; + for (int i = 0; i < 3; i++) + sum += x[i]; + return sum; +} +#+end_src + +#+begin_export latex +\begin{align*} + \texttt{sum} \rightarrow \texttt{sum}^{0} + \text{Mem}[i^{0} * 4] =\\ \texttt{x5} \rightarrow 0 \cup \texttt{x4} \rightarrow \text{Mem}[\texttt{x1}^{0} * 4]\\ \cup\ \texttt{x2} \rightarrow \texttt{x2}^{0} + \text{Mem}[\texttt{x1}^{0} * 4] +\end{align*} +#+end_export + +*** Text :B_column: +:PROPERTIES: +:BEAMER_ENV: column +:BEAMER_COL: 0.45 +:END: + +**** Text 1 :B_onlyenvNH: +:PROPERTIES: +:BEAMER_ACT: <1> +:BEAMER_env: onlyenvNH +:END: + +Example of simple loop accumulating values in array. + +**** 3AC Code 2 :B_onlyenv: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <2> +:END: + +#+attr_latex: :options fontsize=\scriptsize,highlightlines={2-3} +#+begin_src C +main() { + 15: x8 = 1 + 14: int32[stack(0)] = x8 + 13: x7 = 2 + 12: int32[stack(4)] = x7 + 11: x6 = 3 + 10: int32[stack(8)] = x6 + 9: x2 = 0 + 8: x1 = 0 + 7: x5 = stack(0) (int) + 6: x4 = int32[x5 + x1 * 4 + 0] + 5: x2 = x2 + x4 + 0 (int) + 4: x1 = x1 + 1 (int) + 3: if (x1 <s 3) goto 7 else goto 2 + 2: x3 = x2 + 1: return x3 +} +#+end_src + +**** 3AC Code 3 :B_onlyenv: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <3> +:END: + +#+attr_latex: :options fontsize=\scriptsize,highlightlines={2-5} +#+begin_src C +main() { + 15: x8 = 1 + 14: int32[stack(0)] = x8 + 13: x7 = 2 + 12: int32[stack(4)] = x7 + 11: x6 = 3 + 10: int32[stack(8)] = x6 + 9: x2 = 0 + 8: x1 = 0 + 7: x5 = stack(0) (int) + 6: x4 = int32[x5 + x1 * 4 + 0] + 5: x2 = x2 + x4 + 0 (int) + 4: x1 = x1 + 1 (int) + 3: if (x1 <s 3) goto 7 else goto 2 + 2: x3 = x2 + 1: return x3 +} +#+end_src + +**** 3AC Code 4 :B_onlyenv: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <4> +:END: + +#+attr_latex: :options fontsize=\scriptsize,highlightlines={2-7} +#+begin_src C +main() { + 15: x8 = 1 + 14: int32[stack(0)] = x8 + 13: x7 = 2 + 12: int32[stack(4)] = x7 + 11: x6 = 3 + 10: int32[stack(8)] = x6 + 9: x2 = 0 + 8: x1 = 0 + 7: x5 = stack(0) (int) + 6: x4 = int32[x5 + x1 * 4 + 0] + 5: x2 = x2 + x4 + 0 (int) + 4: x1 = x1 + 1 (int) + 3: if (x1 <s 3) goto 7 else goto 2 + 2: x3 = x2 + 1: return x3 +} +#+end_src + +**** 3AC Code 5 :B_onlyenv: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <5> +:END: + +#+attr_latex: :options fontsize=\scriptsize,highlightlines={8} +#+begin_src C +main() { + 15: x8 = 1 + 14: int32[stack(0)] = x8 + 13: x7 = 2 + 12: int32[stack(4)] = x7 + 11: x6 = 3 + 10: int32[stack(8)] = x6 + 9: x2 = 0 + 8: x1 = 0 + 7: x5 = stack(0) (int) + 6: x4 = int32[x5 + x1 * 4 + 0] + 5: x2 = x2 + x4 + 0 (int) + 4: x1 = x1 + 1 (int) + 3: if (x1 <s 3) goto 7 else goto 2 + 2: x3 = x2 + 1: return x3 +} +#+end_src + +**** 3AC Code 6 :B_onlyenv: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <6> +:END: + +#+attr_latex: :options fontsize=\scriptsize,highlightlines={9,13-14} +#+begin_src C +main() { + 15: x8 = 1 + 14: int32[stack(0)] = x8 + 13: x7 = 2 + 12: int32[stack(4)] = x7 + 11: x6 = 3 + 10: int32[stack(8)] = x6 + 9: x2 = 0 + 8: x1 = 0 + 7: x5 = stack(0) (int) + 6: x4 = int32[x5 + x1 * 4 + 0] + 5: x2 = x2 + x4 + 0 (int) + 4: x1 = x1 + 1 (int) + 3: if (x1 <s 3) goto 7 else goto 2 + 2: x3 = x2 + 1: return x3 +} +#+end_src + +**** 3AC Code 7 :B_onlyenv: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <7> +:END: + +#+attr_latex: :options fontsize=\scriptsize,highlightlines={10} +#+begin_src C +main() { + 15: x8 = 1 + 14: int32[stack(0)] = x8 + 13: x7 = 2 + 12: int32[stack(4)] = x7 + 11: x6 = 3 + 10: int32[stack(8)] = x6 + 9: x2 = 0 + 8: x1 = 0 + 7: x5 = stack(0) (int) + 6: x4 = int32[x5 + x1 * 4 + 0] + 5: x2 = x2 + x4 + 0 (int) + 4: x1 = x1 + 1 (int) + 3: if (x1 <s 3) goto 7 else goto 2 + 2: x3 = x2 + 1: return x3 +} +#+end_src + +**** 3AC Code 8 :B_onlyenv: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <8> +:END: + +#+attr_latex: :options fontsize=\scriptsize,highlightlines={11} +#+begin_src C +main() { + 15: x8 = 1 + 14: int32[stack(0)] = x8 + 13: x7 = 2 + 12: int32[stack(4)] = x7 + 11: x6 = 3 + 10: int32[stack(8)] = x6 + 9: x2 = 0 + 8: x1 = 0 + 7: x5 = stack(0) (int) + 6: x4 = int32[x5 + x1 * 4 + 0] + 5: x2 = x2 + x4 + 0 (int) + 4: x1 = x1 + 1 (int) + 3: if (x1 <s 3) goto 7 else goto 2 + 2: x3 = x2 + 1: return x3 +} +#+end_src + +**** 3AC Code 9 :B_onlyenv: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <9> +:END: + +#+attr_latex: :options fontsize=\scriptsize,highlightlines={12} +#+begin_src C +main() { + 15: x8 = 1 + 14: int32[stack(0)] = x8 + 13: x7 = 2 + 12: int32[stack(4)] = x7 + 11: x6 = 3 + 10: int32[stack(8)] = x6 + 9: x2 = 0 + 8: x1 = 0 + 7: x5 = stack(0) (int) + 6: x4 = int32[x5 + x1 * 4 + 0] + 5: x2 = x2 + x4 + 0 (int) + 4: x1 = x1 + 1 (int) + 3: if (x1 <s 3) goto 7 else goto 2 + 2: x3 = x2 + 1: return x3 +} +#+end_src + +** Example of Iterative Modulo Scheduling + +*** Initial loop :B_column: +:PROPERTIES: +:BEAMER_ENV: column +:BEAMER_COL: 0.45 +:END: + +**** Code :B_onlyenvNH: +:PROPERTIES: +:BEAMER_ACT: <1> +:BEAMER_env: onlyenvNH +:END: + +#+begin_src C +for (int i = 1; i < N; i++) { + x = A[i]; + sum = sum + x; + A[i] = sum; +} +#+end_src + +*** Transformed loop :B_column: +:PROPERTIES: +:BEAMER_ENV: column +:BEAMER_COL: 0.45 +:END: + +**** Code :B_onlyenvNH: +:PROPERTIES: +:BEAMER_ACT: <1> +:BEAMER_env: onlyenvNH +:END: + +#+begin_src C +x = A[0]; +sum = sum + x; +x = A[1]; +for (int i = 0; i < N - 2; i++) { + A[i] = sum; + sum = sum + x; + x = A[i + 2]; +} +A[N-2] = sum; +sum = sum + x; +A[N-1] = sum; +#+end_src +** Example of Iterative Modulo Scheduling + +*** Initial loop :B_column: +:PROPERTIES: +:BEAMER_ENV: column +:BEAMER_COL: 0.45 +:END: + +**** Code :B_onlyenvNH: +:PROPERTIES: +:BEAMER_ACT: <1> +:BEAMER_env: onlyenvNH +:END: + +#+begin_src C +for (int i = 1; i < N; i++) { + c1 = acc[i-1] * c; + c2 = x[i] * y[i]; + acc[i] = c1 + c2; +} +#+end_src + +*** Transformed loop :B_column: +:PROPERTIES: +:BEAMER_ENV: column +:BEAMER_COL: 0.45 +:END: + +**** Code :B_onlyenvNH: +:PROPERTIES: +:BEAMER_ACT: <1> +:BEAMER_env: onlyenvNH +:END: + +#+begin_src C +c1 = acc[0] * c; +c2 = x[1] * y[1]; +for (int i = 1; i < N - 1; i++) { + acc[i] = c1 + c2; + c2 = x[i+1] * y[i+1]; + c1 = acc[i+1] * c; +} +acc[i] = c1 + c2; +#+end_src |