（计算机应用技术专业论文）基于gste理论的抽象与细化问题的研究.pdf

：，皇! ，l 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工 作及取得的研究成果。据我所知，除了文中特别加以标注和致谢的地 方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含 为获得电子科技大学或其它教育机构的学位或证书而使用过的材料。 与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明 确的说明并表示谢意。 签名：型 日期：少夕年，月砰日 论文使用授权 本学位论文作者完全了解电子科技大学有关保留、使用学位论文 的规定，有权保留并向国家有关部门或机构送交论文的复印件和磁 盘，允许论文被查阅和借阅。本人授权电子科技大学可以将学位论文 的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或 扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后应遵守此规定) 签名：塑星导师签名：j 玺国丞二 日期：z 驴年r 月2 伊e l 摘要 摘要 近年来，由于电路规模不断增大和集成度不断提高，使得超大规模集成电路 ( v l s i ) 变得越来越复杂，而设计过程又难以保证逻辑设计的正确性。同时集成电路 设计时的差错所带来的损失巨大，当前没有修复芯片的技术不可能对v l s i 中的错 误部分进行修正。因此，设计和建立高可靠性的集成电路系统成为一个关键问题。 验证作为一个的保证设计正确的重要环节，正发挥着越来越重要的作用，并引起 人们越来越多的关注和兴趣。本课题在g s t e 理论的基础上，研究抽象以及细化 处理在该理论上的应用，希望解决由抽象所带来的效率以及验证精确性的统一问 题。通过变量划分技术，对变量集有区别的进行抽象以有效表示状态空间；为有 效地表示相关变量的状态集，使用参数化表示将状态空间进行压缩化处理，并利 用b d d 技术实现g s t e 理论验证算法。 由于当前形式化验证方法基于状态搜索的处理方法，因此存在处理能力有限 的问题，而不能验证大规模的电路系统。当前大部分形式化验证工具都引入了抽 象与细化处理，来解决状态爆炸的问题。在研究方法上，首先，本文讲述了为解 决状态爆炸问题而产生的形式化验证方法，简要分析了它们的验证思想以及存在 的问题。其次，讲了形式化验证方法如何对验证电路进行建模，并重点介绍当前 主要的形式化验证方法：s t e 和g s t e ，并且对电路模型的定义，验证规范的描述 以及验证算法进行分析，同时针对它们验证模拟的原理和方法，分析其优缺点， 并对它们进行对比分析。进一步了解了抽象处理的方法以及对电路的符号化处理 技术，同时分析了g s t e 的抽象处理以及细化处理的过程。在以上理论学习和分 析的基础上，本文提出了基于g s t e 的抽象处理以及状态参数化表示的改进算法， 并在验证过程中对验证的性质进行变量的划分，只验证与断言相关的变量，有效 地减少了状态数。在验证过程中引入参数化表示方法，可以对状态空间进行有效 地表示，尽可能压缩状态空间并使用b d d 来实现g s t e 验证算法。通过这些技术 有效提高了g s t e 模拟验证的处理能力以及它的验证效率。 关键词：形式化验证，g s t e ，抽象，细化，参数表示，变量划分 a b s t r a c t a b s t r a c t i nr e c e n t y e a r s ，d u et ot h ei n c r e a s i n g s c a l eo ft h ec i r c u i ta n dt h ei m p r o v i n g i n t e g r a t i o n ，v e r y - l a r g es c a l ei n t e g r a t i o n ( v l s i ) h a sb e c o m em o r ea n dm o r ec o m p l e x ， a n dt h ed e s i g np r o c e s si t s e l fi sd i f f i c u l tt oe n s u r et h el o g i c a ld e s i g n sc o r r e c t n e s s a tt h e s a m et i m e ，b e c a u s et h ei ce r r o r sc a u s e db yd e s i g np r o c e s sm a k et h el o s se n o r m o u s ，a n d b e c a u s eo fn or e p a i r i n gc h i pt e c h n o l o g y , i ti si m p o s s i b l et oa m e n dv l s ie r r o r s ，t o d e s i g na n db u i l dh i g h - r e l i a b i l i t yi n t e g r a t e dc i r c u i ts y s t e mh a sb e c o m eak e yi s s u e a sa n i m p o r t a n tp a r tf o rg u a r a n t e e i n gt h ed e s i g np r o p e r l y , t h ec e r t i f i c a t i o ni sp l a y i n ga n i m p o r t a n tr o l ei n c r e a s i n g l y , a n dr a i s e sm o r ea n dm o r ea t t e n t i o na n di n t e r e s t t h es u b j e c t b a s e do nt h et h e o r yo fg s t e ，r e s e a r c h e sa b s t r a c t i o na n dr e f i n e dt e c h n o l o g yt od e a lw i t h t h ea p p l i c a t i o no ft h et h e o r y , w i s h e st or e s o l v et h ee f f i c i e n c yc a u s e db yt h ea b s t r a c t i o n a sw e l la st h er e u n i f i c a t i o ni s s u eo fv e r i f i n gt h ea c c u r a c y , d ot h ed i f f e r e n t i a la b s t r a c t i o n f o rt h ev a r i a b l es e tb vt h ev a r i a b l ed i v i s i o nt e c h n o l o g yi no r d e rt or e d u c e st h es t a t e s p a c e ，u s et h ep a r a m e t e r i z e ds t a t es p a c et o e x p e s st h es t a t eo ft h er e l e v a n tv a r i a b l e s g s t et h e o r ya u t h e n t i c a t i o na l g o r i t h m c o m p r e s sp r o c e s s i n gi no r d e rt oe f f e c t i v e l y s e t a p p l yb d dt e c h n o l o g yt oi m p l e m e n t a st h ef o r m a lv e r i f i c a t i o nm e t h o di sb a s e do nt h es e a r c h i n gs t a t ea p p r o a c h ，t h e r ei s p r o b l e mo fl i m i t e dp r o c e s s i n gc a p a c i t y , a n di tc a nn o tv m f yt h el a r g e - s c a l ee l e c t r o n i c c i r c u i t r y a tp r e s e n t ，a b s t r a c t i o na n dr e f i n e m e n tp r o c e s s i n gi n t r o d u c e db ym o s tf o r m a l v e r i f i c a t i o nt o o l s ，d e a lw i t ht h es t a t ee x p l o s i o np r o b l e m i nr e s e a r c hm e t h o d s ，f i r s t l y , d e s c r i b en e wf o r m a lv e r i f i c a t i o nm e t h o d e st oa d d r e s st h es t a t ee x p l o s i o np r o b l e m ，a n d a n a l y s i st h e i ri d e a sa n dp r o b l e m so ft h em e t h o d sb r i e f l y s e c o n d l y , l e a r nh o wt om o d e l v e r i f i n gt h ec i r c u i tf o rt h ef o r m a lv e r i f i c a t i o nm e t h o d ，a n df o c u s eo nu n d e r s t a n d i n gt h e c u r r e n tm a i nf o r m a lv e r i f i c a t i o nm e t h o d s ：s t ea n dg s t e a n a l y s i sm e i rd e f i n i t i o no f t h ec i r c u i tm o d e la n dt h es p e c i f i c a t i o nv e r i f i e dr e s p e c t i v e l y , a sw e l la sv a l i d a t i o no f t h e i ra u t h e n t i c a t i o na l g o r i t h m ，a c c o r d i n gt ot h e i rp r i n c i p l e sa n dm e t h o d so fs i m u l a t i o n v e r i f i c a t i o n ，a n a l y s i st h e i rs t r e n g t h sa n dw e a k n e s s e s ，c o m p a r ea n da n a l y s i sa m o n g t h e m u n d e r s t a n dt h ea b s t r a c t i o nt r e a t m e n tm e t h o d sf u r t h e r l y , a sw e l la ss y m b o lp r o c e s s i n g t e c h n i q u e so ft h ec i r c u i t ；a n da n a l y s i st h ea b s t r a c tp r o c e s s i n ga n dr e f i n n i n gp r o c e s s i n g i l 垒星墨婴盟 一一 _ l _ - i - _ _ i - _ _ _ - _ i _ _ _ - _ i _ i _ _ _ _ i _ _ _ _ _ _ _ _ _ _ _ _ - 。_ _ 。_ - _ - _ _ _ - _ - _ _ - _ 。- 。_ _ - _ - - i _ - _ _ _ 。i _ _ _ _ _ _ 。一一 o fs t ea n dg s t e t h o u g ht h ea b o v et h e o r e t i c a ls t u d ya n da n a l y s i s ，i nt h i sp a p e r , i m p o s e st h ei m p r o v e da l g o r i t h mb a s e do na b s t r a c t i o np r o c e s s i n ga n ds t a t ep a r a m e t = s r e p r e s e n t a t i o no fg s t ea n di nt h ep r o c e s so fv e r i f i c a t i o n ，d i v i d e st h ev a r i a b l eo f t h e c e r t i f i c a t i o ns p e c i f a t i o n ，o n l yv e r i f i e sa s s e r t i o n r e l a t e dv a r i a b l e ss ot h a ti tr e d u c e st h e n u m b e ro fs t a t e se f f e c t i v e l y a tt h es a m et i m e ，i nt h ev e r i f i c a t i o np r o c e s s ，i n t r o d u c et h e p a r e m e t i cm e t h o dt oe x p r e s st h es t a t es p a c ee f f e c t i v e l ya n dc o m p r e s st h es t a t es p a c e a s m u c ha sp o s s i b l e a p p l yt h eb d dt e c h n o l o g yt oi m p l e m e n tg s t ea u t h e n t i c a t i o n a l g o r i t h m a d o p t i o n so ft h e s et e c h n o l o g i e si m p r o v ec a p a b i l i t i e so f t h eg s t es i m u l a t i o n v e r i f i c a t i o np r o c e s s i n ge f f e c t i v e l y , a sw e l la si t sv e r i f i c a t i o np r o c e s s k e y w o r d s ：f o r m a lv e r i f i c a t i o n ，g e n e r a l i z e d s y m b o l i ct r a j e c t o r y e v a l u a t i o n ， a b s t r a c t i o n ，r e f i n e m e n t ，p a r a m e t r i cr e p r e s e n t a t i o n ， v a r i a b l e p a r t i t i o n i i i 目录 目录 第一章绪论1 1 1 课题背景1 1 2 形式化验证2 1 2 1 形式化验证的基本概念和原理2 1 2 2 形式化验证方法的意义以及不足6 1 3 形式化验证方法的发展7 1 3 1 抽象方法的提出以及意义7 1 3 2 模型验证方法8 1 3 3 有界模型验证9 1 3 4 无界模型检验1 0 1 4 研究意义1 0 1 5 主要研究内容和章节安排1 1 1 5 1 主要研究内容1 1 1 5 2 章节安排1 1 第二章符号轨迹赋值和推广化轨迹赋值简介1 3 2 1 电路模型1 3 2 1 1 硬件电路的功能模型1 3 2 1 2 硬件电路的结构模型一1 4 2 2 符号轨迹赋值( s t e ) 介绍15 2 2 1s t e 电路模型的定义。1 6 2 2 2s t e 验证规范的相关概念17 2 2 3s t e 验证算法过程1 9 2 2 4s t e 的优点与不足2 l 2 3 推广化符号轨迹赋值( g s t e ) 介绍2 2 2 3 1g s t e 电路模型以及性质描述2 2 2 3 2g s t e 验证算法2 5 2 4g s t e 和s t e 检验方法的比较2 9 2 5 本章小结3 0 i v 目录 第三章抽象与细化方法的研究3 1 3 1 符号处理技术3 1 3 1 1 二叉判定图3 1 3 1 2 四值逻辑编码3 5 3 2 抽象的相关概念以及原理3 6 3 2 1 抽象的相关定义以及分类3 7 3 3 2 抽象方法3 9 3 3 细化处理4 5 3 3 1 符号常量4 6 3 3 2 符号变量4 7 3 4 抽象及细化方法在g s t e 中的应用4 8 3 5 本章小结5 2 第四章g s t e 抽象与细化方法的改进5 3 4 1 问题来源5 3 4 2 抽象与细化问题分析5 3 4 2 1 四值模型抽象的问题分析5 3 4 2 2g s t e 抽象细化的问题分析5 5 4 3g s t e 算法改进j 5 7 4 3 1 变量划分算法5 7 4 3 2 参数化表示和提取算法6 0 4 4g s t e 抽象细化处理算法改进6 3 4 4 1 改进g s t e 的软件框架6 3 4 4 2 改进的g s t e 关键代码6 5 4 5 算法分析及验证：6 8 4 5 1 对变量划分的算法的分析6 8 4 5 2 对参数化表示算法的分析6 8 4 5 3 算法验证一7 0 4 6 本章小结7 2 第五章结论与展望7 3 5 1 本文总结7 3 5 1 1 主要研究成果和创新点7 3 5 1 2 存在的不足：7 4 v 目录 5 2 工作的展望7 4 致 射7 5 参考文献7 6 个人简历及硕士期间取得的学术成果8 0 v i 第一章绪论 1 1 课题背景 第一章绪论 随着集成电路制造工艺的不断发展，各种集成电路系统已经获得广泛的应用。 这不仅推动了国民经济的发展，而且大大改观了社会生活和人们的日常生活。然 而如何保证电路系统正确、可靠地运行成为至关重要的问题。事实上，对电路进 行验证消耗了整个电路系统设计周期的三分之二，并且设计过程所需要的验证工 程师的人数一般是r t l 设计工程师的两倍【l 】。特别是随着电路设计的复杂性逐步 地提高，对大规模的电路进行设计验证已成为一个亟待解决的关键问题。 当前比较流行的验证方法就是模拟验证方法以及形式化验证方法。模拟验证 是最普遍的一种验证方法。它通过计算电路系统的可执行模型来查看电路的反馈 情况，然后，根据反馈的结果判断设计的电路是否完成指定的功能。一般来讲， 对电路模型计算的过程就是对该模型使用激励信号进行测试的过程。同需要一个 交互式的错误检测器一样，模拟验证也需要通过尽可能多的系统测试用例去找出 系统设计的错误 1 0 - 1 3 】。尽管模拟验证可以验证很多的测试用例，但由于输入变量 取值空间很大，所以它并不能模拟所有可能的测试用例，造成模拟验证不能完全 地对电路系统进行检错。 为了克服模拟验证不能覆盖所有错误的缺点，人们在1 9 7 0 s 提出了形式化的验 证方法。形式化验证利用严格的数学证明推导系统的行为，使得在利用形式化验 证方法对电路进行验证时，克服了模拟验证不完备的缺点【2 卅。 虽然形式化验证利用数学方法对电路进行完备性验证，克服了模拟验证内在 的缺陷。然而，由于形式化验证方法潜在地存在计算敏感性问题，使得在验证过 程中容易造成状态爆炸，所以它只能对很小的电路设计进行验证。因此，状态爆 炸问题成为形式化验证方法应用在大型工业设计的最大障碍。 电子科技大学硕士学位论文 1 2 形式化验证 1 2 1 形式化验证的基本概念和原理 形式化方法在不同的应用领域中具有不同的含义。要理解形式化方法在验证 中的应用方式，首先要弄清楚它的研究对象、研究目的和研究方法。当前，形式 化方法主要的研究对象是计算机系统的设计和验证。它主要的目的就是帮助工程 师构造正确可靠的计算机系统。而它主要的特点就是利用数学概念、方法和工具 来验证设计的正确性【l o 】。 一般来说，验证就是判断设计的电路系统在逻辑及功能上是否满足给定电路 系统的规范说明。形式化方法用具有形式语义的记号和工具明确地表述所要设计 的计算机系统的设计要求，即系统规范，并根据系统规范利用上述记号和工具对 系统具有的性质和最终实现的正确性进行严格的证明。它扩展了传统模拟输入向 量的范围，通过使用变量符号来表示任意的一个固定值，并将包含这些变量的表 达式同系统的模块联系起来，以便于所有状态都可以以符号的形式进行编码。 同应用的广度和可靠性要求一样，为提高其处理、存储以及提供全球网络连 接能力，电路系统设计的复杂性也越来越高，并且这种复杂性难以管理，常常导 致潜在的设计错误。为了避免这种风险，强烈地需要验证方法以表明系统规范满 足于它的设计。因此，如何全面而精确的验证这种敏感系统是一个严谨的问题。 形式化方法本身就满足用户的这种需求，从形式化方法的特点以及概念上讲，它 可以证明电路系统设计以及定义的规范之间的一致性问题，并且克服模拟过程覆 盖并不完全的缺点【6 】。 形式化验证用形式化法来验证电路系统模型是否满足性质规范。在这个过程 中，它利用功能强大的数学工具，而不是蛮力的对用例进行测试。因此，在一定 程度上，使用形式化验证可以实现自动化的处理。例如定理证明方法利用数学推 导来对电路进行验证。尽管可以对电路所处理的信息进行多个层次的抽象，但是 由于抽取电路信息建立的模型侧重点各有不同，按照抽象级别进行验证的方法也 各有不同。由于验证过程本身使用数学语言定义，使得验证算法更具一般性，所 以形式化验证方法可以在不同的抽象级别上对建立的模型进行验证，只是对模型 的信息以及表示不同而已。如图1 1 所示。 2 第一章绪论 图1 1 形式验证在每个设计阶段的使用 按照验证内容，形式化验证可以分为等价性验证和性质检验两种【1 5 】。 等价性验证要解决的问题是：如何解决两个在逻辑上设计不同的电路系统， 在功能上是否等价? 或者说，对一个设计的电路是否实现了另一个设计电路的功 能? 从整个数字系统的设计流程看，等价性问题几乎存在于电路系统设计的各个 阶段，如图l 一2 所示。 图1 2 数字系统设计流程的等价性问题 尽管等价性验证贯穿这个设计的流程，但是从目前研究和应用的情况来看， 对在同一层次上的两个设计之间的等价性问题验证的较多，而且是对电路的底层 1 电子科技大学硕士学位论文 进行验证，如逻辑综合前后的等价性问题。但是如果对不同的层次间的电路设计 进行等价性验证时，面临更多需要解决的问题。例如，如何从底层描述中抽象出 有用的信息，并与高层次设计进行比较等问题。 根据验证对象的不同，等价性又分为组合等价性和时序等价性两种。并且时 序等价性的验证有赖于组合等价性验证的结果【1 6 】。 性质验证是指对设计的电路方案不是验证它所有的行为，而是验证它是否满 足某些规则或性质，如图1 3 所示，进行性质验证的一般流程。不同于等价性验证， 性质验证更多地用于高层次抽象的电路验证，如行为级验证。在使用性质验证时， 需要对系统模型和要验证的性质进行形式化的描述，而验证的性质一般使用有限 状态机进行表示。然而，性质验证所用的规则和性质一般需要由用户或设计人员 给出。因此，存在需要检验多少性质才能保证验证完整的问题。 广 7 、广 满足 i 原始性质 i 一 形式逻辑h 性质描述卜 或不 l - j、 l j 、满足 (验证工具) _ 研，r 葡，翮t y i 原始设计 l 一 模型抽取u验证模型 l 一、，l j 图1 3 性质验证的过程 等价性验证和性质验证都属于功能性验证。等价性验证需要验证设计的电路 方案在经过自动工具或人工改变以后，是否保持了原有功能。比如，当使用逻辑 综合工具对电路进行优化以后，电路功能是否发生了变化。也就是说，综合工具 在进行综合时会不会产生错误。又比如，根据某种性能要求，对使用网表结构表 示的电路做局部调整时，就需要验证这些修改会不会改变电路的功能。然而，性 质检验需要验证的是设计者所期望的某些功能在设计中是否存在。比如，系统是 否执行了预期的动作等。 由于问题的特殊性，在具体实现时，等价性验证有两个途径：符号方法和增 量方法。 ( 1 ) 符号方法：首先将问题转化为一种特定的符号表示，然后使用各种特定 的问题求解方法进行验证，如b d d ，s a t 等。如果被验证的电路缺乏结构上的相 似性，或者在我们不了解设计电路的内部结构时，则用这种方法检验等价性具有 很多的优势。 ( 2 ) 增量方法：利用被验证电路结构的相似性，逐步验证局部电路的等价性， 直至获得整体电路的等价性。具体实现时，增量方法需要不断地辨识电路中的等 4 第一章绪论 价点，以此减少验证的复杂性。但是对于时序电路，情况要复杂的多，不仅需要 辨识等价点，还要辨识等价寄存器。我们可以看出这种方法对结构相似性较大的 电路系统具有很大的优势。 性质验证也有两个途径：定理证明和模型检测。 ( 1 ) 定理证明：首先从原始设计中抽取模型，使用形式逻辑的命题、谓词、 定理、推理规则表示该模型，要验证的性质则被表示成定理的形式。一阶逻辑和 高阶逻辑是定理证明常用的形式逻辑。定理证明是在验证者的引导下，不断地对 公理、已证明的定理施加推理规则，产生新的定理，直至推导出所需要的定理。 尽管高阶逻辑具有强大的描述能力，但是由于定理证明系统内置各种推理规则， 因此，高阶逻辑定理证明是一个比较复杂的过程。 ( 2 ) 模型检测：使用有限状态机表示设计，而验证的性质用时态逻辑描述。 然后，遍历有限状态机来验证设计是否满足性质。有限状态机模型通常采用k r i p k e 结构。使用线性时序逻辑以及分支时序逻辑描述电路复杂的时序关系。状态空间 爆炸问题是模型检测的主要缺剧1 8 。1 9 】。 按照验证方法，形式化验证又分为两类：基于问题求解的方法和基于状态遍 历的方法【1 7 j 。 基于问题求解的方法首先要选择适当的问题求解器，然后将验证问题转化成 该求解器能够接受的形式完成求解。常用的问题求解器有：定理证明器、s a t 求 解器、a p t g 求解器等。 ( 1 ) 基于定理证明的验证：运用公理、已经证明的定理以及推理规则证明电 路的描述是否正确。定理证明的优点在于：高度抽象，强大的逻辑表达能力；应 用不受限制，可以表示和验证几乎所有的系统行为特征。而它的缺点在于：需要 人工引导；需要验证者有良好的数学训练和经验【1 7 】。 ( 2 ) 基于s a t 的验证：对某个命题逻辑表达式的可满足性进行判断来确定设 计功能的正确性或提供设计错误的反例。这种方法简单易行，效率较高，广泛应 用于组合和时序电路的等价性和性质验证中。缺点在于对时序系统进行验证时， 需要将时序展开。展开的时序过多，s a t 求解效率变低。因此，采用这种方法一 般要牺牲验证的完备性为代价。 ( 3 ) 基于a t p g 的验证：通过测试向量自动生成技术进行等价性和性质验证。 该方法的优缺点和基于s a t 的验证方法类似。 基于状态遍历的方法一般用于对时序电路的验证。这种方法通过对有限状态 机的状态空间进行显示或隐式的遍历，达到验证性质存在性和设计等价性的目的。 电子科技大学硕士学位论文 基于状态遍历方法的优势在于其完备性，即只要性质存在，就会得到验证。空间 爆炸问题是基于状态空间遍历的主要缺点。 1 2 2 形式化验证方法的意义以及不足 在硬件设计领域，设计包含成百万级的电路系统已成为可能。研究电路系统 的正确性设计至关重要。尽管当前有许多设计自动化工具，仍不能保证设计的正 确性。例如，当年奔腾5 8 6 芯片中的除法运算错误造成i n t e l 损失了几亿美元【2 4 。2 5 。 因此为了增强设计的正确性，需要功能强大的验证方法加以保证。 形式化验证方法从2 0 世纪7 0 年代提出来以后，形式化验证一直没有很大的 发展。直到8 0 年代后期，传统的模拟验证的弊端出现之后，人们对形式化验证技 术从数学上完备地证明或验证电路系统的实现方案是否满足电路规范所描述的性 质颇感兴趣，使得形式化验证得到越来越多的关注，推动了形式化验证技术的迅 速发展。 尽管模拟验证对设计有效验证的方法简单，但是它存在很多弊端：首先，产 生测试向量来测试设计性质的方法比较麻烦，并且测试向量只能覆盖有限的状态 空间。其次，为了产生测试向量，设计者必须了解设计的细节并且要设置模拟器 以便于用一个特定的状态去测试特定的事件。再者，验证异步事件比较困难。最 后，通过测试向量验证设计的安全性比较困难【6 】。与模拟验证相比，形式验证有如 下优点：它使用符号技术提供了更好的测试覆盖范围并且没有测试向量模拟的一 些内在的缺陷，因此形式化验证是完备的，能够完全断定设计的正确性；形式化 验证对指定描述的所有可能的情况进行验证，而不是仅仅对其中的一个输入子集 进行多次验证，克服模拟验证的不足；形式验证可以从系统级到门级的验证，而 且验证时间短，有利于尽快地发现和纠正电路设计中的错误，缩短设计周期。例 如对i n t e lp e n t i u m4 处理器的设计验证而言，经过超过2 千亿测试向量的模拟验 证，仍有数以万计的错误未检测出来，并且需要几千个机器花费几个月的时间弘。 为了提高其获得模拟覆盖的范围以及减少获得这个覆盖范围的时间。一个方法就 是在多台机器上同时运行不同的激励信号矢量。另一种方法就是设计一个专用硬 件仿真来提高几个数量级的仿真速度。然而，尽管做了很多的努力，很多设计错 误仍不能发现，而使用形式化方法只需要几个星期就可以，并且只要对验证规范 进行有效地描述就可以完成，不存在无法覆盖的情况。 尽管形式化验证可以在性质层面上对设计进行全面彻底的检查，但是它却并 6 第一章绪论 不能保证电路设计完整功能的正确性，使得形式验证并没有广泛应用。 当前，形式化验证的一个最主要缺点在于计算过程需占有很大的内存空间。 当超出内存容量时，软件工具通常很难说明是哪里出了问题，或者不会对解决问 题提供有价值的指导，因此形式化验证虽然克服模拟验证不完备的缺点，但是形 式化验证方法的内在地计算敏感性问题使得它只能是对很小的设计进行验证。 1 3 形式化验证方法的发展 当前形式化方法最大的技术挑战就是状态爆炸问题，尤其在对大规模的集成 电路进行验证时，这个问题尤其严重。尽管在十几年的发展中，在技术上实现了 关键性的突破。例如在验证中引入符号化处理技术b d d 等，使得验证能力大为 提升，但是状态爆炸问题依然是其应用于大型工业设计的最大障碍。 1 3 1 抽象方法的提出以及意义 从上一节的描述中，我们可以了解目前形式化方法无法处理大规模的电路设 计的主要原因在于它不能更好的描述状态集，造成状态爆炸问题。在形式化方法 以后发展的时期，不少用于如何减少状态空间的方法提出来以缓解由于状态爆炸 而无法验证大规模设计的问题。目前，用于状态减少技术主要有对称技术，局部 有序技术以及抽象技术。在这些技术中，抽象技术被认为是处理状态爆炸问题最 常规和最灵活的方法，也是发展较快的技术 1 2 - j 5 】。 抽象作为解决状态爆炸问题的一种很有效的技术，它基于以下原理：含有数 据路径的系统性质通常和系统数据值之间具有某种关系。当前有两种常用的抽象 技术：影响锥缩减和数据抽象【2 睨8 1 。影响锥缩减通过去掉不影响性质所含变量值 的那些变量来缩减状态空间的规模。数据抽象需要将实际的数据集合映射成一个 小的抽象数据值集合。在很多情况下，通过抽象映射，仅知道抽象值就足够了。 如果把映射扩展到状态集合和迁移关系中，就可以得到一个模拟原有电路结构的 抽象模型。这两种抽象技术都在建立系统模型前，在较高层次上描述系统，并且 得到的抽象系统可以模拟原有的电路模型。为了使抽象技术实用，可以在不用建 立完整模型的情况下直接建立抽象模型，这可以从模型的高层描述实现，将抽象 过程和编译结合起来。更为简单的讲抽象就是去除或者精简一些细节，如同在验 证中去除原始设计中与验证性质无关的部分，而验证精简模型比验证原始模型要 有效的多。然而精简模型造成的信息丢失会有代价：验证抽象模型潜在地会造成 7 电子科技大学硕士学位论文 验证失败即出现伪报错问题。 当前形式化验证中，数据抽象应用较为普遍，它使用更高层次的描述一非确 定性自动机来取代原有的模型，而这个非确定自动机必须包含原有模型的行为。 使用这种更高层次抽象表示，减少了需要进行形式化验证的状态数，因此也减少 了形式化验证工具对状态空间的搜索时间。例如符号化抽象表示技术b d d 的提出 给当时已经陷入低迷的形式化提出了新的发展方法，它使得验证空间状态空间达 到1 0 1 2 0 的数量级，使得验证能力大为提升，而应用广泛的符号模型检测器n u s m v 就是采用这些技术。然而，当b d d 本身的容量过大时，也会存在状态爆炸的问题， 需要更好的抽象技术来解决状态爆炸问题。 1 3 2 模型验证方法 模型检验是形式验证的主要技术，其目标是证明某个电路是否具有规范某一 部分的性质。模型检验方法的基本思想是把时序电路抽象为一种有限状态机和 k r i p k e 结构模型，使用时序分支逻辑( c t l ) 语言来描述要验证的电路所应该满足 的性质；然后对状态机进行分析或者使用状态空间搜索技术来判断时序逻辑所描 述的命题正确与否【1 6 】。符号模型检验方法就是在一般模型检验技术中引入b d d 技 术对电路进行验证的一种方法，它使用b d d 来表示整个电路，并将状态转换函数 和输出函数合在一起加以表示，这称为电路模型的转换关系。 尽管符号模型验证方法引入b d d 技术使得验证能力大为提升，验证的状态空 间达到1 0 1 2 0 ，但是像s o c 这样大的电路系统，使用b d d 表示电路系统也会使用 较大的内存空间，并且模型检测在状态空间搜索中需要保存验证的中间结果，更 加剧了状态爆炸问题的产生。 在当前的符号模型检测技术引入一种新的称为基于反例指导的抽象细化 ( c o u n t e r e x a m p l e g u i d e da b s t r a c t i o nt e c h n i q u e ) 技术【5 】，它在模型检测中对状态模型 进行抽象化处理，使它扩展到存在性抽象验证的一般框架，它把符号模型检测和 存在性抽象整合到一个统一的框架内。该方法效率继承了模型检测技术的高效性 以及无需人工干预的优点。该技术以验证系统相对小的框架表示开始，逐渐地计 算这个系统的精确抽象表示。验证过程的关键就是从错误的否定中抽取信息。并 且在对性质的描述上采用了a c t l * 描述，使得该验证方法对有限和无限轨迹验证 是完整的。 这种反例指导抽象细化技术主要的优势： 第一章绪论 1 ) 它描述了一种从程序文本中抽取抽象函数的方法。在这个方法中，程序根 据控制流程来把状态空间划分等价类，通过这些等价类可以获取电路系统 中具有等价关系的状态集合，并将这些状态集合划分抽象状态。 2 ) 在抽象细化的模型检测技术从程序代码中抽取的抽象函数在变量组上定 义，并允许在抽象函数中表达涉及多个变量的条件，有助于使抽象状态空 间更小。 3 ) 引入符号算法判断抽象中产生的反例是否是一个伪反例或者是否产生一 个具体的反例。如果产生的反例是个伪反例，它会通过查找的反例结果的 最短前缀来判别是否对应具体模型中某个具体的状态轨迹。 1 3 3 有界模型验证 由于当前对布尔可满足问题研究领域技术较为成熟，a b i e r e 在1 9 9 9 年将布 尔可满足方法引入模型检验技术中，进而提出了电路的有界模型验证方法。有界 模型的基本原理就是在初始状态对电路模型的转移关系进行有限次数的迭代计算 从而得到一个有限的状态空间，然后利用可满足问题的引擎在这个状态空间中寻 找违反验证的性质的电路行为。这里有界是指对于给定的路径长度，如果从初始 状态出发到达指定的路径长度，验证是否找到反例，如果在这个状态空间内没有 找到，则将状态路径长度增加。 我们知道电路的功能模型就是一个布尔函数集，布尔函数除了使用b d d 形式 进行正则表示，它还可以使用合取方法进行表示，这在一定程度消除了内存爆炸 问题。然而这并不是一次就可以将将布尔函数表达出来。为了得到使布尔函数结 果为真的情况，需要通过搜索的方式来对布尔函数进行赋值判断该赋值是否使得 函数结果为真。如果我们找到这样的取值，则称布尔函数函数是可满足的。如果 我们在整个状态空间内并没有发现这样的赋值情况，则说明这个布尔函数在这个 状态空间内并不存在这样的赋值使得布尔函数为真，在这种情况下，我们称布尔 函数是不满足的。 s a t 问题求解在近几年得到快速发展，并应用于更多的领域内。s a t 问题求 解算法根据求解的方式分为两种：完全算法和不完全算法。完全算法主要包括 s t i i l m a r c k 算法和d p l l 的搜索算法；不完全算法包括采用各种启发算法的随机方 法，这种方法在人工智能领域有很多应用。 当前有界模型技术获得极大地发展，并已经成功应用与工业界的集成电路的 9 电子科技大学硕士学位论文 验证： 1 ) 利用有界模型检验的方法，对m o t o r o l a 的p o w e r p c t m 微处理器进行验证， 使其安全性得到了保证。 2 ) 利用有界模型检测方法对c o m p a q 的a l p h a 的微处理器进行模型检验，提 高了验证的效率，使其检测时间从几天缩小至几分钟，缩短了其产品的上市时间。 3 ) t h u n d e r 和f o r e c a s t 是i n t e l 公司进行有界模型检验的工具。其中前者 利用可满足性问题的解决方案进行设计验证，而后者利用b d d 的电路模型表示方 式进行设计验证。在对于验证p e n t i u m4 r m 进行设计验证时，通过试验结果的比较 可以看出利用可满足性问题的解决方案在性能和效率上明显优越于后者f o r e c a s t 。 1 3 4