（计算机软件与理论专业论文）基于bdd和sat的形式验证方法的研究.pdf

哈尔滨t 程大学硕士学位论文 葡晏 随着集成电路的设计规模越大越大、复杂度越来越高，产品上市时间却 越来越紧迫，集成电路的验证变得越来越困难。2 0 0 3 年度的国际半导体技术 发展报告( i n t e r n a t i o n a lt 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 ) 指 出，验证已经成为集成电路设计流程中最大瓶颈。传统的模拟验证因其测试 周期长、不能完全覆盖，已经不适合当前对集成电路的验证。过去二十年中， 人们发展了一种新方法一形式化验证( f o r m a lv e r i f i c a t i o n ) 方法。这是 v l s i ( v e r yl a r g es c a l ei n t e g r a t i o n ) 设计验证的一种有希望的方法。 形式验证意味着验证过程是数学化的，而不是如模拟技术那样，是试验 性质的。数学化的验证克服了模拟的不足，因为它的覆盖是完全的。形式验 证可以对电路描述进行自动化的验证，减少了验证的复杂度。形式验证作为 传统基于模拟的验证方法的补充，日益引起人们的关注。它的特点是使用严 格的数学推理来证明一个系统满足全部或部分规范。 本文研究基于b d d 及布尔可满足( s a t ) 算法的形式化验证方法。本文 针对布尔可满足性s a t 算法中存在的搜索空间大且复杂度高等问题，对s a t 算法进行了相应的改进，并提出了一种新的s a t 的全局搜索算法一d c & d s 算 法。其搜索空间比现有的布尔可满足性算法搜索空间都低得多，从而大大提 高了算法的效率。并将该算法应用到结合b d d 和s a 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 ts c h e d u l e so ft o d a y s d 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 n i n t e r n a t i o n a lt 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 r2 0 0 3h a sp o i n t e do u t ，t h a t v e r i f i c a t i o nh a s b e e nt h eb o t t l e n e c ki nt h ei cd e s i g nf l o w t h et r a d i t i o n a l e x t e n s i v es i m u l a t i o ni sn ol 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 d i tg i v e sn oa b s o l u t eg u a r a n t e e sa b o u tt h ec o n e c t n e s so ft h ed e s i g n i nt h ep a s t t w e n t yy e a r s ，p e o p l eh a v ef o u n dan e wm e t h o d - - - f o r m a lv e r i f i c a t i o n i ti s a h o p e f u lm e t h o d f o rt h ed e s i g nv e r i f i c a t i o no f v l s i f o r m a lv e r i f i c a t i o nm e a n st h e p r o c e s so f v e r i f i c a t i o ni sm a t h e m a t i c a l a n dn o t 鹪s i m u l a t i o nt e c h n o l o g yw h i c hi s e x p e r i m e n t a l m a t h e m a t i c a lv e r i f i c a t i o nc o n q u e r st h ei n s u f f i c i e n to fs i m u l a t i o n f o rc o m p l e t e n e s s ，a n dc a nr e d u c et i m ef o rv 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 ni st h e a u t o m a t i cv e r i f i c a t i o nf o rc i r c u i td e s c r i p t i o n , a n dc a nr e d u c et h ec o m p l e x i t yo f v 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 na so n eo fc o m p l e m e n t a r ya p p r o a c h e sh a sb e e np u t f o r w a r dt os o l v et h e s ep r o b l e m s t h ek e yc h a r a c t e r i s f i co ft h i sa p p r o a c hi st h a t f o r m a lm e t h o d sa r ea p p l i e dt oa c t u a l l yc 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 e c o r r e c t n e s so f t h ed e s i g n t h ed i s s e r t a t i o ng i v e st h es t u d yo fb i n a r yd e c i s i o nd i a g r a m sa n db o o l e a n s a t i s f i a b i l i t ya l g o r i t h m si nf o r m a lv e r i f i c a t i o nm e t h o d t h ed i s s e r t a t i o ni m p r o v e o nb o o l e a ns a t i s f i a b i l i t ya l g o r i t h m s a n dg i v e st h ed c & d sa l g o r i t h m s t h ep a p e r g i v e se q u i v a l e n c ec h e c k i n ga l g o r i t h m si nc o m b i n a t i o n a lc i r c u i tb a s i n go ns a t , t h ea r i t h m e t i ci n t e g r a t e st h es t r o n g p o i n to fb d da n ds a t , b yr e s t r i c t i n gt h es i z e o fc o n s t r u c t i n gb d d ，a v o i d se m sm e m o r ye x p l o d i n g a n dr e a s o n i n gm m i s h e s s e a r c h i n gs p a c eo fs a t a n da p p l yt h i sn e wa l g o r i t h mi nf o r m a lv e r i f i c a t i o n m e t h o d b a s i n go nb d d s a t t h e o r e t i c a lr e s e a r c ha n de x p e r i m e n c er e s u l t sh a v ep r o v e dt h ec o r r e c t u e s so f a l g o r i t h m sa n dd e s i g nm e t h o d sp r o p o s e di nt h i sd i s s e r t a t i o n 哈尔滨t 稃人学硕士学位论文 k e y w o r d ：f o r m a lv e r i f i c a t i o n ；s i m u l a t i o n ： b o o l e a ns a t i s f i a b i l i t y ：b i n a r y d e c i s i o nd i a g r a m s ： 哈尔滨工程大学 学位论文原创性声明 本人郑重声明：本论文的所有工作，是在导师的指导 下，由作者本人独立完成的。有关观点、方法、数据和文 献的引用已在文中指出，并与参考文献相对应。除文中已 注明引用的内容外，本论文不包含任何其他个人或集体已 经公开发表的作品成果。对本文的研究做出重要贡献的个 人和集体，均已在文中以明确方式标明。本人完全意识到 本声明的法律结果由本人承担。 作者( 签字) ：垦魉 日期：川年 1 月日 堕玺堡三堡丕堂婴堂丝笙茎 第1 章绪论 1 1e d a 技术 在现代数字系统设计中，电子设计自动化( e l e c t r o n i cd e s i g n a u t o m a t i o n ，e d a ) 技术已经成为一种普遍使用的技术手段。e d a 工具是以计 算机硬件和软件为基本工作平台，集数据库、图形学、图论与拓扑逻辑、计 算数学、优化理论等多学科最新成果研制的计算机辅助设计通用软件工具。 e d a 工具可以代替设计者完成电子系统设计中的大部分工作。e d a 工具从数字 系统设计的单一领域，发展到今天，应用范围已涉及模拟、微波等多个领域， 可以实现各个领域电子系统设计的测试、设计仿真和布局布线等。设计者只 要完成对电子系统的功能描述，就可以借助计算机和e d a 工具完成设计。 1 1 1e d a 技术的发展 当前国际微电子技术的迅猛发展，在集成电路产业中，集成电路设计是 有可能首先取得成功的行业，这一点在国内已取得共识。随着集成电路设计 技术的发展与数字通信、工业自动化控制等领域所用的数字电路及系统的复 杂度的提高，迫切需要掌握新的设计方法以减少复杂劳动，提高工作效率。 e d a 技术伴随着计算机、集成电路、电子系统设计的发展，经历了计算 机辅助设计( c o m p u t e ra i d e dd e s i g n ，c a d ) 、计算机辅助工和设计( c o m p u t e r a i d e de n g i n e e r i n gd e s i g n ，c a e ) 和电子设计自动化( e l e c t r o n i cd e s i g n a u t o m a t i o n ，e d a ) 三个发展阶段。 1 2 0 世纪7 0 年代的c a d 阶段 7 0 年代的第一代e d a 称为计算机辅助设计( c o m p u t e ra i d e dd e s i g n ， c a d ) ，它是以交互式图形编辑和设计规则检查为特点，那时的逻辑图输入， 逻辑模拟，电路模拟与版图设计及版图验证是分别进行的，人们需要对两者 的结果进行多次的比较和修改才能得到正确的设计，它不能适应较大规模的 设计项目，而且设计周期长，费用高。 由于设计师对图形符号使用数量能力有限，传统的手工布图方法又无法 满足产品复杂性的要求，更不能满足工作效率的要求，这时，人们开始将产 品设计过程中高重复性的繁杂劳动，如布图布线工作用二维图编辑与分析的 哈尔滨：j j 程大学硕士学位论文 c a d 工具替代，最具代表性的产品就是美国a c c e l 公司开发的t a n g o 布线软 件。e d a 技术发展初期，p c b 布图布线工具受到计算机工作平台的制约，能支 持的设计工作有限且性能比较差。 2 2 0 世纪8 0 年代的c a e 阶段 8 0 年代出现了第二代e d a 系统，常称为计算机辅助工程( c o m p u t e ra i d e d e n g i n e e r i n g ，c a e ) 系统。它以3 2 位工作站为硬件平台。它集逻辑图输入， 逻辑模拟，测试码生成，电路模拟，版图设计，版图验证等工具于一体，构 成了一个较完整的设计系统。工程师是从输入逻辑图开始设计集成电路，并 在工作站上完成全部的设计工作。它不仅有设计全定制电路的版图编辑工具， 还包括有门阵列、标准单元的自动设计工具和具有经过制造验证的，针对不 同工艺的单元库。在c a e 系统中更重要的是引入了版图和电路图之间的一致 性检查工具和“后模拟”，保证了设计的一次成功率，但是一致性检查和“后 模拟”仍是在设计的最后阶段才实施的，因而一旦发现错误，还需修改版图 或修改电路，仍需付出相当的代价。 3 2 0 世纪9 0 年代的e d a 阶段 进入9 0 年代，芯片设计的高复杂度使得单是依靠原理图输入方式已不堪 承受，采用硬件描述语言的设计方式就应运而生，设计工作从行为、功能级 开始，e d a 向设计的高层次发展，这就出现了第三代e d a 系统，其特点就是 高层次设计的自动化m ”。第三代e d a 中，引入了硬件描述语言，一般采用两 种标准化语言，v h d l 和v e r i l o gh d l 语言；此外引入了高级综合( 行为综合) 和逻辑综合工具。从较高的抽象层次开始，按自顶向下的方法进行设计，可 大大提高处理复杂设计的能力，设计周期也大大缩短；综合优化工具的采用 使芯片的品质如面积、速度和功耗等获得了优化。因而第三代e d a 系统受到 广泛的青睐。 进入9 0 年代中期后，e d a 技术已趋向成熟，但由于半导体工艺技术的不 断进步，集成电路发展到s o c ( s y s t e mo nac h i p ) 和v d s m ( v e r yd e e ps u b m i c r o n ) 阶段，诸多新的问题摆在人们面前，这对设计自动化方法提出了新的 要求。 进入9 0 年代中期以后，集成电路发展到大规模、超大规模的水平，每片 门数达到几十万到几百万门，一个完整的电子系统可集成到一个芯片上，这 哈尔滨t 稃大学硕士学位论文 就是所谓的单片系统、片上系统或系统芯片( s o c ) 。同时，设计技术也从深 亚微米( d e e ps u bm i c r o m e t e r ，d s m ) 、超深亚微米( v d s m ) 技术发展到纳米技 术，这就要求更完备的设计工具和更好的设计方法来代替原有的先进设计技 术“1 。在设计工具方面，相应要求软件公司提供系统级的设计工具，也就是 要将e d a 提升到电子系统设计自动化技术( e l e c t r o n i cs y s t e md e s i g n a u t o m a t i o n ，e s d a ) 。人们正在尝试一种新的系统级设计语言即高级语言( 如 c 语言) 与h d l ( v h d l 、v e r i l o gh d l ) 混合应用来完成这一工作。在设计方 法上，采用可重用设计技术，其核心是知识产权模块( i n t e l l e c t u a l p r o p e r t y ，i p ) ，它是一个高性能、可参数化、可综合、可供测试的，用h d l 语言描述而成，与具体实现工艺无关的“软核”( s o f tc o r e ) 。作为一种独立 于工艺的设计，可嵌入式地应用于各类片上系统中。可重用技术的应用不仅 可以大大缩短芯片的设计周期，而且还可以消除e s d a 与e d a 之间的衔接障碍， 促进e s d a 设计技术迅速发展和成熟起来。 1 1 2e d a 技术特点 现代e d a 技术的主要特征是采用硬件描述语言，具有系统级仿真和综合 能力。具体说，有以下几个方面的特点。 1 采用硬件描述语言 采用硬件描述语言设计数字系统是现代e d a 技术的重要特征之一。与传 统的原理图输入方式相比，硬件描述语言更适合描述大规模系统，能够使设 计者对数字系统进行抽象层次的描述。目前常用的硬件描述语言有v e r i l o g h d l 和v h d l ，它们都已经成为i e e e 标准。 2 具有高层次综合和优化功能 为了更好地支持自上而下的设计方法，现代e d a 技术能够在较高层次的 系统级进行综合和优化。支持高层次综合和优的工具有s y n o p s y s 公司的 b e h a v i o r a lc o m p i l e r ，利用这些综合工具可以达到非常好的优化结果，缩短 设计周期，提高设计效率。 3 支持并行工程设计 并行工程指的是一种系统化的、集成化的、并行的产品及相关过程的开 发过程的开发模式。现代e d a 工具建立了并行工程框架结构的开发环境，支 哈尔滨t 程大学硕十学位论文 持多个开发人员并行进行设计，以适应现代数字系统设计的开发特点。 4 具有开放性和标准化平台 随着设计数据格式的逐步标准化，不同设计风格和应用场合的要求导致 各具特色的e d a 工具被集成在同一个工作站上，从而使e d a 框架标准化。 任何一个e d a 系统只要建立一个符合标准的开放式框架结构，就可以将 第三方的e d a 工具集成在一个统一的环境下，实现资源共享。多种e d a 工具 一起参与设计，实现多种e d a 工具之间的优化组合，可进一步提高e d a 系统 的工作效率和灵活性。 1 2 课题研究的意义 复杂的超大规模集成电路是二十一世纪集成电路( i c ) 的主流，随着集 成电路技术的发展，超大规模集成电路( v e r yl a r g es c a l ei n t e g r a t e d d i r c u i t 。v l s i ) 部件可以是真正的系统级部件，v l s i 正在深刻地改变计算机 系统结构乃至整个电子产品的设计和生产的面貌。计算机系统和数字硬件的 设计者面临两个不同的任务，即完成设计本身并且验证设计的正确性，而设 计v l s i 的数字系统中的关键问题之一是如何检查设计的正确性，即设计验证。 但是设计验证的复杂度随着芯片的规模呈指数增加。2 0 0 3 年度的国际半导体 技术发展报告( i n t e r n a t i o n a lt 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 a 2 0 0 3 ) 指出，验证已经成为超大规模集成电路设计流程中开销最大的工 作。 数字电路设计，特别是芯片设计，一方面对电路的规模、复杂度和可靠性 等不断提出新要求，另一方面由于竞争的压力，产品设计和推向市场的时间不 断缩短。在目前的工程项目中，验证的时间占整个设计周期的5 0 8 0 。因 此设计的正确性验证成为设计的瓶颈。 现在的v l s i 系统异常复杂，设计时容易出错，则时应用往往对它的可靠 性要求极高。为了验证v l s i 系统是否正确，人们提出了种种验证方法，期望 借助e d a 工具的帮助，尽可能地找出错误。 对于v l s i 设计而言，验证的方法主要有模拟验证和形式验证两大类。 进行模拟验证是通过建立系统准确模型，进行反复模拟是目前进行硬件 设计验证的主要途径。但随着芯片的规模日益庞大，运行模拟和检查模拟结 哈尔滨t 稃大学硕十学位论文 果可能需要几天或更多时间。随着系统设计复杂性的不断增加，设计正确性 的证明过程变得非常费时，况且，模拟不可能是穷尽的，它很难发现那些埋 藏在设计深处的设计错误，己无法满足现代i c 设计的需要。传统的验证手段 如模拟、测试、仿真等技术，只能针对某些典型情况或随机进行，验证就很 难发现和排除所有的设计错误。 逻辑设计的形式验证研究是在7 0 年代中期开始的。这个时候，逻辑模拟 已广泛用于验证逻辑设计。由于计算机工业的迅猛发展对设计自动化e d a 的 需要，而且计算机结构和逻辑体系密切联系，形式验证的研究也随之迅速发 展。近年来，陆续有许多有效的方法问世，并逐步向着实用化方向发展。 形式验证作为传统基于模拟的验证方法的补充，日益引起人们的关注。 它用数学方法表达系统的规范或具有所期望的性质，在不能证明所期望的性 质时，则可能发现设计错误。克服了传统验证方法如模拟和测试的不足，通 过形式规范和证明增强了对系统的理解而发现设计错误，或者通过形式化的 自动验证发现了用其他方法不能发现的设计错误。 在验证中，错误发现得越早，对开发进度的影响越小，这时验证就越有 价值。因此，要尽量在设计的早期阶段( 算法架构设计、r t l 设计时) 进行充 分的验证。 形式化方法作为计算机系统设计验证的一条有效途径，对其进行研究是 非常具有理论和实践意义的。本人的论文将对已有的形式验证方法作深入系 统的研究。在此基础上进行创新，在优化形式验证方法的同时，以实现提高 验证效率的目的。 1 3 模拟验证 验证的方法主要有模拟验证和形式验证两大类。一般把模拟验证分为模 拟、测试、仿真。而在模拟验证中，仿真是功能验证的主要手段，其基本原 理如图1 1 所示。 哈尔演t 稃大学硕十学位论文 图1 i 仿真基本原理 仿真( s i m u l a t i o n ) 是在电子系统设计过程中用来对设计者的硬件描述 和设计结果进行查错、验证的一种非常重要的方法。仿真系统的构成如下图 1 2 所示。 图1 2 仿真系统的构成 当设计工程师用v e r i l o g 语言描述、或用逻辑电路图设计了一个电子系统 之后，需要验证其正确性。在分层次自上而下对大规模集成电路进行设计的 过程中，从设计者对电路功能、行为的描述，到每个层次的设计结果，每一 个阶段都要进行正确性验证，以确保设计中的错误早期发现、早期排除。 随着设计规模的增大，片上系统( s o c ) 设计的进展，利用人工方法验证 设计的正确性已经十分困难。e d a 工程的迅速发展，使设计自动化工具逐渐成 熟。尽管如此，自动综合工具生成的设计结果，也需要进行验证。任何e d a 工具都不是完美无缺的，它在满足了某一方面的要求之后，与其对立的方面 就不能较好的兼顾。例如：设计时考虑状态转换正确，考虑元件的利用率， 就可能使延迟时间兼顾不周，造成某些情况下时序配合偏差，产生随机故障。 在工程实践中，设计项目需要增加新功能，设计工程师把原来的设计结 果拿来修改，修改后的设计需要验证其整体功能是否符合要求。还有，常见 的错误还出现在设计者的描述过程中。当v e r i l o g 描述文件没有正确反映设计 思想和目标时，若不加验证，是不能达到设计目标的。 6 哈尔滨t 程大学硕七学位论文 仿真是指从电路的描述抽象出模型，然后将外部激励信号或数据施加于 此模型，通过观察该模型在处部激励信号作用下的反应来判断该电子系统是 否达到了设计目标。仿真方法是e d a 工程常见方法。根据不同的电路层次，有 不同的仿真工具。由于设计工程师对数字电子系统设计的层次不同，形成了 不同的仿真工具。一般分为电路级仿真、逻辑仿真、开关级仿真、寄存器传 输级仿真及高层次仿真这五个层次的仿真。不同的仿真层次不但在描述方法 上不同，在模型抽象、内部实现和仿真算法上也有很大区别。 仿真器的基本思想是模仿实际电路的工作过程。经典的仿真方法是用实 验板来验证设计的正确性。在实验板上根据原理电路图搭接电路，输入端接 入信号发生器，提供激励波形，启动运行后用示波器观察内部和输出端波形， 判断电路是否工作正常。 由于实验板的方法存在许多不足，随着现代电子设计方法和e d a 工具的发 展，已经不用经典的实验板法来仿真大规模、复杂电路。利用计算机进行仿 真，电路模型不用实际元件而用表示电路结构或行为的数据，在输入端加入 输入数据，称为测试矢量，在输出端得到输出数据，比较输出数据，是否达 到设计目标，就能完成仿真的目的。 对同一个电路模型可以施加不同的测试矢量，进行多次仿真。控制仿真 过程需要有控制命令，包括仿真时间、仿真断点、仿真结果输出等。控制命 令可以写到一个文件中顺序执行，称为过程方式；也可以有用户随机键入控 制命令，管理仿真过程，称为交互方式。 逻辑仿真是验证的一种手段。逻辑仿真的技术已经成熟，获得了广泛的 应用。但是用逻辑仿真来验证逻辑设计存在着一些难以解决的问题。 逻辑仿真的基本原理是对逻辑设计结果施加一定的输入数据( 对门和功 能块级的逻辑电路则为一定的输入波形) ，在计算机上逻辑执行，得到相应 的输出结果。通过分析其输出结果查找错误，判断设计是否正确。这里有下 面三个问题： ( 1 ) 输入数据要由用户给出，而输入数据的好坏决定了所能查出的错误 的多少。 ( 2 ) 输出结果的分析要由有经验的人来进行。 ( 3 ) 由于输入数据难以穷举，尽管能查出许多错误，但不能保证不再存 哈尔滨t 稃大学硕十学位论文 在错误。 随着数字系统规模的扩大，逻辑仿真的缺点变得越来越突出。尤其输入 激励波形的确定本身就是个复杂的课题。事实上，一个电路设计结果正确 与否，是否具备所期望的功能，仅仅依赖于设计结果的结构。人们希望不要 指定激励波形，不要依赖于行为的模拟，而是根据逻辑设计的功能和结构的 描述来证明逻辑设计的正确性。 综上所述，仿真虽然是工程中最常用的一种验证方法，但是这种方法是 一个穷举设计中可能存在的错误的过程，只能证明某些错误存在或不存在。 也就很难发现和排除所有的设计错误。为解决设计验证这一难题，过去十多 年中，人们发展了一种新方法形式化验证( f o r m a lv e r i f i c a t i o n ) 方法。 这是v l s i ( v e r yl a r g es c a l ei n t e g r a t i o n ) 设计验证的一种有希望的方法。 形式化验证意味着验证过程是数学化的，而不是如模拟那样，是试验性质的。 数学化的验证克服了模拟的不足，因为它对指定描述中所有可能的输入组合 一次进行了验证，而不是仅仅对其一个子集进行多次试验。它无须测试向量， 在参考设计功能完全正确的前提下，测试的覆盖率可以达到1 0 0 。它已经从 研究阶段进入了应用阶段，是计算机系统设计验证的一条有效途径。 1 4 形式验证方法综述 用仿真的方法验证系统功能有三个缺点：一是很难对一些隐蔽错误进行 定位；二是要耗费大量的仿真时间；三是测试覆盖率低。随着v l s i 系统规模 的增大，这些缺陷越来越令人无法容忍。形式验证( f o r m a lv e r i f i c a t i o n ) 是不同于仿真方法的对逻辑设计结果进行验证的最有希望解决问题的途径。 传统的设计验证是通过模拟来完成的，然而随着电路复杂性的日益增加， 模拟需花费大量的c p u 时间，在实践中实现穷举的模拟来保证设计的正确性几 乎是不可能的。形式验证作为传统基于模拟的验证方法的补充，日益引起人们 的关注。它用数学方法表达系统的规范或系统的性质，并且根据数学理论来证 明所设计的系统满足系统的规范或具有所期望的性质，在不能证明所期望的 性质时，则可能发现设计错误。克服了传统验证方法如模拟和测试的不足，实 践证明形式验证确实通过形式规范和证明而增强了对系统的理解而发现了设 计错误，或者通过形式化的自动验证发现了用其他方法不能发现的设计错误。 堕堑! 堕! 壁盔堂亟主堂堡笙塞 因此有充分的理由说明形式验证方法是计算机系统设计验证的一条有效途 径。 在自上而下的设计过程中，在设计的各个阶段和级别，每一级别设计都 以上一级的设计结果作为设计目标，得到本级的设计结果的结构描述，这是 设计或综合的过程。验证的任务就是所得到的结果正确实现其设计要求。这 里通常包括两个方面： 一 ( 1 )下一级所实现的功能与上一级的设计目标所要求的功能相一致， 即功能验证。 ( 2 ) 下一级本身符合设计规则和条件制约，包括连接关系的限制、时 间关系的配合等。包括结构验证、时序验证和规则验证等。 形式化验证就是这样一种验证方法，它根据逻辑设计的功能和结构描述， 用类似定理证明的方法或数学的方法来证明逻辑设计的正确性。 逻辑设计的形式化验证研究是在7 0 年代中期开始的。这个时候，逻辑模 拟已广泛用于验证逻辑设计，并开始暴露其问题，同时软件程序正确性证明 已经提出了几个有效的方法。人们开始把软件程序证明的方法用在硬件设计 的验证上。在此之后，由于计算机工业的迅猛发展对设计的自动化的需要， 由于计算机结构和逻辑体系密切联系，形式化验证的研究也随之迅速发展。 近年来，陆续有许多有效的方法问世，并逐步向着实用化方向发展。 一般来说，形式验证方法可以分为等价性检验( e q u i v a l e n c ec h e c k i n g ) 、 模型检验( m o d e lc h e c k i n g ) 和定理证明( t h e o r e mp r o v i n g ) 方法。 1 4 1 模型检验 将原始设计表示成有限状态机，将要验证的性质用时态逻辑描述。然后， 遍历有限状态机以检验性质是否存在。有限状态机模型通常采用k r i p k e 结 构，在该结构上路径是无限延伸的。模型检验的优点是：全自动进行而无须 人机交互。当断定某性质不满足时，模型检验能提供反例，以便于定位设计 错误。凭借时态逻辑强大的描述能力，模型检验能够对各种复杂的时序性质 进行验证。 状态空间爆炸问题是模型检验的主要缺点。可以说，模型检验技术的发 展历史就是不断寻找新思路、新策略和新算法来克服空间爆炸问题的历史。 哈尔滨工稃大学硕十学位论文 模型检验技术产生于8 0 年代初，由美国的c l a r k e 和e m e r s o n ，法国的 q u i e l l e 和s i f a k i s 分别独立提出。这时的模型检验算法都是通过显式地枚 举状态空间的可达状态来验证性质，通常所能处理的状态数也就在几百万左 右。状态数呈指数上升的状况和显式模型检验有限的处理能力之间存在难以 克服的矛盾。 1 9 8 6 年，b r y a n t 将传统的b d d ( b i n a r yd e c i s i o nd i a g r a m ) 技术加以改 进，使之成为布尔表达式的规范表示方法。m c m i l l a n 在1 9 8 7 年将这种技术 应用于模型检验中，取得了巨大的成功，使模型检验的发展再度复兴。基于 b d d 的模型检验称为符号模型检验( s y m b o l i cm o d e lc h e c k i n g ) 。符号模型检 验的主要思想是用o b d d 来隐式地表示有限状态机的状态和状态之间的迁移， 其优点是能够表示一组而不是单个的状态和状态之间的迁移关系，因此大幅 度减小了空间需求。实验表明符号模型检验方法能处理的状态数达1 0 2 0 量 级，进一步改进的算法所能处理的状态数达到1 0 1 2 0 。 模型检验理论经提出后，第一次在工业界取得了巨大的成功，并逐渐被 工业界接受，成为模拟技术的重要补充。但符号模型检验并没有彻底地解决 问题，其最大瓶颈仍然是：存储和操作b d d 时对内存要求过大。 定界模型检验技术是继符号模型检验后的又一重要进展。定界模型检验 由b i e r e 等在1 9 9 9 年提出。定界模型检验是基于s a t 的模型检验，它依赖于 可满足性( s a t i s f i a b i l i t y ，s a t ) 问题的求解器。定界模型检验的主要思想 是：在一个限定的步数k 内，考察系统运行的情况，确定性质是否满足。若 不能确定性质是否存在，则提高k 值，重新进行检验。在每一个检验周期内， 定界模型检验问题被转化成s a t 问题求解。 s a t 问题虽然己证明是n p - c o m p l e t e 问题，在实际应用中却很有效。s a t 求解比b d d 求解的最大优势是空间爆炸问题远没有那么严重。i n t e l 的研究 报告显示：在对p e n t i u m - 4 芯片中抽取的典型设计进行验证中，定界模型检 验在验证能力和效率上都比符号模型检验有优势。 综上所述，对模型检验问题的研究虽然取得了重大的进步，但现今仍然 是具有挑战性的研究课题。迄今已提出很多新算法和改进算法，如偏序化简、 组合推理、抽象、利用对称性、基于自动机( a u t o m a t a ) 的验证等。 哈尔滨工程大学硕士学位论文 1 4 2 定理证明 定理证明的原理2 是：首先定义一种数学逻辑，该逻辑系统实际上是一个 形式化的系统，由一系列公理和推理规则组成。然后用这种数学逻辑分别表示 被验证系统和其被期望的特性。所谓定理证明就是从系统的公理出发使用推 理规则逐步推导出其所期望的特性的证明过程。证明所需要的步骤依赖于系 统的公理和推理规则，在某种程度上也依赖于其派生定义和中间引理。定理证 明器的类型很多，既有高度自动化的通用系统，也有为专用目的设计的，具有 交互功能的系统。自动化的定理证明系统可用作通用的搜索程序并且在许多 领域取得了显著的成就：交互式的定理证明系统则更多地用于数学的系统和 形式化处理以及形式方法的机械化。 与模型检验不同，定理证明可直接处理无限的状态空间。它使用类似于结 构化的推导过程来证明具有无限状态的系统。另外值得指出的一点是，由于大 多数定理证明器是交互的，在找到证明的过程中，用户的直觉往往起着决定性 的作用，因此定理证明的速度相当慢而且容易出错。定理证明是形式验证技术 中最先进的方法，但仍需进一步研究。 1 4 3 等价性检验 等价性检验由于其问题的特殊性，验证方法可分为符号方法和增量方法。 符号方法：首先将问题形式化成为一种特定的符号表示，然后诉诸于某 种特定的问题求解方法，如b d d 、s a t 、a t p g 、定理证明器等。如果被检验的 电路缺乏结构上的相似性，或者不能得到电路设计的内部情况时，则适用于 用这种方法检验等价性。 对于组合电路来说，不存在状态寄存器，其输出值是输入向量的函数， 而不依赖于前面的输入值。这时只需要对于每个输入向量证明其输出向量相 同即可证明等价性。对此问题一个直觉的做法是将待检验电路都转化成b d d ， 因为如果它们确实等价，则它们的b d d 就是同构的。如果待检验电路很大，或 者比较特殊( 比如乘法器) ，则b d d 规模就会很大。这时，需要考虑采用其他的 问题求解方法，如s a t 、a t p g 、定理证明器等。 对于时序电路来说，其输出值不仅依赖于输入向量，而且依赖于目前的 状态值。因此，时序电路的等价性检验更加复杂。常见的解决方法是：把时 哈尔滨_ t 程大学硕十学付论文 序电路看成有限状态机，将两个电路的相应输入相连接，相应的输出分别连 接到一个异或门的输入、异或门的输出作为总的输出，这样构成的模型称为 称为m i t e r 。两个时序电路等价当且仅当m i t e r 的输出恒为假。判断m i t e r 的恒 假性可采用显式状态遍历，也可采用b d d 进行隐式状态遍历。 增量方法：利用被检验电路在结构上存在的相似性，逐步检验局部电路 的等价性，进而最终得到电路在整体上的等价性。具体实现时，增量方法需 要不断地辨识电路中的等价点，并据此逐步减小验证的复杂性。对于时序电 路，情况要复杂得多，不仅需要辨识等价点，还要辨识等价寄存器。很明显， 该方法比较适用于相似性比较大的电路。 目前，模型检查与定理证明的方法还不成熟，而等价性检查而等价性检 查已成i c 设计流程的一部分。在三种形式验证方法中等价性检验用得最为广 泛，它用数学方法来验证参考设计与修正设计之间的等价性。利用等价性检 验工具可对这两种设计方案进行彻底的检验以保证它们在所有可能的条件下 都有一致的性能。还可以利用等价性检验来验证不同r t l 或门级实施方案的等 价性。 ab 图1 3 等价性验证的概念 上图给出了等价性验证的基本概念。等价性验证用于验证a 与b 是否等价。 这里b 是由a 转换而成的。这里a 与b 可以是r t l 代码，也可以是门级网表。在进 行等价性验证时，a 称为参考( r e f e r e n c e ) ，b 称为实现( i m p l e m e n t a t i o n ) 。 可以用形式验证来检查综合结果是否正确( r t l 设计与门级网表比较) 、 插扫描链前后网表是否一致、布局前后网表是否一致、插时钟树前后网表是 否一致、布线前后网表是否一致，如图1 4 所示。 堕笙鎏! 型丕堂堕主堂笪堡茎 图1 4v l s i 设计流程中的等价性验证 等价性检验主要目的是用来对两个电路、电路的设计前后或设计的规范 及实现进行逻辑功能的等价性检验。即在一个设计经过变换之后，穷尽地检查 变换前后的功能的一致性，即证明设计的变换没有产生功能的变化。另外：如 果设计者要将原来的设计的功能进行必要的修改，等价性检查产生的信息可 以用来帮助设计者确认所做的修改是否达到了目的。 等价性检验的基本原理是依据数学的定理和公理，以及设计实现所利用 的标准单元库的精确的描述来建立被比较的两个模型之间的关系。等价性检 验程序自动确定放比较的两个设计的关系，而不需要用户的输入。因此它的优 点是使用简单，且很容易集成到设计流程中。目前c a d e n c e 公司已经推出了等 价性验证工具h f f i r m a 。它把建立被比较的两个设计之间的关系和等价性证明 合并为一个步骤进行。它首先假定两个设计的锁存器和存储器元件是等价的， 然后利用随机输入向量对于两个设计进行功能模拟并且根据模拟结果划分锁 存器。在没有用户干预的情况下，利用二叉决策图和可满足性算法，它能够很 快地识别在两个设计之间在功能上相对应的节点。当然每个算法可能把问题 分解为若干子问题。并且对于这些子问题采用另外的算法。利用这些互补的 办法可以验证对应结点的等价性。 堕堡堡工要盔堂堕堂焦鲨塞 功能 一致 功能 一致 功能一致 时序 图1 5y l s i 设计流程与等价性检验 等价性检验的主要任务是比较两种设计中相应的组合功能块。进行该项 检验时先将设计分成较小的比较点或关键点，然后评估一个设计中给定的比 较点上的逻辑功能是否与加外一个设计中对应的比较点关键点的逻辑功能 等价。比较点可以是输入端、状态点( 或寄存器) 和输出端。等价验证工具 在比较两个电路逻辑行为的同时，可确保设计流程和一致性。 当等价性检验工具检测出两个设计之间在功能上的一个差别，它就显示 一个反例，即一组原始输入或若干锁存器以及它们的引起这个差别的原始的 信息。如果把模拟程序同等价性检验工具集成在一起，就可以利用这些信息进 行模拟以便找出造成这种差别的原因。 通常在综合后、在第一次布线完成后以及在每次对网表中的错误进行修 改( e c ) 时均要进行等价性验证。等价性验证可以验证e d a 工具的结果是否正确， 也可以验证网表修改是否正确。 例如，在设计布线完成后，设计者发现设计中有错误。这时候，需要在r t l 代码与网表中同时作修改。如果r t l 与门级修改不一致，通过形式验证可以很 容易发现。 等价性验证工具通过比较设计中比较点的功耗与状态是否等价，以此来 验证两个参考设计实现是否等价。 比较点是等价性验证中的一个重要概念。它包括输出、寄存器、“黑盒 子”的输入等。一般来说，形式工具会根据信号的命名来自动选择比较点。 1 4 堕签堡! 矍盔堂堡圭堂笪笙塞 对于一些特殊的、形式工具难以识别的比较点，设计者也可以手工进行设置。 需要说明的是，等价性验证仅能保证两个设计的一致性，不能保证设计 本身的正确性。因此，在v l s i 设计中，仿真仍是必不可少的步骤。 1 5 形式验证在工业界的应用状况 来自学术界的创新思想是商业软件研究开发的动力源泉。目前b d d 、s a t 、 a t p g 等技术已经成为任何验证工具所依赖的基本技术。等价性检验已经成为 工业界的标准形式验证工具，几乎所有的e d a 供应商都提供这种工具。目前的 等价性检验工具可比较r t l 级、门级、开关级模型，但是，目前还不能很好地 解决在r t l 级及其以上等价性检验问题。 标准的来自学术界的工具不能直接应用于实际系统的验证，因为验证所 面临的一般是一个用硬件描述语言( h d l ) ( 非k r i p k e 自动机) 给出的系统设计， 以及用断言( a s s e r t i o n ) ( 非时态逻辑) 描述的性质。因此，从标准形式验证工 具到商业形式验证工具的转变至少需要做到两点：h d l 到自动机的自动转换： 断言到时态逻辑的自动转换。 断言与时态逻辑一样，描述了系统应有的性质，但表示更为简洁。断言 的主要作用是作为设计工程师和验证工程师之间沟通的桥梁，因为两者都能 理解某种断言。断言的另一个重要作用是成为模拟验证和形式验证的有机结 合的一种途径，因为两者是以不同方式检验断言的正确性。近年来，美欧一 些专业验证技术开发公司得到风险投资而迅速成长，其产品已被大的e d a 公司 融入其设计流程中( 如v e r p l e x 被c a d e n c e ，o _ i nd e s i g na u t o m a t i o n 被m e n t o r g r a p h i c s 所收购) 。一些断言标准如o p e nv e r i f i c a t i o nl i b r a r y ( o v l ) 、 p r o p e r t