（计算机应用技术专业论文）vlsi设计中的形式验证方法研究.pdf

v l s i 设计中的形式验证方法研究 摘要 超大规模集成电路( v 】l s i ) 的设计日趋复杂，验证工作越来越繁重，验证 难度也越来越大。在复杂的v l s i 设计中，验证过程所需的时间约占整个设计 周期的三分之二，设计过程所需要的专业验证工程师人数大约是设计工程师的 两倍，功能验证已成为v l s i 设计的瓶颈。传统的软件模拟和硬件仿真需要花 费大量的时间，且不能完全保证功能的正确性。形式验证作为传统验证方法的 补充，日益引起人们的关注。形式验证使用严格的数学推理来证明设计满足规 范的部分或者全部属性，所需要的验证时间比较少，是克服验证瓶颈的可行途 径。本文对v l s i 的形式验证方法进行了研究，主要工作如下： 1 ) 针对数据密集型电路的等价性验证，提出了w g l 模型的改进模型 w z g l 。w g l 的节点是位级变量，在字级算术运算表示方面具有局限性，而 w 2 g l 能有效地表示字级算术运算。本文还证明了一个有序的、简化的w 2 g l 模型是最小的和正则的，并提出了w 2 g l 模型的变量排序方法及加法和乘法算 法。运用这些方法和算法可以构建寄存器传输级( r t l ) 电路的有序的、简化 的和正则的w 2 g l 模型，进行电路优化前后的等价性验证。实验结果表明，与 * b m d 和w g l 模型相比，w 2 g l 模型对数据密集型电路的等价性验证不论在 存储空间还是在c p u 运行时间上均有明显的减少。 2 ) 针对同时包含字级、位级变量算术运算和逻辑运算的复杂电路的等价 性验证，对w 2 g l 模型进行扩充，提出了混合w g l 模型m g l 。w 2 g l 模型能有效地表示字级算术运算，但在表示字级逻辑运算时比较复杂，需要把 字级变量拆分成位级变量。本文提出的h w g l 模型既可以有效表示字级的算 术运算和逻辑运算，又可以有效表示位级的算术运算和逻辑运算。对复杂电路 构建h w g l 模型，可实现优化前后电路的等价性验证。h w g l 模型的大小与 字长无关，并且需要较少的节点和构造时间。实验结果表明，对复杂的包含字 级变量和位级变量的电路，h w g l 比w 2 g l 和* b m d 更有效。 3 ) 针对性质检验问题，本文在h w g l 模型的基础上，提出了一种分支 w g l 模型叫w g l 。b w g l 模型是对h w g l 模型的扩充，模型中用到的变 量节点是h w g l ，并在模型中增加了分支节点、u n i o n 节点和i n t e r s e c t 节点。 哈尔滨工程大学博十学位论文 暑- ii i 暑暑i 暑宣i i i ；i i i i ；i 昌暑；暑；暑 把b w g l 模型应用于性质检验，把设计中的性质描述成一个线性时间逻辑，根 据时间片选择不同的检验过程验证性质是否满足。把基于b w g l 的性质检验与 基于b d d 的v i s 系统进行比较，实验结果表明，在处理器验证方面，基于b w g l 的性质检验比v i s 系统更有效，可以利用较少的资源在较短的时间内完成验证。 另外，基于b w g l 的性质检验可以同时验证数据通路和控制器，节省了大量的 时间。 关键词：v l s i ：形式验证；w 2 g l ；h w g l ；b w g l ；等价性验证：性质检验 v l s i 设计中的形式验证方法研究 a b s t r a c t w i t ht h ei n c r e a s i n gc o m p l e x i t yo fv e r yl a r g es c a l ei n t e g r a t i o n ( v l s d ，t h e w o r k sf o rd e s i g nv e r i f i c a t i o ni sg e t t i n gm o r ca n dm o r ea r d u o u sa n dd i f f i c u l t f o r c o m p l e xv l s id e s i g n s ，t h ev e r i f i c a t i o np r o c e s sa c c o u n t sf o ra b o u tt w o - t h i r d so ft h e e n t i r ed e s i g nc y c l e ，a n dt h en u m b e ro fp r o f e s s i o n a lv e r i f i c a t i o ne n g i i l e e 巧i nd e s i g n p r o c e s si sa b o u t t w i c eo ft h a to fd e s i g ne n g i n e e r s f u n c t i o n a lv e r i f i c a t i o nh a sb p 比o m e b o t t l e n e c ko fv l s id e s i g n t r a d i t i o n a ls o f t w a r es i m u l a t i o na n dh a r d w a r ee m u l a t i o n c o s tal o to ft i m e , a n dc a n tg u a r a n t e et h ec o r r e c t n e s so ft h ef u n c t i o nc o m p l e t e l y a s o n eo fc o m p l e m e n t a r ya p p r o a c h e s ，f o r m a lv e r i f i c a t i o nh a sa t t r a c t e dt h ei n t e r e s t so f p e o p l ei n c r e a s i n g l y f o r m a lv e r i f i c a t i o nu s e sr i g o r o u sm a t h e m a t i c a lr e a s o n i n gt o d e m o n s t r a t et h a tt h ed e s i g nm e e t sa l lo rp a r t so fi t ss p e c i f i c a t i o nw i t h i nl e s st i m e ， w h i c hi saf e a s i b l ea p p r o a c ht oo v e r c o m et h eb o t t l e n e c ko fv e r i f i c a t i o n i nt h i s d i s s e r t a t i o nf o r m a lv e r i f i c a t i o nm e t h o d sf o rv l s ia l es t u d i e dt h o r o u g h l y t h em a j o r c o n t r i b u t i o n sa r ca sf o l l o w s ： 1 ) f o re q u i v a l e n c ec h e c k i n go fd a t ai n t e n s i v ec i r c u i t s ，aw o r dw g l ( w 2 g l ) ，t h e i m p r o v e dm o d e lo fw g lm o d e l ，i sp r o p o s e d w g l m o d e li sl i m i t e dt ow o r d l e v e l a r i t h m e t i co p e r a t i o n sr e p r e s e n t a t i o nf o rw h i c hn o d ei sb i t q e v e lv a r i a b l e w z g l m o d e lc a l le x p r e s sw o r d - l e v e la r i t h m e t i co p e r a t i o ne f f e c t i v e l y i ti sp r o v e dt h a ta n o r d e r e da n dr e d u c e dwg li sm i n i m a la n dc a n o n i c a l ，a n dt h ev a r i a b l eo r d e r i n g m e t h o di sp r o p o s e d , a n dt h ea d d i t i o na n dm u l t i p l i c a t i o na l g o r i t h m sf o rw g la r e p r e s e n t e di nt h ed i s s e r t a t i o n u s i n gt h e s em e t h o d sa n da l g o r i t h m st h eo r d e r e d , r e d u c e da n dc a n o n i c a lw 2 g lm o d e l sc a l lb ec o n s t r u c t e dt oc a r r yo ne q u i v a l e n c e c h e c k i n gb e t w e e np r e - o p t i m i z e da n dp o s t o p t i m i z e dr t lc i r c u i t s e x p e r i m e n t a l r e s u l t ss h o wt h a tf o re q u i v a l e n c ec h e c k i n go fd a t ai n t e n s i v ec i r c u i t s ，c o m p a r e dw i t h 毒b m da n dw g lm o d e l w 。g lm o d e lh 硒t h eo b v i o u ss u p e r i o r i t yi nb o t hm e m o r y s t o r a g ea n dc p ur u n n i n gt i m e 2 ) f o re q u i v a l e n c ec h e c k i n go fc o m p l e xc i r c u i t sc o n t a i n i n ga r i t h m e t i ca n dl o g i c o p e r a t i o n so fb o t hw o r d - l e v e la n db i t l e v e l ，ah y b r i dw g i ( h w g l ) m o d e li s 哈尔滨t 程大学博士学位论文 p r o p o s e di nt h ed i s s e r t a t i o n , w h i c hi se x p a n d e df r o mw 上g lm o d e l w 2 g lm o d e l c a l le f f e c t i v e l ye x p r e s sw o r d l e v e la r i t h m e t i co p e r a t i o n h o w e v e r , i ti sn e c e s s a r yt o s p l i tt h ew o r d 1 e v e lv a r i a b l e si n t ot h eb i t 1 e v e lv a r i a b l e sw h e nw 2 g l m o d e le x p r e s s w o r l d - l e v e ll o g i co p e r a t i o n , w h i c hm a k e st h ee x p r e s s i o nm o r ec o m p l e x h w g l m o d e lc a ne f f e c t i v e l ye x p r e s sa r i t h m e t i ca n dl o g i co p e r a t i o n so fb o t hw o r d - l e v e la n d b i t l e v e l h w g lm o d e l so fc o m p l e xc i r c u i t s 锄b ec o n s t r u c t e dt oc a r r yo n e q u i v a l e n c ec h e c k i n gb e t w e e np r e - o p t i m i z e da n dp o s t - o p t i m i z e d c i r c u i t s t h e c o n s t r u c t i o no fh w g lm o d e li si n d e p e n d e n to fw o r dl e n g t h , a n dn e e dl e s sn o d e s a n dt i m e e x p e r i m e n t a lr e s u l t ss h o wt h a tf o rc o m p l e xc i r c u i t sc o n t a i n i n gw o r d - l e v e l a n db i t 1 e v e lv a r i a b l e s ，h w g li sm o r ea d v a n t a g e o u st h a nw 2 g la n d 掌b m d 3 ) f o rp r o p e r t yc h e c k i n gp r o b l e m , o nt h eb a s i so fh w g l m o d e lab r a n c hw g l ( b w g l ) m o d e li sp r o p o s e di nt h ed i s s e r t a t i o n b w g lm o d e li se x p a n d e df r o m i - i w g l , i nw h i c hv a r i a b l en o d eb e l o n g st oh w g ln o d ea n db r a n c hn o d e ，u n i o n n o d ea n di n t e r s e c tn o d ea r ea d d e d b w g lm o d e li sa p p l i e dt op r o p e r t yc h e c k i n g t h ep r o p e r t yo fd e s i g ni sd e s c r i b e da sl i n e a rt i m el o g i c ，a n dd i f f e r e n tc h e c k i n g p r o c e d u r ei sc h o s e na c c o r d i n gt ot i m es l i c et ov e r i f yw h e t h e r t h ep r o p e r t yi ss a t i s f i e d p r o p e r t yc h e c k i n gm e t h o db a s e do nb w g l i sc o m p a r e dw i t hv i ss y s t e mb a s e do n b d d e x p e r i m e n t a lr e s u l t ss h o wt h a tf o rp r o c e s s o rv e r i f i c a t i o n ，p r o p e r t yc h e c k i n g b a s e do nb w g li sm o r ee f f e c t i v et h a nv i ss y s t e m ，w h i c hc a nv e r i f yc o m p l e t e l yi n l e s st i m ea n dw i t hl e s sm e m o r y m o r e o v e r , p r o p e r t yc h e c k i n gb a s e do nb w g lc a l l v e r i f yt h ed a t ap a t ha n dc o n t r o l l e rs i m u l t a n e o u s l y ，w h i c hc a l ls a v eag r e a td e a lo f t i m e k e y w o r d s ：v l s i ；f o r m a lv e r i f i c a t i o n ；w 2 g l ；h w g l ；b w g l ；e q u i v a l e n c e c h e c k i n g ；p r o p e r t yc h e c k i n g 哈尔滨工程大学 学位论文原创性声明 本人郑重声明：本论文的所有工作，是在导师的指导下，由 作者本人独立完成的。有关观点、方法、数据和文献的引用已在 文中指出，并与参考文献相对应。除文中己注明引用的内容外， 本论文不包含任何其他个人或集体已经公开发表的作品成果。对 本文的研究做出重要贡献的个人和集体，均已在文中以明确方式 标明。本人完全意识到本声明的法律结果由本人承担。 作者( 签字) ：关饼 日期：伽q 年6 月汐日 哈尔滨工程大学 学位论文授权使用声明 本人完全了解学校保护知识产权的有关规定，即研究生在校 攻读学位期间论文工作的知识产权属于哈尔滨工程大学。哈尔滨 工程大学有权保留并向国家有关部门或机构送交论文的复印件。 本人允许哈尔滨工程大学将论文的部分或全部内容编入有关数据 库进行检索，可采用影印、缩印或扫描等复制手段保存和汇编本 学位论文，可以公布论文的全部内容。同时本人保证毕业后结合 学位论文研究课题再撰写的论文一律注明作者第一署名单位为哈 尔滨工程大学。涉密学位论文待解密后适用本声明。 本论文( 口在授予学位后即可口在授予学位1 2 个月后口 解密后) 由哈尔滨工程大学送交有关部门进行保存、汇编等。 作者( 签字) ：笑昭 e i , 簸i ： 9 , 0 0 彳年；月孑日 导师( 签字) ： 卅年弓月各日 第1 章绪论 第1 章绪论 1 1 课题的研究意义 随着i c 制造技术的飞速发展，半导体制造工艺进入超深亚微米( v e r yd e e p s u b m i c r o r t , v d s m ) 时代，芯片的特征尺寸越来越小，单位芯片上集成的晶体 管数目越来越多，同时芯片的规模也越来越大。现在一个复杂的电路系统可集 成到一个芯片上，超大规模集成电路( v e r yl a r g es c a l ei n t e g r a t i o n , v l s i ) 已 经由专用集成电路( a p p l i c a t i o ns p e c i f i ci n t e r g r a t e dc i r c u i t s ，a s i c ) 时代发展到 系统芯片( s y s t e mo nac h i p ，s o c ) 时代【卜3 】。s o c 是在一个芯片上集成了一个 完整的电子系统。单个s o c 能集成数十亿个晶体管，时钟频率能达到1 0 - 2 0 g h z ， v l s i 已进入超高速芯片设计阶段1 4 , 5 j 。按照i t r s ( i n t e r n a t i o n a lt e c h n o l o g y r o a d m a ps e m i c o n d u c t o r ) 的预测1 6 j ，到2 0 1 0 年4 5 n mc o m s ( c o m p l e m e n t a r y m e t a l o x i d e s e m i c o n d u c t o r ) - 1 - 艺的高速、低功耗v l s i 将能量产。目前量产芯 片的特征尺寸已降到6 5 n m ，实验室最新工艺水平已达到3 2 r i m l 7 。另一方面， 一直遵循m o o r e 定律的i c 制造技术使得设计者在单个芯片上集成了更多的口 核、内存、总线等，构成非常复杂的系统，集成电路的发展呈现出由集成电路 向集成系统( i n t e g r a t e ds y s t e m ，i s ) 转变的趋势。以超深亚微米以及纳米工艺 和口核重用技术为基础的半导体集成化系统芯片技术是国际超大规模集成电 路发展的趋势和二十一世纪集成电路的主流 7 1 。 长期以来，芯片复杂度的增长速度超过了设计能力的增长速度；芯片的制 造能力超过了芯片的设计能力。为满足日益增加的消费需求和充分发挥投资惊 人的集成电路生产线的生产能力，需要更多的设计者及时地提供大量复杂的设 计。另外计算机技术和通讯技术的快速发展，使得数字电力系统渗透到社会生 活的各个领域，特别是许多对于安全性要求较高的关键场合都大量采用了嵌入 式系统，但由于集成电路工艺的复杂性，它的试制费用相当昂贵，而电子产品 市场的激烈竞争，又使得产品的上市时间极为紧迫。因此，集成电路的设计验 证正受到严峻的挑战，电路中的一点微小错误都可能造成巨大的经济损失或者 导致人员伤亡等灾难性后果，例如：i n t e l 公司的奔腾5 8 6 芯片中的除法运算错 哈尔滨t 程大学博十学位论文 误是在大量进入市场后被一位用户发现的，虽然这种错误发生的概率为几亿分 之一，却造成四亿八千万美元的经济损失。国际半导体技术路线图( i n t e r n a t i o n a l t e c h n o l o g yr o a d m a ps e m i c o n d u c t o r , i t r s ) 的报告指出，验证已经成为集成电 路设计流程中开销最大的工作【6 1 。在目前的工程项目中，验证工程师的数目超 过了设计工程师，而对复杂的设计甚至达到了2 ：1 或者3 ：1 的比率，验证的时 间开销已占到整个设计周期的6 0 0 0 - 8 0 ，经济开销更是占到整个设计开销的 8 0 以上。因此验证已经成为当前集成电路设计的瓶颈。 设计大规模的复杂数字系统的关键问题之一是如何检查设计的正确性，即 设计验证。但是，设计验证的复杂度随着芯片的规模呈指数增加。传统的验证 手段包括模拟( s i m u l a t i o n ) 、测试( t e s t i n g ) 和仿真( e m u l a t i o n ) 技术，但是对于大型 的系统，模拟和测试只能针对某些典型情况或者随机地进行，很难检测出所有 的设计错误。随着集成电路复杂度的提高，系统设计中的一个小错误可能造成 较大的经济损失，甚至会引起整机报废等灾难性后果。因此设计的正确性验证 成为设计的瓶颈，被称为“验证危机”。 传统的模拟验证是将激励信号施加于设计，进行计算并观察输出结果，并 判断该结果与预期的是否一致。模拟验证的主要缺点是非完备性，即只能证明 有错而不能证明无错。因此，模拟一般适用于在验证初期发现大量和明显的设 计错误，而难以胜任复杂和微妙的错误。模拟验证还严重依赖于测试向量的选 取，但合理而充分地选取测试向量，从而达到高覆盖率是一个十分艰巨的课题。 由于设计者不能预测所有错误的可能模式，所以尚未发现某个最好的覆盖率度 量。即使选定了某个覆盖率度量，验证时间也是一个瓶颈。特别是随着集成电 路设计规模越来越大，尤其是s o c 的出现，使得模拟验证方法在计算上往往不 可行。 在软件设计中也具有类似的问题，即程序的正确性验证问题。在6 0 年代 末兴起的软件验证技术就反映了计算机科学家和数学家为解决“软件危机”所 做的努力，他们用数学推理的方法严格证明了程序的正确性，这些努力在程序 设计方法学方面做出了很大的贡献。8 0 年代初，人们把类似的方法用于硬件设 计验证，产生了硬件的形式化验证技术。 硬件验证地理论和方法的研究和应用在近十几年来发展很快。许多原来被 认为没有什么前途的硬件形式化验证技术得到了工业界的普遍认可，特别是模 2 第1 苹绪论 型检验技术，已经引起了e d a 产业的轰动和商业界的投资热潮。十几年来， 全世界各主要e d a 公司都相继研制和推出了自己的形式化验证软件，但是在 国内，这种情况尚未引起广泛重视。 模拟的过程是实验性的，而形式验证过程是数学化的，数学化的验证克服 了模拟的不足，因为它对指定描述中所有可能的输入组合进行了全面验证，而 不是仅仅对其一个子集进行多次试验。形式验证是用数学的方法证明设计的正 确性，因而避免了对所有可能测试模式的枚举。与模拟验证相比，形式验证方 法更快、更精确，在近年来受到学术界和工业界的重视【引。 本文针对形式验证中的等价性验证和性质检验问题展开研究，分析了现有 的w g l ( w e i g h t e dg e n e r a l i z e dl i s t ) 模型在数据密集型电路表示上的局限，提 出了w 2 g l ( w o r dw g l ) 模型，并讨论了其在数据密集型电路的等价性验证 中的应用。对w 2 g l 模型进行了扩充，提出了一个h w g l ( h y b r i dw g l ) 模 型，在模型中增加了字级逻辑运算的表示能力，使其适合于复杂的包含字级位 级多种操作的电路的验证。对h w g l 模型进行了扩充，提出了一种b w g l ( b r a n c hw g l ) 模型，在模型中增加了分支结构，并讨论了此模型在性质检验 中的应用。 1 2v l s i 的设计流程 v l s i 的设计一般采用自顶向下的方法，包括了概念设计、系统设计和描述、 系统划分、子系统功能描述、综合、逻辑描述、版图综合、版图描述、芯片制 作等过程。图1 1 描述了。s i 的设计流程。在v l s i 设计的各个阶段都离不 开验证。图1 1 中粗框中的形式验证是本文的研究内容。 1 3v l s i 的功能验证概述 为了确保电路功能的正确性，必须对各抽象层次的电路进行功能验h 正t g 。 集成电路的功能验证可以划分为三类：模拟验证、形式验证和半形式化验证 ( s e m i f o r m a lv e r i f i c a t i o n ) 。它们之间的主要区别在于模拟验证需要测试向量， 而形式验证不需要。模拟的方法是面向输入的，设计者需要给定输入向量进行 测试，而形式验证是面向输出的，设计者需要提供待测试的输出特性【1 0 1 。半形 式化验证是结合了模拟验证方法和形式化验证方法【8 j 。 哈尔滨工程大学博十学位论文 1 3 1 模拟验证 传统的功能验证方法是模拟验证。所谓模拟验证，是指对实际数字系统加 以抽象，提取其模型，将其输入计算机。然后将外部激励信号施加于此模型， 通过观察模型在外部激励信号作用下的反应判断该数字系统是否实现了预期的 功能【l i 】。它主要是通过对被验证电路施加验证激励进行模拟，将得到的输出响 应与预期的正确结果相比较，以此来发现其中的错误。按照运行平台的不同， 可以分为软件模拟( s i m u l a t i o n ) 和硬件仿真( e m u l a t i o n ) 。一般的模拟验证流 程如图1 2 所示，其中激励产生与覆盖评估是模型检验中最核心和最关键的问 题【1 2 1 。 圈? 田 图1 1v l s i 的设计流程 f i g u r e1 1d e s i g nf l o wo fv l s i 4 i， ， 第1 章绪论 设计信息 规范信息 图1 2 模拟验证流程 f i g u r e1 2t h ef l o wo f s i m u l a t i o nv e r i f i c a t i o n 1 ) 模拟验证方法 基于软件的模拟大体分为事件驱动的模拟( e v e n t - d r i v e ns i m u l a t i o n ) 和基于 周期的模拟( c y c l e - b a s e ds i m u l a t i o n ) 。硬件仿真将电路设计下载到诸如f p g a ( f i e l dp r o g r a m m a b l eg a t ea r r a y ) 中，通过f p g a 的运行来仿真实际集成电路 的运行情况。与软件模拟相比，硬件仿真最大的优点就是速度得到了提高，一 般情况下，硬件仿真的速度比软件模拟方法要快几个数量级；但与模拟相比， 它只能观察芯片引脚信号或仿真软件设定的信号，如果要观察其他信号的取值 变化，必须在仿真软件里重新设定然后再次仿真。硬件仿真还有其他一些缺点： 比如硬件仿真器价格昂贵、可以仿真的设计规模受到f p g a 门数的限制等。 2 ) 模拟验证的激励生成 在模拟验证中激励生成是必不可少的，常用的激励生成方法有利用测试向量 的激励生成方法、基于错误模型的激励生成方法、利用层次环结构的激励生成 方法、基于模拟的激励生成方法和基于电路行为描述的激励生成方法等【1 3 】。 3 ) 模拟验证的覆盖评估 覆盖评估在模拟验证中发挥着重要的作用，是模拟验证中的不可或缺的技 术【1 4 ，1 5 】。首先，覆盖评估提供了度量模拟激励集的量化方法，在一定程度上弥 补了模拟验证的不完备性。其次，覆盖评估技术能够诊断出对于当前的激励集 来说，哪部分设计尚未得到充分验证，这有助于后续的激励生成【l5 1 。常用的覆 盖评估准则可分为2 大类，一类是从行为的角度来度量，主要包括代码覆盖准 则、电路结构覆盖准则、有限状态机覆盖准则和可观测性覆盖准则等：另一类 哈尔滨1 二程大学博七学何论文 是从设计错误的角度来度量，主要包括错误模型覆盖准则。 4 ) 模拟验证的局限性 模拟验证是目前工业上最常用的功能验证方法，但它有两个主要的缺陷。 首先由于指数级的时间复杂性，对于大型复杂的设计，不可能对整个输入向量 空间进行穷举的模拟。因此模拟验证能够发现错误的存在，但不能够保证错误 的不存在，即模拟验证难以保证测试的完全性。其次是难以定义合适的验证覆 盖率，而且验证者很难创建理想的测试激励，使之能够覆盖到所定义的各种评 估目标。 1 3 2 形式验证 1 3 2 1 形式验证的概念 集成电路设计早期的验证技术主要是模拟验证。随着数字系统规模的扩 大，逻辑模拟的缺点变得越来越突出，尤其输入激励波形的确定本身就是一个 复杂的课题。模拟器的功能仅表现为某一组外部激励信号作用下该数字系统的 行为，至于加什么样的外部激励信号以及在该外部激励信号作用下系统反应的 正确与否，完全由设计者自己决定。事实上，一个电路设计结果正确与否，仅 依赖于设计的电路结构。人们希望能根据逻辑设计的功能和结构的描述来证明 逻辑设计的正确性，而不是用指定的激励波形进行模拟行为验证。 形式验证就是适应这样的设计要求产生的验证方法。它的主要研究对象是 计算机系统的设计和验证，包括硬件系统、软件系统、嵌入式系统( e m b e d d e d s y s t e m ) 、分布式系统( d i s t r i b u t e ds y s t e m ) 、反应式系统( r e a c t i v es y s t e m ) 、 实时系统( r e a l - t i m es y s t e m ) 和混合系统( h y b r i ds y s t e m ) 等。一般来说，形 式化方法就是用具有形式语义的记号和工具明确地表述系统设计的要求，即给 出系统规范( s p e c i f i c a t i o n ) ，并根据系统规范利用上述记号和工具对系统具有 的性质和最终实现的正确性进行严格地证明。在系统设计的较高层次上，软硬 件的设计没有很大的差别，但由于作为硬件设计规范的硬件描述语言( 如v h d l 和v e r i l o g ) 已经被广泛使用，所以硬件的形式验证方法集中在设计验证方面， 而且硬件验证的研究工作利用了原来程序验证的许多成果。 6 第1 章绪论 1 3 2 2 形式验证的意义 在硬件设计领域，随着集成电路工艺的发展，软件和硬件交织在一起，要 进行软硬件协同设计( c o d e s i g n ) ；离散和连续的信息交互作用，要研究混合系统 的设计和验证方法。尽管出现了许多设计自动化工具和系统，仍然难以保证设 计的正确性。因而在硬件设计中，为了保证设计的正确性，寻求新的验证方法 和技术已引起许多研究者的兴趣。 保证系统正确性的途径是多方面的。对系统的需求分析要全面而准确，不 能有任何实质性的漏洞，以产生正确的系统规范，建立正确的系统规范的有效 方法之一是快速原型法。建立系统准确的模型，进行反复的模拟和仿真是目前 进行硬件设计验证的主要途径。但模拟只能用典型的情况对系统进行考察。对 系统进行穷尽地模拟是不可能的。在大型系统中，要模拟系统完全的行为可能 要连续运行多年的时间，这显然是不实际的。 测试是保证设计正确性的另一种手段。对硬件系统的测试是在加工后进行 的，但是测试只能证明错误存在而不能证明错误不存在。对于复杂的系统，进 行穷尽地测试也是不可能的，甚至设计一个有效的测试方案和评价其故障的覆 盖都是很困难的。现在人们普遍认为利用随机测试也不能对解决问题有很大帮 助。设计冗余表决系统是提高可靠性的另一种方法，但它只能在一定程度上有 效。 形式化验证方法是保证设计正确性的一种重要方法。它用数学方法表达系 统的设计规范或系统的性质，并且根据数学理论来证明所设计的系统满足系统 的规范或具有所期望的性质，在不能证明所期望的性质时，则可能发现设计错 误。实践证明，通过形式化的自动验证方法能发现其它方法不能发现的设计错 误。 1 3 3 半形式化验证 半形式化验证结合了传统的模拟验证和形式验证的思想，试图充分发挥这 两种验证方法的优点，是目前集成电路设计验证技术的一个很有前途的发展方 向之一。半形式化验证将形式化方法的分析、搜索技术同模拟方法结合起来， 模拟的结果被作为形式验证的起点，形式验证的反例被用于重新引导模拟，两 者互相结合、交替进行。一方面，可以在模拟的方法中加入形式化的特征，更 7 哈尔滨丁程大学博十学位论文 有针对性，能够产生高质量的测试，达到好的测试效果；另一方面，可以在形 式化方法中运用模拟的技术，它只分析了全部状态空间的一部分，因而不如纯 粹的模型检验那样容易受到内存爆炸的困扰，使之更加有效，也可以应用于大 规模电路的验证。 符号模拟方法是一种典型的半形式化验证方法，其基本思想是以布尔变量 代替布尔常量作为电路模型的模拟向量，由基本输入出发，依次计算每个节点 的布尔函数，直到在电路输出端得到这些初始变量成的布尔表达式，并以之作 为电路的功能描述。对于等价性验证，符号模拟的目的是证明两个电路的功能 描述是否等价；对于模型检验，其目的则是验证得到的功能描述是否满足给定 性质。由于采用抽象的符号值来进行模拟，因此一次符号模拟相当于模拟了一 个很大的测试集，可以在一个模拟周期内完成传统模拟方式多个周期方能完成 的任务，同时保证了足够可靠的覆盖率。 1 4 形式验证方法 形式验证就是用类似定理证明的方法或其他数学方法来证明逻辑设计的 正确性。一般来说，形式化验证方法可以分为等价性验i 正( e q u i v a l e n c ec h e c k i n g ) 1 & 2 5 1 、模型检验( m 0 d e lc l 蛾k 。一， 2 渊1 ，一 b 、t h p r o v i n g ) 方法1 3 5 州。 形式验证的任务是通过形式化的、数学的严格证明确立电路的实现是否满足设 计规范的要求。一 1 4 1 等价性验证 等价性验证是目前在工业实践中最广泛使用的形式方法，而且已被应用于 验证大型的复杂系统设计【1 6 1 。等价性验证的主要目的是检验一个设计变换前后 的功能一致性【8 j 。这里所说的设计变换可以是综合、布局布线、测试、时钟树 的插入、扫描链的重排序、f p g a 到a s i c 的转换等【l 丌。如果对现有的门级或 物理级网表写出其r t l ( r e g i s t e r t r a n s f e r l e v e l ) 模型，以使原来的设计能够重 用，这时也可以利用等价性验证。另外，如果设计者将原来设计的功能进行了 修改，等价性验证产生的信息可以用来帮助设计者确认所做的修改是否达到了 目的。如果把等价性验证同模拟集成在一起，就可以把等价性验证得到的反例 送给模拟程序进行纠错【1 8 1 。在整个设计流程中，最初的规范与用户的要求应该 8 第l 章绪论 是一致的，并在后续过程中步一步地细化和实现。每一步实现的行为都应该 与前面的设计相一致。这种致性可以用等价性验证来验证。例如，对于一个 专用集成电路的设计，要把r t l 的设计用自动综合工具转换为网表级设计，又 如对于一个结构化的全定制设计，可以由人工来实现门级网表的转换，转换后 的网表是否满足原来的规范可以利用等价性验证来验证。不仅如此，对于某些 设计性能的优化，也可以把优化前后的设计结果进行等价性验证，以证明优化 前后的功能不变。这种等价性验证保证了百分之百的覆盖，而不必担心检验的 完全性。在最后的版图设计中，功能的等价性验证还要同定时验证工具一起使 用，以保证版图的正确性。 等价性验证的基本思想是使用形式化方法验证设计规范与它的实现之间 的功能一致性。由于等价性验证不需要产生测试向量，可以使验证工程师节省 大量时间。等价性验证可以用来验证两个相同或者不同抽象级别设计的等价性， 如r t l 与r t l 级，门级与门级，或r t l 与门级之间的等价性，从而检验出设 计过程中的错误，保证设计在各个阶段的正确性【1 6 1 蛇1 1 。由于等价性验证所具 有的优势，它已被广泛应用于专用集成电路设计流程的不同阶段。通过验证每 一阶段的中间结果，保证这一结果传输到下一阶段之前不出现错误。发现错误 越早，后续的调试和修改时间就越少。目前许多公司都将等价性验证方法集成 到e d a 工具中，如c a d e n c e 公司的形式验证工具h e c k 和a 伍l m a 、s y n o p s y s 公司的f o r m a l i t y 、m e n t o rg r a p h i c s 公司的f o r m a l p r o 等1 8 , 1 6 。 等价性验证的基本原理是建立两个被比较模型之间的关系 2 2 , 2 3 。检验的依 据是数学定理和公理，以及设计实现所利用的标准单元库的精确描述。等价性 验证程序自动检验两个设计的关系，而不需要用户的输入。因此它的优点是容 易集成到设计流程中，使用简单 2 4 , 2 5 1 。目前c a d e n c e 公司已经推出了等价性验 证工具a f f i r m a ，它把建立两个被比较设计之间的关系和等价性证明合并为一体 进行。首先假定两个设计中的锁存器和存储器元件是等价的然后利用随机输 入向量对两个设计进行功能模拟并根据模拟结果划分锁存器。在没有用户干预 的情况下，利用二叉判定图( b i n a r yd e c i s i o nd i a g r a m ，b d d ) 和可满足性算法， 它能很快识别两个设计之间功能相对应的节点。 当等价性验证工具检测出两个设计之间功能的差别时，它就显示出一个反 例，即一组原始输入或者若干锁存器以及引起这个差别的原始输入取值和锁存 9 哈尔滨t 程大学博十学何论文 器取值，并显示一些可以帮助设计者分析产生这些差别的原因信息。如果把模 拟程序同等价性验证工具集成在一起，就可以利用这些信息进行模拟以找出这 种差别的原因。 当前常见的组合等价性检测方法大致可以归结为两大类：功能性的验证和 结构性的验证，但两者之间并没有太严格的界限。功能性方法是通过将电路表 示成一种规范形式来进行验证，两个电路是等价的当且仅当它们的规范形式同 构。最常用的规范形式是简化的有序二叉判决图r o b d d ( r e d u c e do r d e r e d b d d ) i s ，为了验证两个电路的相应原始输出是等价的，必须按相同的输入变量 序分别构造这两个输出函数的r o b d d ，然后判断它们是否同构。这种方法输 入变量排序极为敏感，常遇到内存爆炸的问题。 结构性方法则是通过识别电路内部的等价结点，并利用这些等价结点的功 能蕴涵来简化验证问题。内部等价结点常被称为断点( c u t p o i n t ) ，识别潜在断点 的常用方法有随机模拟、a t p g 方法、基于b d d 的方法以及基于可满足性的推 理方法。所有潜在的断点找出后，依据一定的准则，将整个系统验证分解为关 于这些断点子集的较小的验证任务，分别进行验证。 目前提出的等价性检测方法大多数都是按结构性检验的基本框架，再结合 功能性方法进行验证，如图1 3 所示。首先提取出两个被比较电路的内部相 似性，推导出各断点之间的特殊关系，如等价性、蕴涵及可置换性等等。然后 图1 3 等价性验证的一般流程图 f i g u r e1 3t h eg e n e r a lf l o w c h a r to f e q u i v a l e n c ec h e c k i n g l o 第1 章绪论 使用这些关系，把等价性检测过程分解为关于这些断点子集的较小的验证任务， 分别完成。总的算法是从原始输入向原始输出方向遍历两个电路，从已知的断 点演绎出新的断点，直到所有的相应原始输出被证明等价，或者找到某个输入 向量使得两个电路输出不匹配。 1 4 2 模型检验 c l a r k e 等人提出的基于一种分支时态逻辑即计