From 8627e6424bcd32665c57378ff2a67fb83d30f216 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 25 Feb 2021 13:11:30 +0000 Subject: Improve abstract --- main.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/main.tex b/main.tex index 5874499..dffecb4 100644 --- a/main.tex +++ b/main.tex @@ -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 -- cgit