（计算机应用技术专业论文）组合电路的形式验证方法研究.pdf

摘要 设计大规模数字电路中的关键问题之一是如何检查设计的正确性，即设 计验证。但是设计验证的复杂度随着芯片的规模增大呈指数增加。传统的 验证手段难以排除所有的设计错误，人们转而求助于各种形式验证方法来保 证设计在各种可能输入组合下的正确性。 形式验证是e d a 领域的关键技术，在电路设计中越来越显示出重要性。 本文首先介绍了e d a 的发展，并晚明了课题的研究意义，接着对形式验证 方法做了简要的综述，介绍了等价性检验、模型检验和定理证明等形式化验 证方法，本文主要内容论述改进后的形式验证方法。 等价性检验是形式验证的一个重要方法，但在等价性检验中，一般验证 只考虑了底层的信息，本文把高层的规格晓明信息用在组合电路的等价性检 验中。多项式是表示电路的一种有效方法，但对于包含分支的电路，多项式 表示的阶次一般比较高。本文给出了一种含有分支电路的多项式表示的有效 方法，并把无关项子集考虑进来，以简化多项式阶的求解。在此基础上，给 出一个基于多项式表示的等价性检验方法。 随着集成电路规模的扩大，越来越多的复杂设计适合采用基于i p 核的设 计。由于知识产权的保护，包含黑盒的设计验证是一项非常重要的任务。文 献中这方面的方法基本上是基于b d d 思想的，本文给出了一种基于多项式 表示的特征函数验证方法，对包含黑盒的组合电路能进行有效的验证。 关键词：形式验证；多项式表示；等价性检验：b d d ；黑盒 a b s t r a c t o n eo ft h ec r i t i c a lp r o b l e m si n d e s i g n i n g a v e r yl a r g es c a l ed i g i t a lc i r c u i ti s h o wt oc h e c kt h ec o r r e c t n e s so ft h ed e s i g n h o w e v e r , t h ec o m p l e x i t yo ft h ed e s i g n v e r i f i c a t i o ni s e x p o n e n t i a lw i t ht h ei n c r e a s e o ft h e c h i p s c a l e t h et r a d i t i o n a l v e r i f i c a t i o nm e t h o dc a n te l i m i n a t ea l lt h ed e s i g ne r r o r t h e r e f o r e ，m a n yp e o p l e t u r nt ov a r i o u sf o r m a lv e r i f i c a t i o nm e t h o d st o g r a n t e et h e c o r r e c t n e s so ft h e d e s i g nu n d e ra n yi n p u t s f o r m a lv e r i f i c a t i o ni so n eo ft h ek e yt e c h n o l o g i e si ne d a ，a n di tb e c o m e s m o l ea n dm o r ei m p o r t a n ti n c i r c u i t d e s i g n i n t h ef i r s t p a r t o ft h i s p a p e r , t h e d e v e l o p m e n to fe d a i sd e s c r i b e da n dt h es i g n i f i c a n c eo ft h et o p i ci sn a r r a t e d t h e nt h e c o n c e p t i o n o ff o r m a lv e r i f i c a t i o na n dt h e t e c h n i q u e o ff o r m a l v e r i f i c a t i o n ，s u c ha se 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 ga n dt h e o r e mp r o v i n g a r eb r i e f l yi n t r o d u c e d t h em a i nc o n t e n ti st h em e t h o d so ft b r m a lv e r i f i c a t i o n ， w h i c ha r em o d i f i e d e q u i v a l e n c ec h e c k i n g i sa n i m p o r t a n t m e t h o do ff o r m a l v e r i f i c a t i o n h o w e v e no n l yt h el o wl e v e li n f o r m a t i o ni sc o n s i d e r e di ng e n e r a lv e r i f i c a t i o n i n t h i s p a p e r , t h eh i g h l e v e l s p e c i f i c a t i o n i n f o r m a t i o ni sc o n s i d e r e di nt h e e q u i v a l e n c ec h e c k i n go fc o m b i n a t i o n a lc i r c u i t p o l y n o m i a li sa ne f f e c t i v em e t h o d i nr e p r e s e n t i n gc i r c u i t w h i l ef o rc i r c u i tc o n t a i n i n gb r a n c h e s ，t h eo r d e ri st o oh i g h a ne f f e c t i v em e t h o do fp o l y n o m i a lr e p r e s e n t a t i o no fc o m b i n a t i o n a lc i r c u i tw i t h b r a n c h e si sg i v e n i fw ec o n s i d e rd o n tc a r ei t e m s ，t h ep r o c e s so fc o m p u t i n gt h e o r d e ro ft h e p o l y n o m i a lr e p r e s e n t a t i o n i sr e d u c e dg r e a t l y ，t h e n ，am e t h o do f e q u i v a l e n c ec h e c k i n g b a s e do np o l y n o m i a lr e p r e s e n t a t i o ni sp r o p o s e d w i t ht h ei n c r e a s eo ft h ec i r c u i t s c a l e ，m o r ea n dm o r ec o m p l e xd e s i g n sa r e b a s e do n1 eb e c a u s eo ft h ep r o t e c t i o no fl e , t h ed e s i g nv e r i f i c a t i o nw i t hb l a c k b o xb e c o m e sav e r yi m p o r t a n tt a s k t h em e t h o d so nt h i sp o i n ti nl i t e r a t u r e sa r e m o s t l yb a s e do nb d d i nt h i sp a p e r , ac h a r a c t e r i s t i cf u n c t i o nm e t h o db a s e do n 哈尔滨1 榉人亨颂十学位论文 p o l y n o m i a lr e p r e s e n t a t i o n i s g i v e n ，w h i c h c a l l a v a i l a b l yv e r i f v c o m b i n a t i o n a l c i r c u i tc o n t a i n i n gb l a c kb o x 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 ，p o l y n o m i a lr e p r e s e n t a t i o n ，e q u i v a l e n c e c h e c k i n g ， b d d ，b l a c kb o x 哈尔滨工程大学 学位论文原创性声明 本人郑重声明：本论文的所有工作，是在导师的指导 下，由作者本人独立完成的。有关观点、方法、数据和文 献的引用已在文中指出，并与参考文献相对应。除文中已 注明引用的内容外，本论文不包含任何其他个人或集体已 经公开发表的作品成果。对本文的研究做出重要贡献的个 人和集体，均已在文中以明确方式标明。本人完全意识到 本人声明的法律结果由本人承担。 作者( 签字) ：巡 日期：伊牛年1 月劢日 鉴尘型；堡垒兰鎏璧堡丝塞 1 1 e d a 的发展阶段 第1 章绪论 当前国际微电子技术的迅猛发展，在集成电路产业中，集成电路设计是 有可能首先取得成功的行业，这一点在国内已取得共识。随着集成电路设计 技术的发展与数字通信、工业自动化控制等领域所用的数字电路及系统的复 杂度的提高，迫切需要掌握新的设计方法以减少复杂劳动，提高工作效率。 电子设计自动化( e l e c t r o n i cd e s i g na u t o m a t i c ，e d a ) 的发展大致可分 为以下四个阶段 ”。 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 ) ，它是以交互式图形编辑和设计规则检查为特点，那时的逻辑图输入， 逻辑模拟，电路模拟与版图设计及版图验证是分别进行的，人们需要对两者 的结果进行多次的比较和修改才能得到f 确的设计，它不能适应较大规模的 设计项目，而且设计周期长，费用高。 8 0 年代出现了第二代e d a 系统，常称为计算机辅助工程( c o m p u t e r a i d e d e n g i n e e r i n g ，c a e ) 系统。它以3 2 位工作站为硬件平台。它集逻辑图输入， 逻辑模拟，测试码生成，电路模拟，版图设计，版图验证等工具于一体，构 成了一个较完整的设计系统。工程师是从输入逻辑图丌始设计集成电路，并 在工作站上完成全部的设计工作。它不仅有设计全定制电路的版图编辑工具， 还包括有门阵列、标准单元的自动设计工具和具有经过制造验证的，针对不 同工艺的单元库。在c a e 系统中更重要的是引入了版图和电路图之间的一致 性检查工具和“后模拟”，保证了设计的一次成功率，但是一致性检查和“后 模拟”仍是在设计的最后阶段才实施的，因而一旦发现错误，还需修改版图 或修改电路，仍需付出相当的代价。 进入9 0 年代，芯片设计的高复杂度使得荦+ 是依靠原理图输入方式已不墩 承受，采用硬件描述语言的设计方式就应运而生，设计工作从行为、功能级 哈；滨j 样人学珂h “：位沦文 丌始，e d a 向设计的高层次发展，这就出现了第三代e d a 系统，其特点就 是高层次设计的自动化【9 ” 。第三代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 n ac h i p ) 和v d s m ( v e r y d e e ps u b m i c r o m e t e r ) 阶段，诸多新的问题摆在人们面f j l ，这对设计自动化方法提出了 新的要求。 进入9 0 年代中期以后，集成电路发展到大规模、超大规模的水平，每片 门数达到几卜万到几百万门，一个完整的电子系统可集成到一个芯片上，这 就是所溜的单片系统、片上系统或系统芯片( s o c ) t ”。同时，设计技术也从 深亚微米( d e e p s u bm i c r o m e t e r ，d s m ) 、超深亚微米( v d s m ) 技术发展到纳米 技术，这就要求更完备的设计工具和更好的设计方法来代替原有的先进设计 技术【“。 在设计工具方面，相应要求软件公司提供系统级的设计工具，也就是要 将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 。人们正在尝试一种新的系统级设计语言即高级语言( 如 c 语言) 与h d l ( v h d l 、v e r i l o gh d l ) 混合应用来完成这一工作。在设计 方法上，采用可重用设计技术，其核心是1 p ( i n t e l l e c t u a lp r o p e r t y ，知识产权 模块1 ，它是一一个高性能、可参数化、可综合、可供测试的，用h d l 语言描 述而成，与具体实现工艺无关的“软核”( s o f tc o r e ) 。作为一种独立于工艺 的设计，可嵌入式地应用于各类片上系统中。可重用技术的应用不仅可以大 大缩短芯片的设计周期，而且还可以消除e s d a 与e d a 之间的衔接障碍， 促进e s d a 设计技术迅速发展和成熟起来。 哈尔滨i 群人学硕十学位论文 1 2 课题研究的意义 本课题来源于国家自然科学基余项目基于多项式符号代数的系统芯片 d a 新方法研究( 项目编号：6 0 2 7 3 0 8 1 ) 。 当今微电子学技术的发展，使得含有数百万的集成电路已经能够大批量 地生成出来，真正的系统芯片( s o c ) 正在成为现实。但是如何正确地设计这 些超大规模集成电路的问题还没有解决。可以说集成电路的制造能力超过了 集成电路的设计能力【8 】。为了充分发挥投资惊人的集成电路生产线的生产能 概念设训 一一泵菊i i i 。、 。 系统划分 、 l 。1 1 。1 1 。j、 一) ： i 子系统功能描述 一一 设计者 丫1 罹面i 0 ：= 7 一i 。一 产 一 一 ，7 综合7 t 一 j j ，一一d r ， 逻辑揣述 7 j 1 逻辑验汪l 一一7 j r 。， 厂丽纛订 图1 1 数字系统自动设计的流程 一 一 一 事 i 一 哈尔滨l 科人学预+ 学位论文 力，需要更多的设计者及时地提供大量复杂的设计。另外，计算机技术和通 讯技术的高速发展，使得数字系统渗透到整个社会的各个领域，特别是对于 安全性要求极高的很多关键场合，也大量地采用了嵌入式系统：同时各种数 字硬件的设计变得十分复杂，用传统的设计方法已经很难应付，这些都是对 电路和系统设计者的严峻挑战。 在数字系统设计的各个阶段都离不开验证，图1 1 描述了数字系统设计 的流程。设计大规模的复杂的数字电路中的关键问题之一是如何检查设计的 正确性，即设计验证。但是，设计验证的复杂度随着芯片的规模呈指数增加。 传统的验证手段是模拟( s i m u l a t i o n ) 、测试( t e s t i n g ) 和仿真( e m u l a t i o n ) 技术，但 是对于大型的系统，模拟和测试都不能是完全的，只能针对某些典型的情况 而随机地进行，这就难以完全地排除所有的设计错误。由于集成电路工艺的 复杂性，它的试制费用相当昂贵；又由于电子产品市场的剧烈竞争，产品上 市的时间极为重要。设计中遗留的一点微小的错误将可能造成巨大的经济损 失或者引起人员伤亡等灾难性的后果。掘统计，设计验证的时问占整个设计 周期的5 0 8 0 。因此设计的正确性验证成为设计的瓶颈，被称为“验证 危机”i ”】。 、 在软件设计中也具有类似的问题，即程序的正确性验证问题。在6 0 年代 术兴起的软件验证技术就反映了计算机科学家和数学家为解决“软件危机”， 即软件设计正确性问题所做的努力。他们用数学的理论和方法严格地证明程 序的正确性。这些努力在程序设计方法学方面做出了很大的贡献。然而一般 人认为软件验证技术在工业界的应用基本上是不成功的。8 0 年代初，人们把 类似的方法用来验证硬件，产生了硬件的形式化验证技术。目前普遍认为， 硬件验证技术在工业界的应用前景是十分乐观的。现在可以晓，硬件形式化 验证技术的推广应用正在迅速展丌。出现这种情况的原因之一是软件和硬件 在复杂度方面具有很大的差别。即使最复杂的硬件，比典型软件的复杂程度 也要小的多。这就使得对于硬件可以有效地应用基于状态空间法的工具如模 型检验程序进行验证。另一个重要的原因是软件验证和硬件验证在本质上具 有不同的特点。软件验证经常需要用户利用自己的知识和经验相当深入地指 导验证过程，但是硬件验证系统可以有效地利用自动：状态穷举、语言包含和 符号熏写等方法进行自动验证。由于硬件具有比软件更好的模块性，经常可 4 堕尘垒! 。垒叁釜筌! ；塑：竺三 以把一个大规模的验证问题分解为若干孤立的规模较小问题，然厉用自动化 工具解决。 事实上，硬件验证理论和方法的研究和应用在近十几年来发展很快，特 别是最近几年，某些方面耳) ( 得了突破性进展。前几年被认为没有什么酊途的 硬件设计的形式化验证技术得到了工业界的普遍认可，特别是模型检验技术， 已经引起了e d a 产业的轰动和商业界的投资热潮。据统计，近几年在全世 界的主要e d a 公司都相继研制和推出了形式化验证软件。人们预料这项技 术将在电子设计领域得到更加广泛的应用。但是在国内，这种情况尚未引起 广泛重视，甚至很多人对于形式化验证感到陌生【1 3 】。 在硬件设计领域，由于集成电路工艺的发展，需要人们设计包含几万门 的电路，总的趋势是要把整个系统发计在一个硅片f s o c l 上。这时，软件和 硬件交织在一起，要进行软硬件协同设计( c o d e s i g n ) ；离散和连续的信息交互 作用，要研究混合系统的设计和验证方法。尽管出现了许多设计自动化工具 和系统，仍然难以保证设计的f 确性。例如奔腾5 8 6 芯片中的除法运算错误 是在大量进入市场之后被一位用户发现的，虽然这种错误发生的撅率为几亿 分之一，这个设计错误为i n t e l 公司造成四亿八千万美元的经济损失。因而在 硬件设计中为了增加设计正确性的信心和保证，寻求不同于传统的验证方法 是研究形式化方法的强大动力。 为解决设计验证这一难题，过去十多年中，人们发展了一种新方法 形式验证( f o m a a lv e r i f i c a t i o n ) 方法。这是v l s l ( v e r yl a r g es c a l ei n t e g r a t i o n ) 设 计验证的种有希望的方法。形式验证意味着验证过程是数学化的，而不是 如模拟那样，是试验性质的。数学化的验证克服了模拟的不足，因为它对指 定描述中所有可能的输入组合一次进行了验证，而不是仅仅对其一个子集进 行多次试验。 1 3 验证和确认 随着半导体设计技术走向0 1 5 微米以f ，什么才是设计成功的保障呢? 刚刚在百万门级设司中突破o 1 5 微米设计障碍的工程师们己意u 到，许多i c 设计的。基本习惯必须重新构建力能确保在新的设计水平上取得成功。在o 1 5 ；。；。；。；至皇耋垦尘之逛三ll ； 微米以下发汁中，设训人员发现了许多复杂的线路特性，这在过去h 需大致 估计甚至可以忽略不记，但现在设计师必须立即寻找解决方聚以应f - j 一种小 断增加的需求，即在复杂程度增加的同时得到更为准确的设计结果。采用建 立在瓤型建模万式下的新方法和新设计工具，可以在0 1 5 微米及以下的设汁 中得到一致准确的吲序确认( s 堙n o m 。 芯片线路尺寸变小、密度增加后，设计师们要面临一大堆问题，使得获 取准确可靠的时序收敛更加复杂。芯片越小越密导致电容耦合增加，造成在 门延迟中通常起主要作用的线路延迟更加不确定。事实t ：，设计人员发现已 不能再在逻辑设计中消除物理设计的影响，相反却要处理逻辑和实际连线之 间复杂的相互作用。除此以外，随着芯片设计尺寸和布局复杂度增加，还会 引起整个芯片的温度、 电压和功耗发生显著变化，伎芯片设计叉多了一层问 题。 殴汁口确认( v a l i d a l i o n ) m | 是所有系统设计中最重要的任务。设汁确认意 味着确、系统所做的下是它应该做的，爻质f 一是提供了系统运行的可信室。 而验证是对一个被接受的实体( 通常是个高层次描述) 进行检查。在i c 设计中，验证分为两个主要部分：( 1 ) 随明的验证：( 2 ) 实现的验证。 晚明的验证是验证系统设计从一个抽象层次向另一个层次的转换是否l f 确，且两个模型是否。致。实现的验证是要检查在实际限制下，系统在实现 以后能否工作( 检查它是否按设计工作) 。验证与确认不同，确认的目的是证 明它| f 是在按预想的工作。 s o c 的设计确认可以看作是硬件操作的确认、软件操作的确认及软硬件 结台的系统操作的确认。它包括系统级功能和时序性能两方面。 存s o ci 殳训的初期阶段，在进行设计鹾明和r 1 l ( r e s i s t o rt r a n s i s t o r l o g i c ) 编码的同时，要建立行为模型以便为系统仿真建立测试平台。仞期阶 段的目标应该是，在r t l 和功能模型确定之j u ，丌发一系列良好的测试包承1 测试爻例( 包括实向：的软件应用) 。有效的确认要依赖测试向量、测试、 三台的 完整、0 i 同抽象级别的模型、e d a 工具及仿真环境。 发计验证的策略要随设计层；欠而变化。首先检查叶缎的模块( 在核级) 以保证其 1 身是矿确的。在s o c 巾，硬件设汁包括使用核和设汁一些胶接逻 辑( 由j 二致性的原l 玉j ，胶接逻辑可以看作另种核) 。在捡查了这螳核的助 6 嗡1 i 溟lw 人。j ：帧十学位论文 能之后，检查核之恻的接口以保证执行类型和数掘内容的正确。然后，在整 个芯片的模型上运行应用软件或等效的测试平台。因为一些应用项目只能通 过实际执行软件代码来验证，所以需要进行软硬件协同仿真。然后是模拟和 或用a s i c ( a p p 硅c a “o ns p e c i f i ci n t e g r a t e dc i r c u i t ) 或f p g a ( f i e l dp r o g r a m m a b l e g a t e a r r a y ) 实现硬件原型。 表1 1 列出在不同的抽象级上核的设计和在每一级上可用的方法。核的 设计确认包括几个阶段，例如各个予模块的仿真测试、模块接口的验证和通 过运行应用软件完成整个核的确认。在这一过程中使用的基本测试类型是一 致性检测、极端情况测试( 其中包括复杂情况测试和最小最大情况测试) 、 随机测试、实际代码测试( 运行应用软件) 及回归( r e 辱e s s i o n ) 测试。 表1 】不同抽象级别下确、方法列表 拼| 象级别确认方法 核的设计说明用c 、c + + 仿真 行为级h d l系统仿真器、h d l 仿真器 寄存器传输级h d l 仿真器、代码覆盖、形式验证 门绒形式验证、门级仿真、静态时序分析、硬件加速器、仿真器 物理设计 版图一原理图比较( l v s ) 、设计规则检查器( d r c ) 在这一过程中使用的工具包括基于事件的和基于周期的仿真器。基于事 件驰动的仿真器适用于小规模设计和错误调试；基于周期的仿真器适于仿真 大觇模设计，有利于项目管理时觇划仿真时削：其他有用的工具是硬件建模 工具，这个工具在物理芯片和软件、评估系统和硬件原型之阳j 建立接口。通 常，坪估系统比较昂贵，且需要较长的编译时间：硬件原型更加昂贵，但它 可以实时地运行应用软件。 r t l 确认看起来正得到越来越多设计师的支援，这一先进概念是指主流 a s i c 设计师跳过合成和l c ( i n t e g r a t e dc i r c u i t ) 版图设计步骤，直接在r t l 级 确认个设计。r t l 确认得到支援的情沉似乎一直在增加，但e d a 产业这 项意味深远的变革还需依赖新型l 只的丌发，尤其是所谓的能精确估计晶片 实现情沉的矽虚拟原型。 r t l 确认埘l c 实现j ：具供应商米说是个“坏消息”，o a r t n e rd a t a q u e s t 哈尔涯1 样人。j7 坝十宁何论文 公司e d a 分析师g a r ys m i t h 表示。随着设计师转而采用电子系统及设计： 具和r t l 确认，今天的r t l 和实体层设计t 具的销售步伐将逐渐变得缓慢 起来川。 但对矽虚拟原型供应商来说，r t l 确认将是个好消息，这也是m o n t e r e y 设计自动化公司和c a d e n c e 设计系统公司等e d a 供应商最近潜心于这一领域 的一大主要原因。另外，像i b m 微电子和l s il o g i c 公司等a s i c 供应商已 经丌始有选择地采纳r t l 确认这一做法。 1 4 验证方法 1 4 ，1 模拟验证 所谓模拟验 l t ( s i m u l a t i o nv e r i f i c a t i o n ) ，是指对实际数字系统加以抽象， 提取其模型，将其输入计算机。然后将外部激励信号施加于此模型，通过观 察模型在外部激励信号作用下的反应判断陔数字系统是否实现了预期的功 能。 模拟技术是当前数字系统验证的主要手段。它的局限性在于：模拟器的 功能仅是表现在某一组外部激励信号作用下该数字系统的行为，至于加什么 样的外部激励信号以及在该外部激励信号作用下系统反应的正确与否，完全 由设计者自己决定。 142 形式验证 形式验证是不同于模拟方法的对逻辑设计结果的另一种验证方法。 在自顶向f 的设计过程中，在设计的各个阶段和级别，每一级设计都以 上级的设计结果作为设计目标，得到本当哎的设计结果的结构描述，这是改 计或者综合的过程。验证的任务就是保证所得到的结果正确实现其设计要求。 这犟通常包括两个方面： 1 ) 下级所实现的功能与上级的设计目标所要求的功能相致，即 功能验证。 2 1 _ f 一级本身符合设计规则羽l 条佴：制约，包括连接关系的限制、时f f , i 关系的配合等。包括结构验证、h 0 序验证乖i 舰则检查等。 8 。；。；。；垒尘连0 兰量耋些2 筵；i ； 逻辑模拟是验证的一种手段。逻辑模拟的技术已经比较成熟，获得了广 泛的应用。但是，用逻辑模拟来验证逻辑没汁存在着一些难以解决的问题。 逻辑模拟的基本原理是对逻辑设计结果施加定的输入数据( 对门和功 能级的逻辑电路则为一定的输入波形) ，在计算机上模拟执行，得到相应的输 出结果。通过分析其输出结果查找错误，判断设计是否f 确。这罩有三个问 题： 1 ) 输出数据要由用户给出，输入数据的好坏决定了所能查出错误的多 少。 2 ) 输出结果的分析要由有经验的人来进行。 3 ) 由于输出数据难以穷举，尽管能查山许多错误，但不能保证不再存 在错谋。 随着数字系统觇模的扩大，逻辑模拟的缺点变得越来越突出。尤其输入 激励波形的确定本身就是一个复杂的课题。事实上，一个电路设计结果正确 与否，是否具备所期望的功能，仅仅依赖于设计结果的结构。人们希望不要 指定激励波形，不要依赖行为的模拟，丽是根据逻辑设计的功能和结构的描 述来证明逻辑设计的正确性。 形式验证就是这样一种验证方法，它根据逻辑设计的功能和结构捕述 用类似定理证明的方法或数学的方法来证明逻辑设计的f 确性。 逻辑设计的形式验征研究是在7 0 年代中期丌始的。这个时候，逻辑模拟 已广泛用于验证逻辑设计并丌始暴露其问题，同时软件程序正确性证明已 经提出了儿个有效的方法。人们7 - t ：始把软件程序证明的方法用在硬件设计的 - j 叠i f f ：t 。在此之后，由j 。计算机z , i k 的迅猛发展对设计的自动化的需要由 于训算机结构和逻辑体系密切联系，形式验证的研究也随之迅速发展。近年 来，陆续有许多有效的方法问世，并逐步同着实用化方向发展。 一般束晚，形式化验证方法可以分为等价性检验( e q u i v a l e n c ec h e c k i n 9 1 、 模型检班2 ( m o d e lc h e c k i n g ) n 定理证日) ( t h e o r e mp r o v i n g ) 力- 法。等价性检验用柬 对两个电路进行趔辑功能的等价性捡验。等价性检验的基本思想是使用形式 方法，对照设计的规范柬验证它的实现的功能i j 确性f ”l 。 1 1 j 尔j 套i ￥j , q j 砸 _ iv y ：位论父 1 5 形式验证的现状 近十年，j c 技术和j 二艺不断改进，集成度己达几百兆门，芯片频率超过 g h z ，出现了系统芯片s o c ，越来越复杂的系统都可以集成到一个芯片上实 现。i c 线宽已经降到现在的o 1 3 0 1u m ，实验室中f 进行纳米技术的研究， 然而纳米技术在l c 中的实际应用尚需时同。目前国际上的主流线宽是 o 1 8 - 0 1 3um ，我国的丰流线宽是o 3 5 0 2 5pm 。以v d s m 工艺和i p 重用 技术为支撑的s o c 技术是目前超大规模集成电路发展的趋势。s o c 的设计 给e d a 技术带_ i 了新的挑战，迫切要求人们以系统设计的思想解决芯片设 计的问题、解决系统级描述与软硬件协刊设计技术、有效的高层次综合技术、 l p 重用技术、有效的形式验证方法及由v d s m 工艺所带来的一系列关键技 术i ”j 。 复杂系统j 占片体现了复杂丌放系统的特征，需要在设计模型中体现出系 统论的思想，需要揭示出系统整体的一些本质特征，需要体现出逻辑与数学， 时间与空间的统，需要从高层到低层设计的统一的理论模型。目自h ，芯片 设计的不同层次采用不同的结构模型和描述形式，这给高层次描述到低层次 实现( 综合) ，低层次实现结果与高层次描述的等价性检验以及不同抽象层次 的i p 部件描述和重用带来了很大的麻烦，同时也不利于考虑v d s m 效应的 影响。多项式符号代数支持对未赋值的变量表达式的多项式符号运算。运算 对象和过程允许存在非数值的符号变量，体现了任意精度的运算和推理过程。 在多年研究e d a 方法的实践中发现多项式符号代数的形式化模型能够体现 复杂系统的准全启、特性，模型具有从高层到低层设计的统一性，从而可以无 缝地实现各阶段的模型融合，多项式符号代数在系统芯片设计中具有潜在的 研究价值和应用前景。 多年来，在复杂1 c 综合中，实践证明真i f 有效的布尔函数的分解和替换 疗法足代数分解，而不是行尔分解。人们是将逻辑表达式看作代数多项式， 施加一些限制来完成多项式的运算。凼为多项式符号运算具有处理思想相对 简单易实现的优点，且具有形式上的l f 则性。近两年，国外一些学者用多项 ，弋代数方法描述电路行为，用字级( w o r dl c v e l ) 项式模型形式建芦起高层数 抓通路的描述，进行了一螋数掘通路分配和匹配的工作，并于2 0 0 1 年实现了 i “ 个基于符号代数的数据通路的有效综合算法3 i 。他们的r 作表明多项式 表达式能实现电路数据通路行为的紧凑、i i 则、无二义性的形式化描述，而 目在支持数掘通路的单元匹配和部件重用方面很有效，显示出多项式符号代 数存复杂芯片设计领域的应用价值。用统一的字级多项式模型这种f 则形式可 以实现从系统级到位级( b i tl e v e l ) 各个层次的模型描述以及不同抽象层次的 1 p 部件的模型描述，消除系统级综合、高级综合、r t l 综合、逻辑综合的描 述差异，实现一个统一由系统描述到位级描述的、能充分利用i p 部件的融合 各设计层次的综合模型与算法。这种基多项式符号代数的统一的综合模型 报容易，现有综合优化技术结合在起，如优化调度、设计空问搜索、时序 侧整、资源共享技术等。现有的数学觇划方法和基于演化程序的方法都可以 根扼不同情况使用；目前的芯片设计要求设计高层应当考虑各种物理因素 【v d s m 效应) 的影u m 能够进行i p 模块的早期定位和布局规划，并能列 匾连延迟进行预估，而且要求实现低功耗的设计，并在改计前期就考虑芯片 功能与定时行为的可测性设计。通过在多项式符号模型中引入时间参数，建 立起时变多项式符号运算，办可考虑引入功耗、面积等参数扩充多项式符 号运算，建立起考虑v d s m 效应的多目标优化的综合方法。 目盼人们在实践中采用各种形式的b d d ( b i n a r 3 r d e c i s i o nd i a g r a m ) f 4 1 作为 却尔函数的描述和运算工具来解决形式验证问题。虽然在许多电路设计实例 中有效，但是随着输入个数的增加和功能复杂度的增加，b d d 的空间需求指 数上曾加太快，造成组合爆炸问题，大大限制了它的应用。而且b d d 不能量 化比较两个描述的相似或差异程度，致使形式验证到现在也不能有效用在复 杂电路的i 殳计中。 为提高形式验证的效率，近两年人们叉在探寻将模拟与b d d 模型验证 结台在一起进行电路验证的方法，但是效果并不理想i 。而且由于b d d 不能 描述位级以上的功能，对高层次的功能验证无能为力。后来人们又提出了 r o b d d r r e d u c e do r d e r e db d d l ，虽然能在一定程度上减小复杂皮，但并不 能从根本卜解决问题。b m d ( b i n a r ym o m e n td i a g r a m ) 可以用来产生字绂表达 式验征线性电路的复杂功能，但是j 1 在非线性电路中产生指数级的复杂度“。 其它的一些描述工具如h d d l7 】f h 、- b r i dd e c i s i o nd i a g r a m ) 和m t b d d ( m u l t i t e r m i n a l sb d d ) 等也存存描述能力不足或是复杂度太高的问题。 1 】 字级多项式符号模型可以实现由系统高层到低层的适应多设计层次的功 能验i 模型，而且在将位描述转化成亨描述时，随着输入位数的增加，它只 只有多项式的复杂度。虽然随着不连续状态数日的增加浚描述会具有指数复 杂度，但是目前芯片的设计特点是要求强大的信号处理、数掘通信能力、图 像、多媒体处理和运算能力，一般都具有紧凑的代数运算，不连续状态数日 并不人。因此字级多项式符号模型适于目i u 系统芯片的验证。而且多项式模 型i q 以进行误差的定量化控制，可以实现性能、精度和设计周期的折衷。研 制基于多项式符号运算的从系统级到位级的形式验证方法是一个有意义的课 题。 从系统缎描述到位级描述，多项式符弓代数模型可以实现统+ 的描述， 各1 、阶段可以史现无缝的衔接，可以实现适应多设i t 层次的综合与验旺模型， 并能便于考虑性能优化及物理因素，从而实现复杂高速芯片的高性能设汁。 拓展和丰富多项式符号计算理论使用这个数学工具描述和处理l c 设h 自动 化，可以在e d a 领域建立创新的设计模型，提出适应新的设计环境和发展 趋势的新概念、新思路和新方法。 1 6 本文主要工作 本文主要研究了现在e d a 领域的关键技术形式验证，形式验证在电 路设计t 中越来越显示出其重要性。本文重点研究了组合电路的形式验证技术， 蛭主要改进1 + 作如下。 在等价性检验中，一般的验证只有考虑了电路底层的信息，本文把高层 的舰格说明信息用在组合电路的等价性检验中，给出了一种有效的方法。 咆路的多项式表示是。种表示 乜路的行之有效的方法，本文给出了含有 分支电路的多项式表示方法，并把无关项子集考虑在电路的多项表示中，束 弼化多项式阶的求解，在此基础上，给出基于多项式表示的组合电路等价性 验证方法。 随着集成i 乜路规模的扩大，越来越多的复杂设计适合采用基于i p 核的蹬 i h 山于知| i t l ! 产权的保护，包含黑盒的设计验证足 项非常重要的任务。文 献呻i 这方面的方法基本上是基于b d d 心、想的，本文给出了 种基1 ：多项式 表示的特“l ：函数验证方法，r 叮以列包含黑盒的组合电路进行有效的验证= 本文的章节安排如一f ： 第一章是绪论，主要介绍了e d a 的发展阶段，研究形式验汪的意义， 形式验证的发展现状。第二章概述了数字电路形式验证技术，介绍了等价性 检验，模型检验，定理证明，并介绍了目前主要用到的二兀决策图b d d 。第 三章给出了如何把高层信息考虑在等价性检验中，以便简化验证。第四章给 出了禽有分支电路的多项式表示方法，并给出基于电路的多项式表示的组合 电路等价性验征方法。第五章给出了基于特征函数的包含黑盒的组合电路等 价性检验方法，这种力法也是基f 电路的多项表示的，并给出方法的充分 条件。 一；一 坚垒耋! ；垒垒翟i ：兰生：i 兰 第2 章形式验证概述 形式验证是9 0 年代e d a 领域的新技术它根据逻辑设计的功能和结构 描述，建立公理系统用类似定理证明的方法论证逻辑设计的f 确性。成助设 计个复杂数字系统，要求在设计的各个阶段验证实现的诈确性。传统的设 计验证是通过模拟来完成，然而随着电路复杂性的h 益增加，模拟需要花费 大量的c p u 时蚓，在实践中实现穷举的模拟来保证设计的正确性几乎是不列 能的。为了克服模拟的局限性，人们转而求助于各种形式验证方法。使用形 式验i 正方法有可能保证设计在各种可能的输入组合下的正确性。 一股来说，形式化验证方法可以分为等价性检验、模型检验和定理征明 方法。 2 1 模型检验 e mc l a r k e 等人提出的基于一种分支时态逻辑即计算树逻辑 ( c o m p u t i t i o n a lt r e el o g i c ，c t l ) | f i 有限状态十f l ( f i n i t es t a t em a c h i n e ，f s m ) w j 模型检验已经走过了十多年的艰苦历程【3 1 l 。其基本思想是用c t l 公式表达程 序或电路的时序性质，用f s m 表示程序或电路的状态转移的抽象的结构。通 过遍历f s m 来检验时态逻辑公式的币确性。随着程序或电路规模的增大，状 ：盘数目将呈指数增加而引起组合爆炸。它是模型检验的关键性问题。在1 9 8 7 年，利用识别模型中的次要因素及其层次结构的对称性r k u r s h a n 提出了 “同态化简( h o m o m o r p h i cr e d u c t i o n ) ”的方法。其实质是将复杂的数据结构私l 控制序列同念映射到相对简单的数据结构和控制序列，而后者保尉着用于验 讧e 的足够信息，从而减少了计算复杂度。8 0 年代末，又发展了符号模型检验 和二义判定图r b d d ) 技术。符号模型检验的含义是用一个柿尔公式表示使它 满足的所有状态，而这个布尔公式则以压缩方式存储在b d d 中，而存遍历 过程【_ 卜已经标识的状态也用伽尔函数的b d d 表示。通过适当排列变量的顺 序n 以大大筋化图的结构，这使衔模型检验可以处弹大舰模的数据结沟和控 哈自：灏i 丰1 1 i 凡学硕十学似论文 制序列，从而缓和了组合爆炸问题，经过上述的改进，模型检验方法hi u 已 经达到实用化，并为： 业界所接受。模型检验的优点是完全自动化。如果系 统不满足给定的性质，检验结果可以给出反例，从而帮助设计人员找出设计 错误。这一点可能是它的最有吸引力之处。模型检验已彼用于验证大量实际 i 殳计，包括与奔腾处理器的浮点运算单元复杂度相同的s r t 除法算法，并嗣 检查处奔腾处理器的错误。近几年来模型检验的应用急剧扩大，除了硬件设 计之外，还包括i e e e 的标准的验证、各种协议验证、大型通信软件验证。 b e l l 实验室的l u c e n tt e c h n o l o g i e s 在c o s p a n 的基础i 二开发了商用的模型检 验软件f o r m a lc h e c k e r 。掘报道s g i 公司研究超级讨+ 算机c r a y 研究机构已 经定购f o r m a lc h e c k e r 。各大e d al 。家如c a d e n c e 、s y n o p s i s 、v i e w l o g i c 和 m e n t o r g r a p h i c s 等争相把模型睑验商品化：丌发商用的模型检验软件甚至成 为了投资的热点，目前正在集成到至少五个商品化的e d a 工具中去。另外， 模型捡验也可以用于软件验证。