With (PROGRESS) we present a fully automatic and complete approach for Hardware Model Checking under restrictions. We use the PROGRESS approach in the context of PDR/IC3 [9, 18]. Our implementation of PDR/IC3 restricts input signals as well as state bits of a circuit to constants in order to quickly explore long execution paths of the design. We are able to identify spurious proofs of safety along the way and exploit information from these proofs to guide the relaxation of the restrictions. Hence, we greatly improve the capability of PDR to find counterexamples, especially with long error paths. In experiments with HWMCC benchmarks our approach is able to double the amount of detected deep counterexamples in comparison to Bounded Model Checking as well as in comparison to PDR.
CITATION STYLE
Seufert, T., Scholl, C., Chandrasekharan, A., Reimer, S., & Welp, T. (2022). Making PROGRESS in Property Directed Reachability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 13182 LNCS, pp. 355–377). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-94583-1_18
Mendeley helps you to discover research relevant for your work.