| Summary: | 碩士 === 國立臺灣大學 === 電子工程學研究所 === 104 === Property Directed Reachability has always been the most efficient algorithm for the safety property checking problem for its well performance on both safe and unsafe case since its publication in 2011. However, there are still a large number of cases remaining unsolved due to the intrinsic high complexity of model checking problem. Therefore, improving PDR is an important subject and attracts lots of research recently. In this paper, we present three novel approaches that integrate a sequential optimization technique, called temporal decomposition into PDR. We implemented our work in V3 and compared to original PDR in V3 on HWMCC benchmarks. The experimental result shows that the proposed methods solved many originally unsolved cases, and improved unsafe cases by 1.4x in runtimes. It means that these methods can complement original PDR on a large set of benchmarks.
|
|---|
