BDD-based verification of scalable designs

Many formal verification techniques make use of Binary Decision Diagrams (BDDs). In most applications the choice of the variable ordering is crucial for the performance of the verification algorithm. Usually BDDs operate on the Boolean level, i.e. BDDs are a bit-level data structure. In this paper we present a method to speed-up BDD-based verification of scalable designs that makes use of a learning process for word-level information. In a preprocessing a scalable ordering is extracted from the RTL that is used as a static ordering for large designs. Experimental results show that significant improvements can be achieved.