Add introduction to verification in HLS

1 files changed, 150 insertions, 0 deletions

diff --git a/references.bib b/references.bib
index 63a9f94..82bba12 100644
--- a/references.bib
+++ b/references.bib
@@ -83,3 +83,153 @@
   urldate         = {2020-06-06},
   year            = 2020,
 }
+
+@inproceedings{gupta03_spark,
+  author          = {S. {Gupta} and N. {Dutt} and R. {Gupta} and A. {Nicolau}},
+  title           = {{SPARK}: a high-level synthesis framework for applying parallelizing compiler
+                  transformations},
+  booktitle       = {16th International Conference on VLSI Design, 2003. Proceedings.},
+  year            = 2003,
+  pages           = {461-466},
+  doi             = {10.1109/ICVD.2003.1183177},
+  url             = {https://doi.org/10.1109/ICVD.2003.1183177},
+  ISSN            = {1063-9667},
+  month           = {Jan},
+}
+
+@article{chouksey20_verif_sched_condit_behav_high_level_synth,
+  author          = {R. {Chouksey} and C. {Karfa}},
+  title           = {Verification of Scheduling of Conditional Behaviors in
+                  High-Level Synthesis},
+  journal         = {IEEE Transactions on Very Large Scale Integration (VLSI)
+                  Systems},
+  volume          = {},
+  number          = {},
+  pages           = {1-14},
+  year            = {2020},
+  doi             = {10.1109/TVLSI.2020.2978242},
+  url             = {https://doi.org/10.1109/TVLSI.2020.2978242},
+  ISSN            = {1557-9999},
+  month           = {},
+}
+
+@inproceedings{pnueli98_trans,
+  author          = "Pnueli, A.  and Siegel, M.  and Singerman, E.",
+  title           = "Translation validation",
+  booktitle       = "Tools and Algorithms for the Construction and Analysis of Systems",
+  year            = 1998,
+  pages           = "151--166",
+  address         = "Berlin, Heidelberg",
+  editor          = "Steffen, Bernhard",
+  isbn            = "978-3-540-69753-4",
+  publisher       = "Springer",
+}
+
+@article{chouksey19_trans_valid_code_motion_trans_invol_loops,
+  author =       {R. {Chouksey} and C. {Karfa} and P. {Bhaduri}},
+  title =        {Translation Validation of Code Motion Transformations
+                  Involving Loops},
+  journal =      {IEEE Transactions on Computer-Aided Design of Integrated
+                  Circuits and Systems},
+  volume =       38,
+  number =       7,
+  pages =        {1378-1382},
+  year =         2019,
+  doi =          {10.1109/TCAD.2018.2846654},
+  ISSN =         {1937-4151},
+  month =        {July},
+}
+
+@article{banerjee14_verif_code_motion_techn_using_value_propag,
+  author = {K. {Banerjee} and C. {Karfa} and D. {Sarkar} and C. {Mandal}},
+  title = {Verification of Code Motion Techniques Using Value
+                  Propagation},
+  journal = {IEEE Transactions on Computer-Aided Design of Integrated
+                  Circuits and Systems},
+  volume = 33,
+  number = 8,
+  pages = {1180-1193},
+  year = 2014,
+  doi = {10.1109/TCAD.2014.2314392},
+  ISSN = {1937-4151},
+  month = {Aug}
+}
+
+@inproceedings{kim04_autom_fsmd,
+  author = { {Youngsik Kim} and S. {Kopuri} and N. {Mansouri}},
+  title = {Automated formal verification of scheduling process using
+                  finite state machines with datapath (FSMD)},
+  tags = {hls, verification},
+  booktitle = {International Symposium on Signals, Circuits and
+                  Systems. Proceedings, SCS 2003. (Cat. No.03EX720)},
+  year = 2004,
+  pages = {110-115},
+  doi = {10.1109/ISQED.2004.1283659},
+  month = {March}
+}
+
+@inproceedings{karfa06_formal_verif_method_sched_high_synth,
+  author =       {Karfa, C and Mandal, C and Sarkar, D and Pentakota, S R. and
+                  Reade, Chris},
+  title =        {A Formal Verification Method of Scheduling in High-level
+                  Synthesis},
+  tags =         {hls},
+  booktitle =    {Proceedings of the 7th International Symposium on Quality
+                  Electronic Design},
+  year =         2006,
+  pages =        {71--78},
+  doi =          {10.1109/ISQED.2006.10},
+  acmid =        1126731,
+  address =      {Washington, DC, USA},
+  isbn =         {0-7695-2523-7},
+  numpages =     8,
+  publisher =    {IEEE Computer Society},
+  series =       {ISQED '06},
+}
+
+@inproceedings{leroy06_formal_certif_compil_back_end,
+  author = {Leroy, Xavier},
+  title = {Formal Certification of a Compiler Back-End or: Programming
+                  a Compiler with a Proof Assistant},
+  booktitle = {Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium
+                  on Principles of Programming Languages},
+  year = 2006,
+  pages = {42-54},
+  doi = {10.1145/1111037.1111042},
+  url = {https://doi.org/10.1145/1111037.1111042},
+  address = {New York, NY, USA},
+  isbn = 1595930272,
+  keywords = {the Coq theorem prover, certified compilation, compiler
+                  transformations and optimizations, program proof, semantic
+                  preservation},
+  location = {Charleston, South Carolina, USA},
+  numpages = 13,
+  publisher = {Association for Computing Machinery},
+  series = {POPL '06}
+}
+
+@book{bertot04_inter_theor_provin_progr_devel,
+  author          = {Yves Bertot and Pierre Cast{\'{e}}ran},
+  title           = {Interactive Theorem Proving and Program Development},
+  year            = 2004,
+  publisher       = {Springer Berlin Heidelberg},
+  url             = {https://doi.org/10.1007/978-3-662-07964-5},
+  doi             = {10.1007/978-3-662-07964-5},
+}
+
+@inproceedings{tristan08_formal_verif_trans_valid,
+  author = {Tristan, Jean-Baptiste and Leroy, Xavier},
+  title = {Formal Verification of Translation Validators: A Case Study on
+                  Instruction Scheduling Optimizations},
+  booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on
+                  Principles of Programming Languages},
+  year = 2008,
+  pages = {17-27},
+  doi = {10.1145/1328438.1328444},
+  address = {New York, NY, USA},
+  isbn = 9781595936899,
+  location = {San Francisco, California, USA},
+  numpages = 11,
+  publisher = {Association for Computing Machinery},
+  series = {POPL '08}
+}