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},
}

@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       = {Association for Computing Machinery},
  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}}
  
@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}
}
  
@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}
}
  
@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}
}
  
@article{greaves_note,
  author    = {David J. Greaves},
  title     = {Research Note: An Open Source Bluespec Compiler},
  journal   = {CoRR},
  volume    = {abs/1905.03746},
  year      = {2019}
}

@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          = {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)},
  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 = {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}
}

@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},
  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 = {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},
}



@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          = {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{choi+18,
  author    = {Young{-}kyu Choi and
               Jason Cong},
  title     = {{HLS}-based optimization and design space exploration for applications
               with variable loop bounds},
  booktitle = {{ICCAD}},
  publisher = {{ACM}},
  year      = {2018}
}

@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    = {Ekawat Homsirikamol and
               Kris Gaj},
  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}
}

@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?},
url = {https://bit.ly/2IDhKBR},
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}
}

@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       = {Association for Computing Machinery},
  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       = {Association for Computing Machinery},
  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 = {Association for Computing Machinery},
	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"
}

@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 = {P. {Meredith} and M. {Katelman} and J. {Meseguer} and
                  G. {Ro{\c{s}}u}},
	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"
}

@article{zhao12_formal_llvm_inter_repres_verif_progr_trans,
  author          = {Zhao, Jianzhou and Nagarakatte, Santosh and Martin, Milo M.K. and Zdancewic,
                  Steve},
  title           = {Formalizing the {LLVM} Intermediate Representation for Verified Program
                  Transformations},
  journal         = {SIGPLAN Not.},
  volume          = {47},
  number          = {1},
  pages           = {427-440},
  year            = {2012},
  doi             = {10.1145/2103621.2103709},
  url             = {https://doi.org/10.1145/2103621.2103709},
  address         = {New York, NY, USA},
  issn            = {0362-1340},
  issue_date      = {January 2012},
  keywords        = {LLVM, memory safety, Coq},
  month           = jan,
  numpages        = {14},
  publisher       = {Association for Computing Machinery},
}

@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},
}

@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          = {R. {Nikhil}},
  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       = {Association for Computing Machinery},
  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}
}

@inproceedings{poly_hls_zhao2017,
  title={COMBA: A comprehensive model-based analysis framework for high level synthesis of real applications},
  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)},
  pages={430--437},
  year={2017},
  organization={IEEE}
}

@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}
}

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