@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}, } @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}, } @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}, abstract = {From the Publisher:Synthesis and Optimization of Digital Circuits offers a modern, up-to-date look at computer-aided design (CAD) of very large-scale integration (VLSI) circuits. In particular, this book covers techniques for synthesis and optimization of digital circuits at the architectural and logic levels, i.e., the generation of performance-and/or area-optimal circuits representations from models in hardware description languages. The book provides a thorough explanation of synthesis and optimization algorithms accompanied by a sound mathematical formulation and a unified notation. The text covers the following topics: modern hardware description languages (e.g., VHDL, Verilog); architectural-level synthesis of data flow and control units, including algorithms for scheduling and resource binding; combinational logic optimization algorithms for two-level and multiple-level circuits; sequential logic optimization methods; and library binding techniques, including those applicable to FPGAs.}, 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{intel20_sdk_openc_applic, author = {Intel}, title = {{SDK} for {OpenCL} Applications}, url = {https://intel.ly/30sYHz0}, urldate = {2020-07-20}, year = 2020, } @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", abstract = "This paper presents a formal verification with the Coq proof assistant of a memory model for C-like imperative languages. This model defines the memory layout and the operations that manage the memory. The model has been specified at two levels of abstraction and implemented as part of an ongoing certification in Coq of a moderately-optimising C compiler. Many properties of the memory have been verified in the specification. They facilitate the definition of precise formal semantics of C pointers. A certified OCaml code implementing the memory model has been automatically extracted from the specifications.", address = "Berlin, Heidelberg", editor = "Lau, Kung-Kiu and Banach, Richard", isbn = "978-3-540-32250-4", publisher = "Springer Berlin Heidelberg" }