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