diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-11-13 13:13:43 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-13 13:13:43 +0000 |
| commit | cdbe6f978bf6de9a1b389cebc02dc74666b7a4ee (patch) | |
| tree | c2013228f14222a3fd7f373f3a815edac38806b7 /conclusion.tex | |
| parent | fae93d199b799b3b7ecf9900cec81e548de99d83 (diff) | |
| download | oopsla21_fvhls-cdbe6f978bf6de9a1b389cebc02dc74666b7a4ee.tar.gz oopsla21_fvhls-cdbe6f978bf6de9a1b389cebc02dc74666b7a4ee.zip | |
Update some sections
Diffstat (limited to 'conclusion.tex')
| -rw-r--r-- | conclusion.tex | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/conclusion.tex b/conclusion.tex index 876382d..7c06245 100644 --- a/conclusion.tex +++ b/conclusion.tex @@ -1,5 +1,7 @@ \section{Conclusion} +\vericert{} is the first fully mechanised proof of correctness for HLS, translating C into Verilog. However, to make the tool more usable there are many more optimisations that could be implemented to get the performance closer to \legup{}. The main optimisation that should be performed is scheduling operations into the same clock cycle, so that these can run in parallel. In addition to that, another issue that \vericert{} faces is that \compcert{}'s 3AC uses many different registers, even if these are not anymore later on. It would therefore be useful to have a register allocation algorithm that could ensure that registers could be reused appropriately. Finally, another optimisation would be to support resource sharing to reduce the area that the final design uses. + %%% Local Variables: %%% mode: latex %%% TeX-master: "main" |