基于形式验证的低概率边界条件识别方法研究
1. 电信科学技术研究院, 北京 100083
2. 宸芯科技股份有限公司, 北京 100083
| 摘 要： | 随着信息快速发展，芯片设计复杂度持续攀升，内部数据通路与控制逻辑高度耦合，片上系统（SoC）集成密度急剧增加。传统验证方法学在扩展、复用及平台标准化等方面存在局限，难以在有限资源内实现对全部芯片行为高效覆盖。尽管已有研究借助大规模自动化工具，通过通用验证方法学（UVM）增强随机测试与回归仿真，仍难以在项目周期内高效覆盖可能引发致命故障的极端边界场景，致使验证存在盲区。本文提出一种动态仿真与形式验证（FPV）相结合的混合验证方法，以PWR模块的关键路径为例进行穷尽分析。首先，基于UVM构建动态仿真平台，通过随机测试对模块主要功能与常规场景进行验证，覆盖率达到94%以上；随后，采用FPV方法编写关键属性断言，对设计进行数学化分析，有效识别出UVM难以覆盖的边界条件，推导出设计中隐含的使用约束，进而揭示出潜在缺陷。实验表明，该方法高效发挥动态仿真与形式验证的互补优势，显著提升验证完备性和效率，为芯片设计可靠性提供有力保障。 |
| 关 键 词： | 形式验证; 边界条件; SoC验证; 属性验证; FPV; UVM |
| DOI： | 10.57237/j.cst.2025.04.002 |
View:
Downloads:
收稿日期: 2025-08-25
接受日期: 2025-09-13
在线出版日期: 2025-10-16
Formal Verification-Based Identification of Low-Probability Corner Cases
1. China Academy of Telecommunication Technology, Beijing 100083, China
2. Morningcore Holding Co., Ltd., Beijing 100083, China
| Abstract: | With the rapid development of information technology, the complexity of chip design continues to increase, with highly coupled internal data paths and control logic as well as sharply rising integration density in System-on-Chip (SoC), which impose greater demands on verification methodologies. Traditional approaches show inherent limitations in scalability, reusability, and platform standardization, making it difficult to efficiently achieve comprehensive coverage of all chip behaviors within limited resources. Although large-scale automated tools and the Universal Verification Methodology (UVM) have been widely adopted to enhance random testing and regression simulation, they still fail to efficiently capture extreme boundary scenarios that may lead to fatal failures, leaving potential blind spots in verification. To address this challenge, this paper proposes a hybrid verification method that combines dynamic simulation with Formal Property Verification (FPV), using the critical path of the PWR module as an example for analysis. A UVM-based verification platform is constructed to execute randomized test cases on key functions and typical scenarios, achieving more than 94% coverage in line, toggle, branch, and functional metrics, which confirms the completeness of basic functional validation but also indicates the difficulty of covering corner cases. Then, FPV is applied by formulating property assertions, such as state transition constraints, and performing exhaustive mathematical analysis of the Register Transfer Level (RTL) design, thereby detecting extremely low-probability boundary conditions and revealing implicit usage restrictions in design logic. By incorporating these restrictions into formal constraints, the verification results are corrected and latent design defects are confirmed. This hybrid method effectively leverages the complementary strengths of UVM dynamic simulation and FPV formal analysis, significantly improving the detection capability of corner cases, enhancing verification completeness and efficiency, and strengthening design reliability, while also providing a theoretical basis and practical reference for optimizing verification strategies in future SoC design projects. |
| Keywords: | Formal Verification; Corner Case; SoC Verification; Property Verification; FPV; UVM |
参考文献
| [1] | 田劲, 王小力. 基于UVM验证方法学的AES模块级验证 [J]. 微电子学与计算机, 2012, 29(08): 86-90. |
| [2] | 曹庆年, 姚翌, 孟开元. 数字电路芯片验证方法研究综述 [J]. 工业控制计算机, 2024, 37(02): 53-55+83. |
| [3] | 李晨思. 基于UVM的AMBA总线桥及通信接口的验证研究 [D]. 西安: 西安建筑科技大学, 2024. |
| [4] | 李子豪. 基于UVM的USB接口IP核验证平台的设计与应用 [D]. 北京: 北方工业大学, 2024. |
| [5] | 李智超, 刘冬培, 吕平, 等. 基于UVM的可重用协议转换模块验证平台设计 [J]. 信息工程大学学报, 2024, 25(06): 653-659. |
| [6] | 王鑫, 张畅. 基于UVM的片上网络验证平台设计 [J]. 计算机测量与控制, 2025, 33(03): 323-329. |
| [7] | 徐晓贝. 基于UVM和Python的RSFEC验证平台 [J]. 中国信息界, 2025, (05): 223-225. |
| [8] | 彭莉, 王定. DeepSeek加速GPU芯片验证覆盖率收敛技术的应用 [J]. 集成电路应用, 2025, 42(05): 62-63. |
| [9] | SABRY A, SAID A, MOHAMMAD A, et al. [ART]: A Novel Approach to Automated UVM Testbench Generation [C]//2024 International Conference on Microelectronics (ICM). IEEE, 2024: 1-5. |
| [10] | OWEN A. Corner Case Coverage Challenges in Stress Testing DDR Controllers under Variable Load Conditions [J]. 2024. |
| [11] | 邵奇. 形式验证在数据路径验证中的应用研究 [D]. 北京: 北方工业大学, 2023. |
| [12] | 李旭元. 基于UVM平台的DMA控制器验证 [D]. 沈阳: 辽宁大学, 2024. https://doi.org/10.27209/d.cnki.glniu.2024.002066 |
| [13] | 黄迪. 面向数据库管理系统的形式化验证 [J]. 信息记录材料, 2025, 26(07): 155-157. |
| [14] | GRIMM T, LETTNIN D, HÜBNER M. A survey on formal verification techniques for safety-critical systems-on-chip [J]. Electronics, 2018, 7(6): 81. |
| [15] | 张牧翔. 适用于AHB Matrix的形式验证优化技术研究 [D]. 西安: 西安电子科技大学, 2023. |
| [16] | 维加亚拉哈文. SystemVerilog Assertions 应用指南 [M]. 北京: 清华大学出版社, 2006. |
