摘 要：验证是 FPGA 开发流程和 IC 芯片设计流程中不可或缺的环节，文章首先分析了当前数字仿真验证用例设计无法跨越的不完备性和不充分性，并详细探讨了为什么功能仿真会错过一些角落案例场景。在此基础上，介绍了形式化验证中 FPGA的主要应用场景以及硬件逻辑功能验证语言 SVA，并以实际工程案例阐述了基于 SVA 的形式化验证方法如何更好地在验证关键设计中发挥作用。
关键词：FPGA；形式化验证；SVA
DOI:10.19850/j.cnki.2096-4706.2021.19.007
中图分类号：TN79+1 文献标识码：A 文章编号：2096-4706（2021）19-0030-04
Research on Formal Verification Technology of FPGA Software
CHEN Junhua, SHI Hao, CHAI Jinbao
(Software Test and Evaluation Center of CASIC Fourth Academy (Wuhan), Wuhan 430000, China)
Abstract: Verification is an indispensable link in the FPGA development process and IC chip design process. Firstly, this paper analyzes the incompleteness and inadequacy that the current digital simulation verification use case design cannot leap over, and discusses in detail why functional simulation misses some corner case scenarios. On this basis, this paper introduces the main application scenarios of FPGA in formal verification and the hardware logic function verification language SVA, and expounds how the formal verification method based on SVA better play a role in verifying the key design with a practical engineering case.
Keywords: FPGA; formal verification; SVA
参考文献：
[1] 刘斌 . 芯片验证漫游指南 [M]. 北京：电子工业出版社，2018.
[ 2 ] BERGERON J ， CUERY E ， HUNTER A ， e t al.SystemVerilog 验证方法学 [M]. 夏宇闻，杨雷，陈先勇，等译 . 北京： 北京航空航天大学出版社，2007.
[3] 陈先勇，徐伟俊，杨鑫，等 . SystemVerilog 断言及其应用 [J]. 中国集成电路，2007（9）：19-24.
[4] 斯皮尔 .SystemVerilog 验证测试平台编写指南 [M]. 张春，麦宋平，赵益新，译 . 北京：科学出版社，2019.
[5] VIJAYARAGHAVAN S，RAMANATHAN M. System Verilog Assertions 应用指南 [M]. 陈俊杰，等译 . 北京：清华大学出版社， 2006.
作者简介：陈军花（1990.03—），女，汉族，湖北黄冈人，中级工程师，毕业于南京航空航天大学，硕士研究生，研究方向： FPGA 和 IC 验证测试；石颢（1980.11—），男，汉族，重庆人， 高级工程师，毕业于重庆大学，硕士研究生，研究方向：FPGA 和 IC 验证测试；柴金宝（1993.09—），男，汉族，黑龙江哈尔滨 人，初级工程师，毕业于南京理工大学，硕士研究生，研究方向： FPGA 和 IC 验证测试。