PROGRESS-PDR

| Projektbeschreibung | Software |

PROGESS-PDR is an implementation of the Hardware Model Checking algorithm PDR / IC3 based on IC3ref.

With Proof-Guided Restriction Skipping (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/IC. 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 iden-
tify 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 ap-
proach is able to double the amount of detected deep counterexamples
in comparison to Bounded Model Checking as well as in comparison to
PDR.

We provide all the necessary Tools to reproduce our results from
"Making PROGRESS in Property Directed Reachability" (to be published in VMCAI 2022).

Click here for downloading the reproduction artifact.

The binaries contained in the artifact have been compiled on Ubuntu 20.04 LTS.