path: root/references.bib

@article{leroy09_formal_verif_realis_compil,
  author =       {Leroy, Xavier},
  title =        {Formal Verification of a Realistic Compiler},
  journal =      {Commun. ACM},
  volume =       52,
  number =       7,
  pages =        {107-115},
  year =         2009,
  doi =          {10.1145/1538788.1538814},
  address =      {New York, NY, USA},
  issn =         {0001-0782},
  issue_date =   {July 2009},
  month =        jul,
  numpages =     9,
  publisher =    {ACM},
}

@article{six+20,
 author={Cyril Six and Sylvain Boulm\'e and David Monniaux},
 title = {{Certified and efficient instruction scheduling: Application to interlocked {VLIW} processors}},
  journal   = {Proc. {ACM} Program. Lang.},
  number    = {{OOPSLA}},
  year      = {2020}
 }

@inproceedings{lidbury15_many_core_compil_fuzzin,
  author          = {Lidbury, Christopher and Lascu, Andrei and Chong, Nathan and Donaldson,
                  Alastair F.},
  title           = {Many-Core Compiler Fuzzing},
  booktitle       = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design
                  and Implementation},
  year            = 2015,
  pages           = {65-76},
  doi             = {10.1145/2737924.2737986},
  address         = {New York, NY, USA},
  isbn            = 9781450334686,
  location        = {Portland, OR, USA},
  numpages        = 12,
  publisher       = {ACM},
  series          = {PLDI '15},
}

@misc{polybench,
author = {Pouchet, Louis-No\"el},
title = {PolyBench/C: the Polyhedral Benchmark suite},
url = {http://web.cse.ohio-state.edu/~pouchet.2/software/polybench/},
year = {2020},
}

@INPROCEEDINGS{5522874,
  author={Dan Gajski and Todd Austin and Steve Svoboda},
  booktitle={Design Automation Conference},
  title={What input-language is the best choice for high level synthesis (HLS)?},
  year={2010},
  volume={},
  number={},
  pages={857-858},
  doi={10.1145/1837274.1837489}}

@inproceedings{bluespec,
  author={Nikhil, Rishiyur S. },
  booktitle={Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE '04.},
  title={Bluespec System Verilog: efficient, correct RTL from high level specifications},
  year={2004},
  volume={},
  number={},
  pages={69-70},
  doi={10.1109/MEMCOD.2004.1459818}}

@inproceedings{davidthomas_asap16,
  author    = {Thomas, David B.},
  title     = {Synthesisable recursion for {C++} {HLS} tools},
  booktitle = {{ASAP}},
  pages     = {91--98},
  publisher = {{IEEE} Computer Society},
  year      = {2016},
  doi = {10.1109/ASAP.2016.7760777}
}

@article{cong+11,
  author    = {Jason Cong and
               Bin Liu and
               Stephen Neuendorffer and
               Juanjo Noguera and
               Kees A. Vissers and
               Zhiru Zhang},
  title     = {High-Level Synthesis for FPGAs: From Prototyping to Deployment},
  journal   = {{IEEE} Trans. Comput. Aided Des. Integr. Circuits Syst.},
  volume    = {30},
  number    = {4},
  pages     = {473--491},
  year      = {2011},
  doi = {10.1109/TCAD.2011.2110592}
}

@inproceedings{kiwi,
  author    = {David J. Greaves and
               Satnam Singh},
  title     = {Kiwi: Synthesis of {FPGA} Circuits from Parallel Programs},
  booktitle = {{FCCM}},
  pages     = {3--12},
  publisher = {{IEEE} Computer Society},
  year      = {2008},
  doi={10.1109/FCCM.2008.46}
}

@inproceedings{spatial,
  author    = {David Koeplinger and
               Matthew Feldman and
               Raghu Prabhakar and
               Yaqi Zhang and
               Stefan Hadjis and
               Ruben Fiszel and
               Tian Zhao and
               Luigi Nardi and
               Ardavan Pedram and
               Christos Kozyrakis and
               Kunle Olukotun},
  title     = {Spatial: A Language and Compiler for Application Accelerators},
  booktitle = {{PLDI}},
  pages     = {296--311},
  publisher = {{ACM}},
  year      = {2018},
  doi       = {https://doi.org/10.1145/3192366.3192379}
}

@misc{greaves_note,
      title={Research Note: An Open Source Bluespec Compiler},
      author={David J. Greaves},
      year={2019},
      eprint={1905.03746},
      archivePrefix={arXiv},
      primaryClass={cs.PL}
}

@article{takach16_high_level_synth,
  author          = {A. {Takach}},
  title           = {High-Level Synthesis: Status, Trends, and Future
                  Directions},
  journal         = {IEEE Design Test},
  volume          = {33},
  number          = {3},
  pages           = {116-124},
  year            = {2016},
  doi             = {10.1109/MDAT.2016.2544850},
  url             = {https://doi.org/10.1109/MDAT.2016.2544850},
  ISSN            = {2168-2364},
  month           = {June},
}

@inproceedings{liu16_effic_high_level_synth_desig,
  author          = { {Dong Liu} and B. C. {Schafer}},
  title           = {Efficient and reliable High-Level Synthesis Design Space
                  Explorer for FPGAs},
  booktitle       = {2016 26th International Conference on Field Programmable
                  Logic and Applications (FPL)},
  year            = 2016,
  pages           = {1-8},
  doi             = {10.1109/FPL.2016.7577370},
  ISSN            = {1946-1488},
  month           = {Aug},
}

@article{lahti19_are_we_there_yet,
  author          = {S. {Lahti} and P. {Sj{\"o}vall} and J. {Vanne} and
                  T. D. {H{\"a}m{\"a}l{\"a}inen}},
  title           = {Are We There Yet? a Study on the State of High-Level
                  Synthesis},
  journal         = {IEEE Transactions on Computer-Aided Design of Integrated
                  Circuits and Systems},
  volume          = {38},
  number          = {5},
  pages           = {898-911},
  year            = {2019},
  doi             = {10.1109/TCAD.2018.2834439},
  ISSN            = {1937-4151},
  month           = {May},
}

@misc{mentor20_catap_high_level_synth,
  author          = {Mentor},
  title           = {Catapult High-Level Synthesis},
  url             = {https://www.mentor.com/hls-lp/catapult-high-level-synthesis/c-systemc-hls},
  urldate         = {2020-06-06},
  year            = 2020,
}

@inproceedings{gupta03_spark,
  author          = {{Gupta}, S. and {Dutt}, N. and {Gupta}, R. and {Nicolau}, A.},
  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          = {Chouksey, R. and Karfa, C.},
  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",
  doi = "10.1007/BFb0054170"
}

@article{chouksey19_trans_valid_code_motion_trans_invol_loops,
  author =       {{Chouksey}, R. and {Karfa}, C. and {Bhaduri}, P.},
  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 = {{Banerjee}, K. and {Karfa}, C. and {Sarkar}, D. and {Mandal}, C.},
  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 {Kopuri}, S. and {Mansouri}, N.},
  title = {Automated formal verification of scheduling process using
                  finite state machines with datapath (FSMD)},
  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},
  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,
  location = {Charleston, South Carolina, USA},
  numpages = 13,
  publisher = {ACM},
  series = {POPL '06}
}

@book{bertot04_inter_theor_provin_progr_devel,
  author          = {Bertot, Yves and Cast{\'{e}}ran, Pierre},
  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 = {ACM},
  series = {POPL '08}
}

@inproceedings{kundu08_valid_high_level_synth,
  author          = "Kundu, Sudipta and Lerner, Sorin and Gupta, Rajesh",
  title           = "Validating High-Level Synthesis",
  booktitle       = "Computer Aided Verification",
  year            = 2008,
  pages           = "459--472",
  address         = "Berlin, Heidelberg",
  editor          = "Gupta, Aarti and Malik, Sharad",
  isbn            = "978-3-540-70545-1",
  publisher       = "Springer",
  doi = "10.1007/978-3-540-70545-1_44"
}

@inproceedings{chapman92_verif_bedroc,
  author          = {{Chapman}, R. and {Brown}, G. and {Leeser}, M.},
  title           = {Verified high-level synthesis in BEDROC},
  booktitle       = {[1992] Proceedings The European Conference on Design Automation},
  year            = 1992,
  pages           = {59--63},
  doi             = {10.1109/EDAC.1992.205894},
  month           = {March},
  publisher       = {IEEE Computer Society},
}

@article{hwang91_formal_approac_to_sched_probl,
  author = {{Hwang}, C. -. and {Lee}, J. -. and {Hsu}, Y. -.},
  title = {A Formal Approach To the Scheduling Problem in High Level
                  Synthesis},
  journal = {IEEE Transactions on Computer-Aided Design of Integrated
                  Circuits and Systems},
  volume = 10,
  number = 4,
  pages = {464-475},
  year = 1991,
  doi = {10.1109/43.75629},
  url = {https://doi.org/10.1109/43.75629},
  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 = {{Grass}, W. and {Mutz}, M. and {Tiedemann}, W. -.},
  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",
  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 = "Perna, Juan and Woodcock, Jim",
  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},
  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"
}

@phdthesis{ellis08,
  author = {Ellis, Martin},
  title = {Correct synthesis and integration of compiler-generated function units},
  school = {Newcastle University},
  url = {https://theses.ncl.ac.uk/jspui/handle/10443/828},
  year = {2008},
}



@misc{slec_whitepaper,
  author = {Chauhan, Pankaj},
  title = {Formally Ensuring Equivalence between C++ and RTL designs},
  url = {https://bit.ly/2KbT0ki},
  year = {2020},
}

@inproceedings{loow19_verif_compil_verif_proces,
  author =       {L\"{o}\"{o}w, Andreas and Kumar, Ramana and Tan, Yong Kiam and
                  Myreen, Magnus O. and Norrish, Michael and Abrahamsson, Oskar
                  and Fox, Anthony},
  title =        {Verified Compilation on a Verified Processor},
  tags =         {verification},
  booktitle =    {Proceedings of the 40th ACM SIGPLAN Conference on Programming
                  Language Design and Implementation},
  year =         2019,
  pages =        {1041--1053},
  doi =          {10.1145/3314221.3314622},
  acmid =        3314622,
  address =      {New York, NY, USA},
  isbn =         {978-1-4503-6712-7},
  keywords =     {compiler verification, hardware verification, program
                  verification, verified stack},
  location =     {Phoenix, AZ, USA},
  numpages =     13,
  publisher =    {ACM},
  series =       {PLDI 2019},
}

@inproceedings{canis11_legup,
  author          = {Canis, Andrew and Choi, Jongsok and Aldham, Mark and Zhang, Victor and
                  Kammoona, Ahmed and Anderson, Jason Helge and Brown, Stephen Dean and Czajkowski, Tomasz S.},
  title           = {{LegUp}: high-level synthesis for {FPGA}-based processor/accelerator systems},
  booktitle       = {{FPGA}},
  year            = 2011,
  pages           = {33--36},
  publisher       = {{ACM}},
  doi = {10.1145/1950413.1950423}
}

@INPROCEEDINGS{choi+18,
  author={{Choi}, Y. and {Cong}, J.},
  booktitle={2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)},
  title={HLS-Based Optimization and Design Space Exploration for Applications with Variable Loop Bounds},
  year={2018},
  volume={},
  number={},
  pages={1-8},
  doi={10.1145/3240765.3240815}}


@book{micheli94_synth_optim_digit_circuit,
  author          = {De Micheli, Giovanni},
  title           = {Synthesis and Optimization of Digital Circuits},
  year            = 1994,
  publisher       = {McGraw-Hill Higher Education},
  edition         = {1st},
  isbn            = 0070163332,
}

@article{05_ieee_stand_veril_regis_trans_level_synth,
  title           = {{IEEE} Standard for {Verilog} Register Transfer Level Synthesis},
  journal         = {IEC 62142-2005 First edition 2005-06 IEEE Std 1364.1},
  volume          = {},
  number          = {},
  pages           = {1-116},
  year            = {2005},
  doi             = {10.1109/IEEESTD.2005.339572},
  url             = {https://doi.org/10.1109/IEEESTD.2005.339572},
  ISSN            = {},
  key             = {IEEE Std 1364.1},
  keywords        = {IEC Standards;Verilog;Registers},
  month           = {},
  type            = {Standard},
}

@article{06_ieee_stand_veril_hardw_descr_languag,
  author          = {},
  title           = {{IEEE} Standard for Verilog Hardware Description Language},
  journal         = {IEEE Std 1364-2005 (Revision of IEEE Std 1364-2001)},
  volume          = {},
  number          = {},
  pages           = {1-590},
  year            = {2006},
  doi             = {10.1109/IEEESTD.2006.99495},
  url             = {https://doi.org/10.1109/IEEESTD.2006.99495},
  ISSN            = {},
  key             = {IEEE Std 1364},
  month           = {April},
  type            = {Standard},
}

@misc{xilinx20_vivad_high_synth,
  author          = {Xilinx},
  title           = {Vivado High-level Synthesis},
  url             = {https://bit.ly/39ereMx},
  urldate         = {2020-07-20},
  year            = 2020,
}

@misc{intel_hls,
  author = {Intel},
  title = {High-level Synthesis Compiler},
  url = {https://intel.ly/2UDiWr5},
  urldate = {2020-11-18},
  year = {2020},
  }

@misc{intel20_sdk_openc_applic,
  author          = {Intel},
  title           = {{SDK} for {OpenCL} Applications},
  url             = {https://intel.ly/30sYHz0},
  urldate         = {2020-07-20},
  year            = 2020,
}

@inproceedings{homsirikamol+14,
  author    = {Homsirikamol, Ekawat and Gaj, Kris},
  title     = {Can high-level synthesis compete against a hand-written code in the
               cryptographic domain? {A} case study},
  booktitle = {ReConFig},
  pages     = {1--8},
  publisher = {{IEEE}},
  year      = {2014},
  doi={10.1109/ReConFig.2014.7032504}
}

@INPROCEEDINGS{7818341,
  author={Maxime Pelcat and C\'edric Bourrasset and Luca Maggiani and François Berry},
  booktitle={2016 International Conference on Embedded Computer Systems: Architectures, Modeling and Simulation (SAMOS)},
  title={Design productivity of a high level synthesis compiler versus HDL},
  year={2016},
  volume={},
  number={},
  pages={140-147},
  doi={10.1109/SAMOS.2016.7818341}}

@misc{silexicahlshdl,
author = {Gauthier, Stephane and Wadood, Zubair},
title = {High-Level Synthesis: Can it outperform hand-coded {HDL}?},
note = {White paper},
url = {https://info.silexica.com/high-level-synthesis/1},
year = {2020},
}

@inproceedings{bambu_hls,
  author    = {Christian Pilato and
               Fabrizio Ferrandi},
  title     = {Bambu: {A} modular framework for the high level synthesis of memory-intensive
               applications},
  booktitle = {{FPL}},
  pages     = {1--4},
  publisher = {{IEEE}},
  year      = {2013},
  doi       = {10.1109/FPL.2013.6645550}
}

@inproceedings{nigam20_predic_accel_desig_time_sensit_affin_types,
  author          = {Nigam, Rachit and Atapattu, Sachille and Thomas, Samuel and Li, Zhijing and
                  Bauer, Theodore and Ye, Yuwei and Koti, Apurva and Sampson, Adrian and Zhang,
                  Zhiru},
  title           = {Predictable Accelerator Design with Time-Sensitive Affine Types},
  booktitle       = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design
                  and Implementation},
  year            = 2020,
  pages           = {393-407},
  doi             = {10.1145/3385412.3385974},
  url             = {https://doi.org/10.1145/3385412.3385974},
  address         = {New York, NY, USA},
  isbn            = 9781450376136,
  keywords        = {Affine Type Systems, High-Level Synthesis},
  location        = {London, UK},
  numpages        = 15,
  publisher       = {ACM},
  series          = {PLDI 2020},
}

@inproceedings{bourgeat20_essen_blues,
  author          = {Bourgeat, Thomas and Pit-Claudel, Cl\'{e}ment and Chlipala, Adam and Arvind},
  title           = {The Essence of {Bluespec}: A Core Language for Rule-Based Hardware Design},
  booktitle       = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design
                  and Implementation},
  year            = 2020,
  pages           = {243-257},
  doi             = {10.1145/3385412.3385965},
  url             = {https://doi.org/10.1145/3385412.3385965},
  address         = {New York, NY, USA},
  isbn            = 9781450376136,
  keywords        = {Hardware Description Language, Compiler Correctness, Semantics},
  location        = {London, UK},
  numpages        = 15,
  publisher       = {ACM},
  series          = {PLDI 2020},
}

@inproceedings{yang11_findin_under_bugs_c_compil,
	author = {Yang, Xuejun and Chen, Yang and Eide, Eric and Regehr, John},
	title = {Finding and Understanding Bugs in {C} Compilers},
	booktitle = {Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design
                  and Implementation},
	year = 2011,
	pages = {283-294},
	doi = {10.1145/1993498.1993532},
	url = {https://doi.org/10.1145/1993498.1993532},
	address = {New York, NY, USA},
	isbn = 9781450306638,
	keywords = {random program generation, random testing, automated testing, compiler testing,
                  compiler defect},
	location = {San Jose, California, USA},
	numpages = 12,
	publisher = {ACM},
	series = {PLDI '11}
}

@inproceedings{blazy05_formal_verif_memor_model_c,
	author = "Blazy, Sandrine and Leroy, Xavier",
	title = "Formal Verification of a Memory Model for {C}-Like Imperative
                  Languages",
	tags = {verification},
	booktitle = "Formal Methods and Software Engineering",
	year = 2005,
	pages = "280--299",
	address = "Berlin, Heidelberg",
	editor = "Lau, Kung-Kiu and Banach, Richard",
	isbn = "978-3-540-32250-4",
	publisher = "Springer Berlin Heidelberg",
	doi = {0.1007/11576280_20}
}

@inproceedings{slind08_brief_overv_hol4,
  author          = "Slind, Konrad and Norrish, Michael",
  title           = "A Brief Overview of {HOL4}",
  booktitle       = "Theorem Proving in Higher Order Logics",
  year            = 2008,
  pages           = "28--32",
  address         = "Berlin, Heidelberg",
  editor          = "Mohamed, Otmane Ait and Mu{\~{n}}oz, C{\'e}sar and Tahar, Sofi{\`e}ne",
  isbn            = "978-3-540-71067-7",
  keywords        = {theorem proving;HOL},
  publisher       = "Springer Berlin Heidelberg",
}

@inproceedings{meredith10_veril,
	author = {{Meredith}, P. and {Katelman}, M. and {Meseguer}, J. and {Ro{\c{s}}u} G.},
	title = {A formal executable semantics of {Verilog}},
	tags = {semantics},
	booktitle = {Eighth ACM/IEEE International Conference on Formal Methods and
                  Models for Codesign (MEMOCODE 2010)},
	year = 2010,
	pages = {179-188},
	doi = {10.1109/MEMCOD.2010.5558634},
	url = {https://doi.org/10.1109/MEMCOD.2010.5558634},
	month = {July}
}

@inproceedings{jourdan12_valid_lr_parser,
	author = "Jourdan, Jacques-Henri and Pottier, Fran{\c{c}}ois and
                  Leroy, Xavier",
	title = "Validating LR(1) Parsers",
	booktitle = "Programming Languages and Systems",
	year = 2012,
	pages = "397--416",
	address = "Berlin, Heidelberg",
	editor = "Seidl, Helmut",
	isbn = "978-3-642-28869-2",
	publisher = "Springer Berlin Heidelberg",
	doi = "10.1007/978-3-642-28869-2_20"
}

@inproceedings{zhao12_formal_llvm_inter_repres_verif_progr_trans,
  author    = {Jianzhou Zhao and
               Santosh Nagarakatte and
               Milo M. K. Martin and
               Steve Zdancewic},
  editor    = {John Field and
               Michael Hicks},
  title     = {Formalizing the {LLVM} intermediate representation for verified program
               transformations},
  booktitle = {Proceedings of the 39th {ACM} {SIGPLAN-SIGACT} Symposium on Principles
               of Programming Languages, {POPL} 2012, Philadelphia, Pennsylvania,
               USA, January 22-28, 2012},
  pages     = {427--440},
  publisher = {{ACM}},
  year      = {2012},
  url       = {https://doi.org/10.1145/2103656.2103709},
  doi       = {10.1145/2103656.2103709},
  timestamp = {Thu, 24 Jun 2021 16:19:31 +0200},
  biburl    = {https://dblp.org/rec/conf/popl/ZhaoNMZ12.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}


@inproceedings{hwang99_fsmd,
  author          = {Hwang, Enoch and Vahid, Frank and Hsu, Yu-Chin},
  title           = {FSMD functional partitioning for low power},
  booktitle       = {Proceedings of the conference on Design, automation and test in Europe},
  year            = 1999,
  pages           = {7--es},
  doi = {10.1109/DATE.1999.761092}
}

@inproceedings{loow19_proof_trans_veril_devel_hol,
	author = {L\"{o}\"{o}w, Andreas and Myreen, Magnus O.},
	title = {A Proof-producing Translator for Verilog Development in HOL},
	tags = {hls, semantics},
	booktitle = {Proceedings of the 7th International Workshop on Formal
                  Methods in Software Engineering},
	year = 2019,
	pages = {99--108},
	doi = {10.1109/FormaliSE.2019.00020},
	url = {https://doi.org/10.1109/FormaliSE.2019.00020},
	acmid = 3338828,
	address = {Piscataway, NJ, USA},
	location = {Montreal, Quebec, Canada},
	numpages = 10,
	publisher = {IEEE Press},
	series = {FormaliSE '19}
}

@inproceedings{nikhil04_blues_system_veril,
  author          = {{Nikhil}, R.},
  title           = {Bluespec System Verilog: efficient, correct RTL from high level specifications},
  booktitle       = {Proceedings. Second ACM and IEEE International Conference on Formal Methods and
                  Models for Co-Design, 2004. MEMOCODE '04.},
  year            = 2004,
  pages           = {69-70},
  doi             = {10.1109/MEMCOD.2004.1459818},
  url             = {https://doi.org/10.1109/MEMCOD.2004.1459818},
}

@inproceedings{schuiki20_llhd,
  author          = {Schuiki, Fabian and Kurth, Andreas and Grosser, Tobias and Benini, Luca},
  title           = {LLHD: A Multi-Level Intermediate Representation for Hardware Description
                  Languages},
  booktitle       = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design
                  and Implementation},
  year            = 2020,
  pages           = {258-271},
  doi             = {10.1145/3385412.3386024},
  url             = {https://doi.org/10.1145/3385412.3386024},
  address         = {New York, NY, USA},
  isbn            = 9781450376136,
  location        = {London, UK},
  numpages        = 14,
  publisher       = {ACM},
  series          = {PLDI 2020},
}

@InProceedings{zhu13_mechan_approac_linkin_operat_seman,
  author          = "Zhu, Huibiao and Liu, Peng and He, Jifeng and Qin, Shengchao",
  title           = "Mechanical Approach to Linking Operational Semantics and Algebraic Semantics
                  for Verilog Using Maude",
  booktitle       = "Unifying Theories of Programming",
  year            = 2013,
  pages           = "164--185",
  address         = "Berlin, Heidelberg",
  editor          = "Wolff, Burkhart and Gaudel, Marie-Claude and Feliachi, Abderrahmane",
  isbn            = "978-3-642-35705-3",
  publisher       = "Springer Berlin Heidelberg",
}


@inproceedings{poly_hls_zuo2013,
  title={Improving polyhedral code generation for high-level synthesis},
  author={Zuo, Wei and Li, Peng and Chen, Deming and Pouchet, Louis-No{\"e}l and Zhong, Shunan and Cong, Jason},
  booktitle={2013 International Conference on Hardware/Software Codesign and System Synthesis (CODES+ ISSS)},
  pages={1--10},
  year={2013},
  organization={IEEE},
  doi={https://doi.org/10.1109/CODES-ISSS.2013.6659002}
}

@INPROCEEDINGS{poly_hls_zhao2017,  author={Zhao, Jieru and Feng, Liang and Sinha, Sharad and Zhang, Wei and Liang, Yun and He, Bingsheng},  booktitle={2017 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)},   title={COMBA: A comprehensive model-based analysis framework for high level synthesis of real applications},   year={2017},  volume={},  number={},  pages={430-437},  doi={10.1109/ICCAD.2017.8203809}}

@inproceedings{poly_hls_pouchet2013polyhedral,
  title={Polyhedral-based data reuse optimization for configurable computing},
  author={Pouchet, Louis-Noel and Zhang, Peng and Sadayappan, Ponnuswamy and Cong, Jason},
  booktitle={Proceedings of the ACM/SIGDA international symposium on Field programmable gate arrays},
  pages={29--38},
  year={2013},
  doi={https://doi.org/10.1145/2435264.2435273}
}

@misc{quartus,
  author          = {Intel},
  title           = {{Intel® Quartus® Prime Software Suite}},
  url             = {https://intel.ly/3fpUNhv},
  urldate         = {2020-07-20},
  year            = 2020,
}

@misc{xilinx_vivad_desig_suite,
  author =       {Xilinx},
  title =        {{Vivado Design Suite}},
  url =          {https://bit.ly/2wZAmld},
  urldate =      {2019-01-14},
  year = 2019,
}

@inproceedings{chisel,
  title={{Chisel: Constructing hardware in a Scala embedded language}},
  author={Bachrach, Jonathan and Vo, Huy and Richards, Brian and Lee, Yunsup and Waterman, Andrew and Avi{\v{z}}ienis, Rimas and Wawrzynek, John and Asanovi{\'c}, Krste},
  booktitle={DAC Design Automation Conference 2012},
  pages={1212--1221},
  year={2012},
  organization={IEEE},
  doi={https://doi.org/10.1145/2228360.2228584},
}

@article{aubury1996handel,
  title={Handel-C language reference guide},
  author={Aubury, Matthew and Page, Ian and Randall, Geoff and Saul, Jonathan and Watts, Robin},
  journal={Computing Laboratory. Oxford University, UK},
  year={1996}
}

@inproceedings{clarke03_behav_c_veril,
  author          = {E. {Clarke} and D. {Kroening} and K. {Yorav}},
  title           = {Behavioral consistency of {C} and {Verilog} programs using bounded model checking},
  booktitle       = {Proceedings 2003. Design Automation Conference (IEEE Cat. No.03CH37451)},
  year            = 2003,
  pages           = {368-371},
  doi             = {10.1145/775832.775928},
  url             = {https://doi.org/10.1145/775832.775928},
}

@article{besson18_compc,
	doi = {10.1007/s10817-018-9496-y},
	url = {https://doi.org/10.1007/s10817-018-9496-y},
	year = {2018},
	month = nov,
	publisher = {Springer Science and Business Media {LLC}},
	volume = {63},
	number = {2},
	pages = {369--392},
	author = {Fr{\'{e}}d{\'{e}}ric Besson and Sandrine Blazy and Pierre Wilke},
	title = {{CompCertS}: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics},
	journal = {Journal of Automated Reasoning}
}

@article{sevcik13_compc,
	author = {\v{S}ev\v{c}\'{\i}k, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
	title = {CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency},
	year = {2013},
	issue_date = {June 2013},
	publisher = {ACM},
	address = {New York, NY, USA},
	volume = {60},
	number = {3},
	issn = {0004-5411},
	url = {https://doi.org/10.1145/2487241.2487248},
	doi = {10.1145/2487241.2487248},
	abstract = {In this article, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation on x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behavior of the hardware, the effects of compiler optimization on concurrent code, the need to support high-performance concurrent algorithms, and the desire for a reasonably simple programming model. In turn, this complexity makes verified compilation both essential and challenging.We describe ClightTSO, a concurrent extension of CompCert’s Clight in which the TSO-based memory model of x86 multiprocessors is exposed for high-performance code, and CompCertTSO, a formally verified compiler from ClightTSO to x86 assembly language, building on CompCert. CompCertTSO is verified in Coq: for any well-behaved and successfully compiled ClightTSO source program, any permitted observable behavior of the generated assembly code (if it does not run out of memory) is also possible in the source semantics. We also describe some verified fence-elimination optimizations, integrated into CompCertTSO.},
	journal = {J. ACM},
	month = jun,
	articleno = {22},
	numpages = {50},
	keywords = {semantics, Relaxed memory models, verified compilation}
}

@article{wang20_compc,
	author = {Wang, Yuting and Xu, Xiangzhe and Wilke, Pierre and Shao, Zhong},
	title = {CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files},
	year = {2020},
	issue_date = {November 2020},
	publisher = {ACM},
	address = {New York, NY, USA},
	volume = {4},
	number = {OOPSLA},
	url = {https://doi.org/10.1145/3428265},
	doi = {10.1145/3428265},
	abstract = { We present CompCertELF, the first extension to CompCert that supports verified compilation from C programs all the way to a standard binary file format, i.e., the ELF object format. Previous work on Stack-Aware CompCert provides a verified compilation chain from C programs to assembly programs with a realistic machine memory model. We build CompCertELF by modifying and extending this compilation chain with a verified assembler which further transforms assembly programs into ELF object files.  CompCert supports large-scale verification via verified separate compilation: C modules can be written and compiled separately, and then linked together to get a target program that refines the semantics of the program linked from the source modules. However, verified separate compilation in CompCert only works for compilation to assembly programs, not to object files. For the latter, the main difficulty is to bridge the two different views of linking: one for CompCert's programs that allows arbitrary shuffling of global definitions by linking and the other for object files that treats blocks of encoded definitions as indivisible units.  We propose a lightweight approach that solves the above problem without any modification to CompCert's framework for verified separate compilation: by introducing a notion of syntactical equivalence between programs and proving the commutativity between syntactical equivalence and the two different kinds of linking, we are able to transit from the more abstract linking operation in CompCert to the more concrete one for ELF object files. By applying this approach to CompCertELF, we obtain the first compiler that supports verified separate compilation of C programs into ELF object files. },
	journal = {Proc. ACM Program. Lang.},
	month = nov,
	articleno = {197},
	numpages = {28},
	keywords = {Generation of Object Files, Assembler Verification, Verified Separate Compilation}
}

@inproceedings{10.1145/3437992.3439916,
author = {L\"{o}\"{o}w, Andreas},
title = {Lutsig: A Verified Verilog Compiler for Verified Circuit Development},
year = {2021},
isbn = {9781450382991},
publisher = {ACM},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3437992.3439916},
doi = {10.1145/3437992.3439916},
abstract = {We report on a new verified Verilog compiler called Lutsig. Lutsig currently targets (a class of) FPGAs and is capable of producing technology mapped netlists for FPGAs. We have connected Lutsig to existing Verilog development tools, and in this paper we show how Lutsig, as a consequence of this connection, fits into a hardware development methodology for verified circuits in the HOL4 theorem prover. One important step in the methodology is transporting properties proved at the behavioral Verilog level down to technology mapped netlists, and Lutsig is the component in the methodology that enables such transportation.},
booktitle = {Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs},
pages = {46–60},
numpages = {15},
keywords = {hardware verification, hardware synthesis, compiler verification},
location = {Virtual, Denmark},
series = {CPP 2021}
}

@inproceedings{paulin89_sched_bindin_algor_high_level_synth,
	author = {Paulin, P. G. and Knight, J. P.},
	title = {Scheduling and Binding Algorithms for High-Level Synthesis},
	booktitle = {Proceedings of the 26th ACM/IEEE Design Automation Conference},
	year = 1989,
	pages = {1-6},
	doi = {10.1145/74382.74383},
	url = {https://doi.org/10.1145/74382.74383},
	address = {New York, NY, USA},
	isbn = 0897913108,
	location = {Las Vegas, Nevada, USA},
	numpages = 6,
	publisher = {ACM},
	series = {DAC '89},
}

@inproceedings{venkataramani07_operat,
	keywords = {operation chaining},
	author = {Girish Venkataramani and Goldstein, Seth C.},
	booktitle = {2007 IEEE/ACM International Conference on Computer-Aided Design},
	title = {Operation chaining asynchronous pipelined circuits},
	year = {2007},
	volume = {},
	number = {},
	pages = {442-449},
	doi = {10.1109/ICCAD.2007.4397305}
}

@inproceedings{noronha17_rapid_fpga,
	keywords = {high-level synthesis, FPGA, inlining, compiler optimisation},
	author = {{Noronha}, D. H. and {Pinilla}, J. P. and {Wilton}, S. J. E.},
	booktitle = {2017 International Conference on ReConFigurable Computing and FPGAs (ReConFig)},
	title = {Rapid circuit-specific inlining tuning for FPGA high-level synthesis},
	year = {2017},
	volume = {},
	number = {},
	pages = {1-6},
	doi = {10.1109/RECONFIG.2017.8279807}
}

@misc{yann_herklotz_2021_5093839,
  author       = {Yann Herklotz and
                  James D. Pollard and
                  Nadesh Ramanathan and
                  John Wickerson},
  title        = {Vericert v1.2.1},
  month        = jul,
  year         = 2021,
  publisher    = {Zenodo},
  version      = {v1.2.1},
  doi          = {10.5281/zenodo.5093839},
  url          = {https://doi.org/10.5281/zenodo.5093839}
}

@INPROCEEDINGS{herklotz21_empir_study_reliab_high_level_synth_tools,
	author = {Herklotz, Yann and Du, Zewei and Ramanathan, Nadesh and Wickerson, John},
	booktitle = {2021 IEEE 29th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM)},
	title = {An Empirical Study of the Reliability of High-Level Synthesis Tools},
	year = {2021},
	volume = {},
	number = {},
	pages = {219-223},
	doi = {10.1109/FCCM51124.2021.00034}
}

@article{leroy09_formal_verif_realis_compil,
  author =       {Leroy, Xavier},
  title =        {Formal Verification of a Realistic Compiler},
  journal =      {Commun. ACM},
  volume =       52,
  number =       7,
  pages =        {107-115},
  year =         2009,
  doi =          {10.1145/1538788.1538814},
  address =      {New York, NY, USA},
  issn =         {0001-0782},
  issue_date =   {July 2009},
  month =        jul,
  numpages =     9,
  publisher =    {ACM},
}

@inproceedings{lidbury15_many_core_compil_fuzzin,
  author          = {Lidbury, C. and Lascu, A. and Chong, N. and Donaldson, A. F.},
  title           = {Many-Core Compiler Fuzzing},
  booktitle       = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design
                  and Implementation},
  year            = 2015,
  pages           = {65-76},
  doi             = {10.1145/2737924.2737986},
  address         = {New York, NY, USA},
  isbn            = 9781450334686,
  location        = {Portland, OR, USA},
  numpages        = 12,
  publisher       = {Association for Computing Machinery},
  series          = {PLDI '15},
}

@article{takach16_high_level_synth,
  author          = {A. {Takach}},
  title           = {High-Level Synthesis: Status, Trends, and Future
                  Directions},
  journal         = {IEEE Design Test},
  volume          = {33},
  number          = {3},
  pages           = {116-124},
  year            = {2016},
  doi             = {10.1109/MDAT.2016.2544850},
  ISSN            = {2168-2364},
  month           = {June},
}

@inproceedings{liu16_effic_high_level_synth_desig,
  author          = { {Dong Liu} and B. C. {Schafer}},
  title           = {Efficient and reliable High-Level Synthesis Design Space
                  Explorer for FPGAs},
  booktitle       = {2016 26th International Conference on Field Programmable
                  Logic and Applications (FPL)},
  year            = 2016,
  pages           = {1-8},
  doi             = {10.1109/FPL.2016.7577370},
  ISSN            = {1946-1488},
  month           = {Aug},
}

@article{lahti19_are_we_there_yet,
  author          = {S. {Lahti} and P. {Sj{\"o}vall} and J. {Vanne} and
                  T. D. {H{\"a}m{\"a}l{\"a}inen}},
  title           = {Are We There Yet? a Study on the State of High-Level
                  Synthesis},
  journal         = {IEEE Transactions on Computer-Aided Design of Integrated
                  Circuits and Systems},
  volume          = {38},
  number          = {5},
  pages           = {898-911},
  year            = {2019},
  doi             = {10.1109/TCAD.2018.2834439},
  ISSN            = {1937-4151},
  month           = {May},
}

@misc{mentor20_catap_high_level_synth,
  author          = {Mentor},
  title           = {Catapult High-Level Synthesis},
  url             = {https://bit.ly/32xhADw},
  urldate         = {2020-06-06},
  year            = 2020,
}

@misc{xilinx20_vivad_high_synth,
  author          = {Xilinx},
  title           = {Vivado High-level Synthesis},
  url             = {https://bit.ly/39ereMx},
  urldate         = {2020-07-20},
  year            = 2020,
}

@misc{intel20_sdk_openc_applic,
  author          = {Intel},
  title           = {{SDK} for {OpenCL} Applications},
  url             = {https://intel.ly/30sYHz0},
  urldate         = {2020-07-20},
  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},
  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},
  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 = { Kim, Y. and {Kopuri}, S. and {Mansouri}, N.},
  title = {Automated formal verification of scheduling process using
                  finite state machines with datapath (FSMD)},
  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, C.},
  title =        {A Formal Verification Method of Scheduling in High-level
                  Synthesis},
  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},
  address = {New York, NY, USA},
  isbn = 1595930272,
  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},
  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}
}

@inproceedings{kundu08_valid_high_level_synth,
  author          = "Kundu, Sudipta and Lerner, Sorin and Gupta, Rajesh",
  title           = "Validating High-Level Synthesis",
  booktitle       = "Computer Aided Verification",
  year            = 2008,
  pages           = "459--472",
  address         = "Berlin, Heidelberg",
  editor          = "Gupta, Aarti and Malik, Sharad",
  isbn            = "978-3-540-70545-1",
  publisher       = "Springer",
}

@inproceedings{chapman92_verif_bedroc,
  author          = {R. {Chapman} and G. {Brown} and M. {Leeser}},
  title           = {Verified high-level synthesis in BEDROC},
  booktitle       = {[1992] Proceedings The European Conference on Design Automation},
  year            = 1992,
  pages           = {59--63},
  doi             = {10.1109/EDAC.1992.205894},
  month           = {March},
  publisher       = {IEEE Computer Society},
}

@article{hwang91_formal_approac_to_sched_probl,
  author = {C. -. {Hwang} and J. -. {Lee} and Y. -. {Hsu}},
  title = {A Formal Approach To the Scheduling Problem in High Level
                  Synthesis},
  journal = {IEEE Transactions on Computer-Aided Design of Integrated
                  Circuits and Systems},
  volume = 10,
  number = 4,
  pages = {464-475},
  year = 1991,
  doi = {10.1109/43.75629},
  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",
  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},
  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"
}

@phdthesis{ellis08,
  author = {Ellis, Martin},
  title = {Correct synthesis and integration of compiler-generated function units},
  school = {Newcastle University},
  url = {https://theses.ncl.ac.uk/jspui/handle/10443/828},
  year = {2008},
}

@article{06_ieee_stand_veril_hardw_descr_languag,
  author          = {},
  title           = {IEEE Standard for Verilog Hardware Description Language},
  journal         = {IEEE Std 1364-2005 (Revision of IEEE Std 1364-2001)},
  volume          = {},
  number          = {},
  pages           = {1-590},
  year            = {2006},
  doi             = {10.1109/IEEESTD.2006.99495},
  ISSN            = {},
  month           = {April},
}

@inproceedings{loow19_verif_compil_verif_proces,
  author =       {L\"{o}\"{o}w, Andreas and Kumar, Ramana and Tan, Yong Kiam and
                  Myreen, Magnus O. and Norrish, Michael and Abrahamsson, Oskar
                  and Fox, Anthony},
  title =        {Verified Compilation on a Verified Processor},
  tags =         {verification},
  booktitle =    {Proceedings of the 40th ACM SIGPLAN Conference on Programming
                  Language Design and Implementation},
  year =         2019,
  pages =        {1041--1053},
  doi =          {10.1145/3314221.3314622},
  acmid =        3314622,
  address =      {New York, NY, USA},
  isbn =         {978-1-4503-6712-7},
  keywords =     {compiler verification, hardware verification, program
                  verification, verified stack},
  location =     {Phoenix, AZ, USA},
  numpages =     13,
  publisher =    {ACM},
  series =       {PLDI 2019},
}

@inproceedings{canis11_legup,
  author          = {Andrew Canis and Jongsok Choi and Mark Aldham and Victor Zhang and Ahmed
                  Kammoona and Jason Helge Anderson and Stephen Dean Brown and Tomasz S. Czajkowski},
  title           = {{LegUp}: high-level synthesis for {FPGA}-based processor/accelerator systems},
  booktitle       = {{FPGA}},
  year            = 2011,
  pages           = {33--36},
  publisher       = {{ACM}},
}

@inproceedings{choi18_hls,
  author          = {Young{-}kyu Choi and Jason Cong},
  title           = {{HLS}-based optimization and design space exploration for applications with
                  variable loop bounds},
  booktitle       = {{ICCAD}},
  year            = 2018,
  publisher       = {{ACM}},
}

@article{canis13_legup,
  author          = {Canis, Andrew and Choi, Jongsok and Aldham, Mark and Zhang, Victor and
                  Kammoona, Ahmed and Czajkowski, Tomasz and Brown, Stephen D. and Anderson, Jason
                  H.},
  title           = {Legup: an Open-Source High-Level Synthesis Tool for Fpga-Based
                  Processor/accelerator Systems},
  journal         = {ACM Trans. Embed. Comput. Syst.},
  volume          = {13},
  number          = {2},
  year            = {2013},
  doi             = {10.1145/2514740},
  address         = {New York, NY, USA},
  articleno       = {24},
  issn            = {1539-9087},
  issue_date      = {September 2013},
  keywords        = {High-level synthesis, FPGAs, hardware/software codesign, synthesis,
                  performance, power, field-programmable gate arrays},
  month           = sep,
  numpages        = {27},
  publisher       = {Association for Computing Machinery},
}

@article{coussy09_introd_to_high_level_synth,
  author =       {P. {Coussy} and D. D. {Gajski} and M. {Meredith} and
                  A. {Takach}},
  title =        {An Introduction To High-Level Synthesis},
  tags =         {hls},
  journal =      {IEEE Design Test of Computers},
  volume =       26,
  number =       4,
  pages =        {8-17},
  year =         2009,
  doi =          {10.1109/MDT.2009.69},
  keywords =     {high level synthesis;high-level synthesis;optimized RTL
                  hardware;abstraction level design;HLS techniques;High level
                  synthesis;Assembly;Application software;Circuit
                  simulation;Design methodology;Space exploration;Computer
                  architecture;Design optimization;Hardware design
                  languages;Circuit synthesis;high-level synthesis;RTL
                  abstraction;custom processors;hardware synthesis and
                  verification;architectures;design and test},
  month =        {July},
}

@article{aubury96_handel_c_languag_refer_guide,
  author =       {Aubury, Matthew and Page, Ian and Randall, Geoff and Saul,
                  Jonathan and Watts, Robin},
  title =        {Handel-C Language Reference Guide},
  tags =         {hls},
  journal =      {Computing Laboratory. Oxford University, UK},
  year =         1996,
}

@inproceedings{clarke03_behav_c_veril,
  author          = {E. {Clarke} and D. {Kroening} and K. {Yorav}},
  title           = {Behavioral consistency of C and Verilog programs using bounded model checking},
  booktitle       = {Proceedings 2003. Design Automation Conference (IEEE Cat. No.03CH37451)},
  year            = 2003,
  pages           = {368-371},
  doi             = {10.1145/775832.775928},
  month           = {June},
}

@inproceedings{josipovic18_dynam_sched_high_level_synth,
  author          = {Josipovi\'{c}, Lana and Ghosal, Radhika and Ienne, Paolo},
  title           = {Dynamically Scheduled High-Level Synthesis},
  booktitle       = {Proceedings of the 2018 ACM/SIGDA International Symposium on Field-Programmable
                  Gate Arrays},
  year            = 2018,
  pages           = {127-136},
  doi             = {10.1145/3174243.3174264},
  address         = {New York, NY, USA},
  isbn            = 9781450356145,
  keywords        = {dynamically scheduled circuits, compiler, pipelining, high-level synthesis},
  location        = {Monterey, CALIFORNIA, USA},
  numpages        = 10,
  publisher       = {Association for Computing Machinery},
  series          = {FPGA '18},
}

@inproceedings{cheng20_combin_dynam_static_sched_high_level_synth,
  author          = {Cheng, Jianyi and Josipovic, Lana and Constantinides, George A. and Ienne,
                  Paolo and Wickerson, John},
  title           = {Combining Dynamic \& Static Scheduling in High-Level Synthesis},
  booktitle       = {The 2020 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays},
  year            = 2020,
  pages           = {288-298},
  doi             = {10.1145/3373087.3375297},
  address         = {New York, NY, USA},
  isbn            = 9781450370998,
  keywords        = {high-level synthesis, dynamic scheduling, static analysis},
  location        = {Seaside, CA, USA},
  numpages        = 11,
  publisher       = {Association for Computing Machinery},
  series          = {FPGA '20},
}

@article{josipovic17_out_of_order_load_store,
  author          = {Josipovic, Lana and Brisk, Philip and Ienne, Paolo},
  title           = {An Out-Of-Order Load-Store Queue for Spatial Computing},
  journal         = {ACM Trans. Embed. Comput. Syst.},
  volume          = {16},
  number          = {5s},
  year            = {2017},
  doi             = {10.1145/3126525},
  address         = {New York, NY, USA},
  articleno       = {125},
  issn            = {1539-9087},
  issue_date      = {October 2017},
  keywords        = {Load-store queue, dynamic scheduling, allocation, spatial computing},
  month           = sep,
  numpages        = {19},
  publisher       = {Association for Computing Machinery},
}

@inproceedings{josipovic20_buffer_placem_sizin_high_perfor_dataf_circuit,
  author          = {Josipovi\'{c}, Lana and Sheikhha, Shabnam and Guerrieri, Andrea and Ienne,
                  Paolo and Cortadella, Jordi},
  title           = {Buffer Placement and Sizing for High-Performance Dataflow Circuits},
  booktitle       = {The 2020 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays},
  year            = 2020,
  pages           = {186-196},
  doi             = {10.1145/3373087.3375314},
  address         = {New York, NY, USA},
  isbn            = 9781450370998,
  keywords        = {buffers, high-level synthesis, dataflow circuits, timing optimization},
  location        = {Seaside, CA, USA},
  numpages        = 11,
  publisher       = {Association for Computing Machinery},
  series          = {FPGA '20},
}

@article{leroy09_formal_verif_compil_back_end,
  author          = {Leroy, Xavier},
  title           = {A Formally Verified Compiler Back-End},
  journal         = {Journal of Automated Reasoning},
  volume          = {43},
  number          = {4},
  pages           = {363},
  year            = {2009},
  doi             = {10.1007/s10817-009-9155-4},
  issn            = {1573-0670},
}

@inproceedings{yang11_findin_under_bugs_c_compil,
  author          = {Yang, Xuejun and Chen, Yang and Eide, Eric and Regehr, John},
  title           = {Finding and Understanding Bugs in C Compilers},
  booktitle       = {Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design
                  and Implementation},
  year            = 2011,
  pages           = {283-294},
  doi             = {10.1145/1993498.1993532},
  address         = {New York, NY, USA},
  isbn            = 9781450306638,
  keywords        = {random program generation, compiler defect, automated testing, compiler
                  testing, random testing},
  location        = {San Jose, California, USA},
  numpages        = 12,
  publisher       = {Association for Computing Machinery},
  series          = {PLDI '11},
}

@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},
  doi             = {10.1007/978-3-662-07964-5},
}

@article{bowen98_handel_c_languag_refer_manual,
  author          = {Bowen, Matthew},
  title           = {Handel-C Language Reference Manual},
  journal         = {Embedded Solutions Ltd},
  volume          = {2},
  year            = {1998},
}

@inproceedings{herklotz20_findin_under_bugs_fpga_synth_tools,
  author          = {Yann Herklotz and John Wickerson},
  title           = {Finding and Understanding Bugs in {FPGA} Synthesis Tools},
  booktitle       = {ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays},
  year            = 2020,
  doi             = {10.1145/3373087.3375310},
  isbn            = {978-1-4503-7099-8/20/02},
  keywords        = {automated testing, compiler defect, compiler testing, random program
                  generation, random testing},
  location        = {Seaside, CA, USA},
  numpages        = 11,
}

@misc{xilinx_vivad_desig_suite,
  author =       {Xilinx},
  title =        {{Vivado Design Suite}},
  url =          {https://bit.ly/2wZAmld},
  urldate =      {2019-01-14},
  year = 2019,
}

@misc{intel_intel_quart,
  author =       {Intel},
  title =        {{Intel Quartus}},
  url =
                  {https://intel.ly/2m7wbCs},
  urldate =      {2019-01-14},
  year = 2019,
}

@misc{wolf_yosys_open_synth_suite,
  author =       {Clifford Wolf},
  title =        {{Yosys Open SYnthesis Suite}},
  url =          {https://bit.ly/2kAXg0q},
  urldate =      {2019-01-11},
  year = 2019,
}

@misc{xilinx_xst_synth_overv,
  author =       {Xilinx},
  title =        {{XST} Synthesis Overview},
  url = {https://bit.ly/2lGtkjL},
  urldate =      {2019-01-11},
  year = 2019,
}

@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},
  tags =         {verification},
  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,
  keywords =     {the coq proof assistant, translation validation, verified
                  compilers, scheduling optimizations},
  location =     {San Francisco, California, USA},
  numpages =     11,
  publisher =    {Association for Computing Machinery},
  series =       {POPL '08},
}

@inproceedings{kildall73_unified_approac_global_progr_optim,
  author          = {Kildall, Gary A.},
  title           = {A Unified Approach to Global Program Optimization},
  booktitle       = {Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of
                  Programming Languages},
  year            = 1973,
  pages           = {194-206},
  doi             = {10.1145/512927.512945},
  address         = {New York, NY, USA},
  isbn            = 9781450373494,
  location        = {Boston, Massachusetts},
  numpages        = 13,
  publisher       = {Association for Computing Machinery},
  series          = {POPL '73},
}

@inproceedings{bertot06_struc_approac_provin_compil_optim,
  author          = "Bertot, Yves and Gr{\'e}goire, Benjamin and Leroy, Xavier",
  title           = "A Structured Approach to Proving Compiler Optimizations
                  Based on Dataflow Analysis",
  booktitle       = "Types for Proofs and Programs",
  year            = 2006,
  pages           = "66--81",
  address         = "Berlin, Heidelberg",
  editor          = "Filli{\^a}tre, Jean-Christophe and Paulin-Mohring,
                  Christine and Werner, Benjamin",
  isbn            = "978-3-540-31429-5",
  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},
  tags =         {hls, verification},
  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},
}

@inproceedings{karfa07_hand_verif_high_synth,
  author =       {Karfa, C. and Sarkar, D. and Mandal, C.
                  and Reade, C.},
  title =        {Hand-in-hand Verification of High-level Synthesis},
  tags =         {hls},
  booktitle =    {Proceedings of the 17th ACM Great Lakes Symposium on VLSI},
  year =         2007,
  pages =        {429--434},
  doi =          {10.1145/1228784.1228885},
  acmid =        1228885,
  address =      {New York, NY, USA},
  isbn =         {978-1-59593-605-9},
  location =     {Stresa-Lago Maggiore, Italy},
  numpages =     6,
  publisher =    {ACM},
  series =       {GLSVLSI '07},
}

@article{karfa08_equiv_check_method_sched_verif,
  author =       {C. {Karfa} and D. {Sarkar} and C. {Mandal} and P. {Kumar}},
  title =        {An Equivalence-Checking Method for Scheduling Verification in
                  High-Level Synthesis},
  tags =         {hls, verification},
  journal =      {IEEE Transactions on Computer-Aided Design of Integrated
                  Circuits and Systems},
  volume =       27,
  number =       3,
  pages =        {556-569},
  year =         2008,
  doi =          {10.1109/TCAD.2007.913390},
  ISSN =         {1937-4151},
  month =        {March},
}

@article{karfa10_verif_datap_contr_gener_phase,
  author =       {C. {Karfa} and D. {Sarkar} and C. {Mandal}},
  title =        {Verification of Datapath and Controller Generation Phase in
                  High-Level Synthesis of Digital Circuits},
  tags =         {hls, verification},
  journal =      {IEEE Transactions on Computer-Aided Design of Integrated
                  Circuits and Systems},
  volume =       29,
  number =       3,
  pages =        {479-492},
  year =         2010,
  doi =          {10.1109/TCAD.2009.2035542},
  ISSN =         {1937-4151},
  month =        {March},
}

@article{karfa12_formal_verif_code_motion_techn,
  author =       {Karfa, C. and Mandal, C. and Sarkar, D.},
  title =        {Formal Verification of Code Motion Techniques Using
                  Data-Flow-Driven Equivalence Checking},
  tags =         {hls, verification},
  journal =      {ACM Trans. Des. Autom. Electron. Syst.},
  volume =       17,
  number =       3,
  year =         2012,
  doi =          {10.1145/2209291.2209303},
  address =      {New York, NY, USA},
  articleno =    {Article 30},
  issn =         {1084-4309},
  issue_date =   {June 2012},
  month =        jul,
  numpages =     37,
  publisher =    {Association for Computing Machinery},
}

@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},
  ISSN            = {1557-9999},
  month           = {},
}

@inproceedings{kundu08_valid_high_level_synth,
  author          = "Kundu, Sudipta and Lerner, Sorin and Gupta, Rajesh",
  title           = "Validating High-Level Synthesis",
  booktitle       = "Computer Aided Verification",
  year            = 2008,
  pages           = "459--472",
  address         = "Berlin, Heidelberg",
  editor          = "Gupta, Aarti and Malik, Sharad",
  isbn            = "978-3-540-70545-1",
  publisher       = "Springer Berlin Heidelberg",
}

@inproceedings{kundu07_autom,
  author          = { {Sudipta Kundu} and S. {Lerner} and {Rajesh Gupta}},
  title           = {Automated refinement checking of concurrent systems},
  booktitle       = {2007 IEEE/ACM International Conference on Computer-Aided Design},
  year            = 2007,
  pages           = {318-325},
  doi             = {10.1109/ICCAD.2007.4397284},
  ISSN            = {1558-2434},
  month           = {Nov},
}

@inproceedings{tristan10_simpl_verif_valid_softw_pipel,
	author = {Tristan, Jean-Baptiste and Leroy, Xavier},
	location = {Madrid, Spain},
	publisher = {Association for Computing Machinery},
	url = {https://doi.org/10.1145/1706299.1706311},
	booktitle = {Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
	year = {2010},
	doi = {10.1145/1706299.1706311},
	isbn = {9781605584799},
	keywords = {symbolic execution,coq,verification,translation validation,loop scheduling,compiler optimisation,software pipelining},
	pages = {83--92},
	series = {POPL '10},
	title = {A Simple, Verified Validator for Software Pipelining}
}

@article{barthe14_formal_verif_ssa_based_middl_end_compc,
	abstract = {CompCert is a formally verified compiler that generates compact and efficient code for a large subset of the C language. However, CompCert foregoes using SSA, an intermediate representation employed by many compilers that enables writing simpler, faster optimizers. In fact, it has remained an open problem to verify formally an SSA-based compiler. We report on a formally verified, SSA-based middle-end for CompCert. In addition to providing a formally verified SSA-based middle-end, we address two problems raised by Leroy in [2009]: giving an intuitive formal semantics to SSA, and leveraging its global properties to reason locally about program optimizations.},
	author = {Barthe, Gilles and Demange, Delphine and Pichardie, David},
	location = {New York, NY, USA},
	publisher = {Association for Computing Machinery},
	url = {https://doi.org/10.1145/2579080},
	date = {2014-03},
	doi = {10.1145/2579080},
	issn = {0164-0925},
	journaltitle = {ACM Trans. Program. Lang. Syst.},
	keywords = {CompCertSSA,CompCert,SSA,coq,verification,compiler optimisation},
	number = {1},
	title = {Formal Verification of an SSA-Based Middle-End for CompCert},
	volume = {36}
}

@inproceedings{ottenstein90_progr_depen_web,
	abstract = {The Program Dependence Web (PDW) is a program representation that can be directly interpreted using control-, data-, or demand-driven models of execution. A PDW combines a single-assignment version of the program with explicit operators that manage the flow of data values. The PDW can be viewed as an augmented Program Dependence Graph. Translation to the PDW representation provides the basis for projects to compile Fortran onto dynamic dataflow architectures and simulators. A second application of the PDW is the construction of various compositional semantics for program dependence graphs.},
	author = {Ottenstein, Karl J. and Ballance, Robert A. and MacCabe, Arthur B.},
	location = {White Plains, New York, USA},
	publisher = {Association for Computing Machinery},
	url = {https://doi.org/10.1145/93542.93578},
	booktitle = {Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation},
	date = {1990},
	doi = {10.1145/93542.93578},
	isbn = {0897913647},
	keywords = {gated-SSA,SSA,program dependence graph},
	pages = {257--271},
	series = {PLDI '90},
	title = {The Program Dependence Web: A Representation Supporting Control-, Data-, and Demand-Driven Interpretation of Imperative Languages}
}