CUDD包的分析与应用论文

1、摘 要近几年来，模型检验技术在保证设计正确性的验证上得到了工业界的普遍认可。但随着电路规模的增大，状态数目将呈指数增加而引起组合爆炸，这就限制了模型检验的应用。使用二元决策图BDD表示布尔函数，可以减小布尔函数在计算机内部的存储空间。将BDD引入模型检验中，可以比较有效地缓解模型检验中状态爆炸的问题，极大地提高了模型检验所能验证的系统的规模。本论文就是基于CUDD（Colorado University Decision Diagram）包在BDD方面的研究与应用。CUDD是一个操纵决策图的软件开发包，它已成为了BDD应用的一个通用模板。论文首先介绍二元决策图的理论基础上，阐述布尔函数，二元决

2、策图，有序二元决策图，精简有序二元决策图等基本概念；然后介绍CUDD软件包，论述了CUDD包整体的基础架构，并着重对其采用的数据结构和关键算法进行的分析和说明；最后以一个半加器程序为实例来展示CUDD在BDD方面的具体应用。关键字：模型检验；布尔函数；CUDD；BDD；算法AbstractIn recent years, model checking technology to ensure the correctness of the verification on the design industry has been generally recognized. However, as

3、circuit size increases, the number of states increased exponentially combinatorial explosion caused, which limits the application of model checking. Using binary decision diagram BDD, said Boolean function, Boolean function can reduce the storage space inside the computer. BDD model checking will be

4、 introduced, you can more effectively alleviate the model checking problem in the state explosion, which greatly improved the model checking can verify the system size.This paper is based on the CUDD (Colorado University Decision Diagram) package of research and application of BDD. CUDD decision dia

5、gram is a manipulation of the software development kit, it has become a common template BDD applications.Paper first introduces the theory of binary decision diagram based on the set of Boolean functions, binary decision diagram, ordered binary decision diagram, ordered binary decision diagram to st

6、reamline the basic concept; then introduced CUDD package, discusses the CUDD package as a whole infrastructure, and focus on its use of data structures and key algorithms of the analysis and description; the last one and a half adder program as an example to demonstrate the CUDD BDD of the specific

7、application in. Keywords: Model checking; Boolean function; CUDD; BDD; Algorithm目 录第一章 绪 论- 1 -1.1本选题的实际意义- 1 -1.2 本论文的主要工作- 2 -第二章 二元决策图的理论基础- 3 -2.1 布尔函数- 3 -2.2 二元决策图- 3 -2.3 二元决策图的构造- 3 -使用香农展开式转化布尔函数- 3 -构造矩阵- 4 -构造BDD- 4 -2.3.4 BDD的简化- 5 -2.4 有序二元决策图- 5 -2.5 其它相关理论- 5 -2.5.1 零压缩二元决策图- 5 -2.5.2

8、 代数决策图- 5 -第三章 CUDD包- 6 -3.1 CUDD包的简介- 6 -3.2 CUDD包的安装- 7 -3.3 CUDD各模块的功能分析- 8 -3.4 CUDD的基本结构- 8 -垃圾回收- 8 -唯一表- 8 -数据结构- 9 -3.5 重排BDD- 10 -3.5.1 手动重排- 10 -3.5.2 自动重排- 10 -3.5.3 其他常用的重排函数- 11 -第四章 半加器实例- 12 -4.1 创建BDD- 12 -4.2 限制BDD- 13 -4.3 打印BDD- 14 -4.4 主函数- 15 -第五章 总 结- 16 -5.1 结束语- 16 -5.2 研究动态和

9、未来的发展- 16 -致 谢- 17 -参考文献- 18 -第一章 绪 论1.1本选题的实际意义在数字控制系统，计算机辅助设计CAD(Computer Aided Design)，计算机辅助测试CAT(Computer Aided Test)，人工智能AI(Artificial Intelligence)以及可编程控制器等领域的许多问题都可以表示成一系列关于布尔函数的运算，这些运算有赖于布尔函数的符号表示和算法的有效性。一般而言，我们通常采用布尔函数表达式或真值表来描述数字逻辑函数。布尔函数是一种可以精确地描述数字逻辑函数的方法。但随着大规模和超大规模集成电路的迅速发展，数字逻辑函数的运算变得

