chisel-uvm.bib

% This file was created with JabRef 2.7.2.
% Encoding: ISO8859_1


@BOOK{strunk:white,
  title = {The Elements of Style},
  publisher = {Allyn and Bacon},
  year = {2000},
  author = {William Strunk Jr. and E. B. White},
  edition = {4th},
  keywords = {scglib}
}

@INPROCEEDINGS{dobisCoverage:ETS22,
	year = {2022-05},
	author = {Dobis, Andrew and Damsgaard, Hans Jakob and Tolotto, Enrico and Hesse, Kasper and Petersen, Tjark and Schoeberl, Martin},
	abstract = {Ever-increasing performance demands are pushing hardware designers towards designing domain-specific accelerators. This has created a demand for improving the overall efficiency of the hardware design and verification cycles. The design efficiency was improved with the introduction of Chisel. However, verification efficiency has yet to be tackled. One method that can increase verification efficiency is the use of various types of coverage measures. In this paper, we present our open-source, coverage-related verification tools targeting digital designs described in Chisel. Specifically, we have created a new method allowing for statement coverage at an intermediate representation of Chisel, and several methods for gathering functional coverage directly on a Chisel description.},
	keywords = {Hardware Verification; Statement Coverage; Functional Coverage; Chisel; Scala},
	language = {en},
	title = {Enabling Coverage-Based Verification in {Chisel}},
	Note = {27th IEEE European Test Symposium (ETS 2022); Conference Location: Barcelona, Spain; Conference Date: May 23-27, 2022; Conference lecture on May 25, 2022.}
}

