（微电子学与固体电子学专业论文）vlsi中形式化的组合电路等价验证方法.pdf

y6 5 2 3 1 8 摘要 随着集成电路技术的飞速发展，电路的规模也不断增大。电路验证领域正面 临前所未有的挑战， 如何快速并且完备地完成超大规模集成电路的等价验证， 己 经成为当前的研究热点。 与传统的基于模拟的验证方法相比， 形式化的验证方法具有完备性的优点。 本文提出的形式化的大规模集成电路中组合电路的等价验证方法主要的创新之 处在于: ( 1 ) 基于层分划的等价配对点生成方法。 这方法可以大大提高配对点的 命中率，并降低配对点的生成时间， 从而大大加快整个验证的速度。 ( 2 ) 基于闻 值的错反问 题( f a l s e n e g a t i v e ) 回溯控制。 有效地选取回溯的时机， 控制无效回溯 次数， 保证计算的效率。 ( 3 ) 基于s a t问 题解决框架的子电路分划。 将电 路的分 划、回溯等过程，有机地融入s a t问题d l l算法解决框架之中，避免了反复回 溯中的 重复计算， 并结 合s a t % 7 题研究 在b c p ( b o o l e a n c o n s t r a i n p r o p a g a t i o n ) 和 变量选择方面比较成功的技术，加快验证的速度。 此外，我们的验证算法具有很强的灵活性。对于内部，子电路的验证上可以 调用不同的s a t s o l v e r 来完成; 对于外部， 可以 作为独立的 等价电 路验证软件 使用，也可以作为一个模块被其他算法调用，比如用于时序电路的等价验证。 关键词:等价验证、配对点、电路分划、回溯控制 卿 ;3梦 作补、 导师禅件 a; ab s t r a c t wi t h f a s t e v o l u t i o n o f i c t e c h n o l o g y , t h e s c a l e o f c ir c u i t s i s a l s o b e c o m i n g b i g g e r a n d b i g g e r . v l s i c i r c u i t v e r i fi c a t i o n e n c o u n t e r e d e n o r m o u s c h a l l e n g e s t o fi n i s h e q u i v a l e n c e c h e c k i n g c o m p l e t e l y w h i l e e ff i c i e n t l y . n o w f o r m a l v e r i fi c a t i o n , e s p e c i a l l y i n e q u i v a l e n c e c h e c k i n g , h a s b e c o m e t h e h o t s p o t o f r e s e a r c h c o m p a r e d w i t h t r a d i t i o n a l v e r i f i c a t i o n m e t h o d w h i c h w a s b a s e d o n s i m u l a t i o n , f o r m a l v e r i f i c a t i o n h a s i t s a d v a n t a g e i n c o m p l e t e n e s s . t h e m a i n c o n t r i b u t i o n s o f t h i s t h e s i s a r e : ( 1 ) l e v e l b a s e d p a rt i t i o n i n g i n c a n d id a t e e q u i v a l e n t p a i r g e n e r a t i o n . t h i s w o u l d g r e a t l y e n h a n c e t h e h i t t i n g r a t e o f r a n d o m s i m u l a t i o n , a n d r e d u c e t h e t i m e c o s t o f c a n d id a t e p a i r g e n e r a t i o n . ( 2 ) t h r e s h o l d b a s e d b a c k t r a c k c o n t r o l i n f a l s e n e g a t i v e p r o b l e m . wi t h h e u r i s t i c a l l y s e l e c t e d t h r e s h o ld v al u e , w e c o u l d c o n t r o l t h e u s e l e s s b a c k t r a c k b e l o w a r e a s o n a b l e l e v e l s o a s t o g u a r a n t e e t h e e f f i c i e n c y o f o u r al g o r i t h m ( 3 ) s u b - c i r c u i t p a rt i t i o n i n g i n s a t s o l v e r fr a m e w o r k . we m e r g e d t h e w h o l e v e r i f i c a t i o n p r o c e s s , w h ic h in c l u d e s p a r ti t i o n , b r a n c h v a r i a b l e s e l e c t i o n , b a c k t r a c k i n g a n d e t c ., i n t o s a t s o l v e r . t h i s c o u l d h e l p i m p r o v e t h e s p e e d o f o u r a l g o r i t h m b y a v o i d i n g r e d u n d a n t c a l c u l a t i o n . b e s i d e s , t h e p r e s e n t e d a l g o r it h m i s a l s o v e ry fl e x i b l e . f o r i n t e rna l s u b - c i r c u it v e r i f i c a t i o n , i t c o u l d a d o p t a n y s a t s o l v e r a s t h e c o m p u t i n g e n g i n e . f o r e x t e rn a l u s a g e , i t c o u l d b e u s e d a s a n i n d e p e n d e n t e q u i v a l e n c e c h e c k i n g s o ft w a r e , o r a s a m o d u l e t o b e e m b e d d e d i n t o o t h e r a p p l i c a t i o n s , s u c h a s s e q u e n t i a l c i r c u it v e r i fi c a t i o n . k e y w o r d : e q u i v a l e n c e c h e c k i n g , c a n d i d a t e p a i r , c i r c u i t p a r t i t i o n i n g , b a c k t r a c k co n t r o l i t 第一章绪论 第一章绪论 1 . 1现代集成电 路技术的发展 自 六十年代初第一块集成电路诞生到现在， 集成电路技术已从初期的几十个 元 件， 很 快跨越了 中 小规 模， 大规 模和超大规 模， 直到 今天g i g a s c a l e 的阶 段。 近四十年来，集成电路技术的高速发展主要表现在以下三个方面: ( 1 )电 路 规模日 益 增大。 根据m o o r e 定 律， 数字集 成电 路的 规模以 每1 8 个月 翻 一番的速度持续增长。六十年代初期，一片集成电路只能集成几个晶体管。 而现在的 奔腾ii i 处理器中， 晶体管数就已 达到2 8 0 0 万个。 1 g ( 千兆) 位存储 器己经问世。目 前的工艺水平与器件的基本物理极限还有相当的距离， 因此 可以预测芯片的集成度仍有很大的增长空间。 ( 2 )工作速度不断提高。 根据有关报道， 八十年代初期微处理器芯片的工作频率 一般为 1 mh z左右，而当今的微处理器芯片其时钟频率可高达几个 g h z . 例如，i n t e l 公司最近推出时钟主频3 .6 g h z的芯片，a md公司也己推出主 频超过2 . 8 g h z 的产品，同时i n t e l 正在研究主频约为 l o g h z 的新一代数字 芯片。 ( 3 )特征尺寸持续 减小。 近十 年来， 集成电 路的 最小 特征尺寸经历了0 . 2 5 1 a m , 0 . 1 8 11 m, 0 . 1 3 8 m等一系列变化。目前，i n t e l 公司己经推出t 0 .0 9 u m的 工艺技术。 表1 - 1 给出了n a t i o n a l t e c h n o l o g y r o a d m a p s e i a 9 7 在1 9 9 7 年 对半导体业未 来所作出的预测。 而当今集成电路的实际发展状况有些己超过了当初的预测， 这 充分说明集成电路技术发展的日新月异。 ye a r1 9 9 71 9 9 9 2 0 0 12 0 0 32 0 0 6 2 0 0 9 t e c h n o l o g y ( u m ) 0 . 2 50 . 1 8 0 . 1 50 . 1 30 . 1 00 . 0 7 t r a n s i s t o r s 1 1 m 21 m4 0 m7 6 m2 0 0 m 5 2 0 m o n - c h i p c l o c k ( m h z ) 7 5 0 1 2 0 01 4 0 01 6 0 02 0 0 0 2 5 0 0 a r e a (mm) 3 0 0 3 4 03 8 54 3 05 2 0 6 2 0 wi ri n g l e v e l s 6 6 - 7777 - 8 8 - 9 表1 - 1国家技术道路1 9 9 7 年对半导体业未来所作出的预测 第一章绪论 1 .2本文的 研究背景和内 容 随着集成电路设计和制造技术的不断进步，半导体集成化芯片系统( 简称 s o c ) 成为国际超大规模集成电路发展的趋势和二十一世纪集成电路技术的主 流。但随着复杂度和规模的不断增加，s o c的验证和测试也变得越来越复杂。 据统计，验证过程消耗了整个设计周期的三分之二，甚至高达 9 0 %。功能验证 己 经成为s o c设计的瓶颈。传统的基于模拟的 验证方法在编写测试向量、生成 测试程序等方面就要耗费大量的时间， 况且， 模拟不可能是无穷尽的， 它很难发 现那些埋藏在深处的设计错误， 也就是说模拟不能保证检测出所有存在的设计功 能错误。 形式验证作为基于模拟的验证方法的补充，日益引起人们的关注， 它旨 在形式化地证明一个设计的实现满足其规范，用来保证功能设计的质量和正确 ,胜. 形式验证方法包含三个基本方面:等价性验证、 模型检验和定理证明。 等价 性验证用于验证两个结构化的描述等价， 模型检测用于验证设计属性被满足， 定 理证明则验证电路满足其规范。 三者通常互为补充， 来验证一个完整的设计流程。 其中等价验证用来检测经过某种改动或优化过的电路和原来的电路在逻辑功能 上是否完全等价。 组合电路的等价验证是整个电路验证的基础，同时，我们主要在 r t l - - -r t l , r t l - - -g a t e , g a t e - - - - g a t e级进行电路的等价验证。 其中， g a t e - - - -g a t e级的验证最为基本， 是所有验证的基础， 我们工作的重点就放 在这一层。r t l级可以转化为g a t e级再进行验证。 基于这样的背景， 我们致力于开发一套同时具有完备性和高速性的组合电路 形式化等价验证系统。该系统还具有灵活性的特点，可以选择不同的s a t计算 引 擎， 同时也可以 被当 作一个模块被其他软件调用。 而且， 该系统的 构架设计将 有利于未来的错误定位工作。 1 .3国内 外研究进展 针对组合电路的等价验证， 国内外己 有大量的 研究工作， 主要分为三个方向: ( 1 ) 基于函数逻辑( f u n c t i o n - b a s e d ) 的方法。 该类方法试图 将整个电 路 ( 函 数) 转化为一种范式表达， 所谓范式表达就是指一个逻辑函 数只对应于唯一的一种表 达结构， 而验证等价的过程就是比 较两个范式是否相等。由于范式的唯一性，当 第一章绪论 电 路至范式的转化己 经完成， 最后比较过程将十分简单。 其中比 较有代表性的 有 m a t s 9 6 k u e h 9 7 和 h u l g 9 9 。 大 多 数 此 类 方 法是 基于b ry a n t b r y a 8 6 提 出 的r o b d d ( r e d u c e d o r d e r e d b i n a ry d e c i s i o n d i a g r a m ) 方法， 或对于r o b d d的 简单变化。 这种方法的一个主要的缺陷是二分决策树( b d d ) 的大小在一些常用例 子上 ( 比如乘法器) 同电路的输入个数呈指数关系， 从而很快地消耗完计算机所 有的内 存空间。 它的优点在于可以自 动保存那些电路结构上的信息于图形的拓扑 结构之中，方便对于冗余的化简。 ( 2 ) 基于自 动测试生成 ( a t p g , a u t o m a t i c t e s t p a t t e rn g e n e r a t i o n ) 的 方法。 此 类方法主要着眼于电路的结构， 通过对于包括原始输入点和电路内部节点的整个 变量空间的遍历来确定是否等价。由于部分变量的某些赋值就能导致冲突 ( c o n fl i c t ) 的产生从而导致决策树上的回溯， 所以事实上往往不需要全部变量赋 值的遍历就能完成整个搜索过程。 此类方法相比于基于函数逻辑的方法还有两个 比较重要的优点，它可以在方法中加入学习过程( l e a r n i n g ) 和 b c p ( b o o l e a n c o n s tr a in t p r o p a g a t i o n ) 过 程， 这 些 过 程的 加入 可以 排除 那 些不 必 要的 搜 索空 间， 从而大大提高效率。 a t p g的算法最先由a b r a m o v i c i 于1 9 9 0 年提出【 a b r a 9 0 . 目 前 采用基于a t p g的 等价验 证算法主要有【 s i l v 9 9 . e v g u 0 1 和 f e l u 0 3 算法的不同主要体现在随机过程的实现、变量的选择、学习策略的采用等等。 ( 3 ) 以 上两 种方 法的 混合。 鉴于以 上两种方法各自 的 优点， 不少结 合了 两种 方 法的 等价验证方法己 经被提出 ， 著名的 有【 g u p t 9 8 . p a r u 0 0 和 r e d a 0 1 . 其中 g u p t 9 8 采 用在电 路的 输 入 部 分 用s a t 完 成， 输出 用b d d完 成; r e d a 0 1 则采用了 相反的策略， 输入部分形成许多锥形的( c o n e ) b d d结构， 输出 用 s a t 完成; p a r u 0 0 的策略更有所不同， 它将b d d方法和s a t方法7 1 合到一起， 在每次迭代的开始用 b d d ，尽量压缩搜索空间，并用启发式算法来决定什么时 刻开始把余下的工作交给 s a t来完成。以上这些方法各有自己的优点， 但如何 高效紧密地将两种方法结合仍然是努力的重点。 1 . 4本文主要贡献 本文采用的验证方法主要是基于自 动测试生成的方法， 但在分划方面也借鉴 了基于逻辑函数方法的一些优点。 算法的核心思想是: 在工业界实际电路的情况 下， 待测的两个电路在结构上总有相似的地方， 电路内部也会有一些逻辑状态完 第一章绪论 全相同的点。 如果我们能预先找出一些这样的可能相等的配对点， 再证明其中一 部分是相等的。 那么电路中相等的部分就可以共用， 并利用已 经验证的点作为下 一个子电路的输入。 这样从电路的输入端往电路的输出端反复执行， 子电路的规 模相比原先整个电 路大大降低，从而得以 快速地完成整个电路的验证。 本文 提出 的 形式化的 等价验证方 法( f d c e c ) 主要的 创新之处在于: ( 1 ) 基于 层 分划的等价配对点生成方法。 这方法可以大大提高配对点的命中率， 并降低配对 点的生成时间， 从而大大加快整个验证的 速度. ( 2 ) 基于闽 值的 错反问 题( f a l s e n e g a t i v e ) 回 溯控制。 有效地选取回 溯的 时 机， 控制无 效回 溯次 数， 保证计算的 效 率。 ( 3 ) 基于s a t问 题解决框架的子电 路分划。 将电路的分划、回溯等过程， 有 机 地融 入s a t 问 题d p l l 算法 d a v 1 6 2 解决 框 架 之中 ， 避免了 反 复回 溯中 的 重 复 计 算， 并结合s a t 问 题研究 在b c p ( b o o l e a n c o n s t r a i n t p r o p a g a t i o n ) 和变量 选择 方面比较成功的技术，加快验证的速度。 此外，我们的验证算法具有很强的灵活性。 对于内部，子电路的验证上可以 调用不同的s a t s o l v e r 来完成;对于外部，可以 作为独立的等价电 路验证软件 使用，也可以作为一个模块被其他算法调用，比如用于时序电路的等价验证。 1 .5论文的组织结构 本文第一章为绪论，介绍等价验证方面国内外的研究进展和自己工作的贡 献; 第二 章简要介绍s a t问题及主要解决策略;第三章介绍我们的组合电路等 价 验证方 法 ( f d c e c ) 以 及其中的 算 法环节; 第四 章给出 基于s a t问 题 解决 框架 的f d c e c方法，实现与s a t s o l v e r 的无缝结合:第五章给出论文总结及展望。 第二章 s a t问题与等价验证问题简介 第二章 s a t问题与等价验证问题简介 2 . 1 s a t问 题简介 逻辑公式的可满足性问题是理论计算机科学和人工智能中的著名问题， 世界 各国学者在这方面做了大量的研究工作， 特别是关于命题逻辑中合取范式的可满 足性问题 ( 即s a t问题)。早在1 9 7 1 年的a c m的计算机理论研讨会 s t o c ) 上， s a t问 题就在算法复杂度上被证明是一 个 n p - c o m p l e t e ( n o n d e t e r m i n i s t i c p o l y n o m i a l ) 问 题。 鉴于 大量工 程上遇到的 实际问 题都是n p 完全问 题， 比 如， 在 人工智能 ( a d 方面需要进行自 动定理证明， 在计算机辅助设计方面， 有测试和验 证、 逻辑综合、 布线和路径延迟分析等问题， 而这些具体问题都可以转化为表现 形式比较简单的s a t问题进行求解， 因此s a t问题的求解具有非常重要的实际 意义。 根 据目 前计 算机界的 研究成果， 人们通常 认为， 对于n p - c o m p l e t 。 问 题， 不太可能有多项式时间复杂度的 算法， 7 0 个变量的规模， 就是2 7 0 的计算量， 是 当今计算机处理的极限。由 此产生了一种主导观念: 无论解的效果如何， 能找到 一个算法或比较己有的各种方法求得一个解即可。 因此， 启发式算法在求解s a t 问题的过程中被广泛使用。 经典的理论结果一般是考虑所有情况， 特别是最坏情 况， 但在各个领域的实际应用中， 最坏情况不会每次都出现， 人们往往可以利用 实例的一些具体特性对算法加以 优化从而突破理论上的禁区。现在，人们在 s a t问题上己经可以处理 1 0 0 0 0 个变量以上规模的实例，因此，s a t问题的理 论研究已 经走向了实际应用，利用 s a t解决算法来处理超大规模集成电路中的 等价验证问题成为可能。 2 . 1 . 1 合取范式的可满足性问题 命题逻辑( 又称布尔逻辑) 是最简单的一种形式逻辑系统。 命题是其主要的 研 究对象， 每个命题可能为真， 也可能为假。 例如， 1 + 2 = 3 ”是真的，而 “ 5 除以2 余数为。 ” 则是假的。 通常我们用p , 9 , r ,. ， 这些符号代表任意的 命题， 称为命题变元， 我们用1 , 0 分别表示命题的 真假值。 本文采 用布尔 逻辑函 数符号中的“ a n d ” 为“ 八” ， o r ” 为“ v , n o t 为 “ 一”。 第二章 s a t问题与等价验证问题简介 由命题变元和连接符可以按以下规则形成命题逻辑公式: 1 .命题变元时公式( 称为原子公式) 。 2 如果 中是公式，则( 一由 ) 也是公式。 3 .如果 中: 和 中2 是公式，则( 。l* 中 2 ) 也是公式。这里的* 表示任何一个二 元连接符，常用的包括八，vo 我们称原子公式或其否定为文字( l i t e r a l ) 。原子公式本身称为正文字， 而原 子公式的否定称为负文字。 若千个文字的 或( v ) 构成子句( c l a u s e ) ， 其长度是指 所含文字的个数。 只有一个文字的子句或者只包含一个文字没有被赋值的不满足 ( u n s a t i s f i a b l e ) 子句称为单子句( u n i t c l a u s e ) ，没有文字的子句称为空子句。 下面 给出 合取范式( c o n j u n c t i v e n o r m a l f o r m ， 简写为c n f ) 的定 义， 后面的 文章中一概简称为c n f . 定义若干个子句的逻辑与称为合取范式( c n f ) ，它的一般形式为: ( l v . v l , ) 八 一 八 ( l m , v . v l . . ) 这 里的 每个与是li t e r a l . 下面的定理可以 保证所有的逻辑函数都可以转化为其对应的c n f 表达: 定理对任意公式，都有与之等值的合取范式。 这里，我们给出s a t问题的定义: 定 义 对 于 函 数 f = ( lv . . v l , ) a . . a ( l . , v . v l . . ) , 问 是 否 可 以 找 到 一组赋值 ( l , : ， l , ， ， ， l i , )， 使得函 数f 的取值为1 ， 这就是s a t问 题( 可 满足性问题) 。如果可以找到这样一组赋值，则称该 s a t问题是可以满足的 ( s a t i s fi a b l e ) ;如果不存在这样一组赋值，则称该 s a t问题为不可满足 ( u n s a t i s f i a b l e ) o 对于n 变量的s a t问 题，有2 n 种可能的赋值情况需要被检查，也就是搜索 空间的大小为2 n ，如图2 - 1 所示: 图2 - 1 s a t问 题的 搜索空间( 2 n ) 第二章 s a t 问题与等价验证问题简介 的删除隔一定时间才执行一次。 决策点的 变量选择显然非常重要， 会指数级地影响计算时间。 尤其是决策树 最顶端的那些变量， 它们选择是否合理直接决定了算法的效率。 然而， 没有一种 策略可以保证自己在最初的选择就一定能找到那些最有价值的变量。 因此， 重启 ( r e s t a r t ) 的 思 想被提出， 希望通过重 启过程 来改善 决策情况。 重启 过程在g r a s p 就已经有其实现，g r a s p依赖当前信息作出 重启， 清除整个决策树，重启过程 本身不影响之后的决策过程。 z c h a f f 也会重启， 同样会清除当前整个决策树。 由 于重启的过程并不清空那 些c o n fl i c t c l a u s e ， 而那些c o n fl i c t c l a u s e 事实上保存了先前搜索过的变量空间， 所以， 重启之后不会重复搜索。 而且， 在变量的选择中加入一定的随机因素， 有 助于在重启后不再按照原先的变量选择次序产生搜索分支，否则即使不重复搜 索，按照原来的变量次序进行分支决策也会失去了重启的意义。 这里必须指出的是，由于子句删除策略的引入，使得整个 s a i问题的解决 变得不再完备， 因为在极端情况下， 如果记录先前搜索空间的c o n fl i c t c l a u s e 正 好都被删除， 则重启之后， s a t s o l v e r 不得不进行重复搜索， 而如果这种极端情 况反复出现， 会导致s a t s o l v e r 陷入了反复重启的死循环。为了解决这种情况， g r a s p的做法是不断增大重启的时间间隔， z c h a ff采用的方法则是慢慢增大子 句删除策略中的参数n ， 使得子句越来越不容易被删除， 从而保证了算法的完备 性 o 此外， z c h a ff的重启策略结合它的随机选择等地位变量的策略， 使得z c h a f f 可能在搜索的初期经常重启， 不断作新的尝试， 试图从各个变量组合的尝试中找 出比 较优的变量决策次序，虽然这种大量的尝试未必会带来效率的提高。 2 .2等价验证方法介绍 2 . 2 . 1 基于函数逻辑的方法 2 .2 . 1 .1 b i n a r y d e c i s i o n d i a g r a m s ( b d d ) b i n a ry d e c i s i o n d i a g r a m s 作为一种表达布尔函数的 数据结构是由l e e 在 1 9 5 9 年首先提出 l e e 5 9 , 首先给出符号定义: f l , =, (. .， 一 ，x ，一: ,x , ,x t+i ,.,x n ) :一 f (x , ， 二 一 ， c , x ;* 1， 一 x ) 第二章 s a t问 题与等价验证问 题简介 有如下的: s h a n n .定 理: 对 于 布尔函 数f e b , , b 。 为n 变 量的 布尔 空间， x= 1 x l , . . ., x n ) , 对 于 所 有 的 i e 1 1 ,. ， 。 ， 有: f = -v , f ,。 十 x ;刃 x1 x 2 x 3 图2 - 1 2完全o b d d树 图2 - 1 2是一棵 c o b d d树( c o m p l e t e o r d e r e d b d d ) ， 它对应的函 数就是 f = x , (x 2 ( x , ( 1 ) + 石 ( 1 ) + 两 (x , ( 1 ) + 石 ( 0 ) ) + x , (x 2 (x , ( 1 ) + 石 ( 0 ) ) + 刃 ( x , (1 ) + 石 ( 0 ) ) ，图中每个节点都对应一个函数表达式， 分支则是该点的s h a n n o n 分解， 其中实 线箭 头 表 示 该 节点 的1 分 支刃， 虚 线 剪头 表 示该 节点的0 分支尸 o r d e r e d 指的是从b d d树的 根部到底部的任何一条路径所得的变量序列的 先后都相同 而且变量无重复，图2 - 1 2 对应的变量序列为x l - x 2 - x o c o m p l e t e 指的 是 这棵 j 的 表 达 是 完 全的， 它 展开 每 一 个节点 的 每一 个 分 支， 所以 在 树的 最底 部 就 有2 ” 个分 支。 与c o m p l e t 。 相 对的 一 个概 念就 是r e d u c e d , 指的是没有冗余节点的b d d 树， 图2 - 1 2 所对应的r o b d d ( r e d u c e d o r d e r e d b d d ) 如图2 - 1 3 所示: j沪产 ，寿以谈回 图 2 - 1 3示意图 第二章 s a t问 题与等价验证问 题简介 从c o b d d到r o b d d要经过合并化简过程， 有三条规则: 1 . 合并叶节点 图2 - 1 4 b d d合并规则一 2 . 合并相同节点 图2 - 1 5 b d d合并规则二 3 . 去处冗余节点 x 图 2 - 1 6 b d d合并规则三 2 .2 . 1 .2 利用b d d进行等价验证 先给出一个定理: 定理:等价的两个布尔函数 ( 即 使表现形式可能不同)，它们对应的b d d 相同。 对于任意两个布尔函 数或组合电 路，只要能分别生成它们对应的 b d d ， 剩 下的等价验证工作只是比较这两张b d d是否相同，而这步骤可以在线性时间内 第二章 s a t问魔与等价验证问题简介 完成。所以说，基于函数逻辑的方法来解决等价验证问题，就是如何快速建立、 化 简b d d树的问 题。 这 方面 也己 经 有 大量的 工作 m ina 9 0 f u j i 9 1 r u d e 9 3 r a n j 9 6 ， 算法细节就不再赘述了。 2 .2 .2 基于自 动测试生成的方法 此类方法主要着眼于电路的结构， 通过对于包括原始输入点和电路内部节点 的整个变量空间的遍历来确定是否等价。 由于部分变量的某些赋值就能导致冲突 ( c o n fl i c t ) 的产生从而导致决策树上的回溯， 所以 事实上往往不需要全部变量赋 值的遍历就能完成整个搜索过程。 我们不妨来看看图2 - 1 7 验证a 和b 是否等价的简单实例。 ( a + 人 ) ( a + 几 ) ( a + 人+ 人) 介 下补气 尽 (f + 万 + b ) ( f + a + b ) ( f + a + b ) ( f + a + b ) ( b + 入 ) ( b + i z ) ( b + 石+ 人 ) 图2 - 1 7 a t p g方法等价验证示意图 每种逻辑门都有对应的c n f 表达式， 而电路中各个门之间的约束关系为“ 同 时满足”，也就是逻辑中的 “ 与” 关系，所以我们把每个门对应的c n f与在一 起， 形成一个大的c n f 表达， 这就是这个m i t e r 电 路对应的s a t问 题。 将m i t e r 的输出f 赋值为 1 ，如果该s a t问题可以满足，则表明可以找到一组输入激励， 使得f = 1 满足，也就是两个电 路不等价，反之则两个电路等价。 s a t问题的解决算法在前面的2 . 1 节中已 经介绍了很多，这里就不再赘述。 当 然在实际验证中电 路往往还会先进行分划， 形成一个个规模比 较小的子电路再 验证，我们的方法也是基于这一类，在第三章和第四章中有详细的算法介绍。 2 . 2 .3 基于以上两种方法的混合 为了利用以上两种方法各自 的优点， 不少结合了两种方法的等价验证方法已 经 被提出 。 著 名的 有 g u p t 9 8 , p a r u 0 0 和 【 r e d a 0 1 等， 我 们不 妨以 g u p t 9 8 为例介绍混合方法的大致思路。 第三章组合电 路等价验证的f d c e c方法 第三章组合电路等价验证的f d c e c方法 3 . 1引言 组合电路等价验证， 就是对于两个组合电路的网表， 验证其是否等价。 一张 网表由 输入节点， 输出节点和中间节点构成。 节点之间由逻辑关系相连接， 具体 实 现中 就是 逻 辑门， 主要由 与门 ( a n d ) 、 或门 ( o r ) 、 非门 ( n o t ) , 缓冲门 ( b u f ) , 异或门 ( x o r ) ，同 或门 ( x n o r ) 构成。 对于 两张 待测网 表， 要求己 经给出 一一 对 应的输入节点和输出节点，否则就是明显的不等价。 现实中需要验证的网表规模往往比较大，会包含多达几百个输入节点，以 5 0 0 个 输 入 节点， 1 0 0 0 0 个所 有节点 的网 表 来 举 例， 它的 解 空间 的 规 模就 是2 5 0 0 搜索空间更是达到了2 10 0 0 0 。 这么大的计算量，即使有强大的诸如z c h a f f 的 计算 引擎， 也不能直接解决。 但是网表的节点之间有其蕴涵关系， 两张网表之间也往 往具有相似的部分， 如果我们能利用这种结构上的有利条件而进行处理， 许多理 论上不可能求解的实例将会很好地被解决。 一种直观的想法就是利用电路的拓扑结构将电路分划为许多规模比较小的 子电路， 由于计算量同问题的规模呈指数关系， 而子问题的计算总量只是各个子 问 题计算量之和， 因此电路分划能大大降低总的计算量， 这种方法已 经被广泛地 接受。 然而传统的等价验证方法在最为重要的电路分划环节所做的工作还不够， 往往对于整个电路一次性地分划完毕， 这样会引入相当多的伪等价点， 后面再花 费大量时间去验证这些伪等价点的等价性， 造成效率不高. 考虑到实际电 路的特 点， 本文提出了分层划分的新的电 路分划方法。 其主要思想是电路中输入层数相 差较远的两个点只有很小的等价概率， 为了验证此类小概率等价的可能性却要花 费相当多的验证时间， 这类无效操作必须避免， 这样的配对点必须在生成的过程 中就加以忽略而不能带到验证过程。 为了达到这个目的， 本文提出的方法是将电 路中 包含的 所有节点按照对应的 输入深度进行分层， 再决定每次待测等价配对点 生成时的递进层数， 然后按照此层数在每次随机模拟的生成过程中只选择那些对 应层内的节点进行配对。 在下次配对点生成周期中则用上次停止的边界作为激励 向量， 生成新一批配对点。这样利用分层方法生成的配对点的实际等价率很高， 因为大量层数相隔很远的伪等价点在分层配对的过程中被过滤掉， 从而节省了大 量的验证时间。 第三章组合电路等价验证的f d c e c 方法 由 于子电路的支持点集选中了一组在原始输入激励下不可能得到激励向量， 使得实际等价的子电 路被判定为不等价， 这叫做错反问 题。 基于分划的 等价验证 不可避免地会遇到使得验证可能不完备的错反问题， 为了保证算法的完备性， 子 电路的 支持点集必须向后回溯。 在回溯上， 以往的算法采用了较为简单的回溯策 略， 如若不等价则一直回溯到原始输入点。 在验证过程中， 常常会遇到不等价的 配对点， 对于它们， 以 往的算法不得不反复进行验证， 而且每次回溯后生成的子 电 路规模都不断变大造成验证规模的 指数上升， 在浪费大量时间之后往往得到配 对点不相等的信息。 这里我们注意到只要配对点不是原始输出， 它们的放弃不会 影响整个验证的完备性， 为此， 本文提出了 基于阐 值的回溯控制方法， 在回溯时 先 观察当 前子电 路的 规模( 以 子 句数作为衡量 标准 ) ， 如果已 经超过了 某个阐 值， 则认为继续回溯的时间代价会超过该配对点实际等价的数学期望， 继续验证不合 理，从而放弃该配对点。闽值由电路特性和经验公式来确定。 从后面的详细分析和结果可以 看到， 这些措施的引入极大地提高了等价验证 算法的效率。 3 .2组合电路等价验证的f d c e c方法 在集成电路设计过程中， 由于功耗或者面积不符合设计要求， 往往会自 动或 者手动对于电路进行改动， 人们希望改动后的电路在逻辑功能上和原来的电路完 全相同。 改动往往只是部分的， 因此等待检验的两个电路多数情况下在结构上有 相似的 地方，在电路内 部也会有一些工作状态完全相同的点。如图3 - 1 所示: s u e c t i c n ho n i ml e ren t e t i a n 图3 - 1替换方法示意图 我们在两个网表中 找出 可能的 等价点a , 和a 2 ， 将他们作为一个虚拟的异或 门的输入， 输出为f , 我们称这样新构成的电路为mi t e r 电路。 如果a t 和a 2 对于 电 路任意输入都等价， 那么f 的 值将恒为0 ( s t u c k - a t 0 ) 。 逆命题同样成立， 如果 f 对于电路的任何输入恒等于0 ， 则a ， 和a 2 等价。 这样就可以进行图3 - 1 的操作， 第三章组合电路等价验证的f d c e c方法 将其中一个节点由另外一个节点替代。 如果我们能预先找出一些这样的可能相等的配对点， 再证明其中一部分是等 价的。 那么电路中相等的部分就可以共用， 并用这些等价点替代电路的原始输入 来作为后面子电路的测试激励， 减小子电路规模。 这样反复执行子电路的等价验 证，使得最后需检验的电路规模大大降低。如图3 - 2 所示: 图3 - 2 f d c e c算法示意图 基于这 样的思路， 我们开发出f d c e c ( f u d a n c o m b i n a t i o n a l e q u i v a l e n c e c h e c k i n g ) 算法， 其流程图 如图3 - 3 所示: 第三章组合电路等价验证的f d c e c方法 s o e w r f c a uo c r1 口 e l we o t n ue n c 2 在当前s a p p . r t 的基础上，向前作n 层的 r a n d o m s i m u l a t i o n .得到可能的配对点，若 层数己 经 达到 最 后要验 证的 p 曰n a r y o u t p u t ，则同样将其归入c a n d i d a t e p a i r 将c a n d i d a t e p a i r s 以某种策略放入一个堆找 ( 这里的策 略暂定为扇入总敌).若是遇到p r i m a r y o u p u t 组成的 c a n d i d a t e p a l 则 将 其 直 接 放 入 堆 找 的 底 部 堆找中是否还有 a n d i d a t e p a i r 认为( a l . a 2 ) 不相 取出 位 于 堆 找 顶 部 的c a n d f d a t e”行 ( a l , a 2 ) 找到t 卜 ef i r s t l e v e l s u p p o r t o f ( a l , a 2 ) 将al用a 2 代替， 冗余部分 将a l . a 2 与其 u p p o r t 构成的电 路合井成一个n i t e r ，井交给 s a t s o l v e r 计算 c1! =c2 退出 ( . l. 2 ) 相等 图3 - 3 f d c e c算法流程图 2 5 第三章组合电路等价验证的f d c e c方法 算法对应的伪代码如图3 - 4 所示: a l g o r i t h m f d c e c ( s p e c if i c a t i o n c l . i m p l e m e n t a t i o n c 2 ) wh i l e ( u n c h e c k e d o u t p u t p a i r . s i z e q ! = 0 ) i s e a r c h d e p t h = s e a r c h d e p t h l e v e p r o d u c e r ( ) ; g e n e r a t e c a n d i d a t e p a i r ( s e a r c h d e p t h ) ; h a n d l e c a n d i d a t e p a i r ( s e a r c h d e p t h ) ; wh i l e ( c a n d i d a t e p a i r .s i z e ( ) ! = 0 ) c u r r e n t p a i r = g e t c a n d i d a t e p a i r ( ) ; i f ( j u d g e v a l i d a t i o n ( c ti r r r e n t p a ir ) =0 ) b r e a k ; b u i l d s u p p o r t ( c u r r e n t p a i r ) ; s a t r e s u l t =u n d e t e r mi n e d ; wh i l e ( s a t es r e s u l t 一u n d