Design of SystemVerilog Assertions Hardware Towards Efficient Processor Functional Verification

Zhang Ziqing; Shi Kan; Xu Shuoxiang; Wang Lianghui; Bao Yungang

doi:10.7544/issn1000-1239.202331003

Journal of Computer Research and Development > 2024 > 61(6): 1436-1449. > DOI: 10.7544/issn1000-1239.202331003 CSTR: 32373.14.issn1000-1239.202331003

Zhang Ziqing, Shi Kan, Xu Shuoxiang, Wang Lianghui, Bao Yungang. Design of SystemVerilog Assertions Hardware Towards Efficient Processor Functional Verification[J]. Journal of Computer Research and Development, 2024, 61(6): 1436-1449. DOI: 10.7544/issn1000-1239.202331003

Citation:

PDF (1427 KB)

Design of SystemVerilog Assertions Hardware Towards Efficient Processor Functional Verification

Zhang Ziqing^{1, 2,},
Shi Kan^{1, 2, ,},
Xu Shuoxiang³,
Wang Lianghui⁴,
Bao Yungang^{1, 2}

1.
State Key Lab of Processors (Institute of Computing Technology, Chinese Academy of Sciences), Beijing 100190
2.
School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing 100049
3.
School of Information Science and Technology, Shanghaitech University, Shanghai 201210
4.
School of Computer Science and Technology, University of Science and Technology of China, Hefei 230027

Funds: This work was supported by the National Key Research and development Program of China (2023YFB4405105), the Innovation Project of Institute of Computing Technology, Chinese Academy of Sciences (E261100), and the Major Program of the National Natural Science Foundation of China (62090023).

More Information

Author Bio:
Zhang Ziqing: born in 2002. PhD candidate. His main research interests include FPGA, chip verification, and computer architecture

Shi Kan: born in 1988. PhD, associate professor. His main research interests include agile chip design and verification, FPGA, and computer architecture

Xu Shuoxiang: born in 1999. Master candidate. His main research interests include FPGA, and agile chip design and verification

Wang Lianghui: born in 2000. Master candidate. His main research interests include FPGA, and chip design and verification

Bao Yungang: born in 1980. PhD, professor. His main research interests include data-center architecture, agile design methodology of processor chips, and ecosystem of open-source processor chips
Received Date: December 13, 2023
Revised Date: March 21, 2024
Available Online: April 14, 2024

Graphical Abstract

Abstract

Abstract

Processor verification occupies more than 70% of the time in the processor development flow, so it is necessary to optimize the efficiency of the processor verification process. Traditional verification methods such as software simulation provide various verification mechanisms including assertions to improve the fine-grained visibility and self-checking capability of verification, but software simulation runs slowly and lacks in efficiency. FPGA-based hardware simulation acceleration methods can greatly improve the verification performance, but debugging ability is weak, and it is difficult to locate the specific location and cause of vulnerabilities. In order to solve the above problems of verification efficiency and effectiveness, we propose a method to automatically convert non-synthesizable SystemVerilog Assertion (SVA) into logically equivalent but synthesizable RTL circuits, focusing on assertions, which is a type of non-global modeling of the design, and vertically penetrates through the various levels of abstraction, and complements the verification capability of the global ISA-based model, which can be used to verify the design. Our method complements the global ISA model-based verification capability. At the same time, combined with the advantages of FPGA fine-grained parallelization and high scalability, the verification process of the processor is hardware-accelerated, which improves the development efficiency of the processor. In this paper, we implement an end-to-end hardware assertion platform, integrate a complete toolchain for hardware-enabling SVAs, and count the triggering and coverage of hardware-enabled assertions running on FPGAs. Experiments show that the proposed method achieves more than 20000 times verification efficiency improvement compared with software simulation.
- assertion,
- processor verification,
- hardware simulation,
- FPGA,
- prototyping

FullText(HTML)

References (24)

References

