diff options
Diffstat (limited to 'references.bib')
| -rw-r--r-- | references.bib | 844 |
1 files changed, 844 insertions, 0 deletions
diff --git a/references.bib b/references.bib index 03e91cc..8dd4b3b 100644 --- a/references.bib +++ b/references.bib @@ -1001,3 +1001,847 @@ series = {CPP 2021} 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} +} |