Improving Property Directed Reachability Using Gate-Level Abstraction
Date Issued
2015
Date
2015
Author(s)
Fan, Kuan
Abstract
Property directed reachability(PDR aka IC3) is an efficient and complete model checking procedure. However, for large problems, the complexities of design logic might hinder PDR from construction of over-approximations, leading to failure to prove them. In this thesis, we present a novel model-checking technique that integrates PDR/IC3 with gate-level, hybrid abstraction, which makes PDR a more scalable model checking method. We implemented the technique in ABC and evaluated it on the HWMCC13, HWMCC14 benchmark suites. Our results show that the proposed method significantly outperforms standard PDR and complements it on a large number of benchmark instances.
Subjects
Property Directed Reachability
Gate-Level Abstraction
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-104-R02943084-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):b5852844b61b48ce4bf8b02ea4ea84b7