From 8ba729708446b87baf9ec19cc25d9726ea247db7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 15 May 2022 15:30:49 -0400 Subject: Add initial files --- .gitignore | 15 + beamercolorthemeauriga.sty | 35 + beamerthemeauriga.sty | 127 +++ flashlight22.bib | 9 + flashlight22.org | 185 ++++ notes.org | 52 + outline.org | 9 + pipeline.sv | 68 ++ presentation.org | 2373 ++++++++++++++++++++++++++++++++++++++++++++ setup.org | 54 + 10 files changed, 2927 insertions(+) create mode 100644 .gitignore create mode 100644 beamercolorthemeauriga.sty create mode 100644 beamerthemeauriga.sty create mode 100644 flashlight22.bib create mode 100644 flashlight22.org create mode 100644 notes.org create mode 100644 outline.org create mode 100644 pipeline.sv create mode 100644 presentation.org create mode 100644 setup.org diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..347c527 --- /dev/null +++ b/.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/beamercolorthemeauriga.sty b/beamercolorthemeauriga.sty new file mode 100644 index 0000000..6c9cf63 --- /dev/null +++ b/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/beamerthemeauriga.sty b/beamerthemeauriga.sty new file mode 100644 index 0000000..e4b18e4 --- /dev/null +++ b/beamerthemeauriga.sty @@ -0,0 +1,127 @@ +% 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} + {\includegraphics[height=1cm]{./assets/imperial_logo.pdf}\hfill\includegraphics[height=1cm]{./assets/oopsla21.png}} +} + +% Footer +\setbeamertemplate{footline}{% + \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/flashlight22.bib b/flashlight22.bib new file mode 100644 index 0000000..11e20ad --- /dev/null +++ b/flashlight22.bib @@ -0,0 +1,9 @@ +@inproceedings{9444067, + author={Herklotz, Yann and Du, Zewei and Ramanathan, Nadesh and Wickerson, John}, + booktitle={2021 IEEE 29th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM)}, + title={An Empirical Study of the Reliability of High-Level Synthesis Tools}, + year={2021}, + volume={}, + number={}, + pages={219-223}, + doi={10.1109/FCCM51124.2021.00034}} diff --git a/flashlight22.org b/flashlight22.org new file mode 100644 index 0000000..ae68e33 --- /dev/null +++ b/flashlight22.org @@ -0,0 +1,185 @@ +#+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 + +** Why HLS is unreliable +** Small Introduction to Coq +** Solution: Formally Verify HLS +*** Vericert +** Current Status of Vericert +* Loop Pipelining +** The Need for Loop Pipelining + +# - really useful, or you might say necessary optimisation that HLS performs. + +- Main difficulty with having hardware as a target is the need to pipeline loops. + +*** Column left +:PROPERTIES: +:BEAMER_COL: 0.45 +:END: + +#+attr_latex: :options fontsize=\small,escapeinside=|| +#+begin_src c +for (int i = 0; i < N; i++) { +|\sA{1}| x18 = i - 1 +|\sR{1}| x16 = load[1, x18 * 4] +|\sM{1}| x8 = x16 * x1 +|\sR{2}| x12 = load[3, i * 4] +|\sR{3}| x13 = load[2, i * 4] +|\sM{2}| x7 = x12 * x13 +|\sA{2}| x11 = x8 + x7 +|\sW{1}| store[1, i * 4] = x11 + i = i + 1 +} +#+end_src + +*** Column right +:PROPERTIES: +:BEAMER_COL: 0.45 +:END: + +#+begin_export latex +\begin{tikzpicture}[lnode/.style={circle,draw=black,minimum size=4mm,scale=0.8},nlabel/.style={midway,right +,font=\tiny},node distance=1.3cm,shorten >=1pt] + \node[lnode,fill=s1col] (A1) {1}; + \node[lnode,fill=s2col,below of=A1] (R1) {1}; + \node[lnode,fill=s3col,below of=R1] (M1) {1}; + \node[lnode,fill=s2col,right of=A1] (R2) {2}; + \node[lnode,fill=s2col,right of=R2] (R3) {3}; + \node[lnode,fill=s3col,below of=R2,xshift=0.7cm] (M2) {2}; + \node[lnode,fill=s1col,below right of=M1,xshift=0.4cm] (A2) {2}; + \node[lnode,fill=s4col,below of=A2] (W1) {1}; + + \draw[->,thick] (A1) -- (R1); + \draw[->,thick] (R1) -- node[nlabel] {2} (M1); + \draw[->,thick] (R2) -- node[nlabel] {2} (M2); + \draw[->,thick] (R3) -- node[nlabel] {2} (M2); + \draw[->,thick] (M1) -- (A2); + \draw[->,thick] (M2) -- (A2); + \draw[->,thick] (A2) -- (W1); + \draw[->,thick] (R1) to [out=220,in=180,loop,looseness=2] (W1); +\end{tikzpicture} +#+end_export + +** Ideas Behind Static Hardware Loop Pipelining + +*** One Possible Workflow + +- Generate scheduling constraints for linear code as well as loops. +- Solve for a scheduling using an ILP solver. +- Place the instructions into the cycle that it was assigned to. + +#+begin_export latex +\begin{center} + \begin{tikzpicture}[lnode/.style={circle,draw=black,minimum size=4mm,scale=0.8},node + distance=1.3cm,shorten >=1pt] + \node[lnode,fill=s1col] (A1) {1}; \node[lnode,fill=s2col,below of=A1] (R2) {2}; + \node[lnode,fill=s2col,below of=R2] (R3) {3}; \node[lnode,fill=s2col,right of=A1] (R1) {1}; + \node[lnode,fill=s3col,right of=R1] (M2) {2}; \node[lnode,fill=s3col,right of=M2] (M1) {1}; + \node[lnode,fill=s1col,right of=M1] (A2) {2}; \node[lnode,right of=A2] (E1) {}; + \node[lnode,fill=s4col,right of=E1] (W1) {1}; \node[lnode,right of=W1] (E2) {}; \node[above + right of=R1,xshift=-0.35cm] (S1T) {}; \node[below of=S1T,yshift=-2.5cm] (S1B) {}; \draw[very + thick] (S1T) -- (S1B); \node[above right of=M1,xshift=-0.35cm] (S2T) {}; \node[below + of=S2T,yshift=-2.5cm] (S2B) {}; \draw[very thick] (S2T) -- (S2B); \node[above right + of=E1,xshift=-0.35cm] (S3T) {}; \node[below of=S3T,yshift=-2.5cm] (S3B) {}; \draw[very thick] + (S3T) -- (S3B); + \end{tikzpicture} +\end{center} +#+end_export + +** Verifying Hardware Pipelining is Difficult + +- Normally part of the scheduling step. +- Lose control about how the loops are translated, the fundamental structure of the loop could + change and would be difficult to identify again. + +* Verifying Loop Pipelining +** Ideas Behind Software Loop Pipelining + +*** Main Idea + +Can perform a source-to-source transformation which generates a pipeline purely in software. + +*** Column left +:PROPERTIES: +:BEAMER_COL: 0.45 +:END: + +#+attr_latex: :options fontsize=\small,escapeinside=|| +#+begin_src c +for (int i = 0; i < N; i++) { +|\sA{1}| x18 = i - 1 +|\sR{1}| x16 = load[1, x18 * 4] +|\sM{1}| x8 = x16 * x1 +|\sR{2}| x12 = load[3, i * 4] +|\sR{3}| x13 = load[2, i * 4] +|\sM{2}| x7 = x12 * x13 +|\sA{2}| x11 = x8 + x7 +|\sW{1}| store[1, i * 4] = x11 + i = i + 1 +} +#+end_src + +*** Column right +:PROPERTIES: +:BEAMER_COL: 0.45 +:END: + +#+attr_latex: :options fontsize=\footnotesize,escapeinside=|| +#+begin_src c +for (int i = 0; i < N; i++) { +|\sA{1}| x18[i] = i - 1 +|\sR{2}| x12[i] = load[3, i * 4] +|\sR{3}| x13[i] = load[2, i * 4] +|\sM{2}| x7[i-1] = x12[i-1] * x13[i-1] +|\sA{2}| x11[i-2] = x8[i-2] + x7[i-2] +|\sW{1}| store[1, (i-3) * 4] = x11[i-3] + +|\sR{1}| x16[i] = load[1, x18[i] * 4] +|\sM{1}| x8[i-1] = x16[i-1] * x1 + i = i + 1 +} +#+end_src + +** Verifying Software Loop Pipelining + +*** Symbolic Execution + +Define an $\alpha$, such that $\alpha(\mathcal{C})$ evaluates some code $\mathcal{C}$ and returns +*symbolic states* for all registers. + +*** Example + +Executing the following code will evaluate to the following symbolic code: + +*** Column left +:PROPERTIES: +:BEAMER_COL: 0.45 +:END: + + + +*** Column right +:PROPERTIES: +:BEAMER_COL: 0.45 +:END: + +* Comparing Software and Hardware Loop Pipelining +** Comparing Pipelines in Hardware and Software + +*** Pipelines can be identical + +- In terms of expressivity, both hardware and software pipelining can express the same loop + pipelines. + +** Resource Usage of Pipelines + +Naively, They will both contain + +* Wrapping up +** Conclusion + +- To verify loop pipelines, it seems easier diff --git a/notes.org b/notes.org new file mode 100644 index 0000000..39e93f8 --- /dev/null +++ b/notes.org @@ -0,0 +1,52 @@ +Yes! It's loads better! I'm glad I made a fuss! :) + +Ok, lots of feedback below, but it's mostly low-level details now. Here goes... + +TALK 1: You say "formally verified" but the slide says "formal verification of" which is a bit jarring. + +TALK 3: Don't start with "So...". Just launch straight in with "The need for...". (I'm getting such deja +vu from 2012-ish when I was given exactly the same advice when giving a practice talk for a +fellowship interview. I started with "So..." and was immediately heckled for it!) + +TALK 3: I like the SSD/SSD/HDD example. It's nifty. And perfectly understandable too. I think there +are one or two bits that could still be slightly optimised, for instance, you say "It will always +perform the same task" and then "which would always do the same task" a few moments later. + +TALK 5: The .v -> FPGA diagram is very good -- I would just change your words from "use logic synthesis" +to "use a logic synthesis tool" to emphasise that it's not a manual process. + +6: The text about "difficult to debug" appears too soon. I found myself reading the text and being a +bit confused because it didn't match what you were saying. Only introduce the text at the moment you +talk about it. Same happens on slide 16 -- the diagram appears a few seconds too soon and it +distracts me from what you're saying. + +TALK 7: "we're gonna call 3AC [because RTL is already an established abbreviation in hardware design]" + +TALK 14: I still think there's an opportunity for a little bit of humour/showmanship when you make the +point about the RAM interface. For instance, you could say something like "Actually here is a mildly +terrifying example of quite how fragile the logic synthesis tools are -- if the RAM interface +doesn't use this _exact_ Verilog syntax, then the tool won't know to use RAM and will synthesise +thousands of registers instead, and the circuit will be disastrously inefficient." + +TODO 17: Similar comment as before: I recommend making sure that each piece of text only appears at +the instant you talk about it. Currently I'm reading about "Wrong" while you're talking about +"Converging" and that's not ideal :) + +TALK 20: I like the addition of "bad news" -- that's really helpful for telling the audience how to +interpret this slide. I suggest beginning this slide by saying which benchmarks you use (and why) +and emphasise that you can compile almost all of them. And then, when you show the graphs, you need +to give a bit of time for them to be digested. You were talking about interpreting the results, but +I was still trying to read the labels on the y-axes. You need to say what the top and bottom graphs +are showing, say what the three colours of bar mean, whether higher bars are good or bad (and say +things like "we see that the green bars really high, and way higher than the others"), and say that +the x-axis shows all 27 benchmarks plus the median. I think you need to spend a good 2 minutes on +this slide alone. + +TALK 22: Rather than "0% (0.03%)", I suggest showing "0.03%" first, explaining what's going on, and +then striking it out and writing "0%", so the end result looks like ^0.03%^ 0%. (As for Bambu, I'd +be tempted to drop the 13.7% point altogether, as it's an unnecessary detail. (Let's just be kind to +them!)) And I'd encourage a little bit of showmanship here -- you could put the "Vericert" text in +first, leaving the number blank, and then say something "and of course, since this is all proven in +Coq we'd expect a nice 'zero percent' here...[then introduce the 0.03%]...well ok, that's not quite +how it worked out at first...but what happened was...". And I'd mention that this is exactly what +happened when the Csmith people fuzzed CompCert for the first time. diff --git a/outline.org b/outline.org new file mode 100644 index 0000000..3d7470e --- /dev/null +++ b/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/pipeline.sv b/pipeline.sv new file mode 100644 index 0000000..7c7c27c --- /dev/null +++ b/pipeline.sv @@ -0,0 +1,68 @@ +module ram(clk, addr, idata, wr_en, odata); + input logic clk; + input logic [31:0] addr; + input logic [31:0] idata; + input logic wr_en; + + output logic [31:0] odata; + + logic [31:0] ram [9:0]; + + always @(posedge clk) begin + if (wr_en) begin + ram[addr] <= idata; + end + end + + assign odata = ram[addr]; +endmodule + +module pipeline(valid, clk, x1, x6, fin, val); + input logic start; + input logic clk; + input logic [31:0] x1; + input logic [31:0] x6; + + output logic fin; + output logic [31:0] val; + + logic [31:0] x18, x16, x8, x12, x13, x7, x11; + + logic [1:0] state; + + logic [31:0] ram1 [9:0]; + logic [31:0] ram2 [9:0]; + logic [31:0] ram3 [9:0]; + + parameter IDLE = 0; + parameter STATE1 = 1; + parameter STATE2 = 2; + + initial begin + state = IDLE; + end + + always @(posedge clk) begin + case(state) + IDLE: begin + if (start) state <= STATE1; + end + STATE1: state <= STATE2; + STATE2: state <= STATE1; + endcase + end + + always @(posedge clk) begin + if (state == STATE1) begin + x18 <= x6 - 1; + x12 <= ram2[x6]; + x13 <= ram3[x6]; + end + end + + always @(posedge clk) begin + if (state == STATE2) begin + x16 <= ram1[x18]; + end + end +endmodule 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 +: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/setup.org b/setup.org new file mode 100644 index 0000000..67e3696 --- /dev/null +++ b/setup.org @@ -0,0 +1,54 @@ +#+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: \usepackage{natbib} +#+latex_header: \usepackage{graphicx} +#+latex_header: \usepackage{pgfplots} +#+latex_header: \usepackage{pgfplotstable} + +#+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}}} +#+latex_header_extra: \bibliographystyle{plainnat} +#+latex_header_extra: \pgfplotsset{compat=1.16} +#+latex_header_extra: \usetikzlibrary{pgfplots.groupplots} +#+latex_header_extra: \tikzexternalize + +#+latex_header_extra: \newcommand\legup{Leg\-Up} +#+latex_header_extra: \newcommand\legupnoopt{\legup{} no-opt} +#+latex_header_extra: \newcommand\legupnooptchain{\legup{} no-opt no-chaining} +#+latex_header_extra: \newcommand\vericert{Veri\-cert} + +#+latex_header_extra: \definecolor{s1col}{HTML}{7fc97f} +#+latex_header_extra: \definecolor{s2col}{HTML}{beaed4} +#+latex_header_extra: \definecolor{s3col}{HTML}{fdc086} +#+latex_header_extra: \definecolor{s4col}{HTML}{ffff99} +#+latex_header_extra: \definecolor{s5col}{HTML}{386cb0} + +#+latex_header_extra: \newcommand*{\makedfgstate}[2]{\raisebox{-2pt}{\tikz{\node[circle,draw=black,minimum +#+latex_header_extra: size=4mm,fill=#1,scale=0.5](#1#2){#2};}}} +#+latex_header_extra: \newcommand*{\sA}[1]{\makedfgstate{s1col}{#1}} +#+latex_header_extra: \newcommand*{\sR}[1]{\makedfgstate{s2col}{#1}} +#+latex_header_extra: \newcommand*{\sM}[1]{\makedfgstate{s3col}{#1}} +#+latex_header_extra: \newcommand*{\sW}[1]{\makedfgstate{s4col}{#1}} + +#+exclude_tags: noexport + +#+beamer_theme: auriga +#+beamer_color_theme: auriga -- cgit