diff options
Diffstat (limited to 'presentation/presentation.org')
| -rw-r--r-- | presentation/presentation.org | 179 |
1 files changed, 92 insertions, 87 deletions
diff --git a/presentation/presentation.org b/presentation/presentation.org index 3902b42..cce2850 100644 --- a/presentation/presentation.org +++ b/presentation/presentation.org @@ -41,7 +41,7 @@ Translation of a high-level programming language such as C/C++ into a hardware d 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*. +- Intel's OpenCL could not be fuzzed because of too many issues (cite:lidbury15_many_core_compil_fuzzin). - We fuzzed HLS tools and found they failed on *2.5%* of simple random test cases. *** HLS Difficulties :B_blockNH: @@ -50,11 +50,11 @@ High-level synthesis is often quite unreliable: :BEAMER_ACT: <3-> :END: -Debugging HLS tools when they go wrong is difficult: +Difficult to debug HLS tools: #+attr_beamer: :overlay <+-> -- It is not clear what part of the input caused the bug. -- Only testing the input specification is not enough. +- Simulation can take a long time. +- Correctness is important in hardware, testing is done at every level. ** Solution :B_frame: :PROPERTIES: @@ -198,7 +198,7 @@ main() { } #+end_src -** HTL Overview +** Example: HTL Overview The representation of the *finite state-machine with datapath (FSMD)* is abstract and called **HTL**. @@ -272,7 +272,7 @@ Translation from *control-flow graph (CFG)* into a *finite state-machine with da $\quad\longrightarrow\quad$ ~{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}~ -** Memory Inferrence Pass +** Example: Memory Inference Pass :noexport: - An HTL $\rightarrow$ HTL translation removes loads and stores. - Replaced by accesses to a proper *RAM*. @@ -461,7 +461,7 @@ endmodule - Control logic is translated into another case statement with a reset. * Verification -** Verilog Syntax +** Verilog Syntax :noexport: *** Column 1 :B_column: :PROPERTIES: @@ -526,15 +526,16 @@ endmodule #+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')} +%\inferrule[Nonblocking]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \downarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ <= } e) \downarrow_{\text{stmnt}} (\Gamma, \Delta [n \mapsto v])} \quad \inferrule[Blocking]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \downarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ = } e) \downarrow_{\text{stmnt}} (\Gamma [n \mapsto v], \Delta)} \\ +\inferrule[Module]{(\Gamma, \epsilon, \vec{m})\ \downarrow_{\text{module}^{+}} (\Gamma', \Delta') \\ (\Gamma'\ //\ \Delta', \epsilon, \vec{m}) \downarrow_{\text{module}^{-}} (\Gamma'', \Delta'')}{(\Gamma, \yhkeyword{module}\ \yhconstant{main} \yhkeyword{(...);}\ \vec{m}\ \yhkeyword{endmodule}) \downarrow_{\text{program}} (\Gamma''\ //\ \Delta'')} \end{gather*} #+end_export #+attr_beamer: :overlay <+-> - Two separate association maps: current ($\Gamma$) and next ($\Delta$). - Maps are merged at the end of the clock cycle. -** How the Verilog semantics changed + +** How the Verilog semantics changed :noexport: Changed the semantics in *5* minor ways to make it a better HLS target. @@ -620,11 +621,11 @@ This describes the main proof that is needed to show that the HLS tool is correc :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. -#+beamer: \vspace{1em} - *** Minipage :B_minipage: :PROPERTIES: :BEAMER_env: minipage @@ -809,7 +810,54 @@ Fuzzed Vericert with Csmith to check correctness theorem. \end{tikzpicture} #+end_export -* Extensions +** Conclusion + +Written a formally verified high-level synthesis tool in *Coq* based on *CompCert*. + +#+attr_beamer: :overlay <+-> +- Base translation *proven correct* by proving translation of CFG into FSMD. +- Small optimisations implemented such as *Ram Inference*. +- Performance without divisions comparable to LegUp without optimisations. + +** Thank you :B_fullframe: +:PROPERTIES: +:BEAMER_env: fullframe +:END: + +#+begin_export latex +\begin{center} + {\usebeamerfont{frametitle}\Large Thank you\par} + {\color{lightgreen}\rule{350pt}{2pt}\par} + \vspace{1em} + \begin{minipage}{5cm} + \begin{center} + Documentation\\ + \includegraphics[width=50pt]{assets/formal_hls_docs.pdf}\\ + \tiny\url{https://vericert.ymhg.org} + \end{center} + \end{minipage} + \begin{minipage}{5cm} + \begin{center} + GitHub\\ + \includegraphics[width=50pt]{assets/formal_hls_github.pdf}\\ + \tiny\url{https://github.com/ymherklotz/vericert} + \end{center} + \end{minipage}\vspace{1em} + \begin{minipage}{5cm} + \begin{center} + OOPSLA'21 Preprint\\ + \includegraphics[width=50pt]{assets/formal_hls_paper.pdf}\\ + \tiny\url{https://ymhg.org/papers/fvhls_oopsla21.pdf} + \end{center} + \end{minipage} +\end{center} +#+end_export +** References + +bibliography:./references.bib + + +* Extensions :noexport: ** Current work Many optimisations missing: @@ -867,41 +915,6 @@ Inductive instr: Type := | 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 @@ -1448,48 +1461,41 @@ r_{3}^{0} + r_{3}^{0} + r_{4}^{0} \stackrel{?}{=} r_{3}^{0} + r_{3}^{0} + r_{4}^ \end{equation*} #+end_export -** Conclusion +** New passes -Written a formally verified high-level synthesis tool in *Coq* based on *CompCert*. +#+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 -#+attr_beamer: :overlay <+-> -- Base translation *proven correct*. -- Some optimisations *implemented*, proofs being worked on. -- Small issues such as *unsigned comparisons* not working. +#+beamer: \vspace{1em} -** Thank you :B_fullframe: -:PROPERTIES: -:BEAMER_env: fullframe -:END: +Add two more passes, from *RTLBlock* $\rightarrow$ *RTLBlock* and from *RTLBlock* to *RTLPar*. -#+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 <+-> @@ -2072,4 +2078,3 @@ for (int i = 1; i < N - 1; i++) { } acc[i] = c1 + c2; #+end_src - |