Presentation
A Novel Way to Handle Non-Convergence of Properties in Formal Verification of Digital Systems
DescriptionThe increasing complexity of modern digital designs presents significant challenges for formal verification, particularly when properties fail to converge within practical proof bounds. Non-convergent assertions hinder verification sign-off and limit the ability to expose deep corner-case bugs. This work proposes a contract-based refinement framework to enhance property convergence in the formal verification of complex hardware systems. The methodology employs proof decomposition to identify refinement properties—helper assertions selected through overlapping cones of influence (COI)—which are then composed to strengthen the convergence of the target property. Implemented and evaluated using the Cadence JasperGold formal verification platform, the approach demonstrates improved proof bounds and enhanced bug detection across multiple architectures, including memory controllers and CPUs. Results show that the proposed technique systematically improves convergence for critical properties while maintaining scalability and broad applicability to diverse digital designs.
Event Type
Work in Progress
TimeMonday, July 275:27pm - 5:28pm PDT
LocationExhibit Hall