PDR bit-level symbolic model checking algorithm

I recommend this paper from UC Berkeley about implementing a sequential model checking algorithm called property directed reachability (PDR), discovered by Aaron Bradley, that is stronger than interpolation-based model checking on industrial problems. According to Niklas Een, Alan Mishchenko, and Robert Brayton

In this paper, we explore PDR and try to understand the reason for its effectiveness. We propose a number of changes to the algorithm to improve its performance and to simplify its implementation. In particular:

  • We achieve a significant speedup by using three-valued simulation to reduce the burden on the SAT-solver.
  • We eliminate a tedious and error-prone special-case handling of counterexamples of length 0 or 1.
  • We show experimentally that two elements of the original algorithm give no speedup: (i) variable activity and (ii) cube generalization beyond non-inductive regions.
  • We separate the main algorithm from the handling of SAT queries through a clean interface. This separation reduces the overall complexity.
  • We refute some potential improvements experimentally.
  • We present detailed pseudo-code to fully document our implementation.

Update: Aaron Bradley, the discoverer of the algorithm, added commentary below. I’m copying up here so it doesn’t get overlooked. I’m not going to put it in block quotes, because it makes it harder to read.

Aaron Bradley writes:

I think the primary contribution of this paper is this point:

We achieve a significant speedup by using three-valued simulation to reduce the burden on the SAT-solver.

It provides a faster method of generating inductive clauses, which refines the method of

Aaron R. Bradley and Zohar Manna, “Checking Safety by Inductive Generalization of Counterexamples to Induction”, in Proc. Formal Methods in Computer Aided Design (FMCAD), November 2007. [pdf]

The trade-off is that, if I understand correctly from a discussion with Niklas, the transition relation must be in function form. I’ve found it useful for finding counterexamples on some systems to invert the TR and swap the initial and error conditions, but then the three-valued method apparently wouldn’t work.

Regarding the other points:

We show experimentally that two elements of the original algorithm give no speedup: (i) variable activity and (ii) cube generalization beyond non-inductive regions.

I think that (ii) is relevant in the context of the three-valued simulation method. In my implementation using the FMCAD’07 technique, I find it worthwhile to generalize all the way. In the original IC3 paper, I already stated that (i) was a heuristic whose value I doubted; however, in a personal communication, Niklas said that he had (subsequent to writing this paper) came across benchmarks on which (i) made a difference, in particular for choosing a seed literal (which matches my observation). That said, Fabio Somenzi has described a heuristic based on the SCC graph of the latches that seems to be quite effective — much better than variable activity alone.

We eliminate a tedious and error-prone special-case handling of counterexamples of length 0 or 1.

I have to say that this statement is simply ridiculous. I find it aesthetically displeasing to make the main case non-uniform simply to drop a base case. But to each their own, I guess. In any case, it’s not a substantive change; it’s more of a loop un-optimization 😉

We separate the main algorithm from the handling of SAT queries through a clean interface. This separation reduces the overall complexity.

Okeedokee, a change in presentation. I think the original paper is still worth a read.

We refute some potential improvements experimentally.

Yup, I tried a whole bag of bad tricks over the years while developing IC3.

We present detailed pseudo-code to fully document our implementation.

Again, I think the original paper, which has detailed pseudo-code with an embedded Floyd-Hoare style proof of correctness, is worth a read.

Let me emphasize that I think that the paper makes a substantial contribution in describing a better method of generating clauses, a significant improvement over the FMCAD’07 approach that I’ve been using. I also like their attempt at explaining why it works in the context of their deep understanding of Ken’s interpolation method. These are the reasons why I think people should read their paper.

-Aaron

 

Advertisements

2 Comments

  1. Thanks, Aaron! I’ve integrated a copy of your comments into the body of the text.

    Like

  2. Hi Brad,

    I think the primary contribution of this paper is this point:

    * We achieve a significant speedup by using three-valued simulation to reduce the burden on the SAT-solver.

    It provides a faster method of generating inductive clauses, which refines the method of

    Aaron R. Bradley and Zohar Manna, Checking Safety by Inductive Generalization of Counterexamples to Induction, In Proc. Formal Methods in Computer Aided Design (FMCAD) November 2007.

    The trade-off is that, if I understand correctly from a discussion with Niklas, the transition relation must be in function form. I’ve found it useful for finding counterexamples on some systems to invert the TR and swap the initial and error conditions, but then the three-valued method apparently wouldn’t work.

    Regarding the other points:

    * We show experimentally that two elements of the original algorithm give no speedup: (i) variable activity and (ii) cube generalization beyond non-inductive regions.

    I think that (ii) is relevant in the context of the three-valued simulation method. In my implementation using the FMCAD’07 technique, I find it worthwhile to generalize all the way. In the original IC3 paper (since you didn’t link to it in your post, here it is: http://ecee.colorado.edu/~bradleya/ic3), I already stated that (i) was a heuristic whose value I doubted; however, in a personal communication, Niklas said that he had (subsequent to writing this paper) came across benchmarks on which (i) made a difference, in particular for choosing a seed literal (which matches my observation). That said, Fabio Somenzi has described a heuristic based on the SCC graph of the latches that seems to be quite effective — much better than variable activity alone.

    * We eliminate a tedious and error-prone special-case handling of counterexamples of length 0 or 1.

    I have to say that this statement is simply ridiculous. I find it aesthetically displeasing to make the main case non-uniform simply to drop a base case. But to each their own, I guess. In any case, it’s not a substantive change; it’s more of a loop un-optimization 😉

    * We separate the main algorithm from the handling of SAT queries through a clean interface. This separation reduces the overall complexity.

    Okeedokee, a change in presentation. I think the original paper is still worth a read.

    * We refute some potential improvements experimentally.

    Yup, I tried a whole bag of bad tricks over the years while developing IC3.

    * We present detailed pseudo-code to fully document our implementation.

    Again, I think the original paper, which has detailed pseudo-code with an embedded Floyd-Hoare style proof of correctness, is worth a read.

    Let me emphasize that I think that the paper makes a substantial contribution in describing a better method of generating clauses, a significant improvement over the FMCAD’07 approach that I’ve been using. I also like their attempt at explaining why it works in the context of their deep understanding of Ken’s interpolation method. These are the reasons why I think people should read their paper.

    -Aaron

    Like

Tell me (anonymous OK)

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s