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

揍簧 摘要 随着集成电路的设计规模越来越大、复杂度越来越高，产晶上市时间却越来 越紧迫，集成电路的验证变得越来越困难。2 0 0 3 年度的国际半导体技术发展报告 指出，验证已经成为集成电路设计流程中的最大瓶颈。传统的模拟验证因其测试 周期长、不能完全覆盖，已经不适合当前对集成电路验证的需求。形式化验证其 原理是使用严格的数学推理来证明一令系统满足全部或部分规范，从焉提高了验 证的正确率，保证了市场需求。另外，它作为对传统基于模拟验证方法的补充， 豳益引起入们的关注。 本课题在较为全面、深入地研究和总结国内外形式验证技术研究成果的基础 上，对当前主流形式化验证方法中的推广化符号轨迹赋值( g s t e ) 验证方法进程 了深入的研究和扩展，以期进一步减少伪报错现象，提高g s t e 验证方法在集成 电路验证中的正确性。 本课题在研究方法主，首先，针对符号轨迹赋值( s t e ) 验证方法的基本理论 和技术，详细分析其优点和不足。对s t e 验证规范做出的图形化扩展和断言图， 以及基于断言图的验证算法做认真的论证和分析。然后，分析g s t e 验证方法， 比较s t e 和g s t e 的优缺点。进一步分析由于g s t e 继承s t e 的抽象行为，而带 来的伪报错问题产生的原因。在以上学习和分橱的基础上，本文提逡g s t e 中s m c 算法的改进算法，并通过验证平台f o r t e 对改进后的算法进行编码实现和验证。 结果显示，在降低伪报错和查错方面都有较大改良和提高。另外，在不熟悉电路 的情况下，进行集成电路验证时，可以通过使用g s t e 中改进的s m c 算法来验证 电路的正确性。若非常熟悉本电路的设计，也可以按照回路进行手动扩展。 同时，针对验涯工具的盘动化程度，本谍题创造饿地提出并设计了麴动捶入 故障容错结构工具。在实际的某个电路设计流程中，如果验证结果返回为错误， 对于没有参力曩本电路设计的人员来讲，发现镄误并改正错误将是非常困难的。大 部分电路设计的修改和优化，只是涉及电路部分结构的变化。如何能更有效、更 准确地给出问题所在，是保证验证电路设计正确性的酋要问题。 关键词：形式化验证，g s t e ，伪报错，s m c ，故障容错 a b s t r a c t 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 ya n dt i g h tt i m e t o - m a r k e rs c h e d u l e so ft o d a y sd i g i t a l ， v e r i f i c a t i o ni sb e c o m i n gm o r ea n dm o r ed i f f i c u l t t h er e p o r ti ni 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 pf o rs e m i - c o n d u c t o r2 0 0 3h a sp o i n t e do u t , t h a tv e r i f i c a t i o nh a sb e e nt h e b o t t l e n e c ki nt h ei cd e s i g nf l o w e x t e n s i v es i m u l a t i o n ，t h et r a d i t i o n a la p p r o a c hi sn o l o n g e ra d e q u a t e , b e c a u s ei ti st o ot i m e - c o n s u m i n ga n di tg i v e sn oa b s o l u t eg u a r a n t e e s a b o u tt h ec o r r e c t n e s 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 nm e t h o d sa r ea p p l i e dt oa c t u a l l y c o n s t r u c tam a t h e m a t i c a lp r o o ff o rt h ec o r r e c t n e s so ft h ed e s i g n 。s oi tc a ni m p r o v et h e v e r i f i c a t i o n sc o r r e c t n e s sa n da s s u r em a r k e tr e q u i r e m e n t i n a d d i t i o n ,f o r m a l v e r i f i c a t i o n , a so n eo fc o m p l e m e n t a r ya p p r o a c h e s ，h a sb e e np u tf o r w a r dt os o l v et h e s e p r o b l e m s w i t hl o t so fp r e v i o u sw o r ko nf o r m a lv e r i f i c a t i o no nl a r g ed i g i t a li cd e s i g n , s t u d y a n de x t e n dg s t em e t h o dw h i c hi so n eo ft h ec u r r e n t l ym o s ti m p o r t a n tf o r m a l v e r i f i c a t i o nm e t h o d sd e e p l yt or e d u c et h ef a l s en e g a t i v ef u r t h e ra n di m p r o v et h e c o r r e c t n e s sb yu s i n gg s t em e t h o di ni n t e g r a t ec i r c u i tv e r i f i c a t i o n o ns t u d ym e t h o d s ，t h ep a p e ri n t r o d u c e st h eb a s i ct h e o r ya n dt e c h n o l o g yo fs t e v e r i f i c a t i o na l g o r i t h ma n da n a l y z e st h es t r o n g p o i n ta n ds h o r t a g ei nd e t a i l 。f o re x t e n d i n g s t ev e r i f i c a t i o ns p e c i f i c a t i o nu s i n gg r a p h i c a lt h e o r y , i n t r o d u c i n gt h ec o n c e p to f a s s e r t i o ng r a p ha n di m p l e m e n ta s s e r t i o nb a s e dv e r i f i c a t i o na l g o r i t h m ，t h ep a p e r a n a l y z e st h e mi nd e t a i l t h e ni m p o r tc o n c e p to ft h eg s t ea n dc o m p a r et h ea d v a n t a g e s a n dw e a k n e s s e sb e t w e e ns t ea n dg s t e g s t ei n h e r i t st h ea b s t r a c tb e h a v i o ro fs t e i tm e a n si tt a k e sw i t ht h ef a l s en e g a t i v ep r o b l e m s 弧ep a p e ra n a l y z e st h er e a s o nt h a t m a k e st h ef a l s en e g a t i v ep r o b l e m sa n dp u t sf o r w a r da ni m p r o v e da l g o r i t h mo ng s t e s s m ca l g o r i t h m a tl a s tu s ef o r t et ov e r i f yt h ei m p r o v e da l g o r i t h m 。t h er e s u l ts h o w s t h ei m p r o v e da l g o r i t h mm a k ep r o g r e s si nr e d u c i n gt h ef a l s en e g a t i v ea n dc h e c k i n gf a u l t i fs o m e o n ei sn o tf a m i l i a rw i t ht h ec i r c u i t ，t h e yc a nu s et h ei m p r o v e da l g o r i t h mo f g s e tt ov e r i t yt h ec i r c u i tc o r r e c t n e s s f o ro t h e r s 。讯e yc a ne x t e n dt h el o o pb yh a n d s a tt h es a m et i m e ，f o rt h ea u t o m a t i o no ft h ev e r i f i c a t i o nt o o l ，b r i n gf o r w a r daw a y n a m e da u t o m a t i ci n s e r t i o no ff a u l tt o l e r a n t w en o t i c et h a ti nt h ep r a c t i c a ld e s i g n i n g f l o w , i ft h ev e r i f i c a t i o nr e t u r n sf a u l t f o rt h ep e r s o n sw h oh a v en o tt a k e np a r ti nt h e d e s i g n ，h o wt of i n dt h ed e s i g n i n gf a u l ta n dm e n dt h e mi sv e r yd i f f i c u l t h o w e v e r , t h e h a b s t r a c t m o d i f i c a t i o no fm o s td e s i g n i n gc i r c u i t si so n l yt om o d i f yap a r to ft h ec i r c u i ts t r u c t u r e s h o wt or e s o l v et h ep r o b l e mm o r ee f f i c i e n t l ya n dd e t a i l e di st h ec h a l l e n g et om a k es u r e t h ec o r r e c t n e s so ft h ec i r c u i td e s i g n i n g 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 ds 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 ，f a l s e n e g a t i v e ，s t r o n gm o d e lc h e c k i n g ，f a u l tt o l e r a n t i l i 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工 作及取得的研究成果。据我所知，除了文中特别加以标注和致谢的地 方外，论文中不包含其他入已经发表或撰写过的研究成果，也不包含 为获得电子科技大学或其它教育机构的学位或证书而使用过的材料。 与我一同工作的同志对本研究所做的任何贡献均己在论文中作了明 确的说明并表示谢意。 签名：阻日期：年月日 关于论文使用授权的说明 本学位论文作者完全了解电子科技大学有关保留、使用学位论文 的规定，有权保留并向国家有关部门或机构送交论文的复印件和磁 盘，允许论文被查阅和借阅。本人授权电子科技大学可以将学位论文 的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或 扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后应遵守此规定) 、 f、 签名：龇导师签名：王笠些 l 日期：年月 鑫 第一章绪论 1 1 引言 第一章绪论 集成电路自从如现就大大改观了社会生活，并进一步地促进了社会的发展。 从早裳的第一个集成芯片4 0 0 4 的出现，到今天的c p u 以及诸多应用于其它方面 的集成电路，如：m p 3 、机顶盒等，集成电路的集成度已非昔日可比。但是一个 闷题也匿益突显出来，那就是：如何保证更大集成度的电路能够正确、可靠地工 作。这个问题，不仅涉及到电路的设计，更涉及到电路的验证与测试等。i c 流片 l 回来的芯片如果无法正常运作，大致分为逻辑或功能上的错误、时序润题、l c 制造上的问题以及其它问题。有时同时会有两个以上的b u g ，例如同时有时序以及 功能不正确的问题。据一份统计结果，在逻辑上或功能上的错误竟然占了7 4 左 右。事实上逻辑或功能上的错误大部分是可以避免的，雨避免这个闯题的方法不 外乎就是做验证( v e r i f i c a t i o n ) 。2 0 0 3 年度的国际半导体技术发展报告( 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 pf o rs e m i c o n d u c t o r ，i t r s 2 0 0 3 ) 2 1 指出，验证已经成为集成电 路设计流程中开销最大的工作。在目前的工程项目中，验证工程师的数目超过了 设计工程师，对于复杂的设计更是达到了2 ：1 或者3 ：1 的比率；验证的时闻占整个 设计周期的5 0 一8 0 。因此，对设计的正确性的验证成为设计的瓶颈，a s i c 的 验证者面临一系列的压力。 如何检查设计的正确性，即设计验证，是设计大规模复杂数字系统中的关键 问题。设计验证的复杂度随着芯片的规模呈指数增加，但是如何保证这些复杂的 超大规模集成电路设计的正确性离题还没有解决。可以说集成电路制造的能力超 过了集成电路的设计能力，为了充分发挥投资惊人的集成电路生产线的生产能力， 需要更多的设计者及时提供大量复杂的设计。另外，计算机技术和通讯技术的高 速发展，使得数字系统渗透到整个社会的各个领域。特别是对于安全性要求较高 的很多关键场合也大量采用了嵌入式系统。同时，各种数字硬件的设计变褥十分 复杂，用传统的设计方法已经难以应付。集成电路生产工艺的复杂性，决定了它 的试制费用相当昂贵；电子产品市场竞争的激烈性，导致产品上市时间成为企业 生存的关键因素，因为产品的上市时间意味着产品的市场占有率。设计中遗留的 电子科技大学硕士学位论文 一些微小的错误或漏洞将可能造成巨大的经济损失或者导致人员伤亡等灾难性后 果。这些都是电路设计者和系统设计者们面临的严峻挑战。 1 2 验证的基本概念和系统验证的原则 1 2 1 验证的基本概念 验证就是测试设计在功能、时限、可测试性和功耗等方面是否达到了给定的 系统规范说明的要求。对应于v l s i 设计的过程，验证分为设计验证( d e s i g n v e r i f i c a t i o n ) 和实现验证( i m p l e m e n t a t i o nv e r i f i c a t i o n ) 两部分，如图1 1 所示为 v l s i 设计与验证的流程图。 综合步骤 验证步骤 逻辑优 设计验证 实现验证 图1 - 1v l s i 设计与验证流程 设计验证是针对一个设计说明( s p e c i f i c a t i o n ，也称规范说明) 来检验其实现 ( i m p l e m e n t a t i o n ) 的正确与否，实现验证( i m p l e m e n t a t i o nv e r i f i c a t i o n ) 是为了保 证手工或自动设计综合过程的正确无误。验证的任务主要有下列三个方面： 1 验证原始输入描述的正确性； 2 验证设计的逻辑功能是否符合预定的逻辑功能： 3 验证设计结果的时间关系是否符合预定的性能指标。 1 2 2 系统验证的原则 系统设计验证【3 1 是一项非常复杂的任务，如图1 2 所示，它一般要花费整个设 2 第一搴绪论 计周期的5 0 以上的时间。因此，如何提高系统设计验证工作的效率，将对缩短 整个系统设计周期、减少产晶上市时闻( t i m e t o m a r k e t ) 具有非常重要的意义。 基于此，在进行系统芯片验证工作时，应该遵循以下三个原则。 图l - 2 系统设计中的验证 1 统一的验证耀境 一般系统芯片中的所有硬件都要经历r t l 级、门级到最终的物理级三个设计 层次的验证。如果针对每一个设计层次都构造一个测试套，那么，设计的任务就 非常复杂。通常，人们采用统一的验证环境，即在不同的设计层次采用同一个测 试台，从而降低了验证的复杂度。在构造统一的验证环境时，最重要的是，在进 行模块划分时尽量避免出现粘连逻辑( g l u el o g i c ) 。如果设计中没有粘连逻辑， 通过将原测试台中r t l 描述换成门级网表就可完成相应的门级验证。 2 。严格的鸯底向上( b o t t o m u p ) 验证 一般而言，设计越小，就越容易发现设计中的错误，相应的调试工作就越简 单。如果没有进行严格翦模块验证就鸯接进行系统验证，调试工作将会非常复杂， 电子科技大学硕十学位论文 以至于你根本无法进行。 3 多角度验证 对于系统级这样复杂的芯片设计，可能出现的问题是多种多样的。为了提高 设计的可靠性，一般要进行多角度验证，即不仅要采用传统的动态验证技术进行 验证，还要利用新的静态验证技术来进行验证。但随着设计复杂性的提高，人们 不再以门级仿真作为验证的最后一环( s i g n o f f ，v e r i f i c a t i o n ) ，而是改用静态验证， 特别是静态时序分析，作为最终验证。 1 3 验证方法综述 在目前的验证方法中，主要有软件仿真、形式验证和f p g a 验证。 从方法的角度上，验证分为形式化验证与模拟验证。相比较而言，形式化验 证在理论上比较成功，但是在实际应用中受电路规模等因素制约，其应用有限。 目前存在的验证方法以及技术，如图1 3 所示。 图l - 3 验证技术 使用最为广泛的功能验证方法是动态的，之所以被称为动态是因为输入图形 激励信号是在一段时间( 几个时钟周期) 内生成并应用于设计的，相应结果会被 用于与参考黄金模型进行比较，以检验其与规范之间的一致性。下面将详细阐述 4 第一章绪论 现在正在使用的图1 3 中的各种验证技术。 1 3 1 形式化验证 形式化验i 正t 4 j 提出于2 0 世纪9 0 年代，被认为是种有前途的验证方法，包括 等价性检验、模型检验、定理证明和语言包含。形式化验证的涵义是：用形式的 方法来确立设计的实现( i m p l e m e n t a t i o n ) 满足规范( s p e c i f i c a t i o n ) 的要求。形式 化验证方法有多种应用，可用之将一个设计在不同的抽象级别与参考设计相比较， 戮对其进行验 歪，如图l 所示。 图l o 形式验诞在每个设计阶段的使用 形式化验证用于验证不同设计层次之间的一致性，比如：寄存器传输级与门 级。此处，不妨将寄存器传输级称为需求或规范，而将门级称为其实现，这样两 个层次之间的验证可以发现实现与需求是否致。同样的，如果验证是发生于系 统需求级与算法缀，那么算法级便为实现，系统需求级划当然为需求了。如此， 一层层的验证下来，可以尽可能保证最终电路与需求致。克服了传统验证方法 如模拟和测试的不足，实践证明形式讫验证确实通过形式规范和证嗔焉增强了对 系统的理解，进而发现了设计错误：或者通过形式化的自动验证发现了用其他方 法不能发现的设计错误。因此有充分的理由说骧形式化方法是计算机系统设计验 证的一条有效途径。但是，在逻辑上存在一个问题，那就是验证无法确定本层是 否正确，如：在寄存器传输级的验证便无法确定该寄存器传输级描述是否正确， 即逻辑上讲，无法验证自身是否正确。 目f j 因外不少大学、研究机构及大公司( 如i n t e l 和i b m 等公司) 对形式化验 证方法展开了深入的研究，取得了显著成果。许多研究成果已不再停留瓷实验室 5 电子科技大学硕十学位论文 阶段，而被成功应用到实际的工业设计中，如微处理器、浮点部件、协议、存储 阵列和通讯硬件等。如v e r p l e x 公司的b a l c k t i ef u n c t i o n a lc h e c k e r 和c o n f i r m a l l o g i ce q u i v a l e n c ec h e c k e r 。c a d e n c e 公司的f o r m a lc h e c k 工具、i n t e l 公司的v o s s 系统、西门子公司的c v e 验证环境等都能处理较大型的设计验证项目。另外，许 多形式化验证的工具已经开发出来，并成功地进入工程应用领域。例如i n t e l 公司 开发的f o r t e t 5 1 系统，它主要无缝地把模型检验和定理证明集成在一起，并在验证 p e n t i u mp r o 处理器的浮点运算中显示了强大的作用。c a d e n c e 公司的s m v ( s y m b o l i cm o d e lv e r i f i e r ) 【6 】能自动有效验证组合逻辑电路以及交互自动机的性 质。台湾清华大学开发的系统a q u i l a l 7 能够对大规模时序设计进行等价性检验。 在国内，我国学者做了不少研究。清华大学研究人员针对同步时序电路的 v h d l 描述，提出了电路建模和模型检验方法【8 。9 】。复旦大学研究人员在提高可满 足性问题的求解效率方面进行了研究【i 们。中科院对模型检验及等价性验证方面做 了深入的研究o4 1 ，提出了一些高效的验证方法。 下面将分别介绍等价性检验( e q u i v a l e n c ec h e c k i n g ) 、模型检验( m o d e c h e c k i n g ) 和定理证明( t h e o r e mp r o v i n g ) 三种形式化验证方法。 1 等价性检验 等价性检验的主要目的是在一个设计经过变换之后，穷尽地检查变换前后功 能的一致性，即证明设计的变换没有产生功能的变化。这里所说的设计变换可以 是综合、布局布线、测试、时钟树的插入、扫描链的重排序、f p g a 到a s i c 的转 换等。如果要对一个现有的门级或物理级网表写出其r t l 级模型，以使原来的设 计能够重用，这时也可以利用等价性验证。另外，如果设计者要将原来设计的功 能进行必要的修改，等价性检验产生的信息可以用来帮助设计者确认所做的修改 是否达到了目的。 在整个v l s i 设计流程中，如图1 5 所示，最初的规范应当对于用户的要求来 说是正确的，这个规范在后来一步一步地实现和细化，每一步实现的行为应当同 前面的设计相一致。例如，对于一个专用集成电路( a s i c ) 的设计，要把寄存器传 输级( r t l ) 的设计用自动综合工具把它转换为网表级的设计。又如，对于一个结构 化的全定制设计，由人工来验证变换前后功能的一致性。不仅如此，对于某些设 计性能的优化，也可以把优化前后的设计进行等价性检验，以便验证优化后的功 能不变。这种等价性检验保证了百分之百的覆盖，而不必担心检验的完全性。在 最后的版图设计中，功能的等价性检验还要同定时工具一起使用，以便保证版图 的正确性。 6 第章绪论 功能 致 凌辘 致 功缝一致 时序功耗 图1 - 5v l s i 设计漉程中麓等赞性验证 等价性验证的基本原理是建立被比较的两个模型之间的关系。检验的依据是 数学的定理和公理，以及设计实现所利用的标准单元库的精确描述。等价性检验 程序自动确定被比较的两个设计的关系，而不需要用户的输入。因此它的优点是 使用简单，且很容易集成到设计流程中。目前c a d e n c e 公司已经推出了等价性验 证工具a f f i r m e r ，它把建立被比较昀两个设计之间的关系和等价性证明合并为一个 步骤进行。它首先假定两个设计的锁存器和存储器元件是等价的，然后利用随机 输入向量对于两个设计进行功能模拟，并且根据模拟结果划分锁存器。在没有用 户干预的情况下，利用二叉判定树和可满足性算法，它能够很快地识别两个设计 之间在功能上相对应的节点。当然每个算法可能把问题分解为若干子问题，著且 对于这些子问题采用另外的算法。利用这些互补的办法可以验证对应结点的等价 性。 当等价性检验工具检测遗两个设计之闻在功能上的一个差剐时，它就显示一 个反例，即一组原始输入或者若干锁存器以及它们引起这个差别的原始输入的取 值和锬存器的取值，并且显示一些帮助设计者分析产生这些差别的原因的信息。 如果把模拟程序同等价性检验工具集成在一起，就可以利用这些信息进行模拟以 便找出造成这种差别的原因。针对组合电路的等价性检验算法1 1 5 】提出了一种新的 组合电路的新模型o f s m ，用o f s m 表示组合电路所需的节点数是电路中输入变 量的多项式级的规模。 2 。模型检验 模型检验【1 6 l ( m o d e lc h e c k i n g ) 最初在二十世纪8 0 年代早期由c l a r k e 1 7 】和 e m e r s o n 提高，它是一种自动纯程度很高的形式纯验证方法。它把要验证的设计抽 象为状态迁移系统的模型，例如有限状态机( f i n i t es t a t em a c h i n e ) 或者k r i p k e 结 构，如匿1 - 6 酝示。其基本思想是用c t l 公式表示程序绒电路的时序性质，用f s m 7 屯子科技人学硕士学位论文 表示程序或电路的状态转移的抽象结构，通过遍历f s m 来检验时态逻辑公式的正 确性。随着程序或电路规模的增大，状态数目将呈指数增加而引起组合爆炸，它 是模型检验的关键问题。在1 9 7 8 年，利用识别模型中的次要因素及其层次结构的 对称性，r k u r h s n a 提出了“同态化简( h o m o m o r p h i cr e d u c t i o n ) 的方法【1 7 】。其 实质是将复杂的数据结构和控制序列，同态映射到相对简单的数据结构和控制序 列，而后者保留着用于验证的足够信息，从而减少了计算复杂度。9 0 年代初，又 出现并发展了符号模型检验【1 8 舶1 和二叉判定树( b d d ) 技术【2 0 1 。符号模型检验的 含义是用一个布尔公式表示使它满足的所有状态，而这个布尔公式则以压缩方式 存储在b d d 中，在遍历过程中己经标识的状态也用布尔函数的b d d 表示。通过 适当的排列变量的顺序，可以大大简化图的结构，这使得模型检验可以处理大规 模的数据结构和控制序列，从而在一定程度上缓和了组合爆炸问题。 模型检验的优点是完全自动化。如果系统不满足给定的性质，检验结果可以 给出反例，从而帮助设计人员找出设计的错误。这一点可能是它最具有吸引力之 处。模型检验已被用于验证大量的实际设计，包括与奔腾处理器的浮点运算单元 复杂度相同的s r t 除法算法，并且检查出奔腾处理器的错误。通常模型检验仅限 于规模小的系统，因为模型检验要搜寻遍整个系统所能到达的状态，这就不可避 免地遭遇内存爆炸的问题。对于规模大的系统，特别是一些包含大量数据通路的 部件，例如乘法器，此问题尤为突出。 h d l 语言描述 一 设计 嘉蠹鬟釜 、 命题磊蔷覆垂检查 命题 ( a s s e r t i o n ) 图l - 6 模型检验 3 定理证明 定理证明的原理【2 l 】是：首先，定义一种数学逻辑，该逻辑系统实际上是一个 形式化的系统，由一系列公理和推理规则组成。然后，用这种数学逻辑分别表示 被验证系统和其被期望的特性。所谓定理证明就是从系统的公理出发，使用推理 规则，逐步推导出其所期望的特性的证明过程。证明所需要的步骤依赖于系统的 公理和推理规则，在某种程度上也依赖于其派生定义和中间引理。定理证明器的 类型很多，既有高度自动化的通用系统，也有为专用目的而设计的、具有交互功 r 第一章绪论 能的系统。自动化的定理证明系统可用作通用的搜索程序，并且在许多领域都取 褥了显著的成就；交互式的定理证明系统则更多地焉于数学的系统和形式亿处理， 以及形式方法的机械化。 与模型检验不圈，定理证晚可直接处理无限的状态空闻。它使用类似予结构 化的推导过程来证明具有无限状态的系统。另外值得指出的一点是，由于大多数 定理证明器是交互的，在找到证明的过程中，用户的直觉往往起鹫决定性的作用， 因此定理证明的速度相当慢而且容易蝴错。 。3 2 其他验证方法 l 。软件仿真 软件仿真是指建立系统模型，进行反复的软件模拟。它是目前硬件设计验证 的主要途径。但是随着芯片规模的不断扩大，对于超大规模集成电路，运行仿真 和检查仿真结果需要耗费大量的时间，并且仿真是不能穷举所有的情况的。结果 是消耗大量的时间，却很难发现设计底层的错误。 2 。硬 孛仿真 硬件仿真不是靠计算机通过运算束模拟，而是通过相应的硬件，实现被仿真 的逻辑结构，或者通过实际运行系统功能来进行仿真，因而其速度比计算祝软件 模拟要快得多。硬件仿真目前只限予进行功能验证、故障模拟，以及部分的时序 验证。硬件仿真为我们提供了一个不错的加速仿真的途径。但是它的缺点主要是 硬件仿真器相当昂贵，仿真成本较高，而且确定设计和硬件仿真器间的映射关系 也要花费大量的时间。另外，它与软件仿真一样，只能用典型的情况对系统进行 考察，不可能对大爝模的系统进行穷尽的模拟。 3 测试 测试是保证设计正确性的另一个手段。对硬件系统的测试是在加工麓进霉亍的。 但是测试只能证明错误存在而不能证明错误的不存在。对于复杂的系统，进行穷 尽的测试也是不可能的，甚至设计一个有效的测试方案和评价其故障的覆盖都是 相当困难的。现在入们普遍认为利用随机测试也不能对予解决问题有很大的帮助。 事实上，有些错误甚至不可能用上述方法发现。问题的实质是由于目前集成电路 的高度复杂性，极大的损害了模拟时的可控制性和可观察性。 4 模拟验证 模拟验证一般来说是属于功能验证，因此比较起形式化验涯起来，其露样西 9 电子科技大学硕士学位论文 临着复杂度问题。但是通常的模拟验证方法，并不会像形式化验证那样做到至善 至美。很多情况下，模拟验证只是取得一部分结果。想要取得更好的结果，其复 杂度自然就变得更高。基本的思路就是：从电路的描述( 语言描述或图形描述) 生成模型，然后将外部激励信号加到其相应的接口，观察模型在外部激励信号作 用下的反应来判断该电路系统是否实现了预期的功能。即将测试同时施加于两个 电路，一个是待验证电路，一个是参考电路( 一般假设为正确电路) 。比较两个电 路的输出是否一致，如果一致就可以认为待验证电路通过了此次模拟验证，如图 1 7 所示。 输入 序列 输出 序列 图l 一7 模拟验证原理 然而，前面的方法仅能用来验证中等规模以下的电路。对于大型时序电路， 如果使用传统基于有限状态机遍历的方法进行验证，很可能因为状态爆炸而失败。 因此，在实际的设计方法中，常使用组合电路验证方法来降低算法的复杂度。通 过给规范与实现设定相同的状态编码，并要求状态位的名称保持相同，使得设计 规范与实现电路的存储元素存在一一映射关系。这样就可以把时序电路分解成相 对应的组合模块，然后利用组合验证方法证明各组合模块的等价性【1 。7 1 。然而当两 个电路不存在存储元素的一一对应关系时，上述方法不能应用，只能应用状态遍 历的验证方法，这就导致其处理能力非常有限。一般情况下，当状态位数超过几 百时，状态遍历方法就存在极大的困难。时序电路的形式化验证一直是困扰学术 界的难题，如何发挥组合验证技术的优势与提高处理能力是急需解决的关键问题。 1 4 研究意义、选题依据 在国外，s t e ( s y m b o l i c t r a j e c t o r ye v a l u a t i o n ) 符号轨迹赋值是一种基于格子 的模型检测技术。现正在被许多公司使用，像i n t e l ，i b m ，m o t o r o l a 2 2 2 7 1 。s t e 在 集成电路验证方面显示出强大的优越性，例如，它曾经成功应用于检验几种 m o t o r o l a 的拥有百万门级电路的存储单元。在i n t e l ，它曾被应用于检测浮点数单 元和1 2 ，0 0 0 个门的复杂数据路径单元。在s t e 基础之上，g s t e ( 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 ye v a l u a t i o n 推广化符号轨迹赋值) 从语言风格、基于模拟的模 型检测算法、简单抽象域的映射算法三个方面有了极大的提高。 1 0 第一章绪论 目前，形式化验证方法日益为业界所关注。除了国外不少的大学、研究机构 及大公司( 如i n t e l 和穆m 等公司) ，对形式化验证方法展开深入研究之外。同时， 很多公司融经着手把研究成果产品化和产业化了，并取得了显著成果。另外，许 多形式化验证的工具已经开发出来，并成功地进入工程疲用领域。 综合看来，形式化验证工具的研究具有非常高的学术价值和产业价值。这些 正是本课题的研究意义，同时也是本课题的选题依据。 本课题依托于网川省青年软件创新工程基于g s t e 的集成电路验证软 件开发包”项目，进行研究和开发。 1 5 主要研究内容和章节安排 1 5 1 主要研究内容 本文依托以上的研究背景，对基于g s t e 的验证细化问题进行研究，在把集 成电路抽象为模型魏同时，减少伪报错，使其缝更准确黪证明集成电路的露行性。 所以本文的主要研究内容包括以下四个部分： 1 研究验证过程中伪报错产生来源的问题； 2 研究如何把基于g s t e 的伪报错回溯分类细化； 3 研究验证由伪报错导致结果出错率较高的问题； 4 。磺究验证软件的容错、纠错能力。 1 5 。2 章节安排 本文的相关章节安排如下： 第一章，绪论。 主要介绍了验证的基本概念，系统验证需遵循的基本原则，传统的形式化验 涯方法和其他的验证方法，以及国蠢外研究现状。其中着重阐述了墨蓠流行的形 式化验证方法，然后在该研究背景下讲述了本文的研究重点。 第二章，s t e 和g s t e 验证方法简介。 主要介绍形式化验证方法中的符号轨迹赋值和推广化符号轨迹赋值。首先介 绍了符号轨迹赋值的历史背景和它的局限性，然后引出了推广化符号轨迹赋值。 电子科技大学硕士学位论文 其中涉及到许多理论概念以及正在使用的技术，如b d d 等。最后从多方面、多角 度比较了符号轨迹赋值和推广化符号轨迹赋值的差异，以及各自的优缺点。 第三章，伪报错问题的起源、细化、研究以及验证。 本章是本文的研究重点。首先简单介绍了推广化符号轨迹赋值中的模型检验 强可满足性算法。然后分析了伪报错问题产生的来源，通过问题的分析，提出了 对现在的强模型检验算法的改进算法。介绍了函数编程语言一e x l i f 语言，最后 使用该语言进行改进算法的实现，并通过f o r t e 平台验证改进的强模型检验算法 的有效性。 第四章，设计自动插入故障容错结构工具。 通过引入软件系统中的故障容错技术，阐述了目前形式化验证工具中所存在 的问题。然后提出了自动插入故障容错结构工具，在设计此工具的过程中，根据 e x l i f 语言的性质提出了数据信号量优先算法。最后使用f o r t e 验证平台验证该 插入工具的作用，并总结其不足。它同样为本文的研究重点。 第五章，总结和展望。 对本论文的工作进行总结，并提出下一步工作的展望。 1 6 本章小结 本章主要介绍了各种验证方法、选题依据和研究的主要内容。首先，分析了 集成电路的发展现状以及存在的问题。然后，简述了验证的基本概念和系统验证 的原则，并从各个角度、各个方面分析现存的主要验证方法以及其各自的优缺点。 最后，引出了选题依据和研究的主要内容。 1 2 第二牵符号轨迹赋骥蘩l 推广化符号辕迹赋值篱介 第二章符号轨迹赋值和推广化符号轨迹赋值简介 2 1s t e ( 符号轨迹赋值) 介绍 随着集成电路验证技术豹发震，对数字电路进行验证可以运用模拟验证，或 者形式化验证的方法。但二者之间基本上保持着分工合作的关系，被用于不同的 系统或者不同的验证阶段，这种状态到了九十年代初期发生了改变。1 9 9 1 年b r y a n t 和b e a t t y 等人探索将模拟的方法和形式化方法结合，以此充分结合两种验证方法 的优点，克服其中的不足，他们进行了最初的试验并取得了一定的成功【2 8 1 。后来 s e g e r 和b r y a n t 等人不断进行改进和完善，1 9 9 5 年薪方法最终以完整的理论形式 出现并正式定名为s t e e 2 9 1 。今天s t e 验证方法已是数字电路验证中最有效、最快 速的验证方法，它不仅能够完成传统的模拟验证方法霹以完成的验证任务，而且 尤其适合验证流水线等数字时序电路。 s t e 验证方法作为一种先进的数字电路验证技术，跌它一出现便弓 起了学术 界和工业界的广泛关注，目前有关它的研究仍在继续1 3 0 - 3 2 | 。 赣 图2 - 1s t e 验证方法组成 s t e 验证方法大体上可以分为三个部分： 第一部分称为电路模型，展示电路的所有可能行为； 第二部分称为验证规范，指明系统应该满足或者具有的性质： 第三部分是验诞器，完成指定的验证任务。图2 1 是s t e 验证方法的组成框 图。 电子科技大学硕士学位论文 2 1 1 电路模型 电路模型是电路的抽象描述，是展示电路行为的载体。在s t e 验证方法中， 电路模型是一个二元组m = 厂 ，】，7 ，其中 是完备格，表明状态空间； y 是次态函数，具有单调性。 s t e 验证方法首先将电路节点的值域从加，j 7 扩展到徊，j ，脚，其中x 表示 一种不确定的或者未知的信息。其次在值域加，j ，弼上定义了一个偏序关系，即： 如果输入的测试向量中含有未知值x 并且通过模拟得出了二进制值( o 或1 ) 的结果， 那么将输入的测试向量中的x 值替换为任意具体的二进制值时，也能得出相同的 结果。通过这样的处理，s t e 验证方法用一个含有未知值x 的测试向量就可以同 时表示多种不同的测试向量组合，因此用于验证的测试向量可以被显著的约简。 同时，由于电路在某一时刻的状态是由若干节点的取值共同决定的，因此值 域的概念也被扩展。设d = 加，j ，倒表示单个节点的取值集合，那么矿= j r 匈， a m n a ，印，j g 鲕7 表示所有长度为m 的三值向量的集合。相应地，偏序关系也被 扩展到d ，l 上，即a 6 当且仅当a j b f f ，j g 蜘) 。不过， 并不是完备格， 因为任给d 历中的两个元素它们的最小上界都不存在。因此，s t e 验证方法还引入 一个特殊的符号r 来表示这个缺失的最小上界，即c = 矿己，刀。 设s 是