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 |
| DOI: | 10.57237/j.cst.2025.04.002 |
View:
Downloads:
Received: 25 August 2025
Accepted: 13 September 2025
Published Online: 16 October 2025
References
| [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. |
Join the Editorial Board
We invite active, qualified and high profile scientists and researchers to join as Editorial Board Members.
Join UsBecome a Reviewer
Scholars with a strong interest in reviewing are invited to join the reviewer panel to ensure the quality of the research to be published.
Join Us