diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-02-25 13:11:30 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-25 13:11:30 +0000 |
| commit | 8627e6424bcd32665c57378ff2a67fb83d30f216 (patch) | |
| tree | e9c352f8af97ec3cab37ff30aab59b5617049bb6 | |
| parent | ae9823e2f4288c2d6822acd0b1e98a9d6d4cc0f7 (diff) | |
| download | latte21_hlstpc-8627e6424bcd32665c57378ff2a67fb83d30f216.tar.gz latte21_hlstpc-8627e6424bcd32665c57378ff2a67fb83d30f216.zip | |
Improve abstract
| -rw-r--r-- | main.tex | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -145,9 +145,9 @@ % - 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.) \begin{abstract} - High-level synthesis (HLS) is increasingly being relied upon as the size of designs and needs for hardware accelerators increases. However, HLS is known to be quite flaky with each tool supporting different input languages and sometimes generating incorrect designs. + High-level synthesis (HLS) is increasingly being relied upon as the size of designs and needs for hardware accelerators increases. However, HLS is known to be quite flaky with each tool supporting different input languages and sometimes even generating incorrect designs. - A formally verified HLS tool would solve these issues by dramatically reducing the amount of trusted code, and providing a formal description of the input language that is supported. In this respect, we have developed \vericert{}, a formally verified HLS tool, based on \compcert{}, a formally verified C compiler. + We argue that formally verifying HLS could solve this issue by dramatically reducing the amount of trusted code, and providing a formal description of the input language that is supported. In this respect, we have developed \vericert{}, a formally verified HLS tool, based on \compcert{}, a formally verified C compiler. \end{abstract} %% 2012 ACM Computing Classification System (CSS) concepts |