面向处理器功能验证的硬件化System Verilog断言设计  

Design of SystemVerilog Assertions Hardware Towards Efficient Processor Functional Verification

作　　者：张子卿 石侃 徐烁翔 王梁辉 包云岗[1,2] Zhang Ziqing;Shi Kan;Xu Shuoxiang;Wang Lianghui;Bao Yungang(State Key Lab of Processors(Institute of Computing Technology,Chinese Academy of Sciences),Beijing 100190;School of Computer Science and Technology,University of Chinese Academy of Sciences,Beijing 100049;School of Information Science and Technology,Shanghaitech University,Shanghai 201210;School of Computer Science and Technology,University of Science and Technology of China,Hefei 230027)

机构地区：[1]处理器芯片全国重点实验室(中国科学院计算技术研究所),北京100190 [2]中国科学院大学计算机科学与技术学院,北京100049 [3]上海科技大学信息科学与技术学院,上海201210 [4]中国科学技术大学计算机科学与技术学院,合肥230027

出　　处：《计算机研究与发展》2024年第6期1436-1449,共14页Journal of Computer Research and Development

基　　金：国家重点研发计划项目(2023YFB4405105);中国科学院计算技术研究所创新项目(E261100);国家自然科学基金重大项目(62090023)。

摘　　要：功能验证在处理器芯片开发流程中所占用的时间超过70%,因此优化提升功能验证环节的效率非常必要.软件仿真等传统验证方法提供了包括断言等多种验证机制,以提升验证的细粒度可见性和自检查能力,但是软件仿真运行速度较慢,在高效性方面有明显不足.基于FPGA的硬件原型验证方法能极大地加速验证性能,但其调试能力较弱,虽能快速发现漏洞,但难以定位漏洞出现的具体位置和根本原因,存在有效性不足难题.为同时解决上述功能验证有效性与高效性的问题,提出一种将不可综合的断言语言SVA(SystemVerilog Assertion)自动转换成逻辑等效但可综合的RTL电路的方法,聚焦于断言这一类对设计进行非全局建模、纵向贯穿各抽象层级的验证方式,对基于全局指令集架构(instruction set architecture,ISA)模型的验证能力进行补足.同时,结合FPGA细粒度并行化、高度可扩展的优势,对处理器的验证过程进行硬件加速,提升了处理器的开发效率.实现了一个端到端的硬件断言平台,集成对SVA进行硬件化的完整工具链,并统计运行在FPGA上的硬件化断言的触发和覆盖率情况.实验表明,和软件仿真相比,所提方法能取得超过2万倍的验证效率提升.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.

关 键 词：断言 处理器验证 硬件仿真 现场可编程逻辑门阵列 原型验证 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]