blob: 7c0624500f1fc930cb43a66039af54e8dd505c96 (
plain)
1
2
3
4
5
6
7
8
|
\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"
%%% End:
|
