diff options
Diffstat (limited to 'presentation/presentation.org')
| -rw-r--r-- | presentation/presentation.org | 45 |
1 files changed, 23 insertions, 22 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 |