（计算机系统结构专业论文）运算电路的形式化验证方法研究.pdf

摘要 运算电路模块是当代微处理器的关键组件。微处理器电路设计的验证工 乍必须确保 运算电路模块设计的正确性。当电路复杂度达到一定规模后，传统的仿真验证方法已无 法覆盖整个状态空间，从而无法保证缘微处理器运算电路这类复杂设计的正确性。因此， 基于形式化方法的运算电路验证方法，特别是完全自动化的模型检验方法，已经成为当 前国内外科研机构以及e d a 厂商所关注的热点问题。 本文结合龙芯i 号微处理器运算部件的设计和验证工作，系统地研究了运算电路的规 范语言、基于决策图的模型检验方法以及基于可满足性判定的模型检验方法。以下是本 文的主要贡献与创新点： ( 1 ) 定义了运算电路c t l 公式的语法和语义，给出了运算电路c t l 公式的模型检 验方法以及基于* p h d d 的实现方法。 ( 2 ) 提出了基于* p h d d 实现运算操作算法的一般优化原则。特别地，针对运算电 路验证中经常出现的基为2 的整数次幂的整除和取模运算，推出了四条定理t 并且基于 这四条定理对运算过程进行了简化。这些措施有效提高了* p h d d 运算操作算法的效率。 ( 3 ) 提出了更接近于实际取值范围的p r d d 上下界计算算法。在整除、取模以及 比较运算中，上下界可用于简化运算操作。当函数上下界越接近* p h d d 实际取值范围时， 满足简化条件的可能性越大，简化算法越有效。 ( 4 ) 提出了基于条件预处理的条件约束算法，降低了条件约束算法的运行时间；同 时又提出了多级约束机制和约束过滤机制，降低了约束条件的规模，并消除了大量非必 要的约束函数调用。 ( 5 ) 提出了基于可满足性判定算法的运算电路验证方法，突破了现有可满足性判定 算法在应用上的局限性。实验结果表明，该验证方法对于存在设计错误的运算电路或者 约束严格的正确运算电路非常有效，是决策图方法的一个有效补充。 ( 6 ) 基于上述研究结果，实现了一个字级模型检验系统a r i t h s m v ，并使用该系统 验证了龙芯1 号微处理器的浮点加法部件。实验证明该系统具有实用高效的特点。 关键词：形式化方法模型检验运算电路决策图* p h d d 条件模型检验可满足性判定 + 率文研究得到国家自然科学基金重大项目( 6 9 8 9 6 2 5 0 - 1 ) 以及中国科学院计算技术研究所青年基金项日( 2 0 0 2 6 1 8 0 - - 6j 的资助。 r e s e a r c ho nf o r m a lm e t h o d si na r i t h m e t i cc i r c u i t v e r i f i c a t i o + w a n gh a i x i a ( c o m p u t e ra r c h i t e c t u r e ) d i r e c t e db yp r o f e s s o rh a n c h e n g d e a n dh uw e i w u a r i t h m e t i cc i r c u i ti s o n eo ft h e k e yc o m p o n e n t s o fm o d e mm i c r o p r o c e s s o n t h e v e r i f i c a t i o no f r r l i c r o p m c e s s o rd e s i g nm u s te n s u r et h ec o r r e c t n e s so fa r i t h m e t i cc i r c u i ta st h e i n c r e a s eo fc i r c u i tc o m p l e x i t y , t r a d i t i o n a ls i m u l a t i o nm e t h o dh a sb e e nu n a b l et oc o v e rt h e t o t a l s t a t es p a c ea n dt h ec o r r e c t n e s so f r n i c m p m c e s s o ra r i t h m e t i cc i r c u i tc a n n o tb ee n s u r e d t h u s ， u s i n g f o r m a l v e r i f i c a t i o n ，e s p e c i a l l y m o d e lc h e c k i n g m e t h o d ( a nc o m p l e t e l ya u t o m a t e d m e t h o d ) ，t ov e r i f ya r i t h m e t i cc i r c u i t se f f e c t i v e l yb e c o m e sa h o ts p o tc o n c e r n e db yw o r l dw i d e r & di n s t i t u t e sa n de d av e n d o r s b a s e do nt h ew o r ki n d e s i g na n dv e r f i c a t i o no ff l o a t i n g - p o i n t a r i t h m e t i cc i r c u i ti n g o d s o n im i c r o p r o c e s s o r , t h i sd i s s e r t a t i o ng i v e sas y s t e m a t i cr e s e a r c ho nt h es p e c i f i c a t i o n l a n g u a g e , d e c i s i o nd i a g r a mb a s e dm o d e lc h e c k i n gm e t h o da n dv e r i f i c a t i o nm e t h o d o l o g i e sa s w e l la ss a tb a s e dm o d e l c h e c k i n g m e t h o di nt h ev e r i f i c a t i o no f a r i t h m e t i cc i r c u i t t h ed e t a i l e d r e s e a r c hi m p r o v e m e n t sa r ea sf o l l o w s 1 ，t h es y n t a xa n ds e m a n t i c so fc t lf o r m u l ai na r i t h m e t i cc i r c u i ti sd e f i n e d b a s e do i lt h e s e m a n t i c so fc t lf o r m u l ai na r i t h m e t i cc i r c u i t ，m o d e lc h e c k i n gm e t h o df o rc t lf o r m u l ai s p r e s e n t e da n d t h em o d e l c h e c k i n g m e t h o di si m p l e m e n t e d u s i n g p h d d 2 ，t h eg e n e r a lo p t i m i z a t i o np r i n c i p l eo fa r i t h m e t i co p e r a t i o na l g o r i t h m so n p h d di s p r e s e n t e d m o r e o v e lf o rd i v i s i o na n dm o d u l u so p e r a t i o nw i m r a d i xo f p o w e r - o f - 2i n t e g e r , w h i c hi sc o m m o ni na r i t h m e t i cc i r c u i tv e r i f i c a t i o n f o u rt h e o r i e sa r ei n t r o d u c e dt os i m p l i f yt h e a l g o r i t h mr u n n f l l gp r o c e s s t h e s eo p t i m i z a t i o nt e c h n i q u e si m p r o v et h ee f f i c i e n c yo f a r i t h m e t i c o p e r a t i o na l g o r i t h m so n + p h d dg r e a t l y 3 a n u p p e r b o u n da n dl o w e rb o u n dc a l c u l a t i o na l g o r i t h mo i l + p h d di si n t r o d u c e d ，w h i c h m a k e st h eu p p e rb o u n da n dl o w e rb o u n do ff u n c t i o nc l o s e rt ot h em a x i m u mv a l u ea n d m i n i m u mv a l u eo ff u n c t i o n i nt h i sc a s e i ti sm o r e p o s s i b l et os a r i s f yr e d u c t i o nc o n d i t i o n sf o r u p p e r b o u n da n dl o w e rb o u n do ff u n c t i o n t h u s ，t h e r ea r cm o r eo p e r a t i o n sr e d u c e d 4 an e wc o n d i t i o n a lr e s t r i c t i o na l g o r i t h mw i t l lc o n d i t i o np r e p r o c e s s i n gi sb r o u g h tf o r w a r d t or e d u c et h er u nt i m eo fc o n d i t i o n a lr e s t r i c t i o na l g o r i t h m b e s i d e s ，m u l t i l e v e lc o n d i t i o n a l r e s t r i c t i o nm e c h a n i s ma n dc o n d i t i o n a lf i l t e r i n gm e c h a n i s ma r cg i v e nt od e c r e a s et h es i z eo f c o n d i t i o na n de l i m i n a t eu s e l e s sr e s t f i c t i o nf u n c t i o nc a l l s 5 s a ta l g o r i t h mi se x t e n d e dt ov e r i f ya r i t h m e t i cc k c u i t e x p e r i m e n l si l l u s t r a t et h a ts a t b a s e dv e r i f i c a t i o nm e t h o di sh i 曲e f f i c i e n ti nv e r i f y i n gw r o n ga r i t h m e t i cc i r c u i t s o rs t r i c t l y t h i sr e s e a r c hw o r kw a ss u p p o r t e db ym a j o rp r o j e c to f n a t i o n a ls c i e n c ef o u n d a t i o no f c h i n a ( g r a n tn o6 9 8 9 6 2 5 0 。1 ) a n d y o u t h f o u n d a t i o no f i n s t i t u t e o f c o m p u t i n g t e c h n o l o g y , c a s ( g r a n t n o 2 0 0 2 6 1 8 0 - 6 ) 1 1 1 运算电路的形式化验证方法研究：a b s t r a c t c o n s 打m n e d r i g h tc i r c u i t s s a tb a s e dm e t h o di sag o o dc o m p l e m e n to f d e c i s i o nd i a g r a mm e t h o d 6 b a s e do nr e s e a r c hw o r ka b o v e ，aw o r d l e v e lm o d e lc h e c k i n gs y s t e ma r i t h s m vi s d e s i g n e da n di m p l e m e n t e d u s i n gt h i ss y s t e m ，t h ef l o a t i n g p o i n ta d d i t i o nu n i to fg o d s o n i m i c r o p r o c e s s o ri sv e r i f i e d ，w h i c hp r o v e st h ep r a c t i c a b i l i t ya n dh i 曲e f f i c i e n c yo ft h em o d e l c h e c k i n g s y s t e ma r i t h s m v k e y w o r d s ：f o m a a lm e t h o d ，m o d e lc h e c k i n g , a r i t h m e t i cc i r c u i t ，d e c i s i o nd i a g r a m ， + p h d d ，c o n d i t i o n a lm o d e lc h e c k i n g ，s a t 声明 本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得 的研究成果。就我所知，除了文中特另t i d h 以标注和致谢的地方外，论文中 不包含其他人已经发表或撰写过的研究成果。与我一同工作的同志对本研 究所做的任何贡献均已在论文中作了明确的说明并表示了谢意。 作者签名： 洒祀日期：训f 关于论文使用授权的说明 中国科学院计算技术研究所有权处理、保留送交论文的复印件，允许 论文被查阅和借阅；并可以公布论文的全部或部分内容，可以采用影印、 缩印或其它复制手段保存该论文。 作者签名：j 扬霞导师签名搀船磐甜纛 第一章绪论 随着集成电路设计复杂度的增加，功能验证已经成为集成电路设计人员所面临的主 要挑战。当集成电路规模增加时，采用传统仿真验证方法进行功能验证的复杂度呈指数 级增长。这使得集成电路设计能力和验证能力之间的差距越来越大，功能验证成为阻碍 集成电路设计发展的主要原因之一。为了缩短这个差距，形式化验证方法成为目前国内 外科研机构以及e d a 厂商关注的重要研究领域。 本章首先分析了目前设计验证工作面临的挑战，指出了传统仿真验证方法的局限 性，进而说明了形式化验证的必要性。然后，本章对形式化验证方法的两个分支：理论 证明和模型检验迸行了综合论述。接着，本章阐述了对运算电路的形式化方法进行研究 的必要性。最后，总结了本文的创新点，并给出了后续章节介绍。 1 1 引入形式化验证方法的必要性 作者认为，以下三个因素基同决定了在硬件系统设计中必然要引入形式化验证方 法。第一。硬件系统f ；：i 益复杂使得功自2 验证成为硬件系统开发过程中的瓶颈；第二，系 统设计存在缺陷所造成的损失越来越大；第三，传统仿真验证方法已无法对系统进行完 全验证。下面对这三个因素分别进行详细解释。 1 1 1 日益复杂的硬件系统设计 i n t e l 公司创始人之一g o r d o nm o o r e 于1 9 6 5 年指出：集成电路中每平方英寸的晶体 管数目每年增加一倍。后来，集成电路发展速度放慢，集成度每1 8 个月提高一倍，即 当前摩尔定律的定义。按照摩尔定律，2 0 1 0 年微处理器包含的晶体管数将达到1 8 亿个。 工艺水平的提高使单个芯片中可集成的功能部件逐渐增多，随着芯片设计越来越复杂， 验证工作在整个芯片设计中所占的比重也越来越大。如图1 1 所示，2 0 0 3 年，在1 0 0 万 逻辑门的s o c 设计中，仿真验证工作在整个设计工作量中的比重达到5 0 8 0 d s 0 3 1 ， 即项目中有超过一半的设计资源包括计算机和人力资源都在致力于设计验证工作。 因此，随着集成电路复杂度的增加，功能验证已经成为集成电路开发过程中的瓶颈， 对验证方法进行深入研究将有助于缩短集成电路的开发周娟，降低开发成本，帮助制造 商实现收入最大化。 中国科学院博士学位论文一垂算电路的形式化验证方法研究 图1 1 验证在a s i c 设计中所占的比重( d s 0 3 ) 1 1 2 设计缺陷带来的惨重代价 系统设计中存在缺陷造成的代价主要体现在三个方面： 一是重做掩模的巨额经济损失。目前，典型的晶圆代工厂在采用o 1 8 微米工艺时， 掩模费用为5 0 万美元，如果投片后才发现设计缺陷，那么需要改动版图并重做掩模， 以至于造成巨额经济损失。根据c o l l e t ti n t e r n a t i o n a lr e s e a r c h ( c i r ) 公司2 0 0 2 年调查 显示，在所有需要重置掩模的情况中，7 1 来自于设计出错，这说明验证工作未能及时 发现系统设计中存在的缺陷是造成巨额经济损失的主要原因。 二是影响工程进度。要修订缺陷可能会延迟产品面市时间，而集成电路产品上市过 程中的任何延迟都将延长制造商回收成本、获得利润的时间。 三是可能导致人员伤亡事故。在核电控制、航天航空以及医疗诊断等系统设计中， 设计缺陷会导致重大人员伤亡事故。 总之，设计缺陷可能造成惨重代价。可以认为，验证工作的目标已经不是找出多少 设计缺陷，而是判定系统是否完全不存在设计缺陷。 1 1 3 仿真验证方法的局限性 仿真( s i m u l a t i o n ) 验证方法是指：给定测试向量，检查被验证系统的实际输出是 否符合期望输出，从而寻找系统设计中存在的缺陷。仿真验证方法是工业界最常用的测 试方法，在验证初期可发现大量设计缺陷，但是对于较复杂的系统，测试向量无法穷举 状态空间的所有状态，因此无法确认系统设计是否完全正确。评价仿真验证工作的一个 重要指标是测试覆盖率，为了提高测试覆盖率，几大e d a 厂商都提供了代码覆盖率分 析工具。通过覆盖率分析可查找设计中测试向量没有覆盖的部分，并生成附加的测试向 量，从而提高测试覆盖率。但是即使覆盖率达到预定的要求，测试向量未能覆盖的部分 仍然可能存在设计缺陷。 2 第一章绪论 i n t e lp c n t i u mp r o 处理器在量产之前已经进行了超过1 万亿个测试向量的测试，但 是后来仍然发现了几个设计缺陷 g w e + 9 5 ，其中有些严重的缺陷会造成数据损坏和系统 死机。 作者参与了中国科学院计算技术研究所的龙芯i 号微处理器的整个研制过程，负责 浮点a l u 部件的结构设计、r t l 实现、功能验证、f p g a 验证以及a s i c 流程中整个芯 片的仿真验证工作。浮点a l u 部件包含了浮点加法模块、定点浮点转换模块、浮点数 比较模块以及浮点数的求绝对值、求反等基本运算操作模块。这些模块不仅内部结构比 较复杂，而且有的是三级流水，有的是一级流水，因此输出结果需要进行仲裁，设计也 比较复杂。作者在对浮点a l u 部件设计进行自测试时，采用了手工书写测试向量、具 有较高覆盖率的测试向量生成工具生成测试向量以及随机生成测试向量等多种方法相 结合的方式进行测试，其中对每种运算操作的随机生成测试向量达到1 0 万个。但是在 龙芯i 号微处理器芯片级联调以及f p g a 验证过程中，仍然发现了浮点a l u 部件的几 个设计缺陷。 与仿真验证方法不同，形式化方法是指通过数学方法证明被验证系统满足系统规范 的验证方法。它隐含考虑了所有输入向量和输入向量序列，能够完全证明系统规范的正 确性，因此形式化验证方法已受到越来越多地关注。 1 2 形式化方法综述 按照k c m 和g r e e n s t r c c t 在硬件设计形式化方法调查报告 k g 9 9 1 中的定义，形式化 方法是通过数学方法证明被验证系统满足系统规范。 m c m i l l i a n 在 m c m + 9 3 q b 指出了建立形式化验证系统的三个基本要素：被验证系统 的数学模型、系统规范的形式化描述方法和证明被验证系统满足系统规范的验证方法。 三个要素构成了形式化方法的框架。 形式化方法可根据以下标准进行分类： 按照证明方法不同，可分为基于证明的验证方法和基于模型的验证方法两大类。 在基于证明的系统中，被验证系统表示为组公式1 1 ，系统规范表示为另一组 公式西，验证方法是寻找可证明r 卜垂成立的证据；在基于模型的方法中，被 验证系统表示为一个有限状态模型m ，系统规范表示为公式由，验证方式是检 验模型m 是否满足公式垂( mf 圣) 。 按照自动化程度不同，可分为完全自动、半自动以及完全手工的验证方法三大 类。 按照系统规范定义不同，可分为完全系统验证和属性验证两类。完全系统验证 是对系统行为的完全验证，而属性验证只验证系统的某个属性。 按照被验证系统的功能不同，在微处理器验证领域，可分为运算电路验证、存 储子系统验证、接口协议验证以及其它功能模块的验证等类别。 1 中国科学院博士学位论文_ j 重算电路的形式化验证方法研究 目前，主要的两类形式化验证方法是定理证明( t h e o r yp r o v i n g ) 方法和模型检验 ( m o d e lc h e c k i n g ) 方法。定理证明是半自动的基于证明的验证方法，模型检验是完全 自动的基于模型的检验方法。 1 2 1 定理证明方法 定理证明方法的基础是一个形式化的逻辑系统，该逻辑系统由一系列公理和推理规 则组成。定理证明的过程是从系统的公理出发，使用推理规则逐步推导出规范成立的证 明过程。图1 2 给出了定理证明的基本过程以及定理生成和定理检查两种应用模式。如 图1 2 所示，定理证明的第一步是用形式化语言( 如命题逻辑，一阶逻辑或高阶逻辑) 描述被验证系统和系统规范，然后将被验证系统和系统规范间的隐含或等价关系构造为 一个数学定理，最后，若是定理生成，则由定理生成工具自动或在用户指导下生成定理 证明过程。若是定理检查，则由定理检查工具自动或在用户指导下检查给定证明的正确 性。一般情况下，定理证明特指定理生成，即形式化验证系统要给出定理证明过程。 证明对错 图1 2 定理证明的两种应用模式 定理证明过程依赖于系统的公理和推理规则，在某种程度上也依赖于其派生定义和 中间引理。尽管通过内置启发式推导方法、规则重写和化简等方法可以提高定理证明的 自动化程度，但是大多数定理证明都是交互过程，由专家给定证明过程中每一步采用的 推理规则，然后定理证明系统根据推理规则进行推导，直到证明定理成立为止。 在使用定理证明方法验证v l s i 设计时，可以将被验证系统映射为多模块层次化结 构，并为每个模块定义行为规范。定理证明过程首先证明每个子模块满足各自的行为规 范，然后基于每个子模块的规范，证明由子模块组合成的模块满足该模块的行为规范， 该过程一直重复下去，直到子模块组合成的模块对应整个被验证系统为止。这种将被验 证系统分解的验证方法称为层次化( h i e r a r c h i c a l ) 验证方法，可用于验证v l s i 电路， 主要缺点是验证方法与被验证系统相关。 目前，定理证明方法已经广泛应用于工业级的软硬件设计验证中，比较有名的定理 4 第一章绪论 证明系统有h o l ( h i g h e r - o r d e r l o g i c ) g o t + 8 8 ，b o y e r - m o o r e b m 9 0 ，p v s ( p r o t o t y p e v e r i f i c a t i o ns y s t e m ) o r s + 9 4 ，和a c l 2 ( a c o m p u t a t i o n a ll o g i cf o ra p p l i c a t i v ec o m m o n l i s p ) 【k m 9 6 。 h o l 是由英国剑桥大学研制的交互式高阶逻辑定理证明系统。在h o l 系统中，所 有推理规则都是由8 个初始推理规则派生出来，证明过程每一步都由用户选择推理规则， 然后由h o l 系统检查可行性并进行推理。作为比较有代表性的应用，j o y c e j o y + 8 8 和 m e l h a m m e l 8 8 于1 9 8 8 年首先给出了采用h o l 系统实现硬件设计验证的实例，f o x f o x 0 2 采用h o l 验证了a r m 6 微处理器的设计。 p v s 是高阶逻辑证明系统。初始推理规则包括命题和量词推理规则、归纳规则、重 写规则和线性运算函数决策程序等内容，用户可通过组合初始推理规则来构造高级推理 规则，从而证明复杂定理。另外，p v s 还集成了基于b d d 的模型检验，将模型检验和 理论证明有效结合起来。s r i v a s 等人 s m 9 5 1 使用p v s 验证了一些硬件设计，包括商用处 理器验证。c a r r e h o 和m i n e r c m 9 5 给出了基于h o l 和p v s 系统的大部分i e e e 浮点标 准的形式化描述。r u 印等人 r s s 9 6 1 验证了i n t e l 出现除法设计缺陷的s r t 算法和实现。 b o y e r - m o o r e 是一个一阶逻辑定理证明系统。其工作过程为：首先，由用户建立一 组引理作为推理规则，然后根据内置的启发式策略选择推理规则，并基于推理规则进行 推导。b o y e r - m o o r e 定理证明器代表性的成功应用包括：h u n t h u n t 9 4 对1 6 位微处理器 f m 8 5 0 1 进行了验证，v e r k e s t 等 v c d 9 4 证明了不恢复除法( n o n r e s t o r i n g d i v i s i o n ) 算 法，l e e s e r 等 l 0 9 5 验证了基2 开根算法。 a c l 2 是b o y e r - m o o r e 系统n q t h m 的扩展，支持类l i s p 的一阶逻辑。c l i 公司基 于a c l 2 验证了a m dk 5 的浮点除法算法 b k m 9 6 ，验证过程总共使用了1 6 0 0 个定义 和引理。r u s s i n o f f r u s + 9 8 基于a c l 2 成功验证了a m dk 7 处理器的浮点乘法、除法 和开根运算。 c l a r k e 等人 c g z 9 6 基于a n a l y t i c a c z 9 3 】定理证明器验证了s r t 算法和实现的正 确性；k a p u t 等人 k s 9 6 通过定理证明器r r l ( r e w f i t e r u l e l a b o r a t o r y ) 证明了基于华莱 士树( w a l l a c et r e e ) 的整数乘法电路的正确性。 定理证明方法已经成功验证了大量的硬件系统，在目前形式化验证工作中发挥着重 要作用，但是，定理证明方法需要大量来自经验丰富的用户的指导，无法完全自动化， 所以在验证工作中难以大规模应用。 1 2 2 模型检验方法 模型检验方法的框架如图1 3 所示，被验证系统模型化为一个有限状态转移图 ( k r i p k e 结构) 。系统规范表示为组时态逻辑公式，不同模型检验系统可能支持不同 的时态逻辑，如c t l ( c o m p u t a t i o n t r e el o g i c ，计算树逻辑) 、l t l ( l i n e a rt e m p o r a ll o g i c ， 线性时态逻辑) 、b t t l ( b r a n c h i n g t i m e t e m p o r a l l o g i c ，分支时态逻辑) 等等。模型检 中国科学院博士学位论文运算电路的形式化验证方法研究 验系统验证k r i p k e 结构是否满足时态逻辑公式。目前，根据核心算法不同，模型检验方 法主要分为四大类：显式模型检验方法，基于决策图的模型检验方法，基于s a t 的模型 检验方法和基于符号模拟的模型检验方法。以下分别介绍四类模型检验方法，并分析各 种方法的优缺点。 1 2 2 1 显式模型检验方法 图1 3 模型检验方法框架 在二十世纪八十年代，c l a r k e 等 c e 8 1 和q u i e l l e 等 q s 8 2 几乎同时独立提出了时 序逻辑模型检验方法，该方法构造一个搜索程序，判定在给定的有限状态转移模型m 和初始状态s o 下规范f 是否成立，即m ，s off 是否成立。搜索程序对所有的状态进行 遍历，因此该方法又称为显式模型检验方法。由于系统的状态是有限的，所以搜索程序 最终一定会停止。 显式模型检验方法需要遍历系统所有状态，容易发生状态爆炸。最初，显式模型检 验系统最多只能处理大约1 0 8 个状态，许多研究人员预测显式模型检验方法不能实际用 于大规模电路验证，但是后来随着偏序规约( p a r t i a lo r d e rr e d u c t i o n ) f g p 9 3 ，k p 8 8 ， v a l + 9 2 、k u r s h a n 的局部规约( l o c a l i z a t i o nr e d u c t i o n ) k u r + 9 4 】以及对称性规约 ( s y m m e t r yr e d u c t i o n ) c e f + 9 6 ，e s 9 6 ，n d 9 6 等方法的提出，显式模型检验方法可验 证系统规模逐渐增大。 典型的显式模型检验工具包括s p i n 【h p 9 6 ，s t a n f o r d 的m u r p h i d i l l 9 6 ，以及 c o s p a n 【h h k 9 6 】。s p i n 采用了偏序规约方法，比较适合并行软件程序的设计验证、 通信协议以及安全协议的验i 正 c a t + 9 4 ，m s 0 2 等。m u r p h i 采用了基于对称的状态约简 方法，d i l l 等 d d h + 9 2 幂i j 用m u r p h i 验证了s c i ( s c a l a b l e c o h e r e n ti n t e r f a c e ，可扩展一 致性接口) i e e e 标准1 5 9 6 1 9 9 2 协议，发现了该协议的一些设计缺陷。c o s p a n 是 l u c e n t 公司的商用验证工具f o r m a l c h e c k k u r + 9 7 1 的核心部件，它基于语义蕴涵 6 第一章绪论 ( l a n g u a g ec o n t a i n m e n t ) 方法，并使用局部规约算法动态简化电路，典型应用包括在 9 0 秒内发现了m p e g 接口控制器中的一个设计错误 k w + 9 7 。 1 _ 2 _ 2 2 基于b d d 的模型检验方法 a k e r s a k e + 7 8 于1 9 7 8 年提出了用b d d ( b i n a r y d e c i s i o nd i a g r a m s ，二元决策图) 表示布尔函数的方法。1 9 8 6 年，b r y a n t b r y + 8 6 系统阐述了布尔函数表示方法o b d d ( o r d e r e d b i n a r y d e c i s i o n d i a g r a m s ，有序二元决策图) 以及对o b d d 的函数操作算法。 由于b d d 通过符号运算而不是状态枚举方式表示布尔函数，因此，基于b d d 的模型检 验方法又称为隐式模型检验方法或者符号模型检验方法。 与状态枚举相比，b d d 表示布尔函数更加精简，有效缓解了状态爆炸问题。基于 b d d 的模型检验方法一般可以处理大约1 0 2 0 个状态 b c m + 9 0 ，m c m + 9 3 1 ，通过对基于 b d d 的模型检验方法优化改进，模型检验方法的处理规模可达到1 0 1 2 0 个状态 b c l 9 1 ， b c l + 9 4 ，并且通过适当的抽象技术理论上可以检验无限状态系统 c g l 9 4 。 基于b d d 的较有代表性的模型检验工具包括c m u 的s m v m c m + 9 3 ，b e r k e l e y 的v i s b h s + 9 6 】，瑕m 的r u l e b a s e b b e + 9 6 】。 s m v 是第一个基于b d d 的符号模型检验工具，在s m v 系统中，系统规范支持c t l 和c t l * 时态逻辑公式。1 9 9 2 年，c l a r k e 等人利用s m v 验证了i e e ef u t u r e b u s + 标准 8 9 6 1 - 1 9 9 l 描述的c a c h e 一致性协议 c g h + 9 5 1 ，发现了协议设计中三个潜在的错误，这 是人们第一次通过自动验证工具发现了i e e e 标准协议的错误。近年来，为了实现运算 电路设计验证，c h e n 和c l a r k e 等研究人员引入了字级( w o r d l e v e l ) 模型验i 正 c k z 9 6 ， c c h + 9 6 1 ，被验证系统和系统规范中支持字级变量运算，采用h d d ( h y b r i dd e c i s i o n d i a g r a m ，混合决策图) c f z 9 5 作为数据结构，可以自动验证大量运算电路。c h e n 等 人进一步将h d d 扩展为* p h d d c b 9 7 ，并在一系列方法学指导下完成了浮点加法运算 电路的验i e c b 9 8 。 v i s 采用v e r i l o g 语言描述被验证系统，采用c t l * 时序逻辑公式表示规范，不仅包 含模型检验功能，而且包含了组合电路、时序电路等价检查功能。并且通过一个公共的 中间表示格式b l i f m v ，v i s 可以和s i s s s l + 9 2 逻辑综合工具进行交互，简化逻辑。 v i s 小组 v i s 】收集了一些对c a c h e 一致性协议、p c i 局部总线、m p e g 译码器、指令 预取以及d l x 的验证实例。 r u l e b a s e 是基于s m v 、面向工业级应用的模型检验工具，它提供了一个图形化用 户界面，被验证系统用v e r i l o g 或v h d l 描述，系统规范采用s u g a r 语言描述。作为 r u l e b a s e 最早和最大的用户组，g a l i l e ot e c h n o l o g y 公司的y o r a v 等人 y k k 0 1 使用 r u l e b a s e 验证了通信系统控制器，发现了几个涉及同步问题的设计缺陷。z o r a n 微电子 p a r + 0 0 采用r u l e b a s e 验证了m p e g 视频译码、图像处理单元、译码部件、中断仲裁以 及a t a p i 等设计模块。 中国科学院博士学位论文运算电路的形式化验证方法研究 1 2 2 3 基于s a t 的模型检验方法 1 9 9 9 年，b i e r e 等人 b c c + 9 9 提出了b m c ( b o u n d e d m o d e lc h e c k i n g ，有界模型检 验) 方法。b m c 的基本思想是：从初始状态开始，在小于等于k 次状态迁移产生的状 态空间中寻找使规范不成立的反例。通过给定长度界限k ，l t l ( l i n e a r t e m p o r a ll o g i c ， 线性时态逻辑) 模型检验问题可以在多项式时间内转化为c n f ( c o n j u n c t i v en o r m a l f o r m ，合取范式) 表示的s a t 问题，并可以通过通用的完全的s a t 工具求解。 由于s a t 算法复杂度与问题规模无关，仅取决于问题的约束程度( 对于随机s a t 问题，问题的约束程度体现在语句数和变量数的比值大小) ，所以与基于b d d 的模型检 验方法相比，对一些被验证系统和规范，b m c 可以更快地生成反例f b l m 0 1 ，b c r z 9 9 1 ， 需要更少的内存空间，并且不需要手工定义变量序或者费时的动态重排序。但是，当 b m c 无法在k 次状态迁移以内找到反例时，不能说明一定不存在反例，即b m c 无法判 定s a t 问题是否不可满足，因此b m c 是不完全算法。 为了证明s a t 问题不可满足( 相应于被验证系统满足规范的情况) ，需要完全的基 于s a t 的模型检验方法。目前，完全的基于s a t 的模型检验方法包含四个方向的研究 工作： ( 1 ) 、采用传统的基于定点迭代( f i x p o i n ti t e r a t i o n ) 的模型检验方法，用s a t 替 换b d d 进行可达性分析 a b e 0 0 ，w b c g 0 0 ，g y a 0 0 ，可以实现对c t l 属性完全的模 型验证。 s a t 支持向前( f o r w a r d ) 和向后( b a c k w a r d ) 的可达性分析。以向前的可达性分 析为例，从当前状态集r 出发经过一次状态迁移t 后得到的可达状态集为： i m a g e 。( s 。) = 3 s t ( s ，s ) r ( s ) 。s a t 工具被用于判定规范在新产生的可达状态集i m a g e 。 上是否可满足，以及可达状态集是否达到定点( f i x p o i n t ) 。在产生可达状态集i m a g e 。时， 公式中的量词通过j v f = f 0 v v f 1 v 消除。虽然该方法是完全的基于s a t 的模型检 验方法，但是由于消除量词的过程非常复杂，使得该方法只对具有较少输入的系统有效。 ( 2 ) 、采用基于归纳的b m c 方法 s s s 0 0 ，b c 0 0 验证安全属性( s a f e t y p r o p e r t y ) 。 算法过程类似b m c ，对属性在初始状态以及从初始状态出发的1 ，2 ，k 次状态 迁移产生的所有状态上是否成立进行验证，但是基于归纳的b m c 方法限定如果出现环 路，那么在该条路径上的验证结束。 s h e e r a l l 等人 s s s o o 指出，如果k 取所有无环路径( l o o p f r e e p a t h ) 中最长路径的 状态迁移数，并且属性在从初始状态出发的k 次状态迁移内产生的所有状态上都成立， 那么对于所有从初始状态出发的可达状态，属性都成立，从而保证了该算法是完全的验 证算法。在此基础上，s h e e r a n 等人又进行了一些改进，它们包括：对于状态迁移后产 生的状态，如果这个状态是初始状态，那么不需要考虑在这些状态上属性是否成立；从 经过任意次状态迁移后的状态集开始检查属性是否成立，而不是从初始状态；将k 的取 值从所有无环路径中最长路径的状态迁移数变为所有最短路径中的最长路径的状态迁 第一章绪论 移数，等等。该方法的主要问题是k 值有时很大，使得迭代很深，从而无法实现验证。 ( 3 ) 、采用结构化b m c 方法 b k a 0 2 ，该方法根据电路结构将验证任务分解为多 个子任务，对每个子任务，通过结构化算法计算状态迁移图的直径的边界。对几类特定 网表，该直径边界显示出较高的实用价值，能够避免冗余的和过多的状态迁移。但是该 方法需要电路具有特殊结构，而且不一定总是得到有效的边界值。 ( 4 ) 、基于插值( i n t e r p o l a t i o n ) 的b m c 方法 m c m 0 3 1 ，该方法是纯粹的基于s a t 的无界模型检验( u n b o u n d e dm o d e lc h e c k i n g ) 方法。对于k