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

^*Tämän työn vastaava kirjoittaja

Sähkötekniikka

Tutkimustuotos: Artikkeli › Tieteellinen › vertaisarvioitu

22 Sitaatiot (Scopus)

154 Lataukset (Pure)

Abstrakti

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.

Alkuperäiskieli	Englanti
Artikkeli	104737
Sivumäärä	14
Julkaisu	Microprocessors and Microsystems
Vuosikerta	96
Varhainen verkossa julkaisun päivämäärä	2022
DOI - pysyväislinkit	https://doi.org/10.1016/j.micpro.2022.104737
Tila	Julkaistu - helmik. 2023
OKM-julkaisutyyppi	A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä

Rahoitus

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.

YK:n kestävän kehityksen tavoitteet

Tämä tuotos edistää seuraavia kestävän kehityksen tavoitteita:

SDG 7 – Edullinen ja puhdas energia

Julkaisufoorumi-taso

Jufo-taso 1

!!ASJC Scopus subject areas

Software
Hardware and Architecture
Computer Networks and Communications
Artificial Intelligence

Pääsy asiakirjaan

10.1016/j.micpro.2022.104737Lisenssi: CC BY

1-s2.0-S0141933122002666-main-1Final published version, 1,46 MBLisenssi: CC BY

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

Siteeraa tätä

@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

Abstrakti

Rahoitus

YK:n kestävän kehityksen tavoitteet

Julkaisufoorumi-taso

!!ASJC Scopus subject areas

Pääsy asiakirjaan

Sormenjälki

Siteeraa tätä