diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-02-23 16:16:39 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-23 16:16:39 +0000 |
| commit | a484f9bfda9f8f080a3611c763154d4c6b43bc16 (patch) | |
| tree | f793429fe146b1a6a9e2afd49304f5fa68b47ccc | |
| parent | eac948b89034474b601d45ded400083d6e55bb22 (diff) | |
| download | latte21_hlstpc-a484f9bfda9f8f080a3611c763154d4c6b43bc16.tar.gz latte21_hlstpc-a484f9bfda9f8f080a3611c763154d4c6b43bc16.zip | |
Add a proper abstract
| -rw-r--r-- | main.tex | 14 |
1 files changed, 4 insertions, 10 deletions
@@ -137,15 +137,9 @@ \email{j.wickerson@imperial.ac.uk} \begin{abstract} - High-level synthesis is increasingly being relied upon - \JW{A possible story: \begin{itemize} - \item High-level synthesis is increasingly being relied upon. - \item But it's really flaky. (Cite bugs from FCCM submission etc.) - \item There exist some workarounds. (Testing the output, formally verifying the output, etc.) - \item The time has come to prove the tool itself correct. (Mention success of Compcert and other fully verified tools?) - \item 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.) - \item 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.) - \end{itemize}} + 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. + + 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. \end{abstract} %% 2012 ACM Computing Classification System (CSS) concepts @@ -260,7 +254,7 @@ Finally, it is interesting to compare the performance of Vericert compared to ex \section{Improvements to \vericert{}} - +There are many optimisations that need to be added to Vericert to make turn it into a viable and competitive HLS tool. First of all, the most important addition is a good scheduling implementation, which supports operation chaining and properly pipelining operators. %% Acknowledgments %\begin{acks}%% acks environment is optional |