10、日益复杂，上述的传统方法逐渐暴露出一些缺点，比如使用布尔函数来表示数字逻辑函数的话，表达式往往会变得庞大和复杂，使得函数处理时间过长；而使用真值表方式的话，则需要占用大量的存储空间，只能用在一些特殊的领域。鉴于上述的情况，研究人员不断的探索，试图找到描述更加简洁、操作更加方便的数字逻辑函数表达方式。1986年，E.R.Bryant提出了用二元决策图BDD(Binary Decision Diagram)来表示布尔函数，和其他表示法相比BDD在人们寻找大型数字系统的有效分析，测试和计算方法中，由于其固有的优越性能而日益受到重视。综合来说,BDD具有如下的优点： (1)直观，明了，便于逻

11、辑电路的分析。(2)能反映数字电路的逻辑描述的细节，这点对电路的分析和测试非常重要。(3)便于计算机的存储，编写的程序比布尔代数方法编写的程序更短。(4)便于使用人工智能的方法，启发式进行求解空间搜索。(5)不管是硬件还是软件实现，都能获得比布尔代数算法更高的执行速度。模型检测主要是验证某一模型生成的有限状态系统是否满足模型所要求的属性。模型检测技术可以抽象地描述为：给定一个模型M和逻辑描述的性质P，检查模型M中性质P是否成立。模型检测主要是验证某一模型生成的有限状态系统是否满足模型所要求的属性。模型检测中最大的挑战就是状态空间的爆炸问题。这个问题源于系统中有许多不同部件的交互，或者系统中有取

12、值范围很大的复杂数据结构，在这种情况下系统状态的规模将变得非常庞大。由于BDD所用的存储空间较少，因此研究人员将BDD引入到了模型检验中，使得模型检验所能验证的系统规模得到了很大的提高。时态逻辑在模型检测中占有非常重要的地位，模型检测是基于时态逻辑，时态逻辑的模型可能由几个状态构成。时态逻辑公式可能在一些状态为真，在其它为假。因此，该公式的值随着状态的变化而变化。依据对系统状态的时间路径的不同刻画，时态逻辑可以分成两大类：计算树时态逻辑和线性时态逻辑。 计算树时态逻辑CTL(Computation Tree Temporal Logic)是由Clarke和Emerson提出的。它的运

13、算符具有简单的性质，可以有效地计算某一公式在有穷状态模型处于某一状态时是否满足。它是一种时间模型采用树的方式、具有多个分支的不确定状态路径构成。在模型检测过程中采用BDD的主要原因是：采用BDD表达的两个谓词公式时，两个BDD范式逻辑相等当且仅当这两个BDD范式是语法相等，即两个BDD范式逻辑相等，当且仅当这两个BDD范式是同一个BDD范式。目前,利用BDD来对规划问题求解的基本思想是：先将规划问题的状态和动作表示为BDD范式，再将其输入到BDD的求解器，然后将求解得到的结果转化为一般规划问题的表示。1.2 本论文的主要工作本论文是基于CUDD包在BDD方面的研究与应用。它主要由二元决策图的理

14、论基础，CUDD包和一个半加器实例3个模块构成。在BDD的理论基础中重点阐述了布尔函数，二元决策图，有序二元决策图，精简有序二元决策图的基本概念；关于CUDD包，主要论述的是CUDD的简介，CUDD的获取、编译、链接，以及CUDD的基础架构；最后的半加器程序主要针对BDD的创建，重排，限制，打印作了尽可能详细的解释。第二章 二元决策图的理论基础2.1 布尔函数布尔函数的定义：设B,0,1是一个布尔代数,一个从Bn到B的函数,如果能够用该布尔代数上的n元布尔表达式表示,那么这个函数就称为布尔函数。布尔表达式是由0, 1以及变量、布尔运算(与，或，非)构成的符号串,与逻辑公式定义是一致,即：设有布

