（计算机应用技术专业论文）基于gste理论的反例研究.pdf

8s0 j e l 独创性声明 删帅if|f|fi|i|fjjjj|ii| y 18 0 2 5 6 4 本人声明所呈交的学位论文是本人在导师指导下进行的研究工 作及取得的研究成果。据我所知，除了文中特别加以标注和致谢的地 方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含 为获得电子科技大学或其它教育机构的学位或证书而使用过的材料。 与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明 确的说明并表示谢意。 签名：警号孝日期：加o 年夕月2 怕 论文使用授权 本学位论文作者完全了解电子科技大学有关保留、使用学位论文 的规定，有权保留并向国家有关部门或机构送交论文的复印件和磁 盘，允许论文被查阅和借阅。本人授权电子科技大学可以将学位论文 的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或 扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后应遵守此规定) 签名：彬 导师签名：j 叠固过 日期：加d 年厂月碑日 t j v k 、 ， 摘要 摘要 在过去几十年，人们对信息技术大量需求，微电子技术高速发展，使得集成 电路的规模和复杂度越来越高，这些对集成电路的设计和制造提出了更高的要求。 在亿万级的晶体管电路中，完全不出现错误是非常难的，1 9 9 4 年i n t e l 公司的芯片 中的浮点错误就是一个例子，因此设计验证已经越来越受重视。s t e 是基于四值 符号模拟的模型验证技术，在大规模硬件设计中发挥了很大的作用。尽管s t e 验 证很高效，但是s t e 的固有缺陷是它验证的属性种类有限，对于无限时间属性无 能为力，另外s t e 只能进行前向模拟，而不能进行后向模拟，所以也无法查找反 例。在最近的一些年，g s t e ( 广义符号轨迹赋值，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 y e v a l u a t i o n ) 是对s t e 扩展最成功的一个理论，g s t e 可以验证无限时间性质，同时 还可以进行后向模拟，由于g s t e 具有可以后向模拟的特点，所以可以应用g s t e 的这个特点进行本课题的研究，即研究g s t e 理论的反例生成。 因为g s t e 一般进行的是性质相关的验证，性质一旦失败，就需要为其生成 一个反例，提供给设计者来调试失败的错误，通过反例来确定失败的原因。设计 者通过对于反例的调试，可以确定这个错误是由于无效的输入引起的，还是由于 设计错误导致的。在前一种情况下，需要加入约束来消除无效性，后一种则需要 系统设计返工。由于g s t e 理论比较新颖，目前并没有学者对于g s t e 的反例查 找进行系统的研究，所以本课题进行反例查找技术的研究，对于g s t e 理论的完 善来说至关重要。 本文首先对验证的发展进行了介绍，并重点介绍了s t e 验证理论和g s t e 验 证理论，并对它们的优缺点进行了分析。然后介绍了查找反例技术的发展，并重 点介绍了其在g s t e 理论中的的作用，基于以上原因，重点设计了两个查找反例 的算法，通过这两个算法补充了g s t e 理论在反例查找方面的欠缺。当应用g s t e 进行验证时，如果出现断言错误时，可以使用第一个算法找出系统的一个反例。 紧接着对第一个算法进行扩展，当出现断言错误时，可以使用扩展算法将与此错 误相关的所有反例全部列出来。设计完算法后，本文通过编程实现了设计的算法。 设计实现了编译模块、g s t e 验证模块和反例查找模块。在算法的实现过程中，引 入了h a s h 函数和b d d ( 一- - 叉判定图，b i n a r yd e c i s i o nd i a g r a m ) ，通过h a s h 函数和 b d d 的运用，很大的提高了系统的效率，最后通过实例分析了系统的效率和可行 i 摘要 性。 关键词：反例查找，g s t e ，b d d ，s t e ，形式化验证 a b s t r a c t i nt h ep a s ts e v e r a ld e c a d e s ，w i t ht h eg r e a td e m a n d f o ri n f o r m a t i o nt e c h n o l o g y , a n d t l l ek 曲s p e e dd e v d o p m e n to fm i c r o e l e c t r o n i c s ，t h es i z ea n dc o m p l e x i t yo fi n t e g r a t e d c i r c u i t sa r ei n c r e a s i n g l yh i g h s ot h ei n t e g r a t e dc i r c u i t sd e s i g na n dm a n u f a c t u r en e e d h i g h e rq u a l i t yt h a np a s t i t i sv e r yd i f f i c u l tw i t h o u ta l l e r r o ri n t h em i l l i o n so f 包r a n s i s t o r - 1 e 、，e 1c i r c u i t s ，s u c ha st h ef l o a t e r r o ri nt h e19 9 4 ，s ov e r i f i c a t i o n 1 sv e r y i m p o r t a n t 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 ) i sa m o d e lc h e c k i n gt e c h n i q u eb a s e d o naf o u rv a l u es y m b o l i cs i m u l a t i o n i th a ss h o w ng r e a tp r o m i s ei nt h ed e s i g no fl a r g e s c a l eh a r i l w a r e a l t h o u g ht h es t ev e r i f i c a t i o ni sv e r ye f f i c i e n t ，t h ed i s a d v a n t a g eo f t h e s t ei st h el i m i t e da t t r i b m et y p e so fv e r i f i c a t i o na n dh e l p l e s sf o rt h eu n l i m i t e dt i m e a t t r i b u t e i na d d i t i o n ，t h es t eo n l yc a ns i m u l a t ef o r w a r d ，b u tn o tb a c k w a r d s oi t c a l l f i l l dm ea d v e r s ee x a m p l e i nt h er e c e n ty e a r s ，g s t e ( 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 y e v a l u a t i o n ) h a si m p m v e do ns t e ，n o to n l yc a nv e r i f yt h eu n l i m i t e dt i m ea t t r i b u t e ，b u t a l s oc a ns i m u l a t eb a c k w a r d b e c a u s eo ft h ef e a t u r eo fg s t es u p p o r t i n gb a c k w a r d s i m u l a t i o n ，w em a yr e s e a r c hc o u n t e r - e x a m p l e sg e n e r a t e do f g s t e b e c a u s eg s t ei sg e n e r a l l yc a r r i e do u tt h ev e r i f i c a t i o nr e l a t e dt ot h en a t u r e ，o n c e m en a t u r ef i a i l ，w en e e dt og e n e r a t eac o u n t e r - e x a m p l ep r o v i d e d t ot h ed e s i g n e rt od e b u g m ee n o r a i l dt h u st od e t e r m i n et h er e a s o nf o r t h ef a i l u r e t h r o u g hd e b u g g i n gt h e c o u n t e r - e x a m p l e s ，t h ed e s i g n e rc a nd e t e r m i n et h i se r r o ri sc a u s e db y a ni n v a l i di n p u t ，o r d u et od e s i g ne r r o r i nt h ef o r m e rc a s e ，i tn e e d st o a d dc o n s t r a i n t st oe l i m i n a t et h e i n v a l i d i t y ；t h el a t t e rw i l ln e e dt or e d e s i g nt h es y s t e m a st h er e l a t i v e l yn e w t h e o r yo f g s t e t h e r ei sa t ) s c h o l a rt or e s e a r c ht h eg s t ec o u n t e r - e x a m p l es y s t e m a t i c a l l y 1 1 1 e r e f o r e ，t h i st o p i ca b o u tt h es t u d yo fc o u n t e r - e x a m p l et e c h n o l o g yi s c r u c i a lf o rt h e i m p r o v e m e n to f t h eg s t et h e o r y i nt h i sp a p e r , w es t u d i e dt h ev e r i f i c a t i o n ，i n c l u d i n gd e v d o p m e n to fv e r i f i c a t i o n ， s t et h e o r y , a n dg s t et h e o r y , d e v e l o p m e n to fc o u n t e r - e x a m p l e a n da c t i v i t yo f c o u n t e r - e x a m p l e s t h e n , w ed e s i g n e dt w oa l g o r i t h m st of i n dc o u n t e r - e x a m p l e st h r o u g h t h e a n a l y s i so ft h eg s t et h e o r y t h e n , t h i sp a p e ri m p l e m e n t e dt h ea l g o r i t h mb y p r o g r a m m i n g , d e s i g n e da n di m p l e m e n t e dt h em o d u l eo fc o m p i l e ，t h em o d u l e o fg s t e i i i a b s t r a c t a u t h e n t i c a t i o na n dt h em o d u l eo ff i n d i n gc o u n t e r - e x a m p l e s i nt h ep r o c e s so f p r o g r a m m i n gi m p l e m e n t a t i o n ，w ei n t r o d u c e t h eh a s hf u n c t i o na n db d d ( b i n a r y d e c i s i o nd i a g r a m ) t h ep r o g r a m m i n gg r e a t l yi m p r o v e dt h ee f f i c i e n c yo ft h es y s t e m t h r o u g ht h eu s eo fh a s hf u n c t i o na n db d d ；f i n a l l y , w ea n a l y z e dt h ee f f i c i e n c ya n d f e a s i b i l i t yo ft h es y s t e mt h r o u g ha ne x a m p l e k e y w o r d s ：f i n dc o u n t e r - e x a m p l e ，g s t e ，b d d ，s t e ，f o r m a lv e r i f i c a t i o n i v _ i 目录 目录 第一章绪论l 1 1 课题来源和选题依据1 1 2 研究背景与意义1 1 3 主要研究内容4 1 4 章节安排5 第二章s t e 和g s t e 简介7 2 1 验证的基本原理一7 2 2 验证的方法8 2 2 1 硬件的模拟验证8 2 2 2 硬件的形式化验证8 2 2 3 两种验证方法的比较9 2 3s t e 模型验证9 2 3 1 电路模型1o 2 3 3 模型验证的轨迹断言1 1 2 3 3s t e 推演系统1 2 2 4g s t e 模型验证1 2 2 4 1s t e 算法的缺点1 2 2 4 2s t e 问题解决的发展13 2 4 3 g s t e 算法1 4 2 5 本章小结17 第三章查找反例的作用及发展1 8 3 1 查找反例技术的发展1 8 3 2g s t e 算法中抽象及符号变量带来的问题1 9 3 3 反例在g s t e 验证中的作用2 1 3 3 1 辅助设计人员查错21 3 3 2 解决伪报错的基础2 2 3 4 本章小结2 2 第四章查找反例的算法设计2 3 v 目录 4 1 理论基础2 3 4 1 1 集合与运算一2 3 4 1 2 关系、划分、偏序集和格2 4 4 1 3 有限状态自动机与语言2 5 4 1 4 时态结构2 7 4 1 5 符号模拟2 8 4 2 算法的基本思想2 9 4 3 算法设计及分析3 0 4 3 1 算法设计3 0 4 3 2 算法说明3 2 4 3 3 算法优点3 2 4 3 4 实例分析3 2 4 3 5 扩展算法3 3 4 5 本章小结3 5 第五章查找反例的实施与评估3 6 5 1 h a s h 函数和二叉判定图3 6 5 1 1h a s h 函数3 6 5 1 2 二叉判定图。3 7 5 2 编译模块前端实现4 0 5 2 1 编译流程图4 0 5 2 2 所使用到的主要数据结构4 1 5 2 3 语言的记号4 1 5 2 4 编译模块的文法4 2 5 2 5 形成的语法树4 3 5 3 编译器后端实现4 4 5 3 1 将语法树转化为b d d 4 4 5 3 2 迁移关系的转化4 7 5 2 3b d d 化简4 7 5 2 4b d d 布尔运算4 9 5 4 反例查找模块实现5 0 5 4 1g s t e 模块设计51 5 4 2g s t e 模块实现5 2 目录 5 4 - 3 反例查找模块设计5 5 5 4 4 反例查找模块实现5 6 5 5 性能测试分析5 8 5 5 1 测试用例5 8 5 5 2 测试结果分析6 0 5 6 本章小结6 1 第六章总结与展望6 2 6 1 工作总结6 2 6 1 1 主要的研究成果和创新点6 2 6 1 2 存在的不足6 4 6 2 研究展望6 4 致谢6 5 参考文献。6 6 个人简历及硕士期间取得的学术成果7 0 i 第一章绪论 1 1 课题来源和选题依据 第一章绪论 本课题来源于国家自然科学基金面上项目“基于广义符号轨迹赋值理论的模 型检i 贝u ( 6 0 7 7 3 2 0 5 ) 的支持。 选题依据主要有以下三点： 首先本课题来源于国家自然科学基金面上项目的支持，积累了大量的基础， 并投入了2 0 个月的时间来学习研发。 其次，目前形式化验证【l 】的研究热点之一是符号模型验证方法，而g s t e ( 广义 符号轨迹赋值，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 ) 2 】理论是符号模型验证的 最新成果，不仅极大减少了符号模型验证中的状态爆炸而且与s t e ( 符号轨迹赋 值，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 ) 3 - 5 】相比可以验证无限时间性质，并可以进行后 向模拟。 应用g s t e 理论验证电路，发现电路设计有问题时，需要找出问题在什么地 方，所以在g s t e 算法中高效的进行无限时间性质选路及发掘出由于采用抽象和 符号变量而被隐藏的信息，从而来找出正确的反例是必要的。 第三，团队配套的软硬件开发环境。团队引入i n t e l 的实现了s t e 模型验证功 能的仿真软件f o r t e t 6 】来完备项目开发环境。 1 2 研究背景与意义 1 研究背景 在过去几十年，人们对信息技术大量需求，微电子技术高速发展，使得集成 电路的规模和复杂度越来越高，这些对集成电路的设计和制造提出了更高的要求。 在亿万级的晶体管电路中，完全不出现错误是非常难的，1 9 9 4 年i n t e l 公司的芯片 中的浮点错误就是一个例子，因此设计验证已经越来越受重视。 验证的重要性可以从项目团队中设计工程师和验证工程师的人员组成看出， 设计工程师和验证工程师的数量在普通的项目团队中人数相当，有些团队验证工 程师比设计工程师多一倍。从这个人员组成就可以看出验证在集成电路的设计中 电子科技大学硕士学位论文 是非常重要性，因为旦一个芯片出现缺陷，将缺陷芯片回收、返工，不仅会消 耗很多的人力物力，而且还会大大的影响其市场形象，缩小市场份额，甚至会使 公司陷入无法应付的困境。因此，公司如果希望设计完美的芯片，则必须在设计 完成前对其进行验证。 目前有多种验证方法被研究，其中很重要的一个是形式化验证【7 8 】，形式化验 证在上世纪9 0 年代被提出，被认为是非常成功的，未来会有很好应用前景的验证 方法。形式化验证包括定理证明、等价性检验、模型检验、和语言包含。 目前符号模型检验方法是形式化验证【7 】的一个研究热点，因为激励与响应在传 统的模拟中，都是由二进制位组成的。在一个组合电路中，假如有，z 个输入位， 就会有2 ”个向量的输入空间，传统模拟器在每次模拟中只有一个向量被模拟。与 之相反，符号模拟的输入是变量，并以变量产生输入表达式，符号模拟器同时模 拟输入变量可以取到点的全部集合。 s t e 是基于四值符号模拟的模型验证技术们，在大规模硬件设计中发挥了很 大的作用，s t e 算法在门级和晶体管级进行验证都具有高度的自动型，并已经被 应用于i n t e l ，i b m ，m o t o r o l a 等公司。在m o t o r o l a 公司，s t e 被应用于进行内存 单元和百万级晶体管的验证【1 1 - 1 3 1 ，在i n t e l 公司被用于浮点单元的验证，并成功的 对一个具有1 2 ，0 0 0 个l 1 $ d1 1 0 0 个锁存器的复杂的执3 2 器件进行验证【1 4 1 。 尽管s t e 验证很高效，但是s t e 的固有缺陷是它验证的属性种类有限，对于 无限时间属性无能为力，另外s t e 只能进行前向模拟，而不能进行后向模拟，它 的验证方法决定它不需要查找反例。 在最近的一些年，很多学者都致力于扩展s t e 的功能，其中g s t e ( 广义符号 轨迹赋值，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 ) 2 对s t e 的扩展是最成功的一 个方法，因为它不仅可以验证无限时间性质，而且比s t e 更高效和容易使用。 g s t e 可以验证无限时间性质，g s t e 防止发生状态爆炸的关键技术是引入了 抽象技术和符号变量，所以在模拟的过程中就隐藏了一些变量的信息，从而为寻 找反例产生了很多障碍。 g s t e 对s t e 的扩展之一就是解决了s t e 的无限时间性质验证问题，从而出 现了可以后向模拟的性质，这就可以使g s t e 查找反例，验证的目的就是发现错 误，并找出错误。所以对g s t e 算法进行扩展，在g s t e 算法中进行无限时间性 质选路及发掘出由于采用抽象和符号变量而被隐藏的信息，从而来找出正确的反 例是非常必要的。 2 研究意义 2 第一章绪论 由于运行时间和存储容量的限制，一般验证系统并不能验证一个大的整体程 序设计，一般都是使用模型验证工具来对抽出的与性质相关的模块进行验证，性 质一旦失败，就需要工具为其生成一个反例，用来让设计者来调试失败的错误， 从而来确定失败的原因。通过对反例的调试，设计者可以确定错误，是由于无效 的输入引起的错误还是由于设计错误导致的，在前一种情况下，需要加入约束来 消除无效性，后一种则需要系统设计返工，所以反例查找技术对于g s t e 理论的 完善来说是至关重要的一部分。 下面介绍本课题的研究意义，大致从学术价值、产业价值和实际应用价值三 方面来阐述。 ( 1 ) 学术价值。 s t e 已经被成功的应用在大规模电路的验证中，由于它的固有缺陷，g s t e 对 其进行了扩展，使g s t e 算法具有可以反向模拟的能力，由于当验证出现了错误 时，设计者希望找到错误发生在什么地方，所以反例查找对于验证很重要，又由 于g s t e 是最近几年才发明的，并没有学者对g s t e 的反例查找的算法进行研究， 本文对于反例查找算法的研究具有独创性，是对g s t e 理论的补充，所以具有极 高的学术价值。 ( 2 ) 产业价值。 自动化验证理论现在正是发展的活跃期，已经有很多分支，但是都还不健全， 但是实际的工业生产中却非常需要各种验证工具，其中s t e 理论已经应用于很多 实际的工业生产，g s t e 理论对s t e 进行了扩展，如果g s t e 理论能够健全，将 是电路设计工业史上的一个里程碑事件。 因为在芯片设计阶段迫切需要一个高效的自动化验证软件的出现，在电路设 计初级阶段就可以对其进行验证，从而大幅度降低芯片设计的成本。长期以来， 在美国等发达国家大的芯片制造公司，比如i n t e l ，i b m ，摩托罗拉等公司，都在 积极推进验证技术的发展。所以一旦使g s t e 验证理论完善，它的经济效益是无 法估量的，将会使芯片设计制造的周期大大缩短。 ( 3 ) 实际应用价值。 本课题的研究可以对i n t e l 公司的形式化验证软件f o r t e 进行补充，f o r t e 是i n t e l 公司支持的一个形式化验证的开源项目，它实现了s t e 理论，可以用来验证电路， 本课题开发的基于g s t e 理论的反例查找算法，可以被f o r t e 使用，对其功能进行 扩展。 3 电子科技大学硕士学位论文 1 3 主要研究内容 验证技术的最终目的是去验证一个产品是否满足一些特定的属性，近年来模 型验证技术发展很快，已经可以进行自动化验证，并且已经从硬件验证发展到了 软件的验证。在模型验证中的一个关键技术是符号模型验证，符号模拟的每一个 输入都是变量，并以变量产生输入表达式。利用函数表示点的集合，从而使输入 空间减小。 模型验证中，应用于正确的电路时，它可以告诉设计人员，这个电路是正确 的，但当他应用于错误的电路时，设计人员想知道的不仅仅是对还是错，更想知 道，如果发生错误，这个错误发生在什么地方。基于以上原因，这就需要我们研 究怎么生成反例。 g s t e 和s t e 一样，为了减少空间爆炸问题，采用了自动抽象技术，但是高 度抽象就会带来伪报错【”1 1 口- j 题。产生伪报错的主要原因有三点： l 对输入节点的限制； 2 四值函数的并集操作； 3 符号变量的存在。 对于第2 个和第3 个问题的处理有两种方法，第一种是模型细化，即引进布 尔量来更严格的限制表达式的空间。第二种是进行性质细化，即通过保存断言图 的传输关系。但这些细化都是基于手动的操作。这种方法的缺点是要求验证人对 要验证的电路有非常清晰的认识。对于第1 个问题的处理是引进符号常量或者变 量，来限制输入节点。所以现在g s t e 理论的一个瓶颈是如何高效的找到反例， 从而利用反例查找算法，开发高效的自动化抽象重定义工具。 为了寻找正确路径的反例，这时候就需要保存所有路径中的有用信息，从而 避免造成空间浪费，这时候我们需要研究反例查找中如何减少内存的消耗。 由于运行了抽象，这就给查找反例带来了困难，如何对抽象进行还原，从而 得到正确的反例，是急需解决的一个问题。 综上所述，本文的主要研究内容包括以下4 个部分： 1 理论基础 本文首先研究了验证的基本原理，模型验证和形式化验证的优缺点，并重点 介绍了形式化验证理论中的s t e 理论以及对于s t e 理论进行扩展后的g s t e 理论 的发展以及优缺点。 2 反例的作用及发展 4 第一章绪论 本文将介绍反例查找技术的发展，及g s t e 理论中由于抽象和符号变量等引 入的一些新的问题，从而提出反例查找的必要性，并介绍反例查找技术在g s t e 验证中的作用。 3 算法设计 介绍设计查找反例算法所需要的数学、自动机和符号模拟等理论基础，研究 怎么生成反例，以及生成怎样的反例比较合适。结合理论研究提出反例生成算法， 并通过实例对其进行分析论证。 4 反例生成系统的实现 首先介绍了节省内存的理论基础h a s h 函数及b d d 。在此基础之上设计实现了 编译前端模块、编译后端模块、g s t e 算法以及反例查找算法，并通过实际的例子 对系统进行性能分析。 1 4 章节安排 本文共分六章，第一章主要介绍课题来源、研究背景和主要的研究内容，第 二章介绍s t e 理论及g s t e 理论，第三章到第五章是本文的重点，主要介绍课题 的研究成果和进展。本文的具体章节安排如下： 第一章，介绍课题来源、选题依据、研究背景、研究意义，并指出了本论文 的主要研究内容和章节安排。 第二章，简明扼要的介绍了验证理论的发展和形式化验证与模型验证的相关 理论，并对它们进行比较，介绍了各自的优缺点。接下来详细介绍了s t e 理论及 g s t e 理论的原理。重点分析研究了s t e 理论及g s t e 理论的优缺点。为后续工 作的研究和开展提供了扎实的理论基础。 第三章，首先介绍了反例技术的发展，以及由于g s t e 验证中采用了抽象和 符号变量技术，为反例查找带来的障碍。然后详细介绍了反例在验证技术中辅助 设计人员查错和解决伪报错的作用。 第四章，首先介绍了反例查找算法所涉及到的数学、自动机和符号模拟的理 论基础，重点设计了两个反例查找算法，其中一个可以查找到第一个发现的反例， 另外一个可以将所有的反例全部罗列出来，并通过离散型的例子，对本算法进行 了分析和证明。 第五章，首先介绍了可以减少内存消耗的h a s h 函数和b d d 结构，并根据查 找反例的算法设计编译前端模块、编译后端模块，验证器模块及反例查找模块等 5 电子科技大学硕士学位论文 核心模块来实现此反例查找系统，并通过实例来分析与评估系统的优劣。 第六章，对全文进行了系统总结，首先总结了本文的特色和创新点，并指出 了目前存在的不足之处，最后给出了下一步的展望。 6 第二章s t e 和g s t e 简介 第二章s t e 和g s t e 简介 在本章，将首先引入验证的概念，并对形式化验证和模拟验证进行分析比较， 在此基础上引入符号轨迹赋值和广义符号轨迹赋值算法，并重点分析介绍他们各 自的优缺点。 2 1 验证的基本原理 设计过程是将想法转化据具体实现的过程，但是在这种转化过程中，不可避 免会发生某种错误，在硬件电路的设计过程中，主要有两种设计错误。 第一种是实现过程中引入的一些错误，比如人为的对设计功能解释错误，它 是实现错误，而不是规范错误。此类错误的预防方法是利用软件综合一个规范的 实现方案。综合的方法有很多局限性，第一，大多数的规范不是用精确的数学语 言( c + + 或者v e r i l o g 等) 来描述，而是用会话语言( 比如中文) 来描述的，所以综合 出来的结果是不严格的。第二，软件程序的固有缺陷，就算规范是用数学语言来 描述，但是很多设计方案软件不可能综合出来。 除了利用软件综合，另外一种解决此类错误的方法是，使用不同的方法，多 次实现的同样的规范，将得出的结论进行比较，此方法被称为冗余性的验证方法。 验证的可信度从理论上来说和实现的方法和次数是成正比的。但是很少有人会这 么做，因为在成本和时间上的消耗太大。 设计的过程其实就是把规范转换为实现的过程。所以验证的基本过程中，第 一步就是实现设计过程，这个过程，其实是验证工程师对规范模拟的实现，和设 计工程师实现的方案是不同的。第二步就是比较验证的结果和设计的结果，如果 有不相同的地方，则证明有错误。 验证工程师和设计工程师的实现过程差别越大，可信度就越高，l 种解决方 法就是使用c 、c + + 等验证语言来实现设计方案，而不是用设计工程师所使用的 v e r i l o g 、v h s i c 等电路描述语言。 验证的第二部中我们需要一个中间形式来表达两种不同的描述，从而可以用 来对比结果，达到验证的目的。 第二种错误是设计规范固有的错误，这些错误可能是由于功能性描述的不确 7 电子科技大学硕士学位论文 定性，也可能是需求和设计的不一致性造成的。验证此类错误，只能使用多种方 法，多次实现同样的规范，并对多次实现的结果进行比较来实现。这样做的原因 是因为无法找到一个模型，用来和规范进行参考比对。 2 2 验证的方法 验证的方法根据是否使用测试向量可以区分为模型验证和形式化验证。模型 验证依靠测试向量，而形式化验证则不需要。 2 2 1 硬件的模拟验证 最常用的验证方法是模拟验证方法，它是基于冗余性原理的验证方法。它需 要一个测试标准，在测试标准的要求下输入激励，并从输出中得到结果，并用它 的结果与设计结果作比较。 在对设计进行模拟验证前，需要先检查静态错误，静态错误是不需要输入激 励就能发现的错误，比如端口的定义和设计不匹配等。 然后针对特定功能和特征进行测试，测试完成后，开始建立模拟器，模拟器 是使用其他语言做的事件驱动的软件，当然也可以是硬件模拟器。当发现错误后， 验证工程师需要和设计者沟通，跟踪记录错误记录。 但是模拟的验证方法需要依靠大量、合理的测试用例来帮助设计者发现b u g s 。 模拟验证耗费非常多的时间去寻找b u g s ，虽然消耗了很多时间，但是验证完成后， 并不能保证设计没有缺陷【l6 1 。 2 2 2 硬件的形式化验证 除了模拟验证外，另外一种验证的方法是形式化验证，形式化验证不需要设 计测试向量，形式化验证在某种意义上是一种数学定理证明【1 7 - 1 8 】。就像一个定理， 从一个固定域中抽取一个特定的值的集合，对于这个硬件设计的验证，如果这个 形式值是正确的，那么对于这个域中的所有的值都是正确的。因此不用对这个域 中的所有或者部分值进行测试，就可以推断出电路的正确性。 形式化验证方法，目前已经不仅仅停留在理论阶段，已经大量的应用与实际 的工业生产中。在h t t p ：e e t i m e s e o m 中，我们可以看到世界领先的芯片制造商i n t e l ， 使用形式化验证方法发现1 0 0 多个高质量的逻辑b u g s ，这些b u g s 用其他方法都无 8 第二章s t e 和g s t e 简介 法发现。在另一项研究中，w o l f s t h a le ta 1 【19 】通过对i b m 在1 2 个月中使用形式化 验证的研究，证实了形式化验证的优点。i b m 通过使用形式化验证方法发现了数 百个b u g s ，并发现了很多临界b u g s ，这些b u g s 使用其他精心设计的模拟测试工 具都很难发现。形式化验证能够取得如此大的成功是因为他采用了符号模型验证【2 0 】 和抽象【2 l 忽j 。 硬件的形式化验证问题可以理解为建立一个可以被数学定理证明的满足一定 性质的执行。执行是指硬件设计被验证，可以被描述为任何级别的电路设计的抽 象，例如他可以是一个用高级v h d l 语言描述的程序，也可能是在b l i f 中描述的 一个门级网表。性质是指尚待证明的特性，可以使用各种方式来描述，比如可以 使用特性描述也可以使用抽象的结构来描述。 2 2 3 两种验证方法的比较 形式化验证和模型验证的主要区别是，模型验证需要输入向量，而形式化验 证不需要。模型验证的主要原理就是首先设计输入向量，通过模拟产生输出。形 式化验证的思路和模型验证正好相反，用户首先说出想要达到的输出，然后验证 工程师通过验证工具检验是否可以达到这个输出。验证期间，不需要考虑激励是 什么。简而言之就是形式化验证是输出驱动，而模型验证需要输入驱动。对我们 来说输入驱动更容易理解，所以形式化验证的设计难度更大一些。 形式化验证的特点是具有完备性，形式化验证可以对输入空间的所有点进行 验证，但是模拟验证不行，它只是对测试向量进行仿真，模拟验证可以看做是取 了一些样本来进行验证，如果它想达到完备性，就必须对测试空间的所有向量进 行取样，对于大规模电路来说，这是不可能实现的。但是形式化验证，会验证整 个空间的所有输入和状态。模拟验证一次只能验证一个输出点，但形式化验证可 以验证一组输出点。 形式化验证的缺陷是占用内存空间很大，对于一个规模稍微大一些的系统， 需要运行很长的时间才能得到验证结果，所以它只能适用于一些中等规模的电路 设计。 2 3s t e 模型验证 s t e 是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 【2 3 1 的简称，s t e 是一种基于格论的模型 检测技术。1 9 9 1 年b r y a n t 和b e a t t y 等人结合了模拟的方法和形式化方法的优点， 9 电子科技大学硕士学位论文 摒弃了其中的不足。进行了一些初步的实验，取得了成功。后来s e g a r 和b r y a n t 等人对其进行了改进和完善，并在1 9 9 5 年形成了完整的理论形式s t e 。 s t e 是一个高效的模型验证算法，尤其适合验证大规模电路的属性。s t e 最 基本的形式是验证最简单的线性时序逻辑。另外s t e 是基于时序模拟的，它把布 尔数据域 0 ，1 ) 扩展出了另外一个值“x ”，“x 表示既可能是0 也可能是1 ，由 于这个扩展，使s t e 具有非常强大的自动状态空间抽象能力。 由于以上特征，使s t e 与其他传统的模型验证算法相比具有更高效的验证能 力【2 4 粕】。s t e 的限制很弱，所以它被扩展到符号时序逻辑模拟算法。符号时序模 拟【8 1 使用符号变量或者表达式( 例如：b d d 2 7 1 ) 来表示电路结点的整个数据集。每个 时序电路结点的值用一个b d d 数据结构来表示，所以s t e 可以使用符号模拟，一 次来完成对所有集合的模拟。 b d d 表达式可以在不同的电路结点使用相同的变量，所以他可以表达复杂结 点之间的关系。符号变量很大的加强了s t e 对于时序电路的验证能力。例如对于 输入输出关系，就可以使用基于b d d 的符号模拟来进行，它可以在输出点使用函 数的形式来表示输入结点的任意值。 下面我们将介绍s t e 模型验证理论的详细细节。 2 ，3 。1 电路模型 s t e 的三元数据模型来源于集合d = 0 ，1 ，x ) ，并引入了偏序关系_ ，其中 x 一 0 并且x c ，则可以得到 i = n a = n c