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 -