15、尔代数<B,>及其上的n个变元x1, x2, , xn,则布尔表达式可归纳地定义为： (1) 0, 1和x1, x2, , xn均是布尔表达式； (2)如果a1和a2是布尔表达式,则a1a2, a1a2, a1也都是布尔表达式； (3)此外,再没有其它的字符串是布尔表达式。本文所提出的实现布尔函数运算的方法：其布尔函数由有向无环图表示。这种布尔函数的表示方法以二元决策图BDD(Binary Decision Diagram)为基础，且对图中节点的变量的编序作了进一步的限制，从而使本文所用的这种表示方法在表示布尔函数并实现其运算的算法上更加有效。2.2 二元决策图 二元决策图BDD(

16、Binary Decision Diagram)是有限个节点构成的有向无环图。其中，V是G的所有节点的集合，E是G的所有边的集合。V中的结点分为端节点（用方框表示）和非端节点（用圆框表示）。每个端节点用0或1标识，无出边(outgoing edge)；每个非端节点用变量标识，并且有两条出边(outgoing edge)：指向右孩子的then边（用实线表示，表示变量被赋值为1），指向左孩子的else边（用虚线表示，表示变量被赋值为0）。2.3 二元决策图的构造使用香农展开式将布尔函数转化为BDD的形式。使用香农展开式转化布尔函数以为例，进行香农展开：步骤一：生成：将代入，得到；步骤二：生成：将e

17、=1代入，得到；步骤三：将 和分别与与e相乘，得到；步骤四：重复执行步骤一到三，对 和分别进行展开，依次递归，直到没有变量可以替换为止。最终的展开结果为：。构造矩阵以节中的展开式为例。构造矩阵：我们按照从左到右的顺序来依次遍历展开式中的每一个变量，如果遇到的一对变量是以的形式出现。则在矩阵中(X，Y)处填入1；如果遇到的一对变量以的形式出现，则在矩阵中(X，Y)处填人0。YX e b d 1 0 e 0 1 b 1 0 d 1 0 表 矩阵图构造BDD通过矩阵来构造BDD：对于矩阵中的某一项(X，Y)，如果该项的值为1，则在BDD中有从节点X到节点Y的一条1边；如果该项的值为0。则表示在BDD

18、中有从节点X到节点Y的一条0边（1边用实线描述，0线用虚线描述）。构造的BDD如下图：01ebd 图 二元决策图 BDD的简化布尔表达式转化为BDD之后。生成的BDD可能会有重复出现的节点，因此最后还需要对生成的BDD进行简化。按照以下三个原则对BDD进行简化：(1)保证图中只有一对终节点；(2)删除0边与1边重合的非终节点，并将指向该节点的边直接指向其后继节点，即该节点满足：；(3)如果两个非终节点满足：，则只保留其左节点。2.4 有序二元决策图有序二元决策图OBDD(Ordered Binary Decision Diagram)是Bryant提出的一种布尔函数表示法。它通过在二元决策图B

19、DD(Binary Decision Diagram)表示法的基础上引入适当的约束，使之在形式上规范，且能更简单、方便地处理布尔变量间的运算。满足下面条件的BDD称为有序二元决策图：(1)有序性条件。对任意2个相邻变量节点v和u，若u为v的子节点，即或者，则有代表的布尔变量的序号在之前。(2)简约性条件。无重复的节点：不存在同时满足，和的2个节点u和v。若满足，则称u和v为“重复的”节点；无冗余节点：不存在满足的变量节点u。若满足，则称u为“冗余的”节点。精简有序二元决策图ROBDD(Reduced Ordered Binary Decision Diagram)是一个满足以下条件的OBDD：

