From b1723d690ba76c90e810cfbede727a9366e227d1 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 9 Jun 2020 11:34:46 +0100
Subject: Add more citations that I need to include

---
 main.tex       |  3 +--
 references.bib | 62 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 63 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}
 
diff --git a/references.bib b/references.bib
index 5ff4450..8677a96 100644
--- a/references.bib
+++ b/references.bib
@@ -283,3 +283,65 @@
                   processing;Filters;Hardware design languages;Flow graphs},
   month = {April}
 }
+
+@inproceedings{page91_compil_occam,
+  author = {Page, Ian and Luk, Wayne},
+  title = {Compiling Occam into field-programmable gate arrays},
+  booktitle = {FPGAs, Oxford Workshop on Field Programmable Logic and
+                  Applications},
+  year = 1991,
+  volume = 15,
+  pages = {271--283},
+}
+
+@inproceedings{grass94_high,
+  author = {W. {Grass} and M. {Mutz} and W. -. {Tiedemann}},
+  title = {High level synthesis based on formal methods},
+  booktitle = {Proceedings of Twentieth Euromicro Conference. System
+                  Architecture and Integration},
+  year = 1994,
+  pages = {83-91},
+  doi = {10.1109/EURMIC.1994.390403},
+  month = {Sep.}
+}
+
+@inproceedings{jifeng93_towar,
+  author = "Jifeng, He and Page, Ian and Bowen, Jonathan",
+  title = "Towards a provably correct hardware implementation of occam",
+  tags = {hls},
+  booktitle = "Correct Hardware Design and Verification Methods",
+  year = 1993,
+  pages = "214--225",
+  address = "Berlin, Heidelberg",
+  editor = "Milne, George J.  and Pierre, Laurence",
+  isbn = "978-3-540-70655-7",
+  publisher = "Springer"
+}
+
+@article{perna12_mechan_wire_wise_verif_handel_c_synth,
+  author = "Juan Perna and Jim Woodcock",
+  title = {Mechanised Wire-Wise Verification of {Handel-C} Synthesis},
+  journal = "Science of Computer Programming",
+  volume = 77,
+  number = 4,
+  pages = "424 - 443",
+  year = 2012,
+  doi = "10.1016/j.scico.2010.02.007",
+  issn = "0167-6423",
+}
+
+@article{perna11_correc_hardw_synth,
+  author = "Perna, Juan and Woodcock, Jim and Sampaio, Augusto and Iyoda,
+                  Juliano",
+  title = {Correct Hardware Synthesis},
+  tags = {hls},
+  journal = "Acta Informatica",
+  volume = 48,
+  number = 7,
+  pages = "363--396",
+  year = 2011,
+  doi = "10.1007/s00236-011-0142-y",
+  day = 01,
+  issn = "1432-0525",
+  month = "Dec"
+}
-- 
cgit