[1]	Witharana H, Lyu Y, Charles S, et al. A survey on assertion-based hardware verification[J]. ACM Computing Surveys, 2022, 54(11s): 1−33
[2]	Xu Yin’an, Yu Zihao, Tang Dan, et al. Towards developing high performance RISC-V processors using Agile methodology[C]//Proc of the 55th IEEE/ACM Int Symp on Microarchitecture (MICRO). Piscataway, NJ: IEEE, 2022: 1178−1199
[3]	GRAPHICS M. The 2020 Wilson research group functional verification study[EB/OL]. (2020-10-10)[2023-12-08]. https://blogs.sw.siemens.com/verificationhorizons/2022/10/10/prologue-the-2022-wilson-research-group-functional-verification-study/
[4]	Shi Kan, Xu Shuaxiang, Diao Yuhan, et al. ENCORE: Efficient architecture verification framework with FPGA acceleration[C]//Proc of the ACM/SIGDA Int Symp on Field Programmable Gate Arrays. New York: ACM, 2023: 209–219
[5]	Xilinx. Vivado Design Suite User Guide: Synthesis (UG901) [EB/OL]. [2023-04-17]. https://docs.xilinx.com/r/en-US/ug901-vivado-synthesis
[6]	Cerny E, Dudani S, Havlicek J, et al. SVA: The Power of Assertions in SystemVerilog[M]. Berlin: Springer, 2015
[7]	Design Automation Standards Committee. IEEE1800-2017 IEEE Standard for SystemVerilog Unified Hardware Design, Specification, and Verification Language Standard IEEE 1800[S].[2023-12-03]. http://www.edastds.org/sv/
[8]	Zhou Zhili, Xie Zheng, Wang Xin’an. Development of verification envioronment for SPI master interface using SystemVerilog[C]//Proc of the 11th Int Conf on Signal Processing. Piscataway, NJ: IEEE, 2012: 2188−2192
[9]	Gurha P, Khandelwal R R. Systemverilog assertion based verification of amba-ahb[C]//Proc of 2016 Int Conf on Micro-Electronics and Telecommunication Engineering (ICMETE). Piscataway, NJ: IEEE, 2016: 641−645
[10]	Tan Zhangxi, Andrew W, Henry C, et al. A case for FAME: FPGA architecture model execution[C]//Proc of the 37th Annual Int Symp on Computer Architecture. New York: ACM, 2010: 290–301
[11]	Krupnova H, Saucier G. FPGA-based emulation: Industrial and custom prototyping solutions[C]//Proc of Int Workshop on Field Programmable Logic and Applications. Berlin: Springer, 2000: 68–77
[12]	Veneris A, Keng B, Safarpour S. From RTL to silicon: The case for automated debug[C]//Proc of the 16th Asia and South Pacific Design Automation Conf (ASP-DAC 2011). Piscataway, NJ: IEEE, 2011: 306−310
[13]	Ma Jiacheng, Zuo Gefei, Loughlin K, et al. Debugging in the brave new world of reconfigurable hardware[C]//Proc of the 27th ACM Int Conf on Architectural Support for Programming Languages and Operating Systems. New York: ACM, 2022: 946−962
[14]	Kim D, Celio C, Karandikar S, et al. DESSERT: Debugging RTL effectively with state snapshotting for error replays across trillions of cycles[C]//Proc of the 28th Int Conf on Field Programmable Logic and Applications (FPL). Piscataway, NJ: IEEE, 2018: 76−764
[15]	Attia S, Betz V. StateMover: Combining simulation and hardware execution for efficient FPGA debugging[C]//Proc of the 2020 ACM/SIGDA Int Symp on Field-Programmable Gate Arrays. New York: ACM, 2020: 175−185
[16]	Pellauer M, Lis M, Baltus D, et al. Synthesis of synchronous assertions with guarded atomic actions[C]//Proc of the 2nd ACM and IEEE Int Conf on Formal Methods and Models for Co-Design (MEMOCODE’05). Piscataway, NJ: IEEE, 2005: 15−24
[17]	Das S, Mohanty R, Dasgupta P, et al. Synthesis of system verilog assertions[C]//Proc of the Design Automation & Test in Europe Conf. Piscataway, NJ: IEEE, 2006, 2: 1−6
[18]	Kastelan I, Krajacevic Z. Synthesizable SystemVerilog assertions as a methodology for SoC[C]//Proc of the 1st IEEE Eastern European Conf on the Engineering of Computer Based Systems. Piscataway, NJ: IEEE, 2009: 120−127
[19]	Slang-SystemVerilog Language Services [EB/OL]. (2015) [2023-12-01]. https://github.com /MikePopoloski/slang
[20]	OSCPU Nutshell(果壳)处理器核 [EB/OL]. [2023-04-17]. https://oscpu. gitbook.io/nutshell/jie-shao/introduction OSCPU. Nutshell processor core[EB/OL]. [2023-04-17]. https://oscpu. gitbook.io/nutshell/jie-shao/introduction (in chinese
[21]	Bachrach J, Vo H, Richards B, et al. Chisel: Constructing hardware in a scala embedded language[C]//Proc of the 49th Annual Design Automation Conf. San Francisco, CA: DAC, 2012: 1216−1225
[22]	Gal-on S, Levy M. Exploring coremark a benchmark maximizing simplicity and efficacy[R]. The Embedded Microprocessor Benchmark Consortium.2012[2023-12-01].https://www.eembc.org/techlit/articles/coremark—whitepaper.pdf
[23]	Weicker R P. Dhrystone: A synthetic systems programming benchmark[J]. Communications of the ACM, 1984, 27(10): 1013−1030 doi: 10.1145/358274.358283
[24]	Yu Zihao, Jiang Yanyan. Benchmarks for CPU correctness and performance testing[EB/OL]. 2021 [2023-12-01]. https://github.com/NJU-ProjectN/am-kernels/tree/master /benchmarks/ microbench

