Verification of Chisel Hardware designs with ChiselVerify

Andrew Dobis; Kevin Laeufer; Hans Jakob Damsgaard; Tjark Petersen; Kasper Juul Hesse Rasmussen; Enrico Tolotto; Simon Thye Andersen; Richard Lin; Martin Schoeberl

doi:10.1016/j.micpro.2022.104737

Verification of Chisel Hardware designs with ChiselVerify

Andrew Dobis^*
, Kevin Laeufer
, Hans Jakob Damsgaard
, Tjark Petersen
, Kasper Juul Hesse Rasmussen
, Enrico Tolotto
, Simon Thye Andersen
, Richard Lin
, Martin Schoeberl

^*Corresponding author for this work

Electrical Engineering

Research output: Contribution to journal › Article › Scientific › peer-review

22 Citations (Scopus)

154 Downloads (Pure)

Abstract

With the current ever-increasing demand for performance, hardware developers find themselves turning ever-more towards the construction of application-specific accelerators to achieve higher performance and lower energy consumption. In order to meet the ever-shortening time constraints, both hardware development and verification tools need to be improved. Chisel, as a hardware construction language, tackles this problem by speeding up the development of digital designs. However, the Chisel infrastructure lacks tools for verification. This paper improves the efficiency of verification in Chisel by proposing methods to support both formal and dynamic verification of digital designs in Scala. It builds on top of ChiselTest, the official testing framework for Chisel. Our work supports functional coverage, constrained random verification, bus functional models, and transaction-level modeling in a verification library named ChiselVerify, while the formal methods are directly integrated into Chisel3.

Original language	English
Article number	104737
Number of pages	14
Journal	Microprocessors and Microsystems
Volume	96
Early online date	2022
DOIs	https://doi.org/10.1016/j.micpro.2022.104737
Publication status	Published - Feb 2023
Publication type	A1 Journal article-refereed

Funding

Hans Jakob Damsgaard carried out his work at the Technical University of Denmark. He is currently with Tampere University as part of the EU Horizon 2020 APROPOS project, MSCA grant agreement No. 956090.We would like to express our thanks to the members of the Chisel community for their inspiration and help. In particular we are grateful to Tom Alcorn, Daniel Kasza, Jack Koenig, Deborah Soung, Chick Markley, Schuyler Eldridge and Jiuyang Liu. We would also like to thank Clair Wolf for all she has done to advance the open-source Verilog ecosystem. Without yosys as an inspiration we would have never been able to conduct this work. This work was supported in part by Semiconductor Research Corporation and through NSF, USA grants CCF-1900968, CCF-1908870, and CNS-1817122. Any opinions, findings, conclusions, or recommendations in this paper are solely those of the authors and do not necessarily reflect the position or the policy of the sponsors. We would like to express our thanks to the members of the Chisel community for their inspiration and help. In particular we are grateful to Tom Alcorn, Daniel Kasza, Jack Koenig, Deborah Soung, Chick Markley, Schuyler Eldridge and Jiuyang Liu. We would also like to thank Clair Wolf for all she has done to advance the open-source Verilog ecosystem. Without yosys as an inspiration we would have never been able to conduct this work. This work was supported in part by Semiconductor Research Corporation and through NSF, USA grants CCF-1900968 , CCF-1908870 , and CNS-1817122 . Any opinions, findings, conclusions, or recommendations in this paper are solely those of the authors and do not necessarily reflect the position or the policy of the sponsors.

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 7 Affordable and Clean Energy

Keywords

Chisel
Digital design
Scala
Verification

Publication forum classification

Publication forum level 1

ASJC Scopus subject areas

Software
Hardware and Architecture
Computer Networks and Communications
Artificial Intelligence

Access to Document

10.1016/j.micpro.2022.104737Licence: CC BY

1-s2.0-S0141933122002666-main-1Final published version, 1.46 MBLicence: CC BY

https://urn.fi/URN:NBN:fi:tuni-202302022014Licence: CC BY

Cite this

@article{ab276be90264498d9836cc4ab652649a,

title = "Verification of Chisel Hardware designs with ChiselVerify",

abstract = "With the current ever-increasing demand for performance, hardware developers find themselves turning ever-more towards the construction of application-specific accelerators to achieve higher performance and lower energy consumption. In order to meet the ever-shortening time constraints, both hardware development and verification tools need to be improved. Chisel, as a hardware construction language, tackles this problem by speeding up the development of digital designs. However, the Chisel infrastructure lacks tools for verification. This paper improves the efficiency of verification in Chisel by proposing methods to support both formal and dynamic verification of digital designs in Scala. It builds on top of ChiselTest, the official testing framework for Chisel. Our work supports functional coverage, constrained random verification, bus functional models, and transaction-level modeling in a verification library named ChiselVerify, while the formal methods are directly integrated into Chisel3.",

keywords = "Chisel, Digital design, Scala, Verification",

author = "Andrew Dobis and Kevin Laeufer and Damsgaard, \{Hans Jakob\} and Tjark Petersen and Rasmussen, \{Kasper Juul Hesse\} and Enrico Tolotto and Andersen, \{Simon Thye\} and Richard Lin and Martin Schoeberl",

note = "Funding Information: Hans Jakob Damsgaard carried out his work at the Technical University of Denmark. He is currently with Tampere University as part of the EU Horizon 2020 APROPOS project, MSCA grant agreement No. 956090.We would like to express our thanks to the members of the Chisel community for their inspiration and help. In particular we are grateful to Tom Alcorn, Daniel Kasza, Jack Koenig, Deborah Soung, Chick Markley, Schuyler Eldridge and Jiuyang Liu. We would also like to thank Clair Wolf for all she has done to advance the open-source Verilog ecosystem. Without yosys as an inspiration we would have never been able to conduct this work. This work was supported in part by Semiconductor Research Corporation and through NSF, USA grants CCF-1900968, CCF-1908870, and CNS-1817122. Any opinions, findings, conclusions, or recommendations in this paper are solely those of the authors and do not necessarily reflect the position or the policy of the sponsors. Funding Information: We would like to express our thanks to the members of the Chisel community for their inspiration and help. In particular we are grateful to Tom Alcorn, Daniel Kasza, Jack Koenig, Deborah Soung, Chick Markley, Schuyler Eldridge and Jiuyang Liu. We would also like to thank Clair Wolf for all she has done to advance the open-source Verilog ecosystem. Without yosys as an inspiration we would have never been able to conduct this work. This work was supported in part by Semiconductor Research Corporation and through NSF, USA grants CCF-1900968 , CCF-1908870 , and CNS-1817122 . Any opinions, findings, conclusions, or recommendations in this paper are solely those of the authors and do not necessarily reflect the position or the policy of the sponsors. Publisher Copyright: {\textcopyright} 2022 The Authors",

year = "2023",

month = feb,

doi = "10.1016/j.micpro.2022.104737",

language = "English",

volume = "96",

journal = "Microprocessors and Microsystems",

issn = "0141-9331",

publisher = "Elsevier",

}

