Efficient Evolution of Variable Ordering for Binary Decision Diagram Optimization

The hardware complexity related to the number of transistors in electronic devices used by today’s society has grown considerably in the last decades because of technological progress. In order to guarantee the correct behavior of such devices and meet time-to-market constraints, there is a need to continuously develop more efficient data structures and algorithms in formal verification. The performance of verification algorithms depends in particular on the compactness of data structures. A reduced ordered binary decision diagram (BDD) is basically a suitable data structure to verify digital circuits, as it represents Boolean functions canonically respecting a variable ordering and allows direct manipulation of them. However, one of the main challenges with BDDs is to find a variable ordering so that the BDD size of a function is compact and does not become impractical due to a dramatically increasing number of BDD nodes. To address the aforementioned issue, this article presents a novel evolution strategy having an efficient evaluation of variable ordering in a divide-and-conquer manner for BDD optimization. Experiments on benchmarks of multilevel circuits show that using this strategy results in considerably smaller BDDs being found significantly faster compared to state-of-the-art optimization techniques.