diff options
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" |