From 6c48fc6fe1f8d41a76c3661f210b8f42351fc15f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 4 Oct 2021 19:05:44 +0100 Subject: Add some more updates to presentation --- presentation/assets/database-asic.pdf | Bin 0 -> 59199 bytes presentation/assets/fpga-expl2.pdf | Bin 332430 -> 411345 bytes presentation/beamerthemeauriga.sty | 15 ++- presentation/presentation.org | 203 +++++++++++++++++++++++++++++----- presentation/presentation.pdf | Bin 2410748 -> 2524371 bytes presentation/setup.org | 2 +- 6 files changed, 181 insertions(+), 39 deletions(-) create mode 100644 presentation/assets/database-asic.pdf diff --git a/presentation/assets/database-asic.pdf b/presentation/assets/database-asic.pdf new file mode 100644 index 0000000..4a16fff Binary files /dev/null and b/presentation/assets/database-asic.pdf differ diff --git a/presentation/assets/fpga-expl2.pdf b/presentation/assets/fpga-expl2.pdf index 97a5f12..34c6df4 100644 Binary files a/presentation/assets/fpga-expl2.pdf and b/presentation/assets/fpga-expl2.pdf differ diff --git a/presentation/beamerthemeauriga.sty b/presentation/beamerthemeauriga.sty index 5ecc877..e4b18e4 100644 --- a/presentation/beamerthemeauriga.sty +++ b/presentation/beamerthemeauriga.sty @@ -103,12 +103,11 @@ {\usebeamerfont{title page institute}\usebeamercolor[fg]{title page}\insertinstitute\\[1ex]} \vskip0pt plus 1filll \end{centering} - {\hfill\includegraphics[height=1cm]{./assets/oopsla21.png}} + {\includegraphics[height=1cm]{./assets/imperial_logo.pdf}\hfill\includegraphics[height=1cm]{./assets/oopsla21.png}} } % Footer -\setbeamertemplate{footline}{ - \hspace{2em}\includegraphics[height=1cm]{./assets/imperial_logo.pdf}% +\setbeamertemplate{footline}{% \hfill% \usebeamercolor[fg]{page number in head/foot}% \usebeamerfont{page number in head/foot}% @@ -117,11 +116,11 @@ } % Frame title -\setbeamertemplate{frametitle}{ - \nointerlineskip - \vskip2ex - {\usebeamerfont{frametitle}\usebeamercolor[fg]{frametitle}\insertframetitle\\[-2.5ex]} - {\par\color{lightgreen}\rule{390pt}{2pt}} +\setbeamertemplate{frametitle}{% + \nointerlineskip% + \vskip2ex% + {\usebeamerfont{frametitle}\usebeamercolor[fg]{frametitle}\insertframetitle\\[-2.5ex]}% + {\par\color{lightgreen}\rule{390pt}{2pt}}% } % Alert diff --git a/presentation/presentation.org b/presentation/presentation.org index bc580ab..106232e 100644 --- a/presentation/presentation.org +++ b/presentation/presentation.org @@ -1,12 +1,12 @@ #+title: Formal Verification of High-Level Synthesis #+author: \underline{Yann Herklotz}, James D. Pollard, Nadesh Ramanathan, John Wickerson -#+options: H:2 +#+options: H:2 toc:nil #+columns: %45ITEM %10BEAMER_ENV(Env) %10BEAMER_ACT(Act) %4BEAMER_COL(Col) #+setupfile: setup.org ** The Need to Design Hardware Accelerators -Hardware accelerators are needed more and more industries. +Application-specific hardware accelerators are increasingly being needed in industries. *** Column 1 :PROPERTIES: @@ -16,8 +16,10 @@ Hardware accelerators are needed more and more industries. #+attr_beamer: :overlay <+-> - Using a *CPU* everywhere not always the best choice. -- *Field-Programmable Gate Arrays (FPGA)* provide a good alternative. -- FPGAs act as *reprogrammable hardware*, therefore can be made application specific. +- *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: @@ -46,7 +48,17 @@ Hardware accelerators are needed more and more industries. ***** Only 2 :PROPERTIES: :BEAMER_ENV: onlyenvNH -:BEAMER_ACT: 2- +: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 @@ -58,7 +70,7 @@ Hardware accelerators are needed more and more industries. #+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*. -- *BRAMs* provide accessible storage. +- *RAMs* provide accessible storage. *** Minipage :PROPERTIES: @@ -132,7 +144,7 @@ Hardware accelerators are needed more and more industries. ***** Only 2 :PROPERTIES: :BEAMER_ENV: onlyenvNH -:BEAMER_ACT: <2-3> +:BEAMER_ACT: <2> :END: #+begin_export latex @@ -143,7 +155,7 @@ Hardware accelerators are needed more and more industries. ***** Only 3 :PROPERTIES: :BEAMER_ENV: onlyenvNH -:BEAMER_ACT: <4-5> +:BEAMER_ACT: <4> :END: #+begin_export latex @@ -259,7 +271,6 @@ Difficult to debug HLS tools: High-level synthesis is often quite unreliable: -- Intel's OpenCL could not be fuzzed because of too many issues (cite:lidbury15_many_core_compil_fuzzin). - We fuzzed HLS tools (cite:9444067) and found they failed on *2.5%* of simple random test cases. ** Solution :B_frame: @@ -365,7 +376,7 @@ int main() { :BEAMER_ACT: <2> :END: -- *three address code (3AC)* instructions are represented as a control-flow graph (CFG). +- *Three address code (3AC)* instructions are represented as a control-flow graph (CFG). - Each instruction links to the next one. *** Text :B_column: @@ -377,10 +388,10 @@ int main() { **** Text 1 :B_onlyenvNH: :PROPERTIES: :BEAMER_ACT: <1> -:BEAMER_env: onlyenvNH +:BEAMER_ENV: onlyenvNH :END: -Example of a very simple program performing loads and stores. +- Example of a very simple program performing loads and stores. **** 3AC Code 5 :B_onlyenv: :PROPERTIES: @@ -402,7 +413,7 @@ main() { } #+end_src -** Example: HTL Overview +** HTL Overview The representation of the *finite state-machine with datapath* is abstract and called **HTL**. @@ -413,15 +424,23 @@ The representation of the *finite state-machine with datapath* is abstract and c 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}$ +src_coq[:exports code]{Definition controllogic := } $\mathbb{Z}^+ \mapsto \texttt{\small +Verilog.stmnt}$ -*** Module definition :B_blockNH: +*** Minipage :PROPERTIES: -:BEAMER_env: blockNH +:BEAMER_ENV: minipage +:BEAMER_OPT: 5cm +:END: + +**** Module definition :B_blockNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH :BEAMER_ACT: 2 :END: -#+beamer: \vspace{-1.5em} +#+beamer: \vspace{0.25em} + #+attr_latex: :options fontsize=\footnotesize #+begin_src coq Record module: Type := mkmodule { @@ -433,7 +452,58 @@ Record module: Type := mkmodule { }. #+end_src -** Example: Translation (3AC $\rightarrow$ HTL) +**** 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*. @@ -443,7 +513,7 @@ Translation from *control-flow graph* into a *finite state-machine with datapath #+attr_beamer: :overlay <+-> - *Control-flow* is translated into a *finite state-machine*. - Each *3AC instructions* translated into equivalent *Verilog statements*. -- Function *stack* implemented as *Verilog array*. +- Call *stack* implemented as *Verilog array*. - Pointers for loads and stores translated to array addresses. - *Byte* addressed to *word* addressed. @@ -461,7 +531,7 @@ Translation from *control-flow graph* into a *finite state-machine with datapath :BEAMER_ACT: 3 :END: -~x3 = x3 + x5 + 0~ $\quad\longrightarrow\quad$ src_verilog[:exports code]{reg_3 <= {reg_3 + {reg_5 + 32'd0}}} +~x3 = x3 + x5 + 0~ $\quad\longrightarrow\quad$ src_verilog[:exports code]{reg_3 <= {reg_3 + {reg_5 + 0}}} **** Only 2 :B_onlyenvNH:noexport: :PROPERTIES: @@ -469,16 +539,22 @@ Translation from *control-flow graph* into a *finite state-machine with datapath :BEAMER_ACT: 5-6 :END: -~x5 + x1 * 4 + 0~ $\quad\longrightarrow\quad$ src_verilog[:exports code]{{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}} +~x5 + x1 * 4 + 0~ $\quad\longrightarrow\quad$ src_verilog[:exports code]{{{{reg_5 + 0} + {reg_1 * 4}} / 4}} -** Example: Memory Inference Pass +** 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 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}]} +src_verilog[:exports code]{stack[reg_5 / 4]} #+beamer: \vspace{1em} @@ -486,14 +562,68 @@ 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 <= 32'd0; -addr <= {{{reg_3 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}; +u_en <= ( ~ u_en); +wr_en <= 0; +addr <= reg_5 / 4; #+end_src -** Verilog Syntax +***** 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: @@ -556,7 +686,7 @@ endmodule - Always block run in parallel -** Example: Translation (HTL $\rightarrow$ Verilog) :B_frame: +** Translation (HTL $\rightarrow$ Verilog) :B_frame: *** Column :PROPERTIES: @@ -719,7 +849,7 @@ endmodule - 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. +- RAM loads and stores automatically turn off RAM. - Control logic is translated into another case statement with a reset. * Verification @@ -821,7 +951,7 @@ Use integers modulo $2^n$. Those are the only types needed for HLS. -** How do we prove the HLS tool correct? +** How do we prove the HLS tool correct? :noexport: *** Notes :PROPERTIES: @@ -1193,9 +1323,22 @@ Written a formally verified high-level synthesis tool in *Coq* based on *CompCer #+attr_beamer: :overlay <+-> - HLS tool *proven correct in Coq* by proving translation of CFG into FSMD. -- Small optimisations implemented such as *Ram Inference*. +- Small optimisations implemented such as *RAM Inference*. - Performance without divisions comparable to LegUp without optimisations. +*** Future Work +:PROPERTIES: +:BEAMER_ENV: block +:BEAMER_ACT: <4-> +:END: + +Make Vericert not only *correct*, but *competitive*. + +#+attr_beamer: :overlay +- +- Implement *scheduling* and *resource sharing*. +- Add *external module* support. +- Add *global variable* support. + ** Thank you :B_fullframe: :PROPERTIES: :BEAMER_env: fullframe diff --git a/presentation/presentation.pdf b/presentation/presentation.pdf index 22e9e58..0842f3b 100644 Binary files a/presentation/presentation.pdf and b/presentation/presentation.pdf differ diff --git a/presentation/setup.org b/presentation/setup.org index 8fd866f..0b35a82 100644 --- a/presentation/setup.org +++ b/presentation/setup.org @@ -14,7 +14,7 @@ #+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: \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} -- cgit