diff options
Diffstat (limited to 'main.tex')
| -rw-r--r-- | main.tex | 5 |
1 files changed, 2 insertions, 3 deletions
@@ -145,10 +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. - \JW{I'd be tempted to switch that around to make a more interesting opening: `With hardware designs becoming ever more complex and demand for custom accelerators ever growing, high-level synthesis (HLS) is increasingly being relied upon.'} However, HLS is known to be quite flaky \JW{,} with each tool supporting \JW{subtly} different \JWreplace{input languages}{fragments of the input language} and sometimes even generating incorrect designs. + With hardware designs becoming ever more complex and demand for custom accelerators ever growing, high-level synthesis (HLS) is increasingly being relied upon. However, HLS is known to be quite flaky, with each tool supporting subtly different fragments of the input language and sometimes even generating incorrect designs. - We argue that \JWreplace{formally verifying HLS}{a formally verified HLS tool} could solve this issue by dramatically reducing the amount of trusted code, and providing a formal description of the input language that is supported. \JWcouldcut{In this respect,} \JW{To this end,} we have developed \vericert{}, a formally verified HLS tool, based on \compcert{}, a formally verified C compiler. + We argue that a formally verified HLS tool could solve this issue by dramatically reducing the amount of trusted code, and providing a formal description of the input language that is supported. To this end, 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 |