（计算机科学与技术专业论文）vlsi+rtl级模拟矢量自动生成技术研究.pdf

摘要功能验证是保证v l s i 设计功能正确的重要手段。随着现代v l s i 设计复杂度的不断提高，功能验证越来越成为设计验证的瓶颈。目前，功能验证主要集中在r t l 级及更高设计层次，用于保证r t l 级的h d l 描述及高层设计满足设计功能要求。功能验证主要采用形式化验证和模拟验证方法。形式化验证方法不需要输入激励就能静态地验证设计描述是否满足设计要求；而模拟验证方法通过加载输入激励动态地验证设计描述的正确性。随着设计复杂度的提高，这两种方法都遇到了困难。模拟验证方法缺乏评价模拟程度的测度，并且需要大量的模拟矢量来激活设计的各个部分。形式化验证方法存在状态空间爆炸问题，能处理的设计规模较小。覆盖率驱动的验证方法结合了形式化验证方法和模拟验证方法的优点，运用形式化技术分析模拟验证程度，并生成模拟矢量：通过模拟处理大规模设计。因此，该方法一提出就得到了广泛应用。在该方法框架中，模拟矢量自动生成技术是最关键的技术，模拟覆盖率测度是模拟矢量生成的目标，覆盖率分析是模拟矢量生成的依据。本文首先综述了模拟矢量自动生成技术及相关技术迄今为止的研究进展，对现有模拟矢量自动生成方法进行了分类，介绍了每种方法的代表性研究，分析了各种方法的优缺点。为了使模拟矢量自动生成技术能处理大规模的设计描述，需要对设计进行化简，抽取出感兴趣的设计进行处理。本文提出了一种基于程序切片技术的设计化简和设计抽取方法。该方法对切片标准进行了改造，根据给定的感兴趣的信号名，能抽取相关设计：对切片的运算公式进行了改造，能抽取出两组感兴趣的信号间的设计；提出了进程依赖图结构，以及基于进程依赖图的程序切片技术，解决了并发程序的切片问题；对切片过程的正确性进行了理论证明。本文改进了基于值变化导出( v a l u ec h a n gd u m p ，v c d ) 文件的模拟覆盖率分析方法。模拟重放时只执行h d l 描述中的控制语句。实验结果表明，改进后的模拟重放效率提高了2 倍多。本文定义了新的状态对模拟覆盖率测度，重新定义了交互状态机模型基于p r o b d d的可达状态对遍历算法：提出了基于p - r o b d d 的交互状态机模拟矢量自动生成方法。实验结果表明，基于p - r o b d d 的交互状态机模拟矢量自动生成方法能获得更高效的内存使用效率，内存占用率比传统方法减小多倍，避免了状态空间爆炸问题。本文提出了一种新的基于路径覆盖率的面向h d l 描述的模拟矢量自动生成方法。该方法利用决策图模型解决了如何将生成的中间变量和信号的模拟矢量传播到初始输入的问题：约束生成时只考虑控制语句的约束生成，而不需要为所有的语句生成约束t 提高了约束求解效率：能统一处理由位、位向量和整型变量构成的约束系统；能处理各种描述风第1 页国防科学技术大学研究生院学位论文格和各种控制和数据通路组成的设计。实验结果表明该方法在保证路径覆盖率高的前提下，模拟矢量生成速度更快。本文提出了一种基于断言的面向h d l 描述的模拟矢量自动生成方法。该方法运用了字级( w o r d l e v e l ) 约束求解技术，能统一处理控制电路和数据通路问的数据传播，字级约束求解效率更高：基于功能模型的模拟矢量生成目标更明确：与动态加速技术相结合，使搜索过程效率更高：设计化简技术的运用使搜索过程计算复杂度只与断言有关，而不需要搜索整个设计空间。实验结果表明，该方法在查找设计错误方面能获得很高的效率，并且能发现大部分设计错误。本文设计实现了一个r t l 级验证原型框架h r v ( h y b 趟r t - l e v e lv e r i f i c a t i o n ) 。该框架集成了本文提出的设计化简方法、覆盖率分析方法和基于路径覆盖和基于断言的模拟矢量自动生成方法。用该框架对实际设计进行了验证，发现了设计中的错误。为了提高模拟验证速度，本文设计实现了个并行v e f i l o g 模拟原型系统p v s i m 。提出了基于m o d u l e 的模拟实体映射算法，以及和预模拟划分算法结合的高效m o d u l e 划分算法。实验结果表明p v s i m 并行模拟器负载和通讯量平衡，模拟加速比明显。关键词：超大规模集成电路，寄存器传输级，v e r i l o g ，模拟矢量自动生成，程序切片，覆盖率分析，路径覆盖率，断言，约束逻辑编程，并行w a l o g 模拟第1 1 页a b s t r a c tf u n c t i o n a lv e r i f i c a t i o ni so n eo ft h em o s ti m p o r t a n tt e c h n i q u e su s e dt oa s s u r et h ec o r r e c t n e s so fv l s ld e s i g n d u et ot h ei n c r e a s i n gd e s i g nc o m p l e x i t y , f u n c t i o n a lv e r i f i c a t i o ni sn o wt h em a j o rb o t t l e n e c ko ft h ee n t i r ed e s i g np r o c e s s c u r r e n t l y , f u n c t i o n a lv e r i f i c a t i o nc o n c e n t r a t e so na t - l e v e lo re v e nh i l g h e rl e v e l st oa s s u r et h er t - l e v e lo rh i g h l e v e ld e s c r i p t i o n sc o n f o r mt ot h ed e s i g ns p e c i f i c a t i o n s t w op r i m a r ya p p r o a c h e s ，s i m u l a t i o na n df o r m a lv e r i f i c a t i o na r eo r e nu s e df o rf u n c t i o n a lv e r i f i c a t i o n f o r m a lv e r i f i c a t i o nt e c h n i q u e sc a np r o v ew h e t h e rd e s i g n sa r ec o n f o r m e dt ot h ed e s i g ns p e c i f i c a t i o nb ys t a t i ca n a l y s i st e c h n i q u e sw i t h o u tt e s tv e c t o r s w h i l es i m u l a t i o n b a s e da p p r o a c h e sv e r i f yd e s i g n sb yd y n a m i cr u n n i n gw i t hl a r g ea m o u n to ft e s tv e c t o r s h o w e v e gb o t ht e c h n i q u e se n c o u n t e rs o m ed i f f i c u l t i e si nd e a l i n gw i t ht h ei n c r e a s i n gc i r c u i tc o m p l e x i t y t h em a j o rp r o b l e mo ft h es i m u l a t i o n b a s e da p p r o a c h e si st h el a c ko fm e t r i ct og a u g et h eq u a l i t yo ft h ev e r i f i c a t i o n ，a n dn e e d sl a r g ea m o u n to ft e s tv e c t o r st os t i m u l a t ev a r i o u sc o m e rc a s e so ft h ed e s i g n f o r m a lv e r i f i c a t i o nt e c h n i q u e sa r eo f t e nl i m i t e db yt h ec o m p u t a t i o nr e s o u r c e sw h e nd e a l i n gw i t hl a r g ec i r c u i t s t h e r e f o r e ，t h ec o v e r a g e d r i v e na p p r o a c h ，w h i c hc o m b i n e st h ei d e a so fs i m u l a t i o na n df o r m a lv e r i f i c a f i o n ，i sp r o p o s e da n dr a p i d l yg e t t i n gp o p u l a r s o m ew e l l d e f i n e df u n c t i o n a lc o v e r a g em e t r i c sa r eu s e di nt h i sa p p r o a c ht op e r f o r maq u a n t i t a t i v ea n a l y s i so fs i m u l a t i o nc o m p l e t e n e s s w i t ht h ec o v e r a g er e p o r t s ，t h ev e r i f i c a t i o ne n g i n e e r sc a r lf o c u st h e i re f f o n so nt h eu n - v e r i f i e da r e a sa n dg e n e r a t em o r et e s tv e c t o r sb yt h eh e l po ff o r m a lt e c h n i q u e st oa c h i e v eb e a e rf u n c t i o n a lc o v e r a g e a m o n gt h et e c h n i q u e su s e di nc o v e r a g e - d r i v e nv e r i f i c a t i o nf r a m e w o r k ，t h ea u t o m a t i cf u n c t i o n a lv e c t o r sg e n e r a t i o nt e c h n i q u ei st h em o s ti m p o r t a n to n e t h ev e c t o r sg e n e r a t i o ne n g i n et a k e st h ec o v e r a g em e t r i c sa st h eg o a lf o rv e c t o r sg e n e r a t i o n ，w h i l er e l i e so nt h ec o v e r a g ea n a l y s i st e c h n i q u e sf o rf u r t h e rg e n e r a t i o n t h ep r o g r e s so ft h es t u d i e so na u t o m a t i cf u n c t i o n a lv e c t o r sg e n e r a t i o ni si n t r o d u c e di nt h i st h e s i s t h ee x i s t i n ga p p r o a c h e sa r ec l a s s i f i e di n t os e v e r a lc a t e g o r i e s t h er e p r e s e n t a t i v em e t h o d si ne a c hc a t e g o r ya r ei n t r o d u c e da n dt h ea d v a n t a g ea n dd i s a d v a n t a g eo fe a c hc a t e g o r ya r ea n a l y z e d i no r d e rt od e a lw i t hl a r g ed e s i g n s ，o n ep o s s i b l es o l u t i o ni st ou s ea b s t r a c t i o nt e c h n i q u e s an o v e ld e s i g na b s t r a c t i o na n de x t r a c t i o na p p r o a c hb a s e do np r o g r a ms l i c i n gt e c h n i q u ei sp r o p o s e di nt h i st h e s i s w ea l t e rt h es l i c i n gc r i t e r i o no f t h et r a d i t i o n a ls l i c i n gm e t h o d ，s ot h er e l a t e dd e s i g nf o rt h eg i v e ns i g n a l sc a nb ee x t r a c t e dw i t h o u ti n d i c a t i n gl i n en u m b e r w ea l s oi m p r o v et h e第l i i 页国防科学技术人。学研究生l 皖。1 7 能论文s l i c i n gf o r m u l a ，w h i c hm a k e so u rm e t h o db e c o m em o r ep r e c i s ef o re x t r a c t i n gd e s i g n sb e t w e e nt w os e t so fs i g n a l s an e ws t r u c t u r e p r o c e s sd e p e n d e n c eg r a p ha n dt h es l i c i n ga l g o r i t h mb a s e do ni ta r ep r o p o s e d ，w h i c hc a ns l i c eo nc o n c u r r e n tp r o g r a m s a tl a s t ，a ne l e g a n tt h e o r e t i c a lb a s i sb a s e do np r o g r a ms l i c i n gf o rc i r c u i te x t r a c t i o nf r o mv e r i l o gd e s c r i p t i o ni sd e v e l o p e d t h ee x i s t i n gv c d ( v a l u ec h a n g ed u m p ) f i l eb a s e dc o v e r a g ea n a l y s i sm e t h o di si m p r o v e di nt h i st h e s i sb yo n l yr e p l a y i n gt h es i m u l a t i o no ft h ec o n t r o ls t a t e m e n t si nt h eh d ld e s c r i p t i o n w ec a ng a i ns p e e du pi nc o v e r a g ea n a l y s i sw i t hm o r et h a n2t i m e st h a ne x i s t i n gm e t h o d t h i st h e s i sd e f i n e sn o v e ls t a t e p a i rc o v e r a g em e t r i c b yp r o p o s i n gt h es t a t e p a i rs p a c et r a v e r s a la l g o r i t h mf o ri n t e r a c t i n gf s m sb a s e do np - r o b d d ，a na l g o r i t h mt h a tg e n e r a t e sf u n c t i o n a lv e c t o r sf o rs t a t e p a i rm e t r i ci sp r o p o s e d t 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 i sa l g o r i t h mi se f f i c i e n ti nm e m o r yu s a g ew i t hs e v e r a lt i m e so fm a g n i t u d ei nm e m o r yu s a g er e d u c t i o na n dp e r f e c t l ys o l v e st h es t a t e ss p a c ee x p l o r a t i o np r o b l e m an o v e lm e t h o df o ra u t o m a t i cg e n e r a t i o nf u n c t i o n a lv e c t o r sf r o mh d ld e s c r i p t i o n sb a s e do np a t hc o v e r a g ea n dc o n s t r a i n t s o l v i n gt e c h n i q u e si sp r e s e n t e di nt h i st h e s i s i to n l yg e n e r a t e sc o n s t r a i n t sf o rc o n d i t i o ne x p r e s s i o no ft h ec o n t r o ls t a t e m e n t si nt h eg i v e np a t h ，a n db a s e so nd dm o d e ld e r i v e df r o i nh d ld e s c r i p t i o nt op r o p a g a t et h ei n t e r m e d i a t ev a l u e st ot h ep r i m a r yi n p u t s w h i c hc a nr e d u c et h ec o s t so nc o n s t r a i n t ss o l v i n g i tc a nh a n d l ea l lc o n s t r a i n t si n v o l v i n gb i t s ，b i t sv e c t o ra n di n t e g e r si nau n i f yf r a m e w o r k i tc a nh a n d l ev a r i o u sh d ld e s c r i p t i o ns t y l e s a n dv a r i o u st y p e so fd e s i g n s e x p e r i m e n t a lr e s u l t ss h o wt h a tt h i sm e t h o dc a ne f f i c i e n t l yi m p r o v et h ef u n c t i o n a lv e c t o r sg e n e r a t i o np r o c e s s ，w h i l eg a i nh i g hp a t hc o v e r a g e t h i st h e s i sp r o p o s e san o v e la s s e r t i o n b a s e da u t o m a t i cf u n c t i o n a lv e c t o r sg e n e r a t i o nm e t h o d t h em e t h o dc o m b i n e st h ep r o g r a ms l i c i n gb a s e dd e s i g ne x t r a c t i o n ，t h ew o r d - l e v e ls a te n g i n ea n dt h ed y n a m i cs e a r c ht e c h n i q u e s ，w h i c hm a k ei tc a nh a n d l el a r g ed e s i g n sa n dh a n d l ec o n t r o la n dd a t a p a t hd e s i g n si nau n i f i e df r a m e w o r k t h ee x p e r i m e n t a lr e s u l t ss h o wt h a ta s s e r t i o n b a s e df u n c t i o n a lv e c t o r sg e n e r a t i o nm e t h o di sm o r ee f f i c i e n ti nf i n d i n gd e s i g ne r r o r sa n di nv e c t o r sg e n e r a t i o np r o c e s s ap r o t o t y p eo ft h eh y b r i dr t - l e v e lv e r i f i c a t i o nf r a m e w o r k h r v ( h y b r i dr i - i e v c lv e r i f i c a t i o n ) h a sb e e nd e v e l o p e di nt h i st h e s i s ，w h i c hi n t e g r a t e st h ed e s i g ne x t r a c t i o nm e t h o d ，c o v e r a g ea n a l y s i st e c h n i q u e ，a n dp a t hc o v e r a g eb a s e da n da s s e r t i o nb a s e da u t o m a t i cf u n c t i o n a lv e c t o r sg e n e r a t i o nm e t h o d sp r o p o s e di nt h i st h e s i s t h ei n i t i a le x p e r i m e n t sc a r r i e do u to nt h i sp r o t o t y p ew i t hp r a c t i c a ld e s i g n sh a v es h o w nt h a tt h ef r a m e w o r ki sp r a c t i c a la n dc a nb eu s e dt of i n d i n ge r r o r si nd e s i g n s i no r d e rt os p e e du pt h es i m u l a t i o nv e r i f i c a t i o n ，t h i st h e s i sp r e s e n t sap a r a l l e lv e r i l o gs i m u l a t i o np r o t o t y p es y s t e m p v s i m ，w h i c ha d o p t sn o v e lm o d u l e b a s e ds i m u l a t i o nc o m p o n e n t第l v 页m a p p i n gm e m o da n de f f i c i e n tm o d u l e b a s e dp a r t i t i o na l g o r i t h mc o m b i n e dw i t hp r e s i m u l a t i o np a r t i t i o nt e c h n i q u e ，e x p e r i m e n tr e s u l t ss h o wt h a tp v s i mc a ng e tp r o m i s i n gs p e e d u p ，a sw e l la sb a l a n c e dc o m p u t a t i o na n dc o m m u n i c a t i o na c r o s sc o m p u t i n gn o d e s k e y w o r d s ：v l s i ，r t l ，v e r i l o g ，a u t o m a t i cf u n c t i o n a lv e c t o r sg e n e r a t i o n ，p r o g r a ms l i c i n g ，c o v e r a g ea n a l y s i s ，p a t hc o v e r a g em e m c 。a s s e r t i o n ，c o n s t r a i n tl o g i cp m g m m m m g ，p a r a l l e lv e r i l o gs i m u l a t i o n第v 页独创性声明本人声明所呈交的学位论文是我本人在导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表和撰写过的研究成果，也不包含为获得国防科学技术大学或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示谢意。学位沦文题目：逛! ! 笪坠垒邀塞坚叁篷! 鱼动叁壅幽堑学位论文作者签名：，丕! 迭日期：御3 年罗月j 7 日学位论文版权使用授权书本人完全了解国防科学技术大学有关保留、使用学位论文的规定。本人授权国防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子文档，允许论文被查阅和借阅；可以将学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。学位论文题目：选! ! 虹垒鱼曼醴过邀虿型丝建立蕉扬塾学位论文作者签名：基延日期：即弓年罗月7 日作者指导教师签名：垄里曼日期：如。；年? 月知日插图索弓图1 1 典型设计流程1图1 2 覆盖率驱动的验证流程，5图1 3 本文主要工作框架1 2图2 1 示例代码及其c f g 图1 8图2 2 一个简单豹v e r i l o g 程序及其p d g 图2 0图2 3 一个代码段2 2图2 4 示例程序第1 步切片得到的语句2 3图2 5 从第2 步得到的d p n 图2 3图2 6 对d p n 结点进行切片2 5图2 7 进程结点循环2 5图2 8v e r i l o g 切片算法2 6图2 9 示例的最终切片2 6图3 1 基于指令插入的覆盖率分析示例3 2图3 2v c d 文件格式：一3 4图3 3v e r i l o g 进程语句p s t 树构造算法3 6图3 4v e r i l o g 描述及其p s t 结构一3 7图3 5v e r i l o g 示例及其p d g 图3 8图3 6 模拟执行示例4 0图4 1 二叉决策图示例。4 7图4 2 交互状态机模型4 9图4 3 传统的状态遍历算法一5 1图4 4 覆盖测度计算算法5 2图4 5 模拟矢量自动生成算法5 3图51 回溯搜索示例5 8图5 2 位向量算术5 9图5 3 电路示例6 0第v 页图5 4 宽数据逻辑比较分解6 4图5 5 加减法运算分解方法6 8图5 6 乘法运算分解方法6 8图6 1g c d 的v e r i l o g 描述7 4图6 2g c d 描述的c f g 和d d 模型7 5图6 3 新的d d 模型图7 6图6 4 分支语句结构图7 6图6 5 分支示例及其c f g 图7 7图6 , 6 变量a 的d d 模型7 7图6 7 重定向后的d d 模型7 8图6 8c a s e 语句中变量的d d 模型7 8图6 9 循环语句结构7 9图6 1 0 循环语句中变量的d d 模型7 9图6 ，1 1 循环代码示例及其c f g 7 9图6 1 2 变量a 的d d 模型8 0图7 1 串行断言语法9 0图7 2s e q _ a s s e r t _ o n e h o t 和s e q _ a s s e r t _ a m o n e 定义9 0图7 3 并发断言定义9 l图7 4 串行断言转换方法9 2图7 5s e q和的转换方法9 2 _ a s s e r to n e h o ts e qa s s e r ta m o n e图7 6 序列表达式的等价形式9 3图7 7f i f o 设计描述9 6图7 8c n t 变量的d d 模型9 7图7 9c a s e 语句不完全多路选择器约束建模9 8图7 1 0v e r i l o g 循环语句的等价转换方法9 8图7 1 2c l p 约束示例9 9图7 1 1 基于d d 模型的约束生成方法1 0 0图7 1 3 触发f i f o 上溢断言的c l p 约束1 0 2图8 1h r v 系统框架结构图1 0 6第v i 页图8 , 2e x p r 继承关系1 0 8图8 , 3s t a t e m e n t 继承关系1 0 8图8 4g a t e 继承关系一1 0 9图8 5c o v a 系统结构图1 1 2图8 6p a t g 系统结构11 3图8 7a 2 t g 系统结构11 4图8 8 微处理器核模块图1 1 5图8 9 基于断言方法的c l p 约束1 1 7图9 1p v s i m 功能模块图1 1 9图9 2p v s i m 运行环境1 1 9图9 3 信号映射1 2 0图9 4m o d u l e 映射1 2 1图9 5 运行时刻周期组织1 2 1图9 6 连接点示意图图9 7 电路模型图9 8 模块间通讯图9 9 代码转换图9 1 0 划分方法图1 0 1 系统级验证框架1 2 31 2 41 2 61 2 61 2 81 3 5第嘣页表格索弓表2 1 图2 ，2 中结点的d e f 和r e f 集合2 0表2 2 设计的属性2 9表2 3 切片实验结果2 9表3 1 设计属性4 1表3 2 模拟时间和v c d 文件信息4 2表3 3 路径覆盖率实验结果一4 2表3 4 信号t o g g l e 覆盖率分析实验结果4 3表3 5 状态和状态变迁覆盖率分析实验结果4 3表4 1 布尔运算的i t e 操作表示4 8表4 2 与状态机乘积方法的比较5 5表4 3 与将交互状态机当作一个状态机方法的比较5 5表5 1 位逻辑运算6 3表5 2 位向量的位逻辑运算6 3表5 3 比较运算。- 6 3表5 4 数据宽度小于2 8 位时实验结果7 0表5 5 数据宽度为3 2 位时实验结果7 0表5 6 覆盖率比较7 1表6 i 实验电路属性8 7表6 , 2 与现有方法的实验比较结果8 7表6 , 3 与随机生成方法的实验比较结果8 8表7 1 实验电路属性1 0 3表7 2 实验结果1 0 4表9 1l i n u x 集群运行结果1 2 8表9 2l i n u x 集群运算开销1 2 9表9 3y h 3 e 运行结果1 2 9表9 4y h 3 e 运行开销( 2 结点) ，1 2 9表9 , 5y h 3 e 运行开销( 4 结点) 1 3 0第v i i i 页第一章绪论1 1 研究背景现代集成电路( i n t e g r a t e dc i r c u i t ，i c ) 设计通常采用自顶向下方法，一般从用硬件描述语言( h a r d w a r ed e s c r i p t i o nl a n g u a g e ，h d l ) 如v e r i l o g 1 9 戈v h d l 2 卜一描述系统行为开始，由综合工具将描述转换为逻辑网表，为了获得更高的性能和更小的面积，通常要对逻辑进行优化。经过库单元映射和版图设计，直至最后投片。图1 1 给出了典型的自顶向下的设计流程。图1 1 典型设计流程随着半导体工艺的发展，单个芯片上的晶体管数越来越多，现代数字系统也变得越来第1 页国防科学技术大学研究生阮学位论文越复杂。随着设计复杂度的不断增大，设计验证变得越来越困难。目前的：s 片设计队伍结构中，验证人员一般是设计人员的2 倍，验证所花的时间和精力己占整个设计过程的7 0 到8 0 ，其中，r t l 级及高层验证占整个验证开销的5 2 。验证尤其是r t l 级及高层验证已经成为整个设计过程的瓶颈 3 。设计验证要保证设计开始时的h d l 描述是正确的，并且每一设计层次间的设计转换过程不会带来错误。在设计过程中，越早发现设计错误越容易改正，并且修正错误的开销也越小，而到投片后再发现错误，需要改正错误的开销最大，而且对设计的修改将涉及设计过程的各个层次。因此，功能验证主要集中在h d l 描述的r t l ( r e g i s t e r t r a n s i s t o r l e v e l )级设计，以确保尽早发现设计错误。这也是由于r t l 级h d l 描述是后续设计层次设计功能验证的主要参照系。这种保证设计功能正确性的验证被称为功能验证( f u n c t i o n a lv e r i f i c a t i o n ) 。功能验证主要验证r t l 级h d l 描述是否满足设计的功能描述的要求。功能验证方法主要有三种：形式化验证方法、模拟验证方法和覆盖率驱动的验证方法。1 2 1 形式化验证方法1 2 功能验证方法概述形式化验证方法使用数学方法形式化地证明设计实现部分或全部满足系统描述要求。目前形式化验证方法种类较多。模型检验( m o d e lc h e c k i n g ) 是一种检测设计是否具有所需属性的方法；等价性检查( e q u i v a l e n c ec h e c k i n g ) 用于比较设计的两种实现是否一致该方法又可分为组合等价性检查( c o m b i n a t i o n a le q u i v a l e n c ec h e c k i n g ) 和时序等价性检查( s e q u e n t i a le q u i v a l e n c ec h e c k i n g ) 。其它的方法还包括定理证明( t h e o r e mp r o v i n g ) 和符号轨迹求解( s y m b o l i ct r a j e c t o r ye v a l u a t i o n ，s t e ) 等。在形式化验证方法中，通常使用船f p 妇结构来描述反应式系统，描述这种系统的状态变化。k r f # e 结构m 被定义为一个三元组m = ( s ，s o ，r ) ，其中s 是一个有限状态集合，矗s 是初始状态集合，r s s 是状态变迁关系。1 模型检验模型检验用于检羽4 某个具有有限状态集合的系统是否有其描述所规定的属性 8 ，9 】。描述通常用时态逻辑表示，例如计算树时态逻辑( c o m p u t a t i o nt r e el o g i c c t l ) 【9 】和线性时态逻辑( l i n e a rt e m p o r a ll o g i c l t l ) 【1 0 】，而系统被建模为k r i p k e 结构。早期的模型检验方法是显式状态搜索方法【1 l 】，该方法的缺点是状态爆炸问题。m c m i l l a n 等【1 2 】提出第2 页了基于化简有序二分决策图( 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 3 的隐式状态搜索检测方法，称为符号模型检验。虽然符号模型检验方法已经能处理有几百个状态寄存器的设计【1 4 ，但是现代设计常常带有成千上万个状态寄存器，因此，目前模型检验还只能处理小规模的设计。虽然该方法可以直接基于h d l 描述进行，证明h d l 描述在所有输入下满足某些正确性属性。但这些属性通常由设计者给出，要求对设计功能需求有很全面的了解才能给出这些属性，并且只能证明设计满足属性要求，而不能证明设计的正确性。2 定理证明在定理证明中，系统及其需满足的属性都用数理逻辑的形式化语言描述，一个形式化描述的系统包括一组公理和演绎规则，从系统的公理找到对属性的证明的过程就被称为定理证明【1 5 。与模型检验不同。定理证明能在无限状态空间上进行推理。目前有很多定理证明工具用于解决硬件验证问题，例如h o l 系统 1 6 p v s 系统 1 7 】和a c l 2 系统 1 8 1 等，并且都有成功应用案例。m o o r e 等人 1 9 】验证了a m d 5 k 8 6 芯片的除法算法的微码，b r o c k 等 1 8 验证了m o t o r o l a 的c a p 处理器，c l a r k 等 2 0 】验证了s r t 除法算法。该方法需要个设计行为的形式化描述。通过严格的数学证明，比较h d l 描述的设计和系统的形式化描述在所有可能输入下是否一致。该方法存在的问题是，通常h d l 描述就是第一个形式化描述，即便有一个更高层次的形式化描述，还需要保证该描述的正确性才能和h d l 插述进行一致性眈较；形式化描述和h d l 描述的一致性证明很难进行，通常需要假设很多条件，以简化比较证明，而要证明这些假设本身也是很困难的。另一个主要问题是不能完全自动化。3 组合等价性检查组合等价性检查的目的是检查两个组合电路在给定的输入下是否等价。组合等价性检查属于c o - n pi f i j 题 2 1 ，但在实际应用中，要比较的两个电路往往差别很小结构相似性很大。该方法己在工业界得到广泛应用。该方法采用的标识等价点和萃b 用两个电路阈的隐喻关系的方法能加快检查进程，实际实现时采用了多种布尔求解引擎，如b d d 、a t p g 、s a t 等 2 2 ，2 3 1 ，也使其能获得较高的性能。4 对序等价性检查时序等价性检查分为两种应用场景，第一种应用中两个时序电路有对应的状态寄存器，例如，两个电路的状态编码相同，此时，时序等价性检查就变成了组合等价性检查。该类应用包括：比较r t l 级设计在综合前后的等价性：检查逻辑级设计及其版图实现闻的第3 页等价性；对设计进行性能优化前后电路的等价性证明等。第二种情况是两个时序电路状态编码不同，例如，检查电路在r e t i m i n g 后的正确性；比较电路的流水化设计和非流水设计等。解决该问题的一种简单的方法是构造两个时序电路的乘积状态机，通过遍历乘积状态机的状态空间来检测是否等价，显然该方法不能处理大型的设计。针对不同的实际情况，现有研究提出了备种有效检查流水和非流水设计的等价性的方法。例如，b u c h 和d i l l l 2 4 建立了基于u n i n t e r p r e t e d 函数进行抽象验证流水微处理器控制的基础。r i t t e r 等【2 5 基于i n t e r p r e t e d 函数和c a s e 划分检查两个h d l 描述的可计算性等价。这些方法都不是基于状态空间遍历的，而是通过验证设计的实现和描述间检查点( c h e c k p o i n t ) 的等价性来进行验证的。时序等价性检查的问题是需要一个参考模型作为描述，而设计参考模型也是一个很重的任务。5 符号轨迹求解符号轨迹求解 2 6 ，2 7 是一种受限形式的模型检验方法，它提供了符号轨迹公式来描述设计说明。符号轨迹公式由布尔表达式和时态逻辑的“下一时刻”操作符y 构成，属性的定义形式是 4 c ，其中4 是由输入和经过一定时钟周期后的系统状态组成的序列，c是该序列可能的结果行为。例如，反相器可被描述为【i n = a x ( o u t = 、口) 】。检测是通过基于二叉决策图( b i n a r yd e c i s i o nd i a g r a m ，b d d ) 的三元符号模拟进行的。由于每个结点有三种状态( 0 ，1 ，需要用对变量来表示b d d 中的一个结点。在符号模拟时，与要验证的属性无关的初始输入和系统状态都被赋值为“x ”，这使得s t e 比其它模型检验方法有优势，因为其计算复杂度是由属性决定的，而不需要检查整个状态空间。s t e 方法已在逻辑级数据通路设计验证中获得成功应用 2 8 ，2 9 。s t e 的缺点是轨迹公式不能描述“负”和“或”，只支持一种时态逻辑操作符( x ) ，因此s t e 方法的表达能力有限；其次，s t e 使用b d d 进行符号模拟，同样存在状态空间爆炸问题。1 2 。2 模拟验证方法该方法以用户给定的输入，直接模拟运行h d l 描述，根据模