Update all

3 files changed, 23 insertions, 36 deletions

diff --git a/presentation/presentation.org b/presentation/presentation.org
index 539a093..b0a3955 100644
--- a/presentation/presentation.org
+++ b/presentation/presentation.org
@@ -6,15 +6,16 @@
 
 ** Script for start :noexport:
 
-Hi, I'm Yann and I will be presenting our work on formally verified high-level synthesis.
+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 overkill, as one doesn't need the flexibility a CPU offers, and they
-therefore use up too much power.  Instead, one would ideally like to have a special chip that only
-does that one task, thereby using up less power and probably being more performant at that task.
+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, they are reprogrammable hardware, and allow it's circuit to be configured after it
-has left the factory.
+FPGAs come in, whose main benefit is that their circuit can be reprogrammed at any time.
 
 ** The Need to Design Hardware Accelerators
 
@@ -265,25 +266,26 @@ Translation of a high-level programming language such as C/C++ into a hardware d
 
 ** Motivation for Formal Verification
 
-*** HLS Difficulties :B_blockNH:
-:PROPERTIES:
-:BEAMER_env: blockNH
-:END:
-
-Difficult to debug HLS tools:
-
-- Simulation can take a long time.
-- Correctness is important in hardware, testing is done at every level.
-
 *** HLS Unreliable :B_blockNH:
 :PROPERTIES:
 :BEAMER_env: blockNH
-:BEAMER_ACT: <2>
 :END:
 
 High-level synthesis is often quite unreliable:
 
-- We fuzzed HLS tools (cite:9444067) and found they failed on *2.5%* of simple random test cases.
+- 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:
@@ -1301,7 +1303,7 @@ Fuzzed Vericert with Csmith to check correctness theorem.
 |-----------------+-----------------|
 | Vivado HLS      |           1.23% |
 | Intel i++       |            0.4% |
-| Bambu 0.9.7-dev |    0.3% (13.7%) |
+| Bambu 0.9.7-dev |            0.3% |
 | LegUp 4.0       |            0.1% |
 |-----------------+-----------------|
 
@@ -1323,10 +1325,10 @@ Fuzzed Vericert with Csmith to check correctness theorem.
 |-----------------+-----------------|
 | Vivado HLS      |           1.23% |
 | Intel i++       |            0.4% |
-| Bambu 0.9.7-dev |    0.3% (13.7%) |
+| Bambu 0.9.7-dev |            0.3% |
 | LegUp 4.0       |            0.1% |
 |-----------------+-----------------|
-| *Vericert*        |      *0% (0.03%)* |
+| *Vericert*        |        +0.03%+ *0%* |
 |-----------------+-----------------|
 
 ** Conclusion
@@ -1388,7 +1390,6 @@ Make Vericert not only *correct*, but *competitive*.
 
 bibliography:./references.bib
 
-
 * Extensions :noexport:
 ** Current work
 
diff --git a/presentation/presentation.pdf b/presentation/presentation.pdf
index 0842f3b..af5ac63 100644
--- a/presentation/presentation.pdf
+++ b/presentation/presentation.pdf
diff --git a/presentation/references.bib b/presentation/references.bib
index ea2fa3a..11e20ad 100644
--- a/presentation/references.bib
+++ b/presentation/references.bib
@@ -1,17 +1,3 @@
-
-@inproceedings{lidbury15_many_core_compil_fuzzin,
-	author = {Lidbury, Christopher and Lascu, Andrei and Chong, Nathan and Donaldson,
-                  Alastair F.},
-	title = {Many-Core Compiler Fuzzing},
-	booktitle = {Proc. of the 36th ACM SIGPLAN Conf. on Programming Language Design and Implementation},
-	year = 2015,
-	doi = {10.1145/2737924.2737986},
-	keywords = {random testing, Compilers, OpenCL, metamorphic testing, GPUs, concurrency},
-	numpages = 12,
-	publisher = {ACM},
-	series = {PLDI '15}
-}
-
 @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)},