diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-06-09 11:04:41 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-09 11:04:41 +0100 |
commit | 99dcda680cfa6cf64066aa92c2664130d53f8ab4 (patch) | |
tree | f981bed51a8472fd1d43a64f7ab7f86ec9d98738 /main.tex | |
parent | 28a71bb6ee259d6492f479814984dbd4260e94d6 (diff) | |
parent | e7fa1c8a8dbcf42c7f609a213bbd488fc8eb05bc (diff) | |
download | oopsla21_fvhls-99dcda680cfa6cf64066aa92c2664130d53f8ab4.tar.gz oopsla21_fvhls-99dcda680cfa6cf64066aa92c2664130d53f8ab4.zip |
Merge branch 'master' of https://git.overleaf.com/5ed78033b633200001e693d0
Diffstat (limited to 'main.tex')
-rw-r--r-- | main.tex | 9 |
1 files changed, 8 insertions, 1 deletions
@@ -197,6 +197,13 @@ Using CompCert, we can therefore build a fully verified high-level synthesis too \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. @@ -213,7 +220,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\\ |