TY - GEN
T1 - ChiselFV
T2 - 2023 Design, Automation and Test in Europe Conference and Exhibition, DATE 2023
AU - Xiang, Mufan
AU - Li, Yongjian
AU - Zhao, Yongxin
N1 - Publisher Copyright:
© 2023 EDAA.
PY - 2023
Y1 - 2023
N2 - Modern digital hardware is becoming ever more complex. And agile development, an efficient idea in software development, has been introduced into hardware. Furthermore, as a new hardware construction language, Chisel helps to raise the level of hardware design abstraction with the support of object-oriented and functional programming. Chisel plays a crucial role in future hardware design and open-source hardware development. However, the formal verification for Chisel is still limited. In this paper, we propose ChiselFV, a formal verification framework that has supported detailed formal hardware property descriptions and integrated mature formal hardware verification flows based on SymbiYosys. It builds on top of Chisel and uses Scala to drive the verification process. Thus the framework can be seen as an extension of Chisel. ChiselFV makes it easy to verify hardware designs formally when implementing them in Chisel.
AB - Modern digital hardware is becoming ever more complex. And agile development, an efficient idea in software development, has been introduced into hardware. Furthermore, as a new hardware construction language, Chisel helps to raise the level of hardware design abstraction with the support of object-oriented and functional programming. Chisel plays a crucial role in future hardware design and open-source hardware development. However, the formal verification for Chisel is still limited. In this paper, we propose ChiselFV, a formal verification framework that has supported detailed formal hardware property descriptions and integrated mature formal hardware verification flows based on SymbiYosys. It builds on top of Chisel and uses Scala to drive the verification process. Thus the framework can be seen as an extension of Chisel. ChiselFV makes it easy to verify hardware designs formally when implementing them in Chisel.
KW - Chisel
KW - Formal methods
KW - Hardware description language
KW - Hardware verification
UR - https://www.scopus.com/pages/publications/85162658759
U2 - 10.23919/DATE56975.2023.10137221
DO - 10.23919/DATE56975.2023.10137221
M3 - 会议稿件
AN - SCOPUS:85162658759
T3 - Proceedings -Design, Automation and Test in Europe, DATE
BT - 2023 Design, Automation and Test in Europe Conference and Exhibition, DATE 2023 - Proceedings
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 17 April 2023 through 19 April 2023
ER -