diff options
| -rw-r--r-- | main.tex | 7 | ||||
| -rw-r--r-- | references.bib | 8 |
2 files changed, 14 insertions, 1 deletions
@@ -196,8 +196,10 @@ CompCert~\cite{leroy06_formal_certif_compil_back_end} is a C compiler that has b In this paper we describe a fully verified high-level synthesis tool called CoqUp, which adds a Verilog backend to CompCert and proves that the behaviour of the C code does not change according to existing Verilog semantics. The main contributions of the paper are the following: \begin{itemize} + \item first mechanised and formally verified HLS flow \item Proof by simulation mechanised in Coq between CompCert's intermediate language and Verilog. \item Description of the Verilog semantics used to integrate it into CompCert's model. + \item able to run HLS benchmarks which are now known to be correct. \end{itemize} CoqUp is open source and is hosted on Github\footnote{https://github.com/ymherklotz/coqup}. @@ -212,8 +214,11 @@ CoqUp is open source and is hosted on Github\footnote{https://github.com/ymherkl \JW{Some papers to cite somewhere: \begin{itemize} - \item \citet{kundu08_valid_high_level_synth} have done translation validation on an HLS tool called SPARK.\@ + \item \citet{kundu08_valid_high_level_synth} have done translation validation on an HLS tool called SPARK. They don't have \emph{very} strong evidence that HLS tools are buggy; they just say ``HLS tools are large and complex software systems, often with hundreds of +thousands of lines of code, and as with any software of this scale, they are prone +to logical and implementation errors''. They did, however, find two bugs in SPARK as a result of their efforts, so that provides a small bit of evidence that HLS tools are buggy. \@ \item \citet{chapman92_verif_bedroc} have proved (manually, as far as JW can tell) that the front-end and scheduler of the BEDROC synthesis system is correct. (NB:\@ Chapman also wrote a PhD thesis about this (1994) but it doesn't appear to be online.) + \item \citet{ellis08} wrote a PhD thesis that was supervised by Cliff Jones whom you met at the VeTSS workshop thing last year. At a high level, it's about verifying a high-level synthesis tool using Isabelle, so very relevant to this project, though scanning through the pdf, it's quite hard to ascertain exactly what the contributions are. Strange that they never published a paper about the work -- it makes it very hard to find! \end{itemize} } diff --git a/references.bib b/references.bib index 06e7ac5..c72193a 100644 --- a/references.bib +++ b/references.bib @@ -326,3 +326,11 @@ issn = "1432-0525", month = "Dec" } + +@phdthesis{ellis08, + author = {Ellis, Martin}, + title = {Correct synthesis and integration of compiler-generated function units}, + school = {Newcastle University}, + url = {https://theses.ncl.ac.uk/jspui/handle/10443/828}, + year = {2008}, +}
\ No newline at end of file |