20、对于任意节点，不会存在；对于由任意两个节点作为根节点构成的BDD子图，不存在同构。2.5 其它相关理论2.5.1 零压缩二元决策图对从到的布尔函数和给定的变量序（即是有顺序的），有序二元决策图OBDD是用于表示布尔函数的一个有向无环图。零压缩二元决策图ZBDD(Zero-suppressed Binary Decision Diagram)是一种特殊的OBDD,是日本学者Minato为了克服OBDD表示组合集合存在的不足而提出的，进一步降低了组合集合表示的空间需求，从而可更为有效地处理组合集合相关的问题。2.5.2 代数决策图一个代数决策图ADD(Algebraic Decision Diag

21、ram)就是表示一簇伪布尔函数（整数集合）的有一个直接根结点的有向无环图。所有的有限个节点被分为终端节点和非终端节点两类。在图中一般用圆圈表示非终端节点, 用方框表示终端节点。每个终端节点都被标有Z中的一个元素, 并且没有出边。而每个非终端节点都有两条出边, 即0边和1边。0边是指非终端节点取值0后的分支, 在图中一般用虚线表示。1边是指非终端节点取值1后的分支, 在图中一般用实线表示。对于变量的一组赋值, 所得到的函数值由根节点到一个终端节点的一条路径决定。这条路径所对应的分支由变量的这组赋值来决定, 该分支的终端节点所标识的值就是变量在这组赋值下所对应的函数值。不同的变量序的选择对于ADD

22、 的规模有着极大的影响, 因此在求伪布尔函数的ADD时, 必须说明变量的顺序。图(a) 为伪布尔函数的完全二叉表示, 图2.4.2(b)为f在变量序P: x 1< x 2< x 3<x 4下的ADD, 由图可见, 表示伪布尔函数f的ADD所需的节点明显小于表示该函数的完全二叉树的节点, 这表明ADD的存储空间较小。图 伪布尔函数的两种表示ADD 极大地改善了伪布尔函数和有限域取值函数的描述能力。目前,ADD数据结构在矩阵乘、最短路径计算、组合电路的时间分析、网络最大流等领域得到了广泛的应用。第三章 CUDD包3.1 CUDD包的简介CUDD（Colorado Universi

23、ty Decision Diagram）是一个操纵决策图的软件开发包，它提供函数来操纵二元决策图（BDDs），代数决策图（ADDs）和零压缩二元决策图（ZDDs）。它的作者是卡罗拉多州立大学电气工程学院的Fabio Somenzi。CUDD包定义了决策图的数据结构和操作决策图的一系列算法：决策图的建立，遍历，排序，相互转换，决策图上通用算法，ite算法以及节点存储管理等。这个软件包可以从三个方面来加以利用：1作为一个黑盒。在这种情况下，应用程序，需要操作的决策图只需要用软件包导出的函数即可。CUDD包中包含的丰富函数集合使许多应用程序能够以这种方式编写。在包的导出功能上编写的应用程序无须关心内

24、部变量重排的细节。2作为一个白盒。当基于决策图编写一个复杂的应用程序时，由于效率的原因，函数往往直接作为图的递归操作而不是在现有的原始功能上写。所以就必须深入软件包的内部，了解其运行的细节，自己为CUDD包增加新的功能，以满足需求。3 通过一个接口。对于面向对象语言，如C+，能使程序员更自由的管理内存。一个基于C+的接口已经被包含在CUDD包的分配中了。它会自动释放决策图，不再由应用程序和重载函数所使用。几乎所有的功能都是CUDD的导出函数所提供，通过C+接口来利用。这种方式经常被用在快速原型方案。 3.2 CUDD包的安装CUDD包可以用匿名的方式通过FTP从vlsi.colorado.ed

25、u 获得。当前版本为cudd-。cudd-2.4.2包含决策图包，以及基于决策图包的几个应用程序和库，它们可以用ANSI C和C+编译器编译得到。CUDD可以在linux，Cygwin和OS X下编译通过。具体步骤可以参看makefile文件。以下是各平台编译CUDD所要注意的地方。所有平台需要修改makefile中的如下行：XCFLAGS = -mcpu = pentiumpro -malign-double -DHAVE_IEEE_754 DBSD-mcpu标记是不需要的，只需要删除它使之变成：XCFLAGS = -malign-double -DHAVE_IEEE_754 DBSDLin

