@incollection{wang09_chapt_logic, address = "Boston", author = "Jie-Hong Jiang and Srinivas Devadas", booktitle = "Electronic Design Automation", doi = "10.1016/B978-0-12-374364-0.50013-8", editor = "Laung-Terng Wang and Yao-Wen Chang and Kwang-Ting Cheng", isbn = "978-0-12-374364-0", pages = "299 - 404", publisher = "Morgan Kaufmann", title = "CHAPTER 6 - Logic synthesis in a nutshell", year = 2009, } @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}, acmid = 1993532, address = {New York, NY, USA}, isbn = {978-1-4503-0663-8}, keywords = {automated testing, compiler defect, compiler testing, random program generation, random testing}, location = {San Jose, California, USA}, numpages = 12, publisher = {ACM}, series = {PLDI '11}, } @software{herklotz_verismith, author = {Yann Herklotz and John Wickerson}, title = {Verismith: FPGA '20 Artifact}, month = dec, year = 2019, publisher = {Zenodo}, version = {fpga20}, doi = {10.5281/zenodo.3559802}, url = {https://doi.org/10.5281/zenodo.3559802} } @inproceedings{regehr12_test_reduc_c_compil_bugs, author = {Regehr, John and Chen, Yang and Cuoq, Pascal and Eide, Eric and Ellison, Chucky and Yang, Xuejun}, title = {Test-case Reduction for C Compiler Bugs}, booktitle = {Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation}, year = 2012, pages = {335--346}, doi = {10.1145/2254064.2254104}, url = {https://doi.org/10.1145/2254064.2254104}, acmid = 2254104, address = {New York, NY, USA}, isbn = {978-1-4503-1205-9}, keywords = {automated testing, bug reporting, compiler defect, compiler testing, random testing, test-case minimization}, location = {Beijing, China}, numpages = 12, publisher = {ACM}, series = {PLDI '12}, } @inproceedings{lidbury15_many_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}, url = {https://doi.org/10.1145/2737924.2737986}, acmid = 2737986, address = {New York, NY, USA}, isbn = {978-1-4503-3468-6}, keywords = {Compilers, GPUs, OpenCL, concurrency, metamor- phic testing, random testing}, location = {Portland, OR, USA}, numpages = 12, publisher = {ACM}, series = {PLDI '15}, } @incollection{seligman15_chapt_formal, address = "Boston", author = "Erik Seligman and Tom Schubert and M V Achutha Kiran Kumar", booktitle = "Formal Verification", doi = "10.1016/B978-0-12-800727-3.00008-3", editor = "Erik Seligman and Tom Schubert and M V Achutha Kiran Kumar", isbn = "978-0-12-800727-3", keywords = "Formal Equivalence Verification (FEV), Equivalence Checking (EC), combinational equivalence, sequential equivalence, optimization, synthesis", pages = "225 - 259", publisher = "Morgan Kaufmann", title = "Chapter 8 - Formal equivalence verification", year = 2015, } @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{joyce_dan_joyces, author = {Dan Joyce}, title = {Dan Joyce's 16 bug types only found with gate-level simulation}, url = {https://bit.ly/2nnO22M}, urldate = {2019-08-02}, year = 2019, } @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}, booktitle = {Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation}, series = {PLDI '19}, year = {2019}, isbn = {978-1-4503-6712-7}, location = {Phoenix, AZ, USA}, pages = {1041--1053}, numpages = {13}, doi = {10.1145/3314221.3314622}, acmid = {3314622}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {compiler verification, hardware verification, program verification, verified stack}, } @inproceedings{mcdonald06_logic_equiv_check_arriv_fpga_devel, author = {McDonald, William and Liao, Janny}, title = {Logic Equivalence Checking has Arrived for {FPGA} Developers}, booktitle = {Design and Verification Conference (DVCon)}, year = 2006, month = Jan, } @techreport{05_veril_regis_trans_level_synth, type = {Standard}, key = {IEEE Std 1364.1}, 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}, ISSN = {}, keywords = {IEC Standards;Verilog;Registers}, month = {}, } @article{mckeeman98_differ_testin_softw, author = {McKeeman, William M}, title = {Differential Testing for Software}, journal = {Digital Technical Journal}, volume = 10, number = 1, pages = {100--107}, year = 1998, } @article{zeller02_simpl_isolat_failur_induc_input, author = {A. {Zeller} and R. {Hildebrandt}}, title = {Simplifying and Isolating Failure-Inducing Input}, journal = {IEEE Transactions on Software Engineering}, volume = 28, number = 2, pages = {183-200}, year = 2002, doi = {10.1109/32.988498}, url = {https://doi.org/10.1109/32.988498}, keywords = {program debugging;program testing;online front-ends;test case;delta debugging algorithm;failure-inducing input;Mozilla web browser;user actions;HTML;500 MHz;Vehicle crash testing;Debugging;Automatic testing;HTML;Computer crashes;Computer Society;Prototypes;Databases;Computer bugs;Turning}, month = {Feb}, } @misc{xilinx_vivad_desig_suite, author = {Xilinx}, title = {{Vivado Design Suite}}, url = {https://bit.ly/2wZAmld}, urldate = {2019-01-14}, year = 2019, } @misc{xilinx_xst_synth_overv, author = {Xilinx}, title = {{XST} Synthesis Overview}, url = {https://bit.ly/2lGtkjL}, urldate = {2019-01-11}, year = 2019, } @misc{wolf_vlogh, author = {Clifford Wolf}, title = {{VlogHammer}}, url = {https://bit.ly/2kCxjO3}, urldate = {2019-01-11}, year = 2019, } @article{choi17_kami, author = {Choi, Joonwon and Vijayaraghavan, Muralidaran and Sherman, Benjamin and Chlipala, Adam and Arvind}, title = {Kami: a Platform for High-Level Parametric Hardware Specification and Its Modular Verification}, journal = {Proc. ACM Program. Lang.}, volume = 1, number = {ICFP}, pages = {24:1--24:30}, year = 2017, doi = {10.1145/3110268}, acmid = 3110268, address = {New York, NY, USA}, articleno = 24, issn = {2475-1421}, issue_date = {September 2017}, keywords = {formal verification, hardware, proof assistants}, month = Aug, numpages = 30, publisher = {ACM}, } @misc{intel_intel_quart, author = {Intel}, title = {{Intel Quartus}}, url = {https://intel.ly/2m7wbCs}, urldate = {2019-01-14}, year = 2019, } @misc{cadence_confor_equiv_check, author = {Cadence}, title = {{Conformal Equivalence Checker}}, url = {https://bit.ly/2mkp0aa}, urldate = {2019-01-14}, year = 2019, } @inproceedings{ratchev03_verif_correc_fpga_logic_synth_algor, author = {Ratchev, Boris and Hutton, Mike and Baeckler, Gregg and van Antwerpen, Babette}, title = {Verifying the Correctness of FPGA Logic Synthesis Algorithms}, booktitle = {Proceedings of the 2003 ACM/SIGDA Eleventh International Symposium on Field Programmable Gate Arrays}, year = 2003, pages = {127--135}, doi = {10.1145/611817.611837}, url = {https://doi.org/10.1145/611817.611837}, acmid = 611837, address = {New York, NY, USA}, isbn = {1-58113-651-X}, keywords = {FPGA, programmable logic, synthesis, test, verification}, location = {Monterey, California, USA}, numpages = 9, publisher = {ACM}, series = {FPGA '03}, } @inproceedings{aagaard91, author = {M. {Aagaard} and M. {Leeser}}, title = {A formally verified system for logic synthesis}, booktitle = {[1991 Proceedings] IEEE International Conference on Computer Design: VLSI in Computers and Processors}, year = 1991, pages = {346-350}, doi = {10.1109/ICCD.1991.139915}, keywords = {Boolean functions;formal specification;logic CAD;formally verified system;logic synthesis;correctness;weak division algorithm;Boolean simplification;programming language ML;Nuprl proof development system;errors;implementation;Hardware;Algorithm design and analysis;Registers;Logic programming;Computer languages;Process design;Boolean algebra;High level synthesis;Circuit synthesis;Boolean functions}, month = Oct, } @inproceedings{braibant13_formal_verif_hardw_synth, author = "Braibant, Thomas and Chlipala, Adam", title = "Formal Verification of Hardware Synthesis", booktitle = "Computer Aided Verification", year = 2013, pages = "213--228", abstract = "We report on the implementation of a certified compiler for a high-level hardware description language (HDL) called Fe-Si (FEatherweight SynthesIs). Fe-Si is a simplified version of Bluespec, an HDL based on a notion of guarded atomic actions. Fe-Si is defined as a dependently typed deep embedding in Coq. The target language of the compiler corresponds to a synthesisable subset of Verilog or VHDL. A key aspect of our approach is that input programs to the compiler can be defined and proved correct inside Coq. Then, we use extraction and a Verilog back-end (written in OCaml) to get a certified version of a hardware design.", address = "Berlin, Heidelberg", editor = "Sharygina, Natasha and Veith, Helmut", isbn = "978-3-642-39799-8", publisher = "Springer", } @InProceedings{flor18_pi_ware, author = {Jo{\~a}o Paulo Pizani Flor and Wouter Swierstra and Yorick Sijsling}, title = {{Pi-Ware: Hardware Description and Verification in Agda}}, booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)}, year = 2018, volume = 69, pages = {9:1--9:27}, doi = {10.4230/LIPIcs.TYPES.2015.9}, url = {https://doi.org/10.4230/LIPIcs.TYPES.2015.9}, ISBN = {978-3-95977-030-9}, ISSN = {1868-8969}, URN = {urn:nbn:de:0030-drops-84791}, address = {Dagstuhl, Germany}, annote = {Keywords: dependently typed programming, Agda, EDSL, hardware description languages, functional programming}, editor = {Tarmo Uustalu}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, } @misc{constable86_implem_mathem_nuprl_proof_devel_system, author = {Robert L. Constable and others}, title = {Implementing Mathematics with The Nuprl Proof Development System}, year = 1986, } @misc{mcpeak_delta, author = {Scott McPeak}, title = {{Delta}}, url = {https://bit.ly/2kncyG5}, urldate = {2019-06-11}, year = 2019, } @inproceedings{leroy06_formal_certif_compil_back, 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}, acmid = 1111042, address = {New York, NY, USA}, isbn = {1-59593-027-2}, keywords = {certified compilation, compiler transformations and optimizations, program proof, semantic preservation, the Coq theorem prover}, location = {Charleston, South Carolina, USA}, numpages = 13, publisher = {ACM}, series = {POPL '06}, } @InProceedings{brayton10_abc, author = "Brayton, Robert and Mishchenko, Alan", title = {{ABC}: An academic industrial-strength verification tool}, booktitle = "Computer Aided Verification", year = 2010, pages = "24--40", abstract = "ABC is a public-domain system for logic synthesis and formal verification of binary logic circuits appearing in synchronous hardware designs. ABC combines scalable logic transformations based on And-Inverter Graphs (AIGs), with a variety of innovative algorithms. A focus on the synergy of sequential synthesis and sequential verification leads to improvements in both domains. This paper introduces ABC, motivates its development, and illustrates its use in formal verification.", address = "Berlin, Heidelberg", editor = "Touili, Tayssir and Cook, Byron and Jackson, Paul", isbn = "978-3-642-14295-6", publisher = "Springer", } @InProceedings{moura08_z3, author = "de Moura, Leonardo and Bj{\o}rner, Nikolaj", title = {{Z3}: An Efficient {SMT} Solver}, booktitle = "Tools and Algorithms for the Construction and Analysis of Systems", year = 2008, pages = "337--340", abstract = "Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.", address = "Berlin, Heidelberg", editor = "Ramakrishnan, C. R. and Rehof, Jakob", isbn = "978-3-540-78800-3", publisher = "Springer", } @techreport{barrett17_smt_lib_stand, author = {Clark Barrett and Pascal Fontaine and Cesare Tinelli}, institution = {Department of Computer Science, The University of Iowa}, title = {{The SMT-LIB Standard: Version 2.6}}, year = 2017, } @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)}, pages = {1--560}, year = 2006, doi = {10.1109/IEEESTD.2006.99495}, } @misc{zalewski15_americ, author = {Zalewski, Michal}, title = {American fuzzy lop}, url = {http://lcamtuf.coredump.cx/afl/}, urldate = {2019-01-15}, year = 2015, } @inproceedings{misherghi06_hdd, author = {Misherghi, Ghassan and Su, Zhendong}, title = {HDD: Hierarchical Delta Debugging}, booktitle = {Proceedings of the 28th International Conference on Software Engineering}, year = 2006, pages = {142--151}, doi = {10.1145/1134285.1134307}, url = {https://doi.org/10.1145/1134285.1134307}, acmid = 1134307, address = {New York, NY, USA}, isbn = {1-59593-375-1}, keywords = {automated debugging, delta debugging}, location = {Shanghai, China}, numpages = 10, publisher = {ACM}, series = {ICSE '06}, } @inproceedings{brummayer09_fuzzin_delta_smt_solver, author = {Brummayer, Robert and Biere, Armin}, title = {Fuzzing and Delta-debugging SMT Solvers}, booktitle = {Proceedings of the 7th International Workshop on Satisfiability Modulo Theories}, year = 2009, pages = {1--5}, doi = {10.1145/1670412.1670413}, url = {https://doi.org/10.1145/1670412.1670413}, acmid = 1670413, address = {New York, NY, USA}, isbn = {978-1-60558-484-3}, location = {Montreal, Canada}, numpages = 5, publisher = {ACM}, series = {SMT '09}, } @inproceedings{tao10_autom_testin_approac_compil_based, author = {Q. {Tao} and W. {Wu} and C. {Zhao} and W. {Shen}}, title = {An Automatic Testing Approach for Compiler Based on Metamorphic Testing Technique}, booktitle = {2010 Asia Pacific Software Engineering Conference}, year = 2010, pages = {270-279}, doi = {10.1109/APSEC.2010.39}, url = {https://doi.org/10.1109/APSEC.2010.39}, keywords = {automatic programming;formal verification;program compilers;program testing;software development management;automatic testing;metamorphic testing;compiler testing;equivalence preservation relation;Mettoc;fault detection capability;Testing;Program processors;Semantics;Equations;Grammar;Software systems;compiler;metamorphic testing;test automation;test oracle;test input generation}, month = {Nov}, } @misc{intel_intel_fpga_sdk_openc, author = {Intel}, title = {{Intel} {FPGA} {SDK} for {OpenCL} software technology}, url = {https://intel.ly/2WXoTj8}, urldate = {2019-11-07}, year = 2019, } @misc{williams_icarus_veril, author = {Stephen Williams}, title = {Icarus Verilog}, url = {http://iverilog.icarus.com/}, urldate = {2019-12-14}, year = 2019, }