[1]	Wang Yanwei, Li Rengang, Xu Ran, Liu Junkai. Data Center Heterogeneous Acceleration Software-Hardware System-Level Platform Based on Reconfigurable Architecture[J]. Journal of Computer Research and Development, 2025, 62(4): 963-977. DOI: 10.7544/issn1000-1239.202440041
[2]	Qi Le, Chang Yisong, Chen Yuxiao, Zhang Xu, Chen Mingyu, Bao Yungang, Zhang Ke. A System-Level Platform with SoC-FPGA for RISC-V Hardware-Software Integration[J]. Journal of Computer Research and Development, 2023, 60(6): 1204-1215. DOI: 10.7544/issn1000-1239.202330060
[3]	Li Xiaobo, Tang Zhimin, Li Wen. FPGA Verification for Heterogeneous Multi-Core Processor[J]. Journal of Computer Research and Development, 2021, 58(12): 2684-2695. DOI: 10.7544/issn1000-1239.2021.20200289
[4]	Li Junnan, Yang Xiangrui, Sun Zhigang. DrawerPipe: A Reconfigurable Packet Processing Pipeline for FPGA[J]. Journal of Computer Research and Development, 2018, 55(4): 717-728. DOI: 10.7544/issn1000-1239.2018.20170927
[5]	Liu Ke, Cai Xiaojun, Zhang Zhiyong, Zhao Mengying, Jia Zhiping. Design and Verification of NVM Control Architecture Based on High-Performance SOC FPGA Array[J]. Journal of Computer Research and Development, 2018, 55(2): 265-272. DOI: 10.7544/issn1000-1239.2018.20170695
[6]	Zhu Ying, Chen Cheng, Xu Xiaohong, and Li Yanzhe. Design and Implementation of FPGA Verification Platform for Multi-core Processor[J]. Journal of Computer Research and Development, 2014, 51(6): 1295-1303.
[7]	Xu Jianbo, Long Jing, and Peng Li. A High-Capability Scattered IP Watermarking Algorithm in FPGA Design[J]. Journal of Computer Research and Development, 2013, 50(11): 2389-2396.
[8]	He Yi, Ren Ju, Wen Mei, Yang Qianming, Wu Nan, Zhang Chunyuan, and Guo Min. Research on FPGA-Based Paging-Simulation Model for SIMD Architecture[J]. Journal of Computer Research and Development, 2011, 48(1): 9-18.
[9]	Chen Jing, Jiang Junjie, Duncan S. Wong, Deng Xiaotie, Wang Dongsheng. High Performance Architecture for Elliptic Curve Scalar Multiplication Based on FPGA[J]. Journal of Computer Research and Development, 2008, 45(11): 1947-1954.
[10]	Yang Xubing and Chen Songcan. Proximal Support Vector Machine Based on Prototypal Multiclassfication Hyperplanes[J]. Journal of Computer Research and Development, 2006, 43(10): 1700-1705.