26、ux平台如果用的是32位的OS，那么现在就可以准备编译了。如果用的是64位的，那么就要用如下行的XCFLAGS代替上面的：XCFLAGS = -ansi -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P = 8 -DSIZEOF_LONG = 8Cygwin和OS X在$CUDD ROOT/util/cpu_stats.c文件下的void util_print_cpu_stats(FILE *fp)函数可能会引起错误。修复的方法是禁止这个函数。为了禁止这个函数我们需要改动两行。首先在文件头部找到如下代码：#if defined(_IBMR2)#define etext

27、 _etext#define edata _edata#define end _end#endif然后替换第一行(#if defined( IBMR2)为：#if 0下一步替换void util_print_cpu_stats(FILE *fp)函数中的第一行：#ifdef BSD为#if 0最后开始编译。如果编译成功，将会在$CUDD_ROOT(CUDD根目录)中生成一个include目录，里面链接了所有的外部的头文件。我们将用到如下已经存在的头文件：$CUDD_ROOT/include/cuddObj.hh还有如下6个文件被创建了：$CUDD_ROOT/cudd/libcudd.a$CUD

28、D_ROOT/util/libutil.a$CUDD_ROOT/epd/libepd.a$CUDD_ROOT/mtr/libmtr.a$CUDD_ROOT/st/libst.a$CUDD_ROOT/obj/libobj.a根据这些信息，如下就是一个利用CUDD的应用程序的一个简单的makefile。Sample makefile of C+ program utilizing CUDD CC = g+CUDDINCLUDE=cudd/cudd/libcudd.a cudd/util/libutil.a cudd/epd/libepd.acudd/mtr/libmtr.a cudd/st/lib

29、st.a cudd/obj/libobj.a cuddtes t : cudd_example.cpp$ (CC) $ (CUDD INCLUDE) cudd_example.cpp o cudd_example 3.3 CUDD各模块的功能分析CUDD包含有cudd，dddmp，epd，mnemosyne，mtr，nanotrav，st，sis，util，obj，include几个文件包。cudd提供函数来操纵二元决策图（BDDs），代数决策图（ADDs）和零压缩二元决策图（ZDDs）。其它是辅助包，提供各种相关的辅助功能。dddmp包用作图的输出格式描述；epd包提供带有扩展双精度算术功能

30、；mnemosyne包用作内存检测和检查内存泄露等。mnem_malloc()，mnem_calloc()，mnem_realloc()，mnem_free()，mnem_recording()，mnem_setrecording()，mnem_setlog()，mnem_writestats()是其主要声明的函数；mtr这个包提供了两个层次的功能。低层次的功能操纵多路分支树，根据每个节点指向的第一个孩子节点和兄弟节点的位置来实施。高层次的功能处理一组树，这些树通过筛选分组来表示分组变量；nanotrav是个可达性的检验包；st包提供函数用来创建，保持，查询符号表；sis提供与VIS SIS的

31、接口；util包提供一些通用函数，如计算cpu时间的util_cpu_time(void)函数,搜索文件的util_file_search (char const *, char *, char const *)函数等；obj提供c+接口，以便c+程序使用。3.4 CUDD的基本结构3.4.1垃圾回收CUDD有一个垃圾回收系统。当建立BDDs时，是由自底向上的方式。在进程中，建立了许多已归纳好的小的BDDs来遍历我们的树。当一个BDDs被归入，它的内存是可以被回收的。为了使垃圾回收器更方便，需要保证BDD中的每个节点的引用。为了引用一个节点，用Cudd_Ref(DdNode *)函数，为了释放

32、引用调用Cudd_RecursiveDeref(DdNode *)。我将在论文的后面更深入的讨论。3.4.2唯一表虽然唯一表是不直接运行的，但我们必须知道它的存在。特别是在检查CUDD源的时候，它是很有必要的。这个表用来保证指定节点的唯一性，也就是说如果两个节点包含了相同的孩子和相同的变量，那么它就会合成一个节点。3.4.3数据结构CUDD中两个最重要的数据结构是DdManager和DdNode。下面将分别论述。DdManagerDdManager是个CUDD的中央结构体。创建这个结构体是在写一个CUDD程序首先要做的事情，并且几乎所有的CUDD api函数都是需要它。它不需要直接操作和检测结

