From 4bf5c08e1766bfa18b4a1505c34eefdcd043a3d2 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 6 Oct 2021 18:58:37 +0100 Subject: Update all --- presentation/presentation.org | 45 +++++++++++++++++++++--------------------- presentation/presentation.pdf | Bin 2524371 -> 2529950 bytes presentation/references.bib | 14 ------------- 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 Binary files a/presentation/presentation.pdf and b/presentation/presentation.pdf differ 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)}, -- cgit