diff options
Diffstat (limited to 'presentation/presentation.org')
| -rw-r--r-- | presentation/presentation.org | 88 |
1 files changed, 59 insertions, 29 deletions
diff --git a/presentation/presentation.org b/presentation/presentation.org index 2e8a18f..97d7baa 100644 --- a/presentation/presentation.org +++ b/presentation/presentation.org @@ -21,9 +21,49 @@ But: ** FPGA Layout +#+attr_beamer: :overlay <+-> +- FPGA's are programmable circuits with two main components. +- *Look up tables (LUTs)* provide flexible logic gates. They are connected by *configurable switches*. +- *BRAMs* provide accessible storage. + +*** 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=7.5cm]{assets/fpga.pdf} +\includegraphics[width=8cm]{assets/fpga-expl2.pdf} #+end_export ** So How do we Program an FPGA? @@ -339,11 +379,9 @@ The representation of the *finite state-machine with datapath (FSMD)* is abstrac :BEAMER_env: blockNH :END: -#+attr_latex: :options fontsize=\footnotesize -#+begin_src coq -Definition datapath := PTree.t Verilog.stmnt. -Definition controllogic := PTree.t Verilog.stmnt. -#+end_src +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}$ *** Module definition :B_blockNH: :PROPERTIES: @@ -355,9 +393,8 @@ Definition controllogic := PTree.t Verilog.stmnt. #+attr_latex: :options fontsize=\footnotesize #+begin_src coq Record module: Type := mkmodule { - mod_datapath: datapath; mod_controllogic: controllogic; - mod_wf: map_well_formed mod_controllogic - /\ map_well_formed mod_datapath; + mod_datapath: datapath; + mod_controllogic: controllogic; mod_reset: reg; mod_ram: ram_spec; ... @@ -654,42 +691,33 @@ endmodule #+attr_beamer: :overlay <+-> - Verilog example for a simple shift register. - Always block run in parallel + ** Verilog Semantics (Adapted from Lööw et al. (2019)) -#+attr_beamer: :overlay <+-> - Top-level semantics are *small-step operational semantics*. -- Within each small step, a Verilog module is executed in one big step. - -*** Minipage -:PROPERTIES: -:BEAMER_ENV: minipage -:BEAMER_OPT: 5cm -:END: -#+beamer: \vspace{1em} -#+beamer: \centering - -**** Only 1 +*** Only 1 :PROPERTIES: -:BEAMER_ENV: onlyenvNH -:BEAMER_ACT: <1> +:BEAMER_ENV: blockNH +:BEAMER_ACT: <1-> :END: #+begin_export latex -\includegraphics[width=8cm]{assets/semantics_clk.pdf} +{\centering\includegraphics[width=8cm]{assets/clk.pdf}\par} #+end_export -**** Only 2 +*** Only 2 :PROPERTIES: -:BEAMER_ENV: onlyenvNH +:BEAMER_ENV: blockNH :BEAMER_ACT: <2> :END: +- At each clock tick, the *whole module* is executed using *big-step semantics*. + #+begin_export latex -\includegraphics[width=8cm]{assets/semantics.pdf} +{\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. @@ -802,7 +830,7 @@ This describes the main proof that is needed to show that the HLS tool is correc | Wrong | Such as undefined behaviour, no guarantees need to be shown. | |------------+------------------------------------------------------------------| -**** Theorem :B_onlyenvNH: +**** Theorem :B_onlyenvNH:noexport: :PROPERTIES: :BEAMER_env: onlyenvNH :BEAMER_ACT: <3> @@ -928,6 +956,8 @@ Prove the simulation diagram correct: - there exists 1 or more steps in Verilog, - such that after 1 step in RTL, the resulting states match. +* Results + ** With Division approximately 27$\times$ slower #+begin_export latex |