@INPROCEEDINGS{cocotb:2018,
  title = {Digital/Analog Cosimulation using CocoTB and Xyce.},
  author = {Smith, Andrew Michael and Mayo, Jackson and Armstrong, Robert C. and Schiek, Richard and Sholander, Peter E. and Mei, Ting},
  abstractNote = {In this article, we describe a prototype cosimulation framework using Xyce, GHDL and CocoTB that can be used to analyze digital hardware designs in out-of-nominal environments. We demonstrate current software methods and inspire future work via analysis of an open-source encryption core design. Note that this article is meant as a proof-of-concept to motivate integration of general cosimulation techniques with Xyce, an open-source circuit simulator. ------------------------------------------------},
  doi = {10.2172/1488489},
  url = {https://www.osti.gov/biblio/1488489},
  place = {United States},
  year = {2018},
  month = {12}
} 

@INPROCEEDINGS{paper:example,
  author = {First Author and Martin Schoeberl},
  title = {Real-Time Alternative Bread Baking in {Mendocino}},
  booktitle = {Proceedings of the 113th IEEE Symposium on Real-time Computing
	(ISORC 2189)},
  year = {2189},
  address = {Mendocino, Calofornia},
  month = {February},
  publisher = {IEEE},
  owner = {martin},
}


@book{Sutherland2010,
address = {New York},
author = {Sutherland, Stuart and Davidmann, Simon and Flake, Peter},
edition = {2.},
pages = {418},
publisher = {Springer},
title = {{SystemVerilog for Design}},
year = {2010}
}

@misc{IEEE:18002,
author = {IEEE},
title = {{1800.2-2017 - IEEE Standard for Universal Verification Methodology Language Reference Manual}},
url = {https://ieeexplore.ieee.org/document/7932212},
urldate = {2020-09-04}
}

@Electronic{Snyder2019,
author = {Snyder, Wilson},
pages = {13},
title = {{Verilator: Your Big 4th Simulator: Roadmap}},
howpublished = {\url{https://www.veripool.org/papers/Verilator_Roadmap_CHIPS2019b.pdf}},
year = {2019}
}


@article{Asanovic2016,
abstract = {Rocket Chip is an open-source Sysem-on-Chip design generator that emits synthesizable RTL. It leverages the Chisel hardware construction language to compose a library of sophisticated generators for cores, caches, and interconnects into an integrated SoC. Rocket Chip generates general-purpose processor cores that use the open RISC-V ISA, and provides both an in-order core generator (Rocket) and an out-of-order core generator (BOOM). For SoC designers interested in utilizing heterogeneous specialization for added efficiency gains, Rocket Chip supports the integration of custom accelerators in the form of instruction set extensions, coprocessors, or fully independent novel cores. Rocket Chip has been taped out (manufactured) eleven times, and yielded functional silicon prototypes capable of booting Linux.},
author = {Asanovic, Krste et al.},
doi = {10.1023/A:1010000313106},
file = {:C$\backslash$:/Users/kaspe/Downloads/EECS-2016-17.pdf:pdf},
journal = {EECS Department, University of California, Berkeley, Technical Report},
number = {UCB/EECS-2016-17},
title = {{The Rocket Chip Generator}},
url = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2016/EECS-2016-17.html},
year = {2016}
}

@INPROCEEDINGS{ChiselVerify:dobis2021,  
  author={Dobis, Andrew and Petersen, Tjark and Damsgaard, Hans Jakob and Hesse Rasmussen, Kasper Juul and Tolotto, Enrico and Andersen, Simon Thye and Lin, Richard and Schoeberl, Martin},  
  booktitle={2021 IEEE Nordic Circuits and Systems Conference (NorCAS)},   
  title={ChiselVerify: An Open-Source Hardware Verification Library for {Chisel} and {Scala}},   
  year={2021},  
  volume={},  
  number={},  
  pages={1-7},  
  doi={10.1109/NorCAS53631.2021.9599869}
}

@Inbook{Boule2008,
title="PSL and SVA Assertion Languages",
bookTitle="Generating Hardware Assertion Checkers: For Hardware Verification, Emulation, Post-Fabrication Debugging and On-Line Monitoring",
year="2008",
publisher="Springer Netherlands",
address="Dordrecht",
pages="55--82",
abstract="This chapter presents the two main assertion languages that are covered throughout this book, namely the Property Specification Language (PSL) and SystemVerilog Assertions (SVA). The explanation is made to be somewhat comparative, such that the readers can easily find similarities and differences between the two languages. The basic language explanation presented here will be complemented by the details of their compilation and use in the rest of the book, including Appendix A.",
isbn="978-1-4020-8586-4",
doi="10.1007/978-1-4020-8586-4_4",
url="https://doi.org/10.1007/978-1-4020-8586-4_4"
}

@INPROCEEDINGS{DecisionBitVector:1998,  
  author={Barrett, C.W. and Dill, D.L. and Levitt, J.R.},  
  booktitle={Proceedings 1998 Design and Automation Conference. 35th DAC. (Cat. No.98CH36175)},   
  title={A decision procedure for bit-vector arithmetic},   
  year={1998},  
  pages={522-527},  
  doi={10.1145/277044.277186}
}

@inproceedings{MuellerSchwerhoffSummers16,
  author = {P. M{\"u}ller and M. Schwerhoff and A. J. Summers},
  title = {Viper: A Verification Infrastructure for Permission-Based Reasoning},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  editor = {B. Jobstmann and K. R. M. Leino},
  year = {2016},
  publisher = {Springer-Verlag},
  series = {LNCS},
  pages = {41-62},
  volume = {9583},
}

@InProceedings{Nagini:2018,
author="Eilers, Marco
and M{\"u}ller, Peter",
editor="Chockler, Hana
and Weissenbacher, Georg",
title="Nagini: A Static Verifier for Python",
booktitle="Computer Aided Verification",
year="2018",
publisher="Springer International Publishing",
address="Cham",
pages="596--603",
abstract="We present Nagini, an automated, modular verifier for statically-typed, concurrent Python 3 programs, built on the Viper verification infrastructure. Combining established concepts with new ideas, Nagini can verify memory safety, functional properties, termination, deadlock freedom, and input/output behavior. Our experiments show that Nagini is able to verify non-trivial properties of real-world Python code.",
isbn="978-3-319-96145-3"
}

@article{Dax2010:temporal-logics,
	abstract = {The IEEE standardized Property Specification Language, PSL for short, extends the well-known linear-time temporal logic LTL with so-called semi-extended regular expressions. PSL and the closely related SystemVerilog Assertions, SVA for short, are increasingly used in many phases of the hardware design cycle, from specification to verification. In this article, we extend the common core of these specification languages with past operators. We name this extension PPSL. Although all ω-regular properties are expressible in PSL, SVA, and PPSL, past operators often allow one to specify properties more naturally and concisely. In fact, we show that PPSL is exponentially more succinct than the cores of PSL and SVA. On the star-free properties, PPSL is double exponentially more succinct than LTL. Furthermore, we present a translation of PPSL into language-equivalent nondeterministic B{\"u}chi automata, which is based on novel constructions for 2-way alternating automata. The upper bound on the size of the resulting nondeterministic B{\"u}chi automata obtained by our translation is almost the same as the upper bound for the nondeterministic B{\"u}chi automata obtained from existing translations for PSL and SVA. Consequently, the satisfiability problem and the model-checking problem for PPSL fall into the same complexity classes as the corresponding problems for PSL and SVA.},
	author = {Dax, Christian and Klaedtke, Felix and Lange, Martin},
	da = {2010/06/01},
	date-added = {2021-12-14 17:43:12 +0100},
	date-modified = {2021-12-14 17:43:12 +0100},
	doi = {10.1007/s00236-010-0118-3},
	id = {Dax2010},
	isbn = {1432-0525},
	journal = {Acta Informatica},
	number = {4},
	pages = {251--277},
	title = {On regular temporal logics with past},
	ty = {JOUR},
	url = {https://doi.org/10.1007/s00236-010-0118-3},
	volume = {47},
	year = {2010},
	Bdsk-Url-1 = {https://doi.org/10.1007/s00236-010-0118-3}}


@misc{ghdl, title={GHDL}, howpublished={https://github.com/ghdl/ghdl}, author={Tristan Gingold}}


@MISC{ghdl-yosys-plugin,
	author = {Tristan Gingold},
	title = {ghdl-yosys-plugin},
	howpublished = "\url{https://github.com/ghdl/ghdl-yosys-plugin}"
}
@MISC{vhdl2verilog,
	author = {Simon Andersen},
	title = {VHDL2Verilog},
	howpublished = "\url{https://github.com/chisel-uvm/vhdl2verilog}"
}


%% Artificial intelligence a modern approach
@book{russell2002artificial,
  title={Artificial intelligence: a modern approach},
  author={Russell, Stuart and Norvig, Peter},
  year={2002},
  publisher={Prentice Hall}
}


@MISC{axi4vip,
	author = {Xilinx},
	title = {AXI Verification IP (VIP)},
	howpublished = "\url{https://www.xilinx.com/products/intellectual-property/axi-vip.html}"
}

@INPROCEEDINGS{dobisFCFuzzing:WOSET2021,
	copyright = {In Copyright - Non-Commercial Use Permitted},
	year = {2021-11-04},
	author = {Dobis, Andrew and Petersen, Tjark and Schoeberl, Martin},
	size = {4 p. accepted version},
	abstract = {Ever-increasing performance demands are pushing hardware designers towards designing domain-specific accelerators. This has created a demand for improving the overall efficiency of the hardware design and verification cycles. The design efficiency was improved with the introduction of Chisel. However, verification efficiency has yet to be tackled. One method that can increase verification efficiency is the use of various types of coverage measures. In this paper, we present our open-source, coverage-related verification tools targeting digital designs described in Chisel. Specifically, we have created a new method allowing for statement coverage at an intermediate representation of Chisel, and several methods for gathering functional coverage directly on a Chisel description.},
	keywords = {Verification; Fuzzing; Coverage},
	language = {en},
	address = {Lyngby},
	publisher = {Technical University of Denmark},
	DOI = {10.3929/ethz-b-000539444},
	title = {Towards Functional Coverage-Driven Fuzzing for {Chisel} Designs},
	Note = {Workshop on Open-Source EDA Technology (WOSET 2021); Conference Location: online; Conference Date: November 4, 2021}
}

@INPROCEEDINGS{rfuzz2018,  
  author = {Laeufer, Kevin and Koenig, Jack and Kim, Donggyu and Bachrach, Jonathan and Sen, Koushik},  booktitle = {2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)},   
  title = {RFUZZ: Coverage-Directed Fuzz Testing of RTL on FPGAs},   
  year={2018},  
  volume={},  
  number={},  
  pages={1-8},  
  doi={10.1145/3240765.3240842}
}

@Misc{chisel:formal,
  title        = {{Chisel} Formal Verification},
  howpublished = {\url{https://github.com/tdb-alcorn/chisel-formal}},
  author       = {Tom Alcorn},
  note         = {Accessed: 2021-06-03},
}

@Misc{chisel:kiwi-formal,
  title        = {{Chisel} Formal Verification Extension},
  howpublished = {\url{https://github.com/ekiwi/kiwi-formal}},
  author       = {Kevin Laeufer},
  note         = {Accessed: 2021-06-03},
}

@Misc{chisel:dank-formal,
  title        = {{Chisel} Formal Verification Extension},
  howpublished = {\url{https://github.com/danielkasza/dank-formal}},
  author       = {Daniel Kasza},
  note         = {Accessed: 2021-06-03},
}

@INPROCEEDINGS{riscvdv,  
  author={Ahmadi-Pour, Sallar and Herdt, Vladimir and Drechsler, Rolf},  booktitle={MBMV 2021; 24th Workshop},   
  title={Constrained Random Verification for RISC-V: Overview, Evaluation and Discussion},  
  year={2021}
}

@Inproceedings{highperftestapi:Iyer2022,
  title = {{A High Performance Multi-Threaded RTL Testbench API}},
  author = {Iyer, Vighnesh and Laeufer, Kevin and Sen, Koushik and Nikolić, Borivoje},
  booktitle = {OSCAR22},
  year = {2022}
}

@inproceedings{fault:cav2020,
	abstract = {While hardware generators have drastically improved design productivity, they have introduced new challenges for the task of verification. To effectively cover the functionality of a sophisticated generator, verification engineers require tools that provide the flexibility of metaprogramming. However, flexibility alone is not enough; components must also be portable in order to encourage the proliferation of verification libraries as well as enable new methodologies. This paper introduces fault, a Python embedded hardware verification language that aims to empower design teams to realize the full potential of generators.},
	address = {Cham},
	author = {Truong, Lenny and Herbst, Steven and Setaluri, Rajsekhar and Mann, Makai and Daly, Ross and Zhang, Keyi and Donovick, Caleb and Stanley, Daniel and Horowitz, Mark and Barrett, Clark and Hanrahan, Pat},
	booktitle = {Computer Aided Verification},
	editor = {Lahiri, Shuvendu K. and Wang, Chao},
	isbn = {978-3-030-53288-8},
	pages = {403--414},
	publisher = {Springer International Publishing},
	title = {fault: A Python Embedded Domain-Specific Language for Metaprogramming Portable Hardware Verification Components},
	year = {2020}
}

@INPROCEEDINGS{bluecheck:2015,  
  author={Naylor, Matthew and Moore, Simon},  
  booktitle={2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)},  
  title={A generic synthesisable test bench},   
  year={2015},  
  doi={10.1109/MEMCOD.2015.7340479}
}

@inproceedings{papon2017spinalhdl,
  title={SpinalHDL: An alternative hardware description language},
  author={Papon, C},
  booktitle={FOSDEM},
  year={2017}
}

@inproceedings{ruep2022spinalfuzz,
  title={SpinalFuzz: Coverage-Guided Fuzzing for SpinalHDL Designs},
  author={Ruep, Katharina and Gro{\ss}e, Daniel},
  booktitle={European Test Symposium},
  year={2022}
}

@Misc{microchip,
  title        = {Microchip},
  howpublished = {\url{https://www.microchip.com/}},
  note         = {Accessed: 2021-08-29}
}

@book{spear2008systemverilog,
  title={SystemVerilog for verification: a guide to learning the testbench language features},
  author={Spear, Chris},
  year={2008},
  publisher={Springer Science \& Business Media}
}

@Misc{uvm2015,
  title        = {{Universal Verification Methodology (UVM)} 1.2 User’s Guide},
  howpublished = {\url{https://www.accellera.org/images/downloads/standards/uvm/uvm_users_guide_1.2.pdf}},
  year         = {2015},
  author       = {Accellera Systems Initiative (Accellera)},
}

@Inbook{MehtaCRV2018,
author={Mehta, Ashok B.},
title={Constrained Random Verification (CRV)},
bookTitle={ASIC/SoC Functional Design Verification: A Comprehensive Guide to Technologies and Methodologies},
year={2018},
publisher={Springer International Publishing},
address={Cham},
pages={65--74},
abstract={Constrained Random Verification (CRV) is a methodology that is supported by SystemVerilog which has a built-in constraint solver. This allows you to constraint your stimulus to better target a design function, thereby allowing you to reach your coverage goal faster with accuracy. From that sense, coverage and CRV go hand in hand. You check your coverage and see where the coverage holes are. You then constrain your stimulus to target those holes and improve coverage.},
isbn={978-3-319-59418-7},
doi={10.1007/978-3-319-59418-7_5},
url={https://doi.org/10.1007/978-3-319-59418-7_5}
}

@INPROCEEDINGS{firrtl,
  author={A. {Izraelevitz} and J. {Koenig} and P. {Li} and R. {Lin} and A. {Wang} and A. {Magyar} and D. {Kim} and C. {Schmidt} and C. {Markley} and J. {Lawson} and J. {Bachrach}},
  booktitle={2017 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)}, 
  title={Reusability is FIRRTL ground: Hardware construction languages, compiler frameworks, and transformations}, 
  year={2017},
  volume={},
  number={},
  pages={209-216},
  doi={10.1109/ICCAD.2017.8203780}
}

@conference{jacop2013,
  title = {JaCoP - Java Constraint Programming Solver},
  author = {Krzysztof Kuchcinski and Radoslaw Szymanek},
  year = {2013},
  language = {English},
  note = {CP Solvers: Modeling, Applications, Integration, and Standardization, co-located with the 19th International Conference on Principles and Practice of Constraint Programming ; Conference date: 16-09-2013}
}

@article{DBLP:journals/corr/abs-2102-02308,
  author    = {Timothy Trippel and
               Kang G. Shin and
               Alex Chernyakhovsky and
               Garret Kelly and
               Dominic Rizzo and
               Matthew Hicks},
  title     = {Fuzzing Hardware Like Software},
  journal   = {CoRR},
  volume    = {abs/2102.02308},
  year      = {2021},
  url       = {https://arxiv.org/abs/2102.02308},
  eprinttype = {arXiv},
  eprint    = {2102.02308},
  timestamp = {Tue, 09 Feb 2021 13:35:56 +0100},
  biburl    = {https://dblp.org/rec/journals/corr/abs-2102-02308.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@ELECTRONIC{afl:repo,
  author = {Michal Zalewski},
  title = {American Fuzzy Lop},
  howpublished = {https://github.com/google/AFL}
}

@MISC{afl:fuzzingtechniques,
  author = {Michal Zalewski},
  title = {Binary fuzzing strategies: what works, what doesn't},
  howpublished = {\url{https://lcamtuf.blogspot.com/2014/08/binary-fuzzing-strategies-what-works.html}},
  accessed = {2021.08.27}
}