33、构，只需调用CUDD api即可。为了初始化DdManager，调用用如下函数：DdManager *Cudd_Init (unsigned int numVars , /BDD变量的初始数目unsigned int numVarsZ , / ZDD变量的初始数目unsigned int numSlots , / 唯一表的初始数目unsigned int cacheSize , /初始化的缓存大小unsigned long maxMemory / 最大操作内存) ;在程序中，可以这样调用：Cudd_Init (0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS,

34、 0)；有用的DdManager函数：int Cudd_ReadSize(DdManager *dd)； 返回管理器中的变量数目int Cudd_ReadNodeCount(DdManager *dd)； 返回管理器中的节点数目DdNodeDdNode是BDDs的核心结构体。它的定义如下：struct DdNodeDdHalfWord index; / 节点变量索引DdHalfWord ref; / 计数引用DdNode *next; / 指向下一唯一表的指针union CUDD_VALUE_TYPE value; / 常节点DdChildren kids; / 指向子图type; index

35、是节点所代表的变量的唯一索引。这个节点是由0开始的。这些索引是固定的：这意味着我们将用一个启发式的排序来重排BDD，节点会改变排序，但是索引不会改变。为了获得变量排序的位置，可以用Cudd_ReadPerm(DdManager *dd, int i);为了获得变量的索引，可以用Cudd_ReadInvPerm(DdManager *d, int i);ref存储这个变量的引用计数。每次DdNode调用Cudd_Ref,引用计数将增加1，若调用Cudd_Recursive_Deref，引用计数将减1。当引用计数为0时，CUDD就知道节点可以被回收了。所有的Cudd节点所代表的变量都在唯一表里连在

36、一起。next代表的是指向下一个DdNode的指针。每一个DdNode如果它是叶子节点，那么它都包含了一个值和一个指向子DdNode的指针。这些值都被存储在type里。3.5 重排BDD我们遍历BDD的次序对构造所需节点数量有巨大的影响。为了重排BDDs，CUDD提供丰富的工具集合。变量的次序受一个启发式的函数控制。CUDD所提供的这些函数在CUDD的文档里都有描述。重排既可以手动也可以自动。3.5.1 手动重排为了引用手动重排，我们必须调用如下函数：int Cudd_ReduceHeap (DdManager *manager , / DD 管理器Cudd_ReorderingType me

37、thod , / 重排的方法int minsize / 不能重排的最小限制) ;我们总是略过管理器指针。第二个参数允许我们指定重排的类型。以下是CUDD提供的参数表。CUDD_REORDER_NONE CUDD_REORDER_SAMECUDD_REORDER_RANDOM_PIVOT CUDD_REORDER_EXACTCUDD_REORDER_RANDOM CUDD_REORDER_SIFTCUDD_REORDER_WINDOW2 CUDD_REORDER_SIFT_CONVERGECUDD_REORDER_WINDOW2_CONV CUDD_REORDER_SYMM_SIFT_CONVC

38、UDD_REORDER_WINDOW3 CUDD_REORDER_GROUP_SIFTCUDD_REORDER_WINDOW3_CONV CUDD_REORDER_GENETICCUDD_REORDER_WINDOW4 CUDD_REORDER_ANNEALINGCUDD_REORDER_WINDOW4_CONV CUDD_REORDER_GROUP_SIFT_CONVCUDD_REORDER_SYMM_SIFT最后一个参数是在BDD中重排的最小数。它提供了重排足够小的BDDs的花费。3.5.2 自动重排当BDD的节点数超过了一个限制，排序能被自动触发。如下函数用在自动排序：Cudd_Auto

