Enhancing Property Directed Reachability Technique through Cube Analysis

Sequential verification is an important practical problem in these years. But it is hard to solved, both model checking and equivalence checking. There are many different techniques solving this problem such as BMC, ITP, and PDR. In all these different techniques, the recently developed PDR works best. Nevertheless, restricted by its NP complexity, many sequential verification problems remain unsolved. In this thesis we focus on how PDR work on these problems, and construct a cube analysis method try to figure out the bottleneck of PDR. Through the analysis we generate three different algorithms to help PDR get better performance. At the end we integrate all three methods and the original PDR in order to seek complete improvement on hardware model checking problem.