From 3a2fdd98bdd48aeadb6813f38b9f8e968fef0977 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 29 Sep 2021 14:32:31 +0100 Subject: Add presentation --- presentation/presentation.org | 64 +++++++++++++++++++++---------------------- 1 file changed, 32 insertions(+), 32 deletions(-) diff --git a/presentation/presentation.org b/presentation/presentation.org index 2e8a18f..ba5e809 100644 --- a/presentation/presentation.org +++ b/presentation/presentation.org @@ -265,7 +265,7 @@ 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: +** Example: 3AC :B_frame: *** Code example :B_column: :PROPERTIES: @@ -293,7 +293,7 @@ int main() { :BEAMER_ACT: <2> :END: -- *three address code (RTL)* 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: @@ -310,7 +310,7 @@ int main() { Example of a very simple program performing loads and stores. -**** RTL Code 5 :B_onlyenv: +**** 3AC Code 5 :B_onlyenv: :PROPERTIES: :BEAMER_env: onlyenvNH :BEAMER_ACT: <2> @@ -330,7 +330,7 @@ main() { } #+end_src -** Example: HTL Overview +** Example: HTL Overview :noexport: The representation of the *finite state-machine with datapath (FSMD)* is abstract and called **HTL**. @@ -364,7 +364,7 @@ Record module: Type := mkmodule { }. #+end_src -** Example: Translation (RTL $\rightarrow$ HTL) +** Example: Translation (3AC $\rightarrow$ HTL) Translation from *control-flow graph (CFG)* into a *finite state-machine with datapath (FSMD)*. @@ -373,7 +373,7 @@ Translation from *control-flow graph (CFG)* into a *finite state-machine with da #+attr_beamer: :overlay <+-> - *Control-flow* is translated into a *finite state-machine*. -- Each *RTL instructions* translated into equivalent *Verilog statements*. +- Each *3AC 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. @@ -593,7 +593,7 @@ endmodule - Control logic is translated into another case statement with a reset. * Verification -** Verilog Syntax :noexport: +** Verilog Syntax *** Column 1 :B_column: :PROPERTIES: @@ -845,7 +845,7 @@ where \end{align*} #+end_export -** RTL $\to$ HTL: Build a Specification :noexport: +** 3AC $\to$ HTL: Build a Specification :noexport: Assuming $\yhfunction{HLS} (C) = \yhconstant{OK} (V)$ requires reasoning about implementation details. @@ -862,7 +862,7 @@ Instead we build a model of the translation which we can use. #+beamer: \pause -*** RTL to HTL operator conversion :B_example: +*** 3AC to HTL operator conversion :B_example: :PROPERTIES: :BEAMER_env: example :BEAMER_ACT: <2-> @@ -874,7 +874,7 @@ Instead we build a model of the translation which we can use. \end{equation*} #+end_export -** RTL $\to$ HTL: Prove Forward Simulation :noexport: +** 3AC $\to$ HTL: Prove Forward Simulation :noexport: *** Column 1 :PROPERTIES: @@ -924,9 +924,9 @@ 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$, +- 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 RTL, the resulting states match. +- such that after 1 step in 3AC, the resulting states match. ** With Division approximately 27$\times$ slower @@ -1146,8 +1146,8 @@ Many optimisations missing: Currently implemented two new languages for it: -- ~RTLBlock~ :: RTL with basic blocks. -- ~RTLPar~ :: RTL with basic blocks made up of parallel constructs. +- ~3ACBlock~ :: 3AC with basic blocks. +- ~3ACPar~ :: 3AC with basic blocks made up of parallel constructs. #+beamer: \vspace{1.5em} @@ -1157,7 +1157,7 @@ Currently implemented two new languages for it: :BEAMER_OPT: 10cm :END: -**** RTLBlock Basic Block +**** 3ACBlock Basic Block :PROPERTIES: :BEAMER_ACT: 2 :BEAMER_env: onlyenv @@ -1193,8 +1193,8 @@ Inductive instr: Type := \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}}; + \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};% @@ -1204,11 +1204,11 @@ Inductive instr: Type := \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)}};% + \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{RTLPar}};% + \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};% @@ -1218,7 +1218,7 @@ Inductive instr: Type := \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)}};% + \node[draw,ellipse] (ok) at (13,-3) {\small\texttt{\textcolor{constantcolour}{OK}(3ACPar)}};% \draw[->] (schedverification) |- (ok);} \end{scope} \end{tikzpicture}} @@ -1743,11 +1743,11 @@ r_{3}^{0} + r_{3}^{0} + r_{4}^{0} \stackrel{?}{=} r_{3}^{0} + r_{3}^{0} + r_{4}^ \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 (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 RTLBlock}; - \node[language] at (4,-2) (acpar) {\small RTLPar}; + \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}; @@ -1766,7 +1766,7 @@ r_{3}^{0} + r_{3}^{0} + r_{4}^{0} \stackrel{?}{=} r_{3}^{0} + r_{3}^{0} + r_{4}^ #+beamer: \vspace{1em} -Add two more passes, from *RTLBlock* $\rightarrow$ *RTLBlock* and from *RTLBlock* to *RTLPar*. +Add two more passes, from *3ACBlock* $\rightarrow$ *3ACBlock* and from *3ACBlock* to *3ACPar*. ** About Iterative Modulo Scheduling @@ -2043,7 +2043,7 @@ int main() { Example of simple loop accumulating values in array. -**** RTL Code 2 :B_onlyenv: +**** 3AC Code 2 :B_onlyenv: :PROPERTIES: :BEAMER_env: onlyenvNH :BEAMER_ACT: <2> @@ -2070,7 +2070,7 @@ main() { } #+end_src -**** RTL Code 3 :B_onlyenv: +**** 3AC Code 3 :B_onlyenv: :PROPERTIES: :BEAMER_env: onlyenvNH :BEAMER_ACT: <3> @@ -2097,7 +2097,7 @@ main() { } #+end_src -**** RTL Code 4 :B_onlyenv: +**** 3AC Code 4 :B_onlyenv: :PROPERTIES: :BEAMER_env: onlyenvNH :BEAMER_ACT: <4> @@ -2124,7 +2124,7 @@ main() { } #+end_src -**** RTL Code 5 :B_onlyenv: +**** 3AC Code 5 :B_onlyenv: :PROPERTIES: :BEAMER_env: onlyenvNH :BEAMER_ACT: <5> @@ -2151,7 +2151,7 @@ main() { } #+end_src -**** RTL Code 6 :B_onlyenv: +**** 3AC Code 6 :B_onlyenv: :PROPERTIES: :BEAMER_env: onlyenvNH :BEAMER_ACT: <6> @@ -2178,7 +2178,7 @@ main() { } #+end_src -**** RTL Code 7 :B_onlyenv: +**** 3AC Code 7 :B_onlyenv: :PROPERTIES: :BEAMER_env: onlyenvNH :BEAMER_ACT: <7> @@ -2205,7 +2205,7 @@ main() { } #+end_src -**** RTL Code 8 :B_onlyenv: +**** 3AC Code 8 :B_onlyenv: :PROPERTIES: :BEAMER_env: onlyenvNH :BEAMER_ACT: <8> @@ -2232,7 +2232,7 @@ main() { } #+end_src -**** RTL Code 9 :B_onlyenv: +**** 3AC Code 9 :B_onlyenv: :PROPERTIES: :BEAMER_env: onlyenvNH :BEAMER_ACT: <9> -- cgit