Optimizing BDD-based verification analysing variable dependencies

摘要

Automatic verification of sequential designs has been made possible by the use of efficient representations for propositional logic such as Binary Decision Diagrams (BDDs). However the efficient use of BDDs is only possible provided a good ordering of the state variables of the design. This paper presents a novel heuristics, called variable weighting, that provides an initial variable ordering for sequential designs. Experiments are provided to illustrate the quality of this algorithm. An important result is that it combines extremely well with existing dynamic variable reordering techniques. In all experiments, the combination of variable weighting and reordering outperforms reordering alone.