论文部分内容阅读
自从1986年R.E.Bryany等人提出了二叉决策图(Binary Decision Diagrams)的概念以来，由于其空间和时间上表示和处理布尔函数的高效性，BDD被广泛应用于大型数字系统设计中的逻辑功能验证、综合以及模型检测等方面且日益受到重视。然而，传统的BDD运算的实现主要基于哈希表技术，所以在处理大规模BDD运算时经常会遇到内存溢出问题。为了解决该问题有人提出如高效利用内存、基于广度优先实现BDD运算等方法，但由于BDD规模过大或BDD有些层节点过多，内存溢出问题还是会出现。Shin-ichi Minato等人提出了基于流的BDD运算模型，可以从根本上解决这个问题。其主要思想是把BDD转化为流，以流的形式作为运算输入，内存只用作运算缓存而不用存储整个BDD。v本文首先讨论了一个经典BDD包(BuDDy)的具体实现，该包基于哈希表技术采用深度优先算法实现简约有序二叉决策图(ROBDD)的运算。哈希表技术用于保证ROBDD的正则性。通过把哈希表和BDD节点存储表整合到同一个大的数组，提高了内存的利用率。运算过程中用动态规划避免了重复BDD节点间运算，且可以比较低耗的完成自动垃圾回收。由于这些技术的应用，BuDDy在进行BDD运算时比其它BDD实现包的效率高，但由于其基于哈希表技术所以会遇到内存溢出问题。为此，本文在BuDDy的基础上实现基于流的BDD运算，将其作为一个新的运算功能扩展到BuDDy包中。在本文的最后部分给出一个用扩展后的BuDDy包解决大规模BDD运算的实例，分析了流运算模型解决内存溢出问题的正确性和可行性。