blob: 423826faea9255bf1470b71627577d31ed2a9919 (
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
|
#+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
|
