Indexed BDDs: Algorithmic Advances in Techniques to Represent and Verify Boolean Functions
Indexed BDDs: Algorithmic Advances in Techniques to Represent and Verify Boolean Functions
复制标题
索引 BDD：表示和验证布尔函数的技术的算法进步
DOI：
10.1109/12.644298
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
D. Fussell
中科院分区：
文献类型：
--
作者：
J. Jain;J. Bitner;M. Abadir;J. Abraham;D. Fussell
提出了一种新的布尔函数表示方法--索引二叉决策图（IBDD），为有序二叉决策图（OBDD）表示的函数提供了一种紧凑的表示.我们解释IBDDs的属性，并提出从一个给定的电路构建IBDDs的算法。给出了IBDD可满足性测试和等价性检验的实用有效算法及其实现结果。结果表明，许多函数，如乘法器和隐藏的加权位的功能，这是难以分析的OBDD，可以有效地完成使用IBDD。我们报告有效的验证布斯乘法器，以及一个实用的策略，多项式时间验证的一些类的无符号阵列乘法器。
A new Boolean function representation scheme, the Indexed Binary Decision Diagram (IBDD), is proposed to provide a compact representation for functions whose Ordered Binary Decision Diagram (OBDD) representation is intractably large. We explain properties of IBDDs and present algorithms for constructing IBDDs from a given circuit. Practical and effective algorithms for satisfiability testing and equivalence checking of IBDDs, as well as their implementation results, are also presented. The results show that many functions, such as multipliers and the hidden-weighted-bit function, whose analysis is intractable using OBDDs, can be efficiently accomplished using IBDDs. We report efficient verification of Booth multipliers, as well as a practical strategy for polynomial time verification of some classes of unsigned array multipliers.