K*BMDs: a new data structure for verification
K*BMDs: a new data structure for verification
复制标题
K*BMDs：用于验证的新数据结构
DOI：
10.1109/edtc.1996.494118
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
Stefan Ruppertz
中科院分区：
文献类型：
--
作者：
R. Drechsler;B. Becker;Stefan Ruppertz
最近，计算机辅助设计（CAD）领域提出了两种新的数据结构，即有序克罗内克函数决策图（OKFDD）和乘法二元矩图（*BMD）。 OKFDD 是用于在位级表示布尔函数的最通用的有序数据结构。 *BMD 特别适用于整数值函数。在本文中，我们提出了一种新的数据结构，称为克罗内克乘法 BMD（K*BMD），它是 OKFDD 到字级的推广。使用 K*BMD 可以有效地表示具有良好字级描述的函数，因为 K*BMD 是 *BMD 的泛化。另一方面，它们也适用于比特级的验证问题。我们提供实验结果来证明我们方法的效率，包括将 K*BMD 与其他几种数据结构（如 EVBDD、OKFDD 和 *BMD）进行比较。此外，还报告了验证快速乘法器的实验，即最坏情况下运行时间为 O(log(n)) 的乘法器。
Recently, two new dates structures have been proposed in the area of Computer Aided Design (CAD), i.e. Ordered Kronecker Functional Decision Diagrams (OKFDDs) and Multiplicative Binary Moment Diagrams (*BMDs). OKFDDs are the most general ordered data structure for representing Boolean functions at the bit-level. *BMDs are especially applicable to integer valued functions. In this paper we propose a new data structure, called Kronecker Multiplicative BMDs (K*BMDs), that is a generalization of OKFDDs to the word-level. Using K*BMDs it is possible to represent functions efficiently, that have a good word-level description, since K*BMDs are a generalization of *BMDs. On the other hand they are also applicable to verification problems at the bit-level. We present experimental results to demonstrate the efficiency of our approach including a comparison of K*BMDs to several other data structures, like EVBDD, OKFDDs and *BMDs. Additionally, experiments on verification of fast multipliers, i.e. multipliers with worst case running time O(log(n)), are reported.