From e7fa1c8a8dbcf42c7f609a213bbd488fc8eb05bc Mon Sep 17 00:00:00 2001 From: John Wickerson Date: Tue, 9 Jun 2020 09:39:07 +0000 Subject: Update on Overleaf. --- main.tex | 9 ++++++++- references.bib | 25 +++++++++++++++++++++++++ 2 files changed, 33 insertions(+), 1 deletion(-) diff --git a/main.tex b/main.tex index ced45f4..3ac94aa 100644 --- a/main.tex +++ b/main.tex @@ -193,6 +193,13 @@ Therefore, work is being done to prove the equivalence between the generated har \subsection{HLS} +\JW{Some papers to cite somewhere: +\begin{itemize} + \item \citet{kundu+08} have done translation validation on an HLS tool called SPARK. + \item \citet{chapman+92} 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.) +\end{itemize} +} + \section{Verilog Semantics} Definition of state. @@ -209,7 +216,7 @@ based on what they evaluate to. For case I think that would end up being a three \JP{I suppose this would essentially be an ``interpreter'' style semantics but we can prove equivalence pretty easily.} -\YH{To add to that, I used to have both in the Coq code, but commented the recursive definition out, and now only have the inductive definition, which is basically what I copy pasted here.} \JW{Fair enough. Whatever you think ends up being the easiest to read and understand, really. There's something to be said for staying close to the Coq definitions anyway.} \YH{I have added more rules, we can always switch from one to the other now. One more thing I noticed though is that recursive definitions will need an \texttt{option} type.} +\YH{To add to that, I used to have both in the Coq code, but commented the recursive definition out, and now only have the inductive definition, which is basically what I copy pasted here.} \JW{Fair enough. Whatever you think ends up being the easiest to read and understand, really. There's something to be said for staying close to the Coq definitions anyway.} \YH{I have added more rules, we can always switch from one to the other now. One more thing I noticed though is that recursive definitions will need an \texttt{option} type.} \JW{Oh, then my suggestion of `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2' is a bit ill-typed then, unless the second parameter becomes option-typed too. Maybe the inference rules are better overall then.} \begin{align} \text{srun}\ f\ s\ \mathtt{Vskip} &= \mathtt{Some}\ s\\ diff --git a/references.bib b/references.bib index 63a9f94..45c8419 100644 --- a/references.bib +++ b/references.bib @@ -83,3 +83,28 @@ urldate = {2020-06-06}, year = 2020, } + +@InProceedings{kundu+08, +author="Kundu, Sudipta +and Lerner, Sorin +and Gupta, Rajesh", +editor="Gupta, Aarti +and Malik, Sharad", +title="Validating High-Level Synthesis", +booktitle="Computer Aided Verification (CAV)", +year="2008", +publisher="Springer", +pages="459--472", +} + +@INPROCEEDINGS {chapman+92, +author = {Richard Chapman and Geoffrey Brown and Miriam Leeser}, +booktitle = {European Conference on Design Automation (EDAC)}, +title = {Verified high-level synthesis in BEDROC}, +year = {1992}, +pages = {59--63}, +doi = {10.1109/EDAC.1992.205894}, +url = {https://doi.ieeecomputersociety.org/10.1109/EDAC.1992.205894}, +publisher = {IEEE Computer Society}, +} + -- cgit