blob: 92ffecd7339060c88327737c32d593a10ea4ee5d (
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
|
#+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
|