39、dynEnable (DdManager *manager , / DD管理器Cudd_ReorderingType method , / 重排方法)参数相同的还有Cudd_ReduceHeap函数Cudd_ReduceHeap (DdManager *manager , / DD管理器Cudd_ReorderingType method , / 重排方法)3.5.3 其他常用的重排函数int Cudd_ShuffleHeap (DdManager *manager , / DD管理器int *permutation / 需要的变量序列)Permutation是一个排序位置的数组。它值代表的是

40、变量索引 Cudd_ReadPerm(DdManager *manager , / DD管理器int i / 这个变量指示位置)int Cudd_ReadInvPerm(DdManager *manager , / DD管理器int pos / 变量索引位置)第四章 半加器实例4.1 创建BDD 图4.1 电路图这是一个我们编制的一个BDD的半加器电路图。它有如下真值表： sum carry 00 0 0 0 1 1 0 1 0 1 0 1 1 0 1 表4.1 真值表用CUDD生成如上BDD的半加器电路。DdNode *createHalfAdderBDD(DdManager *m

41、anager) DdNode *x0 = Cudd_bddIthVar(manager, 0); DdNode *x1 = Cudd_bddIthVar(manager, 1); DdNode *and1 = Cudd_bddAnd(manager, x0, Cudd_Not(x1); Cudd_Ref(and1);DdNode *and2 = Cudd_bddAnd(manager, Cudd_Not(x0), x1);Cudd_Ref(and2);DdNode *sum = Cudd_bddOr(manager, and1, and2);Cudd_Ref(sum); Cudd_Recurs

42、iveDeref(manager, and1); Cudd_RecursiveDeref(manager, and2);DdNode *carry = Cudd_bddAnd(manager, x0, x1); Cudd_Ref(carry); / 返回两个BDD根DdNode *outputs = new DdNode *2; outputs0 = sum; outputs1 = carry; return outputs; 如上代码创建了一个半加器电路的BDD。这个电路用两位作为输入，返回它们的和与进位。这个BDD是从底向上构建的。通过创建两个Cudd变量，一个作为输入。然后用与或者或的方

43、法联合这些变量直到构建BDD。下面通过一些细节来认识：Cudd_bddIthVar(manager,i)：为了描述输入变量，用Cudd_bddIthVar。如果索引不存在，这个函数将创建一个索引i的变量，如果存在，这个函数将返回一指向存在索引变量的指针。Cudd_bddAnd(manager,node1,node2)(或者Cudd_bddOr)：使用这些函数是为了用结合和拆分操作来联合DdNode指针。如果有一个BDD代表x，另一个代表y，这个函数将返回一个新的BDD分别代表或者。Cudd_Ref(manager,node)：注意通过Cudd_bddAnd 和Cudd_bddOr的返回必须要增

44、加所有DdNode结构的引用计数。Cudd_RecursiveDeref(manager, node)：注意在被归入新的BDD所指向的总和之后不得不减少and1和与and2的引用计数。4.2 限制BDDDdNode *Cudd_bddRestrict (DdManager *manager , / DD管理器DdNode *BDD, /用来限制的BDD DdNode *restrictBy /被限制的BDD ) 以下代码是限制一个BDD的输入为分配的。它需要一个节点来限制和一个分配图来输入。图的关键是指定变量的索引和指定值的真假值。这个函数返回原来被限制分配的BDD。void test (Dd

45、Manager *manager , DdNode *node )DdNode *x0 = Cudd_bddIthVar(manager, 0) ;DdNode *x1 = Cudd_bddIthVar(manager, 1) ;const int SIZE=4;DdNode *restrictBySIZE ;DdNode *testSumSIZE ;DdNode *testCarrySIZE ;/ 通过如下方式来限制restrictBy0 = Cudd_bddAnd(manager, Cudd_Not (x0), Cudd_Not (x1); /x1=0 and x2=0restrictBy

46、1 = Cudd_bddAnd(manager, Cudd_Not (x0), x1); / x1=0 /and /x2=1restrictBy2 = Cudd_bddAnd(manager, x0, Cudd_Not (x1); / x1=1 /and /x2=0restrictBy3 = Cudd_bddAnd(manager, x0, x1); / x1=1 and x2=1for(int i = 0; i<SIZE; i+) Cudd_Ref(restrictByi); / 限制引用/ 通过一个新函数限制testSumi = Cudd_bddRestrict(manager, n

47、ode 0, restrictByi);testCarryi = Cudd_bddRestrict(manager, node1, restrictByi);Cudd_RecursiveDeref(manager, restrictByi); / 清理限制cerr << ” ( x1=0, x2=0): sum = ” << 1Cudd_IsComplement (testSum0)<< ” Carry = ” << 1Cudd_IsComplement(testCarry0) << endl<< ” (x1=0, x2=

48、1): sum = ” << 1 Cudd_IsComplement(testSum1)<< ” Carry = ” << 1 Cudd_IsComplement(testCarry1) << endl<< ” (x1=1, x2=0): sum = ” << 1 Cudd_IsComplement(testSum2)<< ” Carry = ” << 1 Cudd_IsComplement(testCarry2) << endl<< ” (x1=1, x2=1): sum

49、= ” << 1 Cudd_IsComplement(testSum3)<< ” Carry = ” << 1 Cudd_IsComplement(testCarry3) << endl;for(int i = 0; i<SIZE; i+) Cudd_RecursiveDeref(manager, testSumi);Cudd_RecursiveDeref(manager, testCarryi);4.3 打印BDDvoid toDot(DdManager *manager, DdNode *output s)char *inputName

50、s = new char *2; / 标记两个输入节点inputNames0 = new char3;inputNames1 = new char3;inputNames0 = ”x1”;inputNames1 = ”x2”;char *outputNames = new char *2; / 标记两个输出节点outputNames0 = new char4;outputNames1 = new char6;strcpy(outputNames0, ”sum”);strcpy(outputNames1, ”carry”);FILE *f = fopen(”./halfadder.dot ” ,

51、 ”w”);/ manager : CUDD管理器/ 2 : 输出的数量/ output s : 输出节点的数组/ inames : 输入名称图/ onames : 输出名称图/ f : 要写入的文件Cudd*DumpDot(manager, 2, outputs, inputNames, outputNames, f);4.4 主函数int main()/ 初始化管理器/ 0 : 初始化bdd变量的数目/ 0 : 初始化zdd变量的数目/ CUDD_UNIQUE_SLOTS: 初始化唯一表的大小（256）/ CUDD_CACHE_SLOTS : 初始化缓存大小 (262144)/ 0 : 最

52、大目标内存 (0 代表没有限制)DdManager *manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);/ 创建BDDDdNode *outputs = createHalfAdderBDD(manager);/ 写入BDD到一个点文件toDot(manager, outputs);test(manager, outputs);return 0;第五章 总 结5.1 结束语本论文所涉及的主要是在CUDD包中对BDD的应用，并以一个半加器程序为例子做了尽可能详细的论述。读者可以从中学习到BDD，OBDD，ROBDD，布

53、尔函数等相关理论知识，并且对CUDD软件包的基础架构有个大致的了解。通过最后的半加器实例程序，读者可以对CUDD包中有关BDD的一些函数有更形象的认识。本论文重点在于对CUDD的应用，所以对CUDD包的研究没有进一步深入的探讨，并且只涉及到BDD模块。而CUDD本身是一个功能强大的并且通用的软件包，应用非常广泛。5.2 研究动态和未来的发展1978年，S.B. Aker，提出了BDD的概念，之后，Lee,又引入了OBDD的概念(Ordered Binary Decision Diagram)。1986年，Bryant提出了ROBDD (ReducedOBDD精简有序二元决策图)。ROBDD利用传统的技术(如限定因子、香农展开、函数可满足集合等概念)消除BDD中同构图和冗余节点。自提出bdd概念以来，人们对它的研究成果层出不穷，其中本论文提及CUDD包，更是出类拔萃，它定义了决策图的数据结构,和决策图上的操作集和一系列算法（排序算法）：决策图的建立，遍历，排序，bdd、add、zdd之间相互转换，决策图上通用算法，ite算法以及