#+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.