返回
Efficient Evolution of Variable Ordering for Binary Decision Diagram Optimization
DOI:10.1109/TEVC.2025.3569778.png)
摘要
En 中文
近年来,由于技术进步,与社会当前使用的电子设备中晶体管数量相关的硬件复杂性已显著增长。为了确保这些设备的正确行为并满足上市时间限制,需要在形式验证中持续开发更高效的数据结构和算法。验证算法的性能尤其取决于数据结构的紧凑性。降阶二元决策图(BDD)本质上是一种适用于验证数字电路的数据结构,因为它以遵循变量顺序的规范方式表示布尔函数,并允许直接对其进行操作。然而,使用BDD的一个主要挑战在于找到一种变量顺序,使得函数的BDD尺寸紧凑,且不会因BDD节点数量急剧增加而变得不切实际。为解决上述问题,本文提出了一种新颖的进化策略,采用分治方式高效评估变量顺序,以优化BDD。针对多级电路基准的实验表明,采用该策略能够比当前最先进的优化技术更快地找到显著更小的BDD。
Keyword:
Binary decision diagrams (BDDs)
clustering
evolution strategies
evolutionary algorithms
formal verification
期刊
IF:
12
论文数:
1.9K
被引数:
2.4W

