Learning to Order BDD Variables in Verification
  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.