TY - JOUR

T1 - Verification of Chisel Hardware designs with ChiselVerify

AU - Dobis, Andrew

AU - Laeufer, Kevin

AU - Damsgaard, Hans Jakob

AU - Petersen, Tjark

AU - Rasmussen, Kasper Juul Hesse

AU - Tolotto, Enrico

AU - Andersen, Simon Thye

AU - Lin, Richard

AU - Schoeberl, Martin

N1 - Funding Information: Hans Jakob Damsgaard carried out his work at the Technical University of Denmark. He is currently with Tampere University as part of the EU Horizon 2020 APROPOS project, MSCA grant agreement No. 956090.We would like to express our thanks to the members of the Chisel community for their inspiration and help. In particular we are grateful to Tom Alcorn, Daniel Kasza, Jack Koenig, Deborah Soung, Chick Markley, Schuyler Eldridge and Jiuyang Liu. We would also like to thank Clair Wolf for all she has done to advance the open-source Verilog ecosystem. Without yosys as an inspiration we would have never been able to conduct this work. This work was supported in part by Semiconductor Research Corporation and through NSF, USA grants CCF-1900968, CCF-1908870, and CNS-1817122. Any opinions, findings, conclusions, or recommendations in this paper are solely those of the authors and do not necessarily reflect the position or the policy of the sponsors. Funding Information: We would like to express our thanks to the members of the Chisel community for their inspiration and help. In particular we are grateful to Tom Alcorn, Daniel Kasza, Jack Koenig, Deborah Soung, Chick Markley, Schuyler Eldridge and Jiuyang Liu. We would also like to thank Clair Wolf for all she has done to advance the open-source Verilog ecosystem. Without yosys as an inspiration we would have never been able to conduct this work. This work was supported in part by Semiconductor Research Corporation and through NSF, USA grants CCF-1900968 , CCF-1908870 , and CNS-1817122 . Any opinions, findings, conclusions, or recommendations in this paper are solely those of the authors and do not necessarily reflect the position or the policy of the sponsors. Publisher Copyright: © 2022 The Authors

PY - 2023/2

Y1 - 2023/2

N2 - With the current ever-increasing demand for performance, hardware developers find themselves turning ever-more towards the construction of application-specific accelerators to achieve higher performance and lower energy consumption. In order to meet the ever-shortening time constraints, both hardware development and verification tools need to be improved. Chisel, as a hardware construction language, tackles this problem by speeding up the development of digital designs. However, the Chisel infrastructure lacks tools for verification. This paper improves the efficiency of verification in Chisel by proposing methods to support both formal and dynamic verification of digital designs in Scala. It builds on top of ChiselTest, the official testing framework for Chisel. Our work supports functional coverage, constrained random verification, bus functional models, and transaction-level modeling in a verification library named ChiselVerify, while the formal methods are directly integrated into Chisel3.

AB - With the current ever-increasing demand for performance, hardware developers find themselves turning ever-more towards the construction of application-specific accelerators to achieve higher performance and lower energy consumption. In order to meet the ever-shortening time constraints, both hardware development and verification tools need to be improved. Chisel, as a hardware construction language, tackles this problem by speeding up the development of digital designs. However, the Chisel infrastructure lacks tools for verification. This paper improves the efficiency of verification in Chisel by proposing methods to support both formal and dynamic verification of digital designs in Scala. It builds on top of ChiselTest, the official testing framework for Chisel. Our work supports functional coverage, constrained random verification, bus functional models, and transaction-level modeling in a verification library named ChiselVerify, while the formal methods are directly integrated into Chisel3.

KW - Chisel

KW - Digital design

KW - Scala

KW - Verification

U2 - 10.1016/j.micpro.2022.104737

DO - 10.1016/j.micpro.2022.104737

M3 - Article

AN - SCOPUS:85145606559

SN - 0141-9331

VL - 96

JO - Microprocessors and Microsystems

JF - Microprocessors and Microsystems

M1 - 104737

ER -

Verification of Chisel Hardware designs with ChiselVerify

Abstract

Funding

UN SDGs

Keywords

Publication forum classification

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this