blob: 35ded6410c02b75a684e24c1a6c267f65994571c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
#+title: Paper Outline and Draft
#+author: Yann Herklotz
** A possible story:
- High-level synthesis is increasingly being relied upon.
- But it's really flaky. (Cite bugs from FCCM submission etc.)
- There exist some workarounds. (Testing the output, formally verifying the output, etc.)
- The time has come to prove the tool itself correct. (Mention success of Compcert and other fully verified tools?)
- We've made some encouraging progress on this front in a prototype tool called Vericert. (Summarise current state of Vericert, and how it compares performance-wise to LegUp.)
- But there's still a long way to go. (List the main things left to do, and how you expect Vericert to compare to LegUp after those things are done.)
- Performance vs correctness.
* Introduction
- Importance of correctness, especially in HLS.
- [cite:lahti19_are_we_there_yet]: Talks about being able to trust synthesis tools.
- Current focus of HLS is mainly on optimisations
- Correctness guarantees help with duplicate verificaton.
* How can we prove an HLS tool correct?
* Guarantees and trusted code
* Performance of such a tool
- ramp up more about the future.
- formally verifying other algorithms
TODO:
- move second part of first paragraph.
- add to intro what this document is
- last paragraph more like last part of abstract (To that end we have made one.)
- Separate second point into are already reliable and existing testing techniques are enough.
- Most hardware designs start in C.
- First John bacceses fortran compiler.
|
