Formal Verification-Based Identification of Low-Probability Corner Cases

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. 随着信息快速发展，芯片设计复杂度持续攀升，内部数据通路与控制逻辑高度耦合，片上系统（SoC）集成密度急剧增加。传统验证方法学在扩展、复用及平台标准化等方面存在局限，难以在有限资源内实现对全部芯片行为高效覆盖。尽管已有研究借助大规模自动化工具，通过通用验证方法学（UVM）增强随机测试与回归仿真，仍难以在项目周期内高效覆盖可能引发致命故障的极端边界场景，致使验证存在盲区。本文提出一种动态仿真与形式验证（FPV）相结合的混合验证方法，以PWR模块的关键路径为例进行穷尽分析。首先，基于UVM构建动态仿真平台，通过随机测试对模块主要功能与常规场景进行验证，覆盖率达到94%以上；随后，采用FPV方法编写关键属性断言，对设计进行数学化分析，有效识别出UVM难以覆盖的边界条件，推导出设计中隐含的使用约束，进而揭示出潜在缺陷。实验表明，该方法高效发挥动态仿真与形式验证的互补优势，显著提升验证完备性和效率，为芯片设计可靠性提供有力保障。