Home | Publications | CS Home

Learning to Order {BDD} Variables in Verification


Orna Grumberg, Shlomi Livne and Shaul Markovitch. Learning to Order {BDD} Variables in Verification. Journal of Artificial Intelligence Research, 18:83-116 2003.


Abstract

The size and complexity of software and hardware systems have significantly increased in the past years. As a result, it is harder to guarantee their correct behavior. One of the most successful methods for automated verification of finite-state systems is model checking. Most of the current model-checking systems use binary decision diagrams (BDDs) for the representation of the tested model and in the verification process of its properties. Generally, BDDs allow a canonical compact representation of a boolean function (given an order of its variables). The more compact the BDD is, the better performance one gets from the verifier. However, finding an optimal order for a BDD is an NP-complete problem. Therefore, several heuristic methods based on expert knowledge have been developed for variable ordering. We propose an alternative approach in which the variable ordering algorithm gains 'ordering experience' from training models and uses the learned knowledge for finding good orders. Our methodology is based on offline learning of pair precedence classifiers from training models, that is, learning which variable pair permutation is more likely to lead to a good order. For each training model, a number of training sequences are evaluated. Every training model variable pair permutation is then tagged based on its performance on the evaluated orders. The tagged permutations are then passed through a feature extractor and are given as examples to a classifier creation algorithm. Given a model for which an order is requested, the ordering algorithm consults each precedence classifier and constructs a pair precedence table which is used to create the order. Our algorithm was integrated with SMV, which is one of the most widely used verification systems. Preliminary empirical evaluation of our methodology, using real benchmark models, shows performance that is better than random ordering and is competitive with existing algorithms that use expert knowledge. We believe that in sub-domains of models (alu, caches, etc.) our system will prove even more valuable. This is because it features the ability to learn sub-domain knowledge, something that no other ordering algorithm does.


Keywords: Speedup Learning, BDD Ordering
Secondary Keywords:
Online version:
Bibtex entry:
 @article{Grumberg:2003:MLE,
  Author = {Orna Grumberg and Shlomi Livne and Shaul Markovitch},
  Title = {Learning to Order {BDD} Variables in Verification},
  Year = {2003},
  Journal = {Journal of Artificial Intelligence Research},
  Volume = {18},
  Pages = {83-116},
  Url = {http://www.cs.technion.ac.il/~shaulm/papers/pdf/Grumberg-Livne-Markovitch-jair2003.pdf},
  Keywords = {Speedup Learning, BDD Ordering},
  Secondary-keywords = {Learning to Order, Decision Trees},
  Abstract = {
    The size and complexity of software and hardware systems have
    significantly increased in the past years. As a result, it is
    harder to guarantee their correct behavior. One of the most
    successful methods for automated verification of finite-state
    systems is model checking. Most of the current model-checking
    systems use binary decision diagrams (BDDs) for the representation
    of the tested model and in the verification process of its
    properties. Generally, BDDs allow a canonical compact
    representation of a boolean function (given an order of its
    variables). The more compact the BDD is, the better performance
    one gets from the verifier. However, finding an optimal order for
    a BDD is an NP-complete problem. Therefore, several heuristic
    methods based on expert knowledge have been developed for variable
    ordering. We propose an alternative approach in which the variable
    ordering algorithm gains 'ordering experience' from training
    models and uses the learned knowledge for finding good orders. Our
    methodology is based on offline learning of pair precedence
    classifiers from training models, that is, learning which variable
    pair permutation is more likely to lead to a good order. For each
    training model, a number of training sequences are evaluated.
    Every training model variable pair permutation is then tagged
    based on its performance on the evaluated orders. The tagged
    permutations are then passed through a feature extractor and are
    given as examples to a classifier creation algorithm. Given a
    model for which an order is requested, the ordering algorithm
    consults each precedence classifier and constructs a pair
    precedence table which is used to create the order. Our algorithm
    was integrated with SMV, which is one of the most widely used
    verification systems. Preliminary empirical evaluation of our
    methodology, using real benchmark models, shows performance that
    is better than random ordering and is competitive with existing
    algorithms that use expert knowledge. We believe that in sub-
    domains of models (alu, caches, etc.) our system will prove even
    more valuable. This is because it features the ability to learn
    sub-domain knowledge, something that no other ordering algorithm
    does.
  }

  }