Learning to Order BDD Variables in Verification

paper

Learning to Order BDD Variables in Verification

Orna Grumberg
Shlomi Livne
Shaul Markovitch
Computer Science Department
Technion - Israel Institute of Technology Haifa 32000, Israel

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 verifica- tion 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.

Choco solver download and example code

Step 1.
* Download the choco-solver 4.0.4 from:
https://github.com/chocoteam/choco-solver/releases/tag/4.0.4
* unzip the choco-4.0.4.zip, and place it in the directory.

Step 2.
Setting for Scala Eclipes IDE
* Right click the target package, e.g. ChocoHandler, in package explorer in Eclipse.
* Select "Build Path" -> "Add External Arachives..."
* Select "choco-solver-4.0.4-with-dependencies.jar"

Step 3.
* Execute the attached Scala example code "ChocoHandler.scala".


import org.chocosolver.solver.Model
import org.chocosolver.solver.variables.IntVar;

object ChocoHandler{

def main(args: Array[String]): Unit = {

println("Sbt says Hello!")

val model: Model = new Model("Choco solver Hello world");
val a: IntVar = model.intVar("a", Array(4,6,8));
val b: IntVar = model.intVar("b", 0, 2);

model.arithm(a, "+", b, "<", 8).post();
var i: Int = 1;
while(model.getSolver().solve()) {
println("Solution " + i + " found : " + a + ", " + b);
i += 1;
}
}
}

Why the model checking technique is successful for HW verification, and failing for SW verification?

Why the model checking technique is successful for HW verification, and failing for SW verification?

  • For HW verification, HW like digital circuits are easy to model checking. But for SW, SW is usually so huge, we can only apply MC for abstract model of programs. However, two obstacles there: 1. it is costly to prepare the abstract models and severe cost effectiveness 2. abstract models of programs are not any more programs.

■

林晋さんのこと、根拠なきイチャモンのこと

http://d.hatena.ne.jp/m-hiyama/20151109/1447026954

いずれにしても、既存の方法や習慣とギャップがあると受け入れてもらえないので、今のやり方のなかに少しずつ形式性や厳密性を注入していくしかないような気がしています。