diff options
| author | John Wickerson <j.wickerson@imperial.ac.uk> | 2022-01-17 21:44:30 +0000 |
|---|---|---|
| committer | node <node@git-bridge-prod-0> | 2022-01-17 21:44:31 +0000 |
| commit | f46938d3f88262093879c8ca4bf352fb8f4d07c6 (patch) | |
| tree | faba9af0ef8408d5fe66d792d0bf43f868e0956a | |
| parent | fd77b37bcc5911c84f527b6eb2e8ca43acc6b72d (diff) | |
| download | fccm22_rsvhls-f46938d3f88262093879c8ca4bf352fb8f4d07c6.tar.gz fccm22_rsvhls-f46938d3f88262093879c8ca4bf352fb8f4d07c6.zip | |
Update on Overleaf.
| -rw-r--r-- | verified_resource_sharing.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex index 27e6df5..3613cf4 100644 --- a/verified_resource_sharing.tex +++ b/verified_resource_sharing.tex @@ -102,7 +102,7 @@ However, doubts have been raised about the reliability of the current crop of HL Aiming to address this issue is \vericert{}~\cite{vericert}, a new HLS tool whose correctness has been checked to the highest possible standard: machine-checked proof. It provides a proof, checked using the Coq proof assistant~\cite{coq}, that every step of its translation from C to Verilog preserves the semantics of its input program. This means that we can always trust any Verilog design produced by \vericert{} to behave the same way as the C program given as input. %It is based on the CompCert~\cite{compcert_Leroy2009} verified C compiler. -Clearly, however, it is not enough for an HLS tool simply to be \emph{correct}; the generated hardware must also enjoy high throughput, low latency, and good \emph{area efficiency} -- the last of which is the topic of this paper. A common optimisation employed by HLS tools to improve area efficiency is \emph{resource sharing}; that is, re-using hardware for more than one purpose. Accordingly, our work adds resource sharing to \vericert{}, Keeping with the aims of the \vericert{} project, work is ongoing to extend the correctness proof. +Clearly, however, it is not enough for an HLS tool simply to be \emph{correct}; the generated hardware must also enjoy high throughput, low latency, and good \emph{area efficiency} -- the last of which is the topic of this paper. A common optimisation employed by HLS tools to improve area efficiency is \emph{resource sharing}; that is, re-using hardware for more than one purpose. Accordingly, our work adds resource sharing to \vericert{} a new prototype HLS tool called Keeping with the aims of the \vericert{} project, work is ongoing to extend the correctness proof. The entire \vericertfun{} development is fully open-source~\cite{vericertfun-github}. Further details about the implementation and proofs are available in a technical report~\cite{pardalos_thesis}. |