summaryrefslogtreecommitdiffstats
path: root/main.tex
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-06-09 11:34:46 +0100
committerYann Herklotz <git@yannherklotz.com>2020-06-09 11:34:46 +0100
commitb1723d690ba76c90e810cfbede727a9366e227d1 (patch)
tree39192d078a1f77ccc3221ae1e71a33a0866026d3 /main.tex
parent4aaeb6659756407b1373177fdb07f72ff6e82447 (diff)
downloadoopsla21_fvhls-b1723d690ba76c90e810cfbede727a9366e227d1.tar.gz
oopsla21_fvhls-b1723d690ba76c90e810cfbede727a9366e227d1.zip
Add more citations that I need to include
Diffstat (limited to 'main.tex')
-rw-r--r--main.tex3
1 files changed, 1 insertions, 2 deletions
diff --git a/main.tex b/main.tex
index 4ef0593..a988a1f 100644
--- a/main.tex
+++ b/main.tex
@@ -204,8 +204,7 @@ Using CompCert, we can therefore build a fully verified high-level synthesis too
\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}.}
+\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} or \citet{grass94_high}. There are also the Occam papers that I need to mention too, like \citet{page91_compil_occam}, \citet{jifeng93_towar}, \citet{perna11_correc_hardw_synth} and \citet{perna12_mechan_wire_wise_verif_handel_c_synth}.}
\section{Verilog Semantics}