.png){kind=icon}
.png){kind=icon}
Return
Efficient Evolution of Variable Ordering for Binary Decision Diagram Optimization
.png){kind=icon}
PRE
AI
DOI：10.1109/TEVC.2025.3569778.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
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.
Keywords:
Binary decision diagrams (BDDs)
clustering
evolution strategies
evolutionary algorithms
formal verification
Journal
IF:
12
Papers:
1.8K
Citations:
2.4W