diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-06-09 11:24:45 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-09 11:24:45 +0100 |
commit | 4aaeb6659756407b1373177fdb07f72ff6e82447 (patch) | |
tree | 62ddd750ebbd5dee8d07dce6a54f13a0c05c6ec6 /main.tex | |
parent | 99dcda680cfa6cf64066aa92c2664130d53f8ab4 (diff) | |
download | oopsla21_fvhls-4aaeb6659756407b1373177fdb07f72ff6e82447.tar.gz oopsla21_fvhls-4aaeb6659756407b1373177fdb07f72ff6e82447.zip |
Add response
Diffstat (limited to 'main.tex')
-rw-r--r-- | main.tex | 7 |
1 files changed, 5 insertions, 2 deletions
@@ -199,11 +199,14 @@ Using CompCert, we can therefore build a fully verified high-level synthesis too \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.) + \item \citet{kundu08_valid_high_level_synth} have done translation validation on an HLS tool called SPARK.\@ + \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.) \end{itemize} } + +\YH{Amazing, thank you, yes it seems like Kundu \textit{et al.} have quite a few papers on formal verification of HLS algorithms using translation validation, as well as~\citet{karfa06_formal_verif_method_sched_high_synth}, all using the SPARK~\cite{gupta03_spark} synthesis tool. And yes thank you, will definitely cite that paper. There seem to be similar early proofs of high-level synthesis like~\citet{hwang91_formal_approac_to_sched_probl}.} + \section{Verilog Semantics} Definition of state. |