（计算机应用技术专业论文）bdd实现分析及其流化扩展.pdf

b d d 实现分析及其流化扩展 摘要 论文题目： 专业： 硕士生： 指导教师： b d d 实现分析及其流化扩展 计算机应用技术 吴家宝 张治国副教授 摘要 自从1 9 8 6 年r e b r y a n y 等人提出了二叉决策图( b i n a r yd e c i s i o nd i a g r a m s ) 的概念以来，由于其空间和时间上表示和处理布尔函数的高效性，b d d 被广泛应 用于大型数字系统设计中的逻辑功能验证、综合以及模型检测等方面且日益受到 重视。然而，传统的b d d 运算的实现主要基于哈希表技术，所以在处理大规模 b d d 运算时经常会遇到内存溢出问题。为了解决该问题有人提出如高效利用内存、 基于广度优先实现b d d 运算等方法，但由于b d d 规模过大或b d d 有些层节点过多， 内存溢出问题还是会出现。s h i n i c h im i n a t o 等人提出了基于流的b d d 运算模 型，可以从根本上解决这个问题。其主要思想是把b d d 转化为流，以流的形式作 为运算输入，内存只用作运算缓存而不用存储整个b d d 。 本文首先讨论了一个经典b d d 包( b u d d y ) 的具体实现，该包基于哈希表技 术采用深度优先算法实现简约有序二叉决策图( r o b d d ) 的运算。哈希表技术用 于保证r o b d d 的正则性。通过把哈希表和b d d 节点存储表整合到同一个大的数组， 提高了内存的利用率。运算过程中用动态规划避免了重复b d d 节点间运算，且可 以比较低耗的完成自动垃圾回收。由于这些技术的应用，b u d d y 在进行b d d 运算 时比其它b d d 实现包的效率高，但由于其基于哈希表技术所以会遇到内存溢出问 题。为此，本文在b u d d y 的基础上实现基于流的b d d 运算，将其作为一个新的运 算功能扩展到b u d d y 包中。在本文的最后部分给出一个用扩展后的b u d d y 包解决 大规模b d d 运算的实例，分析了流运算模型解决内存溢出问题的正确性和可行性。 关键词：二叉决策图( b i n a r yd e c i s i o nd i a g r a m s ，b d 劝，流式b d d 运算，b d d 运算，b u d d y ，模型检测 b d d 实现分析及其流化扩展a b s t r a c t t i t l e ： m a j o r ： n a m e ： s u p e r v i s o r ： t h ei m p l e m e n t a t i o na n a l y s i so fb d da n di t ss t r e a m i n g e x t e n s i o n c o m p u t e ra p p l i c a t i o na n dt e c h n o l o g y j i a b a ow u a s s o c i a t ep r o f e s s o rz h i g u oz h a n g a b s t r a c t s i n c et h ec o n c e p to ft h eb d d ( b t o r yd e c i s i o nd i a g r a m ) w a sp r o p o s e db y r e b r y a n ti n19 8 6 ，a st h e i re x c e l l e n te f f i c i e n c yi nt e r m so ft i m ea n ds p a c e ，b d di s n o wc o m m o n l yu s e df o rh a n d i n gb o o l e a nf u n c t i o n b d db r o a d l yu s e di nl a r g es c a l e i n t e g r a t e dc i r c u i ta n dc o m p u t e r - a i d e dd e s i g n , s u c ha sl o g i cf u n c t i o n a lv e f i f i c m i o nt e s t , s y n t h e s i z e ，m o d e lc h e c k i n ga n ds oo n h o w e v e r ，t h ec o n v e n t i o n a li m p l e m e n t a t i o no f b d dm a n i p u l a t i o na l g o r i t h mi s s t r o n g l yb a s e do nt h eh a s ht a b l et e c h n i q u e ，s oi t a l w a y se n c o u n t e r st h em e m o r yo v e r f l o wp r o b l e mw h e nh a n d i n gl a r g e - s c a l eb d d d a t a s e v e r a li d e a sh a v eb e e np r o p o s e dt os o l v et h ep r o b l e m ，s u c ha si n c r e a s i n gt h e e f f i c i e n c yo fm e m o r yu s e ，i m p l e m e n t i n gt h eb d dm a n i p u l a t i o nu s i n gb r e a d f i r s t a l g o r i t h ma n ds oo n h o w e v e l 勰e n d l e s sr e q u i r e m e n tf o rh a n d l i n gl a r g e s c a l eb d d a n dt h e “w i d t ho fb d d ”m a yb et o ol a r g e ，m e m o r yo v e r f l o wp r o b l e ms t i l lo c c u r s s t r e a m i n gb d dm a n i p u l a t i o nw a sp r o p o s e db ys h i n - i c h im i n a t o ，w h i c hc a l lh a n d l e v e r yl a r g e s c a l eb d db e y o n dt h em e m o r yl i m i t a t i o n t h i st h e s i sf i r s t l ya n a l y z e st h ei m p l e m e n t a t i o no fac l a s s i c a lb d d p a c k a g e ( b u d d y ) ，w h i c hi sb a s e do nt h eh a s ht a b l et e c h n i q u e ah a s ht a b l ei su s e dt o m a i n t a i nas t r o n gc a n o n i c a lf o r mi nt h er o b d d ，a n dm e m o r yu s ei si m p r o v e db y m e r g i n gt h eh a s ht a b l ea n dt h er o b d di n t o ab i gc o n t i g u o u s a r r a y b d d m a n i p u l a t i o ne f f i c i e n c yi si m p r o v e db yu s i n gr u l e st od e t e c tw h e ne q u i v a l e n tb d d n o d e sa r ec o m p u t e d t h eu s e f u l n e s so ft h ep a c k a g ei se n h a n c e db ya na u t o m a t i ca n d l o w - c o s ts c h e m ef o rr e c y c l i n gm e m o r y t h ep a c k a g ei ss i g n i f i c a n t l yf a s t e ra n dm o r e m b d d 实现分析及其流化扩展 a b s n a c t m e m o r y - e f f i c i e n tt h a no t h e rb d dp a c k a g e s h o w e v e r , i ts t i l le n c o u n t e r st h em e m o r y o v e r f l o wp r o b l e m 雒i ti sb a s e do i lh a s ht a b l et e c h n i q u e w i t ht h ew e l lk n o w l e d g eo f b u d d y , w ei m p l e m e n tt h es t r e a m i n gb d dm a n i p u l a t i o n , w h i c hb ea d d e di nb u d d y 船an e wf u n c t i o n a lm o d u l e a tl a s t al a r g es c a l eb d d c o m p u t a t i o nt a s ki ss o l v e db y t h ee x t e n d e db u d d y a n dt h ee x p e r i m e n t a lr e s u l t ss h o wt h a tt h es t r e a m i n gb d d m a n i p u l a t i o nm o d e lo v e r c o m e st h em e m o r yo v e r f l o wp r o b l e m k e yw o r d s ：b i n a r yd e c i s i o nd i a g r a m s ，b d d ，s t r e a m i n gb d dm a n i p u l a t i o n , b u d d y , m o d e l c h e c k i n g 论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独 立进行研究工作所取得的成果。除文中已经注明引用的内容外，本论 文不包含任何其他个人或集体已经发表或撰写过的作品成果。对本文 的研究作出重要贡献的个人和集体，均已在文中以明确方式标明。本 人完全意识到本声明的法律结果由本人承担。 学位论文作者签名：墨宝室 日期：羔旦! 些? 学位论文使用授权声明 本人完全了解中山大学有关保留、使用学位论文的规定，即：学 校有权保留学位论文并向国家主管部门或其指定机构送交论文的电 子版和纸质版，有权将学位论文用于非赢利目的的少量复制并允许论 文进入学校图书馆、院系资料室被查阅，有权将学位论文的内容编入 有关数据库进行检索，可以采用复印、缩印或其他方法保存学位论文。 学位论文作者虢曼必导师签名数同 日期：占q 【o 年6 月_ 日 日期锄i o 年6 月力日 b d d 实现分析及其流化扩展第1 章绪论 第1 章绪论 1 1 研究背景与问题陈述 在很多硬件与软件系统设计中，布尔函数是一种重要的形式描述机制。b d d 由于其时间和空间上的高效性，其被广泛用于大型数字系统设计中的逻辑功能验 证、综合以及模型检测等方面【3 】 4 1 【5 1 1 2 4 。目前已经有很多研究人员对b d d 的操 作做了实现【8 】【1 6 】 1 4 】【1 7 】 1 8 】，这些b d d 实现包都在现实生活中都有广泛应用。 在传统的b d d 包( 如：b u d d y ，c u d d 等) 中，整个b d d 表示的数据结构 都存放在主存中，当逻辑运算一遍一遍的执行后，产生的中间b d d 个数，以及 每个b d d 的规模可能会非常迅速的增长，最后由于内存溢出导致运算失败。一 般情况下，我们是无法知道b d d 运算中所需最高内存是多少，所以内存溢出是 必须要考虑的问题。这也是基于b d d 运算的一个常见的缺点。 导致b d d 运算的过程中内存溢出的主要原因是是其靠哈希表技术来保证产 生的b d d 节点都是唯一的。用哈希表技术就必须能进行随机存储，所以当内存 不够时，就会溢出导致计算失败。 因此，对于超大规模的b d d 运算通常考虑的不仅仅是时间或空间上的效率 问题，更多的是能不能成功执行相关b d d 运算。 相关研究人员对如何正确执行大规模b d d 运算而不受内存大小的限制做了 很多努力。传统的b d d 运算时基于深度优先的，于是h o c h i 等人就提出了基于 广度优先的b d d 运算【1 9 1 。这种算法根据输入变量把b d d 按层切成一层一层， 然后一层一层的对b d d 进行运算。这样对大规模b d d 运算时就可以在硬盘中 读入一层b d d 数据然后在主存中对其运算。b y a n g 等人后来提出了深度优先和 广度优先混合的b d d 运算【2 0 】。但这些解决办法都存在一个问题，在读入一层 b d d 结点时，当该层b d d 结点很多( b d d 的结构很宽) 时，内存溢出问题还 是会发生。s h i n i c h im i n a t o 等人提出了基于流的b d d 运算模型【捌，可以从根 本上解决这个问题。其主要思想是把b d d 转化为流，以流的形式作为运算输入， 主存空间只用作运算缓存，不用存储整个b d d ，计算结果也是以流的形式输出。 b d d 实现分析及其流化扩展 第】章绪论 目前一些b d d 实现包，基本上都是基于哈希表技术实现的b d d 运算，所 以在实际应用中对超大规模b d d 运算时都会遇到前面所提到的内存溢出问题。 一个可以从根本上解决该问题实现基于流运算的b d d 实包还现尚待研发。本文 主要的工作就是实现一个可以从根本上解决大规模b d d 运算可能遇到的内存溢 出问题的b d d 包。b u d d y 是一个经典的比较高效的开源b d d 实现包，该包基 于哈希表技术采用深度优先算法实现简约有序二叉决策图( r o b d d ) 的运算。 哈希表技术用于保证r o b d d 的正则性。通过把哈希表和b d d 节点存储表整合 到同一个大的数组，提高了内存的利用率。运算过程中用动态规划避免了重复 b d d 节点间运算，且可以比较低耗的完成自动垃圾回收。由于这些技术的应用， b u d d y 在进行b d d 运算时比其它b d d 实现包的效率高，但由于其几乎所有的 操作都基于哈希表技术所以内存溢出问题经常会出现。 为了解决该问题，本文首先讨论了b u d d y 包的具体实现，然后比较详细的 介绍s h i n - i c h im i n a t o 等人提出了基于流的b d d 运算模型理论，对应流数据的 格式及如何转换，并且对基于流的逻辑运算及其算法进行深层次的分析。基于上 面的工作，我们在b u d d y 的基础上实现基于流的b d d 运算的各个功能模块， 将基于流的b d d 运算作为一个新的运算功能扩展到b u d d y 包中。形成一个可 以处理大规模b d d 运算而不会出现内存溢出问题的b d d 实现包。在实际应用 中可以根据不同的需求，调用扩展后的包不同的运算接口( 传统或基于流) 解决具 体问题。 1 2 研究现状 为了解决大规模b d d 运算的内存溢出问题，2 0 0 2 年s h i n i c h im i n a t o 等人 在提出了基于流的b d d 运算阱】。这种基于流而实现的b d d 运算，不会造成内 存溢出等问题。b d d 数据是以流的方式进行输入输出，内存只是用来一个做流 运算的缓存，而在传统的b d d 运算中，内存要存储整个b d d 数据。基于该模 型实现的b d d 运算，由于可以通过网络来存取b d d 数据流，使得参与运算的 b d d 规模不仅可以不受内存大小的限制，而且可以不受硬盘空间大小的影响，。 目前有很多的传统的b d d 包，有基于深度优先实现的( 如：b u d d y ，c u d d ) ， 2 b d d 实现分析及其流化扩展第1 章绪论 有基于广度优先实现的( 如：c a l ) 0 9 ，也有混合的方法实现b d d 运算( 如： y a n g a l lc h e n sb d dp a c k a g e ) 1 2 0 。其中b u d o y 在b d d 的运算操作方面相对于 其它的一些b d d 实现包效率都高。但这些对与超大规模b d d 运算时这些包都 会出现上面所说的内存溢出问题。目前还没有一个b d d 实现包，既可以对一些 小规模b d d 进行高效的运算，又可以处理大规模b d d 运算的内存溢出问题。 虽然可以用不同的包来计算不同的b d d ，但b d d 的存储就不能得到统一，容易 造成不必要的麻烦和其他一些问题。因此本文就是在高效的b d d 包b u d d y 的 基础上实现基于流的b d d 运算，并作为一个新的运算功能扩展到该包中，形成 一个功能完善，能灵活正确处理大规模b d d 运算的b d d 包。 1 3 论文组织 本文首先讨论了一个经典b d d 包( b u d d y ) 的具体实现，分析了其一些核 心算法及相关机制实现细节。而后引入s h i n i c h im i n a t o 等人提出的基于流的 b d d 运算，在b u d d y 的基础上实现了基于流的b d d 运算，并作为一个新的运 算功能扩展到该包中，形成一个功能完善，能灵活正确处理大规模b d d 运算的 b d d 包。最后给出了一个用扩展后b d d 包解决大规模b d d 运算的例子。 在论文结构上，全文共分为7 章，其中第一章是对现有的理论和研究的总结 和分析；第三、四、五、六章是本文的重点，也是作者的主要工作。各章的主要 内容说明如下： 第一章，主要介绍了b d d 运算问题的背景，目前国内外研究的现状和本文 主要的研究工作。 第二章，主要介绍了b d d 及其运算的一些基本概念。 第三章，对经典的一个开源b d d 实现包b u d d y 进行深度分析，并给出了一 个实例应用。 第四章，引入s h i n i c h im i n a t o 等人提出基于流的b d d 运算，分析其基本原 理以及在本文在重新实现该算法时用到一些相关基本概念和方法。 第五章，在b u d d y 的基础上实现基于流的b d d 运算并将其整合到b u d d y 包中。 3 b d d 实现分析及其流化扩展 第1 章绪论 第六章，主要是对前面完成的整合后的b d d 实现包进行相关实验测试，并 对结果进行分析。 第七章，是结束语，是对本文的简要总结，以及对未来的工作的展望。 4 b d d 实现分析及其流化扩展第2 章二叉决策图 第2 章二叉决策图 二叉决策图( b i 肋d ，d e c i s i o nd i a g r a n 】s ) 的概念【l 】是由r e b r y a n y 等人1 9 8 6 年提出的。由于其空间和时间上表示和处理布尔函数的高效性，被广泛应用于大 型数字系统设计中的逻辑功能验证、综合以及模型检测等方面。本章给出了b d d 一些基本定义及其构造与操作。 2 1 基本定义 定义2 11 2 5 1 对于( 0 ，1 ) n 到( 0 ，1 ) 的布尔函数厂( x 1 ，x 2 ，x n ) ，二叉决策图( ( b i i l i 珂 d e c i s i o nd i a g r a m ，b d d ) 是用于表示布尔函数族# 厂( x 1 ，x 2 一，) 的一个有向无 环图，它满足： 1 ) b d d 节点分为根节点、终节点和内部节点三类。没有父辈节点或者没有输入 弧的节点称为根节点；没有后继子节点或者没有输出弧的节点称为终节点； 除根节点和终节点之外或者具有输入和输出弧的节点称为内部节点。 2 ) 终节点仅有2 个，分别标记为o 和1 。每一个终节点t 具有属性c u a l ( 0 ，1 ) ，表 示布尔常量0 和l 。 3 ) 每个非终节点u 具有四元组属性( 厂札，v a t ，l o w ，h i g h ) ，其中，厂u 表示节点u 所对应的布尔函数；v a i 表示节点u 的标记变量；l o w 表示1 1 v 盯= o 是，节点 u 的o 一分支子节点；h i g h 表示u v a r = l 时，节点u 的1 - 分支子节点。 4 ) 每个非终节点均具有两条输出分支弧，将它们和各自的两个分支子节点连接 在一起。节点u 和u 1 0 w 的连接弧称为0 边，节点u 和u 1 l i g l l 的连接弧称为 1 边。 5 ) b d d 的任一有向路径上，布尔函数f ( x 1 ，x 2 ，) 中的每个变量至多出现一 次。 在b d d 的图形表示中，通常用方框表示0 、l 终节点，用圆圈表示其他节点， 节点之间通过虚线或实线连接。通常，假设连接弧的方向向下，0 边用虚线表示， 5 b d d 实现分析及其流化扩展第2 章二叉决策图 1 边用实线表示。 例如图2 - l 所示为布尔函数厂= ( x l 铮y o a 2 营y 2 ) 所对应的- - y 决策图。 从b d d 的定义及上面的图形表示示例中可以看出，对于布尔函数中变量的 一组赋值，其函数值是由从根节点到一个终节点的一条路径决定，而这条路径所 对应的分支由这组变量赋值决定，该分支节点的终节点标记的值就是变量在这组 赋值下的所得的函数值。 图2 - 1 布尔函数厂= ( 魂营y t ) 2 营y 2 ) 所对应的二叉决策图 2 2 有序二叉决策图 b r y a n t 等人对b d d 附加了变量序和简化约束【2 】，引入了有序二叉决策图 ( o r d e r e db i n a r yd e c i s i o nd i a g r a m ，o b d d ) 和简化的有序二叉决策图( r e d u c e d o r d e r e db i n a r yd e c i s i o nd i a g r a m ，r o b d d ) ，使b d d 成为表述布尔函数的一种规范 型。有序二叉决策图( o b d d ) 不同于普通b d d 之处在于，o b d d 中任一根从根 节点到叶节点的路径上变量出现的顺序保持一致。下面是从文法和语法两个方面 对o b d d 进行定义。 定义2 - 2 口习对于( 0 ，1 ) n n o ，1 ) 的布尔函数f u 和给定的变量序弧，在表示布尔函数 族# f ( x 1 ，x 2 ，x n ) 的二叉决策图( b d d ) 中，如果任一有向路径上的变量 6 b d d 实现分析及其流化扩展 第2 章二叉决策图 x l , x 2 ，x n 均以变量序霞所规定的次序次出现，则称该b d d 为布尔函数 f ( x 1 ，x 2 一，x n ) 的有序二叉决策图。 定义2 - 3 2 5 1 每个o b d d 上的节点u 表示一个从( 0 ，1 ) n 到( 0 ，1 ) 的布尔函数f u ，满足： 1 ) 若u 是终节点，则f u = u 。v a l 。 2 ) 若u 是非终节点，则 f u = u v a r f u h i g h + ( u v a 0 7 f u - l o w = u v a r 骷v a r ：1 + ( u v a r ) 骷v a r ；o 其中，聪v a r 一1 和f u v a r = o 分别表示布尔函数f u 中的变量u v a t 取值1 和0 后所 得到的布尔函数，即节点u h i g h 和u 1 0 w 所对应的布尔函数。 定义2 - 4 【2 5 1 在有序二叉决策图( o b d d ) 中，如果内部节点满足： 1 ) 对于节点u ，u 1 0 w u h i 曲。 2 ) 对于u v a r = v v a r 的不同节点u 和v ，则u 1 0 w v 1 0 w 或者u h i t h v h i 曲或 者u 1 0 w v 1 0 w 且u h i g h v - h i 曲。则称该o b d d 为简化的有序二叉决策 图( r e d u c e do r d e r e db i n a r yd e c i s i o nd i a g r a m ，r o b d d ) 【1 】【2 】。 对于不满足定义2 3 中条件的o b d d ，可以应用如下简化规则，将o b d d 简化为r o b d d ： 赢例j 停嬲豫规则) ：对于o b d d 中的节点u ，如果u 1 0 w = u h i g h ，则删 除节点u ，并将节点u 的父节点直接连接至u 1 0 w 所对应的节点。 删2 ( ，兮孝规则) ：对于o b d d 节点中的节点u 和v ，如果u v a r = v v a r ， u 1 0 w = v 1 0 w ，且u 1 l i 曲孔b j 曲，则删除节点u ，并将节点u 的父节点直接连接至 节点v 。 定义2 - 51 2 5 香农展开：f = ( x f i x = o ) + ( x - f | x ；1 ) ，其中 f l x i = a ( x l ，x 2 ，x n ) = f ( x 1 ，x i l ，a ，x i + l ，x n ) 表示布尔函数厂中的变量x i 赋值 为a ，利用香农展开可以把复杂的布尔函数一步一步展开为一些简单的布尔函数。 7 b d d 实现分析及其流化扩展 第2 章二叉决策图 2 3o b d d 的构造与操作 o b d d 的构造可以通过简单的递归过程来实现，在后面的章节里我们将详细 叙述如何递归构建一个o b d d 。而构造一个r o b d d 的方法主要有一下两种：第 一种方法是先构造对应o b d d ，然后调用相关的简化函数对其进行简化；另一种 方法是在构造o b d d 的过程中同时应用简化规则( 前面介绍的规则1 和规则2 ) 对o b d d 进行简化。 o b d d 是表示布尔函数的一种等价规范型1 6 ，布尔函数的许多运算都可以 转换为对应o b d d 的符号操作。o b d d 的符号操作在时间和空间的高效性是其 得到的广泛应用的重要原因。在实际应用中我们经常用到的有如下这些基本的运 算操作，如：逻辑复合( a p p l y ) 、i t e 操作、函数求值、等价性判定、可满足性 判定、置换、全称量化、和存在量化等。当然，这些要进行这些o b d d 基本操 作的前提是参与操作的o b d d 已经构建出来了。 2 4 本章小结 本章首先介绍了二叉决策图( b d d ) 的基本定义，让我们理解什么是二叉决 策图，其有哪些基本特性，而后引入有序二叉决策图( o b d d ) 以及简约的有序 二叉决策图( r o b d d ) 的定义和其必须满足的一些性质。接着简单介绍了关于 o b d d 的构造和操作。为接下来各章节所要讨论的内容做一个铺垫。本文后面所 有提到的b d d 若不做特殊说明都指的是r o b d d 。 8 b d d 实现分析及其流化扩展第3 章b u d d y 实现分析 第3 章b u d d y 实现分析 3 1 b u d d y 简介及相关术语 b u d d y 是一个用c 语言实现的b d d 的实现包，其支持几乎所有的b d d 运 算。该包是基于哈希表技术采用深度优先算法实现简约有序二叉决策图( r o b d d ) 的运算，哈希表技术用于保证r o b d d 的正则性。通过把哈希表和b d d 节点存储表 整合到同一个大的数组，提高了内存的利用率。运算过程中用动态规划避免了重 复b d d 节点间运算，且可以比较低耗的完成自动垃圾回收。由于这些技术的应用， b u d d y 在进行b d d 运算时比其它b d d 实现包的效率高。b u d d y 中实现多中变量 排序算法，可以很方便根据不同需求去实现b d d 优化。b u d d y 对b d d 运算时其 性能和一些相关运行参数配置很有关系，例如最大的节点数，什么时候开始停止 运算进行垃圾回收，什么情况下对变量进行重排序等。这些参数在b u d d y 都有 一个默认的值，你可以根据具体的实际应用配置这些参数来使b d d 运算的效率 达到最高。b u d d y 很方便使用，用少量的代码就可以完成一些比较复杂的b d d 运算，而且其效率和可配置性也非常高。 下面在对b u d d y 包进行分析时用到的相关术语见下表： 表3 - 1b u d d y 包相关术语 b d d b i n a r yd e c i s i o nd i a g r a m s ( 二叉决策图) b d dt a b l e b u d d y 中用于存储b d d 的表 v a r i a b l e ss e t s b d d 一些变量的集合 v a r i a b l eo r d e r i n g o b d d 中变量序 d y n a m i cv a r i a b l er e o r d e r i n g 动态变量排序 v a r i a b l el a b e l i n g 变量的标签，也即变量序号 b d d p a i r b d d 对，用于变量替换中 r e f e r e n c ec o u n t引用计数 b d dv a r i a b l es e t 变量集，在包中的表现形式 1 a x 2a ) v a r i a b l eb l o c k s 变量中某一区间变量的集合，或块的集合 9 b d d 实现分析及其流化扩展 第3 章b u d d y 实现分析 3 2 b u d d y 的体系结构 这里我把b u d d y 主要分为5 个模块： 1 b d d 的一些数据结构表示和b d d 运算中所需的一些核心功能( k e r n e l b d do p e r a t i o n sa n dd a t as t r u c t u r e s ) 2 反映当前一些b d d 的相关信息模块( i n f o r m a t i o no nb d d s ) 3 输入与输出的模块( f i l ei n p u t o u t p u t ) 4 b d d 运算模块( b d do p e r a t o r s ) 5 变量排序模块( v a r i a b l er e o r d e r i n g ) 其体系结构图如下： 图3 - 1b u d d y 体系结构 从图3 1 可以看出，b u d d y 的体系结构比较简单，核心的就是k e r n e lb d d o p e r a t i o n sa n d d a t as t r u c t u r e s 模块和b d do p e r a t o r s 模块。各个模块之间的通讯基 本上都是通过全局变量，其中最核心的就这几个：b d dt a b l e 、b d dc a c h es t a t 、 b d dg b es t a t 、b d ds t a t 。通过这几个全局变量各个模块之间可以协调的运作， 执行相关b d d 操作。创建b d d 的过程也a p gj j 建一些变量和执行一步步运算 b d d 的过程，得到的结果就是所需的b d d 。这些过程也就在b d dt a b l e 上修改 相应节点信息的过程。k e r n e lb d do p e r a t i o n sa n dd a t as t r u c t u r e s 模块即定义这些 全局变量以及提供配置b u d d y 包运行参数的接口。i n p u t 和o u t p u t 模块是从b d d 1 0 b d d 实现分析及其流化扩展 第3 壹b u d d y 实现分析 包与外部存储的b d d 进行读写的接口。b d do p e r a t o r s 模块提供的是对b d d t a b l e 中的b d d s 进行相关运算功能，运算的结果当然也是存放在该b d dt a b l e 中。运算的过程中为了避免相同b d d 节点的重复运算会用到b d dc a t c h 来做一 些缓存。同样运算过程中也会有变量排序和自动垃圾回收操作的执行。当你要查 询一些b d d 本身的一些相关信息时，b u d d y 通过i n f o r m a t i o no nb d d s 提供的相 关的接口，该模块也即去对b d dt a b l e 进行相关的查询并返回结果。整个b u d d y 的体系非常的紧凑，效率也非常高。 3 3 模块分析 3 3 1 数据结构和关键运算模块 该模块和即将提到的b d d 运算模块是b u d d y 的核心模块。该模块中主要包 括一些关键的数据结构的定义，一些全局变量的定以义及提供一些设置b d d 包 的运行参数和查询及控制b d d 包的全局性性质的接口。b u d d y 中的垃圾回收相 关的操作也是该模块所提供的功能，本节除了介绍一些关键的数据结构，后面会 详细分析下b u d d y 中垃圾回收算法的实现。 l ? 主要的数据结构 这些数据结构主要包括b d d 中节点sb d d n o d e ，反映b d d 包状态信息的 sb d d s m t ，反映当前垃圾回收状态的sb d d g b c s t a t ，以及反映当前缓存区使用情 况的sb d d c a c h e s t a t 。这些数据结构的定义如下： 1 ) b d d 中节点数据结构sb d d n o d e b d d 实现分析及其流化扩展第3 章b u d d y 实现分析 2 ) 反映b d d 包状态的s b d d s t a t 3 ) 反映垃圾回收状态的s b d d g b c s t a t 4 ) 当前缓存区使用情况的s b d d c a c h c s t a t 我们这里简单举个例子来说明各个步骤的主要操作，以及b u d d y 包的一些 实现机制。该例子的主要代码如下： 1 2 b d d 实现分析及其流化扩展 第3 章b u d d y 实现分析 下面是这个例子的b d d 表示： 图3 22 个b d d 的a n d 运算 其计算结果在b u d d y 中的所对应b d d 的t a b l e 如表3 一l 所示： 表3 1 运算结果b d d t a b l e n r e f o ul e v e ll o w h i 曲 h a s hn e x t 01 0 2 33o0o1 11 0 2 33 1182 21 0 2 3 o o120 31 0 2 301ooo 4 1 0 2 3 1 o1oo 51 0 2 3110oo 6 1 0 2 32 o100 71 0 2 321045 8 l004 o3 90 0 161 0 l oo0171 1 1 1oo- 1 oo 1 3 b d d 实现分析及其流化扩展第3 章b u d d y 实现分析 表3 - 2 初始化后b d dt a b l e nr e f o ul e v e ll o w i l i 曲 h a s hn e x t 01 0 2 3oo0o1 11 0 2 30l1o2 2 oo1 0 3 3o0104 400105 n0o100 1 ) 在所有工作开始的时候进行的是b d d 的初始化操作，然后是设置b d d 的一些相关配置参数，如：设置b d d 的节点数，变量数，缓存大小，最小可以 节点数的控制等。初始化后的b d dt a b l e 如表3 2 所示，在表中的第一个和第二 个节点比较特殊，分别表示b d d 中的终节点o 和l 。 反映当前缓存区使用情况的s b d d c a c h e s t a t 的所有域全部初始化为o ，结过 如表3 3 所示： 表3 - 3s _ b d d c a c h e s t a t 初始化结果 b d d c a c h e s t a t e u n i q u e a c c e s su n i q u e c h a i nu n i q u e h i ti o p h i r i o m i s s s w a p c o u n t 0 o 2 ) 所有初始化工作完成之后及可以设置变量数，添加变量，添加节点数， 获取变量对应的具体b d d ，自动或手动执行垃圾回收等操作。设置变量数的操 作比较重要，因为这个操作要产生一些b d d 运算过程中都要使用到的辅助数据 结构，主要的有以下几个： 1 4 b d d 实现分析及其流化扩展 第3 章b u d d y 实现分析 i m d v a r s e t hl n o t e t a b l e 中该变量所在的位 图3 - 2b d d v a r s e t 结构，其中n u m 为变量数 广 2 * h u mi i 一 该数组主要是存储每个基本变量在b d dt a b l e 中对应的位置，在上面例子中 x = b d d i t h v a r ( o ) 是获取第0 个变量( x o ，0 ，1 ) ，也即返回b d d v a r s e t 0 】；而 y = b d d i t h v a r ( o ) 贝u 返回b d d v a r s e t 3 ；每个变量的引用计数都是最大值做如下 初始化： i i b d d l e v e l 2 v 口， f f 和上面的相反 匝三二h 亚正口工 团 叵三三h 王口互工二 团 图3 - 3b d d v a r 2 1 e v e l 和b d d l e v e l 2 v a r 结构，其中l l u r f l 为变量数 上面2 个数据结构是必须的，由于r o b d d 的变量序对其大小的影响非常大， 所以b u d d y 在节点空间不足时会做一些变量排序工作，为了能正确获取排序后 b d d 中每层的节点的变量序，所以要对这些变量序的调整要做标记。初始的b d d 节点的层数即为该节点对应变量在变量中的次序，所以初始化的结果即为图3 3 一所不o i v b d d r e f s t a c k f f 内u - e f f b d d 节点的引甬栈 1 5 b d d 实现分析及其流化扩展 第3 章b u d d y 实现分析 、 2 * n u m + 4 厂 fb d d r e f s t a c k t o p 卜 l b d d r e f s t a c k 卜 图3 - 4b d d r e f s t a e k 结构，其中l l u m 为变量数 b d d 运算其实是一个递归的过程，为个更好的管理和利用每个递归的计算 结果，就用此栈来完成。 添加节点和添加变量的过程和开始设置变量和设置变量数的过程是类似的， 就是增加上面提到的这些数据结构的大小并作初始化即可。 3 ) 待所有的b d d 运算结束后须进行收尾的工作，即释放所有的空间。 3 。垃圾回收机翩 在前面的介绍中，每个b d dt a b l e 的每一个表项的第2 个元素r c f c o u 是该节 点的引用计数，该元素是b u d d y 进行垃圾回收运算时所依赖的主要信息。在对 一个b d dt a b l e 进行初始化的过程中，首先会把所有节点的r c f c o u 初始化为o ， 除了0 和1 节点，其r c f c o u 为最大值。按照对b d d 计算的步骤，我们首先得设 定变量数n ，每个变量对应t a b l e 中2 个节点，分别表示该变量取0 和取l 对应 的b d d 。这2 x n 个节点的r c f c o u 也为最大值，因为终节点和这些变量节是所有 b d d 构建和运算过程中最基本的节点，无须对其进行引用计数操作也即无须对 其进行垃圾回收操作。在b d d 的运算过程中每建立或取消对一个节点的引用都 要对这些相关节点的r c f c o u 进行加或减的操作。函数b d da d d r e f ( b d dr o o t ) 和 b d d _ d e l r e f ( b d dr o o t ) 分别是完成对r o o t 所指向的节点的r e f c o u 进行加或减的操 作。为了让b u d d y 垃圾回收机制正确的运行，所以在所有的b d d 运算操作中 用户得自己去对每一个新创建的b d d 节点实施b d da d d r e f 操作，若该b d d 以 后不再使用时再对该b d d 进行b d dd e l r e f 操作。 1 6 b d d 实现分析及其流化扩展第3 章b u d d y 实现分析 图3 5 垃圾回收过程 还是用上面的例子，初始化和设置变量分别对应b d d b d ds e t v a m u m 0 ； 接下来的2 步操作只是获取相关变量的基本b d d 而没有增加节点所以x 和y 没 有必要去增加引用计数，z 是x 合取y 的结果，其所对应的节点是新增的节点， 所有要对去r e f c