Presentation
Leveraging Critical Proof Obligations for Efficient IC3 Verification
DescriptionIC3 and its variants are SAT-based model-checking methods that play a critical role in hardware verification. Efficient management of proof obligations, which track states that need to be proven unreachable, is essential for improving verification performance. This paper presents a novel approach that utilizes Critical Proof Obligations (CPOs) to improve proof obligation management. We propose two techniques, CPO-Driven UNSAT Core Generation and CPO-Driven Proof Obligation Propagation, to promote lemma propagation and frame refinement. Experimental results on HWMCC benchmarks demonstrate significant improvements in CPO discovery and lemma propagation, resulting in notable performance gains.
Event Type
Research Manuscript
TimeWednesday, June 254:15pm - 4:30pm PDT
Location3004, Level 3
EDA
EDA2: Design Verification and Validation