Update on Overleaf.

1 files changed, 7 insertions, 1 deletions

diff --git a/conclusion.tex b/conclusion.tex
index 7c06245..a53c268 100644
--- a/conclusion.tex
+++ b/conclusion.tex
@@ -1,6 +1,12 @@
 \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.
+\vericert{} is the first fully mechanised proof of correctness for HLS in Coq, 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 used anymore later on.  It would therefore be useful to have a register allocation algorithm that could ensure that registers could be reused appropriately, where the register allocation algorithm would find the minimum number of registers needed.  Finally, another optimisation would be to support resource sharing to reduce the area that the final design uses, this could include multi-cycle operations and pipelining optimisations so that division and multiplication operators also become more efficient.
+
+Finally, it's worth considering how trustworthy \vericert{} is compared to other HLS tools.  A formally verified tool does not guarantee an output for every input and it is therefore allowed to fail.  However, the subset of C that will compile is well-described and the tool should therefore not fail in surprising ways.  However, the guarantee that the output behaves the same as the input is strong, as it uses well-known C and existing Verilog semantics to prove the equivalence.
+
+
 
 %%% Local Variables:
 %%% mode: latex