diff options
Diffstat (limited to 'main.tex')
| -rw-r--r-- | main.tex | 10 |
1 files changed, 9 insertions, 1 deletions
@@ -216,6 +216,8 @@ There are a couple of theorems one can prove about the HLS tool once it is writt However, there are also assumptions that have to be made about the tool. In the case of \vericert{}, the only assumption that needs to be made is if the C semantics and Verilog semantics can be trusted. This is much simpler than checking that the translation algorithm is implemented properly. Using that assumption, the proofs ensure that the translation preserves the behaviour and doesn't need to be trusted. +Trusting the Verilog semantics is not that easy, since it is not quite clear which semantics to take. Verilog can either be simulated or synthesised into hardware, and has different semantics based on how it is used. We therefore use existing Verilog semantics by \citet{loow19_proof_trans_veril_devel_hol}, which are designed to only model a small part of the semantics, while ensuring that the behaviour for synthesis and simulation stays the same. + \section{Performance of such a tool} Finally, it is interesting to compare the performance of \vericert{} compared to existing HLS tools, to see how correctness guarantees affect the size and speed of the final hardware. This was done on a common compiler benchmark called PolyBench/C~\cite{polybench}. @@ -262,7 +264,13 @@ Finally, it is interesting to compare the performance of \vericert{} compared to \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. +There are many optimisations that need to be added to \vericert{} to 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. Our main focus is trying to implement scheduling based on system of difference constraint~\cite{cong06_sdc}, which is the same algorithm which \legup{} uses. We have currently implemented the scheduling algorithm, as well as a simple verifier for the translation, but are missing the semantic preservation proofs that the verifier should produce. + +The main idea used to prove the scheduling correct, is to split it up into multiple stages. The first stage of the translation will turn basic blocks into a parallel basic block representation, whereas the second + +\section{Conclusion} + +In conclusion, we have shown that a verified HLS tool can achieve similar performance to an existing, unverified HLS tool, while guaranteeing that the output is always correct. %% Acknowledgments %\begin{acks}%% acks environment is optional |