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.