（计算机软件与理论专业论文）基于多项式模型的高层次形式化验证.pdf

哈尔滨1 袢人学颂i “学位沦文 摘要 当今微电子学技术的发展，使得含有数万元件的集成电路已经能够大 批量地生产出来，真正的s o c ( s y s t e mo i lac h i p ) 讵在成为现实。集成电路的 设计能力滞后于集成电路的工艺水平。设计v l s l 中的关键| 、u j 题之一是如何 检查设计的正确性，即设计验证。因为设计验证的复杂度随着芯片的规模呈 指数增加，传统的验证手段，如模拟、测试和仿真技术，对于大型的系统都不是 克全的。由于集成电路工艺的复杂性，它的试制费用相! _ 昂贵。为解决设计 验证这一难题，过去二十年中，人们发展了一种新方法一一形化验证 ( f o r m 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 ) 设计验证的 一种有希望的方法。形式化验_ i l e 意味着验证过程是数学化的，而不是如模拟 技术那样，是试验性质的。数学化的验证克服了模拟的叫i 足，因为它的覆盖 是宠全的，并且叫以减少验证时问。形式化验证刖以对电路描述进行自动化 的验证，减少了验证的复杂度。 本义研究基于多项式符号代数理论的形式化验证方法。关于多项式符号 代数理论在形式化验证方面的研究，人们给出了w g l s ( w e i g h t e dg e n e r a li z e d l is t s ) 和t e d s ( t a y l o re x p a n s i o nd i a g r a m s ) 两个多项式表示模型，并给出 了相应的等价性验证算法。本文的主要工作如下。 i ) 尽f - w ( ；l s 模型，给 l 了高层的数据通路的规格说明j 相应的电路实 现之间的等价性验证算法。出fw g l s 不能应剧于含有布尔变量和字级变量电 路描述的表示，所以给出一个基于w g l s 的新模型l w g l s ( l a b e l e da n d w e f g h t e dg e n e r a i ( z e dl f s t s ) 。l w g l s 可以应用于含有布尔变量和字绒变量 电路描述的表示，并应用于赢层次电路捕述与电路实现或不同的电路。实现之 问的等价性验让。 2 ) 改进了t e d s 的加法和乘法的算法描述，并对算法的复杂度进行分析。 为了对电路的逻辑行为和时序行为进行统一表示，给出了一个基于t e d s 的新 的模型，称为时序泰勒展丁f 图( t i m e dt a y l o re x p a n s i o nd i a g r a m s 。t t e d s ) 。 t t e d s 在保持t e d s 原有的电路表示的规范卜引入了时序信息。 理沦研究和实验结果验汪了文中提出的模型和算法的有效性。 关键词：形式化验证；多项式符号代数：w g 置t e d s 哈尔滨i ：程人学硕十。产何沧文 a b s t r a c t t h em i c r o e l e c t r o n i c s t e c h n o l o g y ，w h i c h c o n t a i nt e n so fm i l l i o n so f c o m p o n e n t so ft h ei n t e g r a t e dc i r c u i t s ( i c ) h a sb e e na b l et os u r v e yt h ep l o t p r o d u c e d ，t h er e a ls o c ( s y s t e mo nac h i p ) i sar e a l i t y t h ea b i l i t yo fi n t e g r a t e d c i r c u i t sf a b r i c a t i o ne x c e e d si t sd e s i g n a t h ec r u c i a lp r o b l e mi nv l s id e s i g n a t i o n i sh o wt oc h e c kt h ed e s i g nc o r r e c t n e s s ，i e d e s i g nv e r i f i c a t i o n b e c a u s eo ft h e c o m p l e x i t yo fd e s i g nv e r i f i c a t i o ni n c r e a s i n ge x p o n e n t i a n l l yw i t ht h es c a l eo fc h i p ， t h ec o m m e r c i a lv e r i f i c a t i o nm a t h o d s ，s u c ha ss i m n l a t i o n ，t e s t i n ga n de m a l a t i o n a r e n o tc o m p ! e t e l yl b rl a r g es c a l es y s t e m t h ec o m p l e x i t yo fi n t e g r a t e dc i r c u i t s t e c h n i c a la r tm a k et h ec o s to ff a b r i c a t i o nf a i r l ye x p a n s i v e i nt h ep a s tt w e n t yy e a r s ， p e o p l eh a sf 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 sah o p e f u lm e t h o df o r t h e d e s i g nv e r i f i c a t i o no fv 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 ep r o c e s so f v e r 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 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 n a ss i m u l a t i o n t e c h n o l o g y w h i c hi s c o n q u e r st h ei n s u f l i c i e a 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 m a a lv e r i f i c a t i o ni st h e a u t o m a t i c a lv e r i f i c a t i o nf o rc i r s u i t sd 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 t h i sp a p e rg i v e st h es t u d yo fp o l y n o m i a ls y m b o l i ca l g e b l a i ct h e o r yi nf o r m a l v e r i f i c a t i o nm e t h o d t h ea p p l i a n c eo fp o l y n o m i a ls y m b o l i ca l g e b r a i ci nf o r m a l v e r i f i c a t i o n ，p e o p l eh a v eg i v e nt w op o l y n a m i a ld e n o t a t i v em o d u l ew g l s ( w e i g h t e dg e n e r a l i z e dl i s t s ) a n dt e d s ( t a y l o re x p a r i s i o nd i a g r a m s ) ，a n dg i v e s t h ec o r r e s p o n d i n ge 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 s t h ei m p o r t a n tw o r ko ft h i s p a p e ra sf o l l o w s 1 ) b a s i n go nw g l sm o d u l e ，t h ee q u i v a l e n c ec h e c k i n gb e t t w e nh i g h l e v e l s p e c i f i c a t i o n sa n di m p l e m e n t a t i o no f c i r c u i t si sg i v e n b e a u s ew g l sc a n tp r e s e n t t h e c i r c u i t s d e s c r i p t i o n s w h i c hc o n t a i nb o o l e nv a r i a b l e sa n d w o r dl e v e l v a r i a b l e s ，t h i sp a p e rp r e s e n t san e wm o d e ll w g l s ( l a b e l e da n d w e i g h t e d g e n e r a l i z e dl i s t s ) b a s i n go nw g l s l w g l sc a np r e s e n tt h e c i r c u i t s ，d e s c r i p t i o n s w h i c hc o n t a i nb o o l e nv a r i a b l e sa n dw o r dl e v e lv a r i a b l e s ，a n dc a nb ea p p l i e dt o 哈尔滨工程大学硕寸：学位论文 v e r i f i c a t i o no fe q u i v a l e n c cp r o p e r t yb e t w e e nt h eh i g h l e v e l ( r t l ) d e s c r i p t i o n so f c i r c u i t sa n dt h ec i r c u i t s i m p l e m e n t so rd i f f e r e n tc i r c u i t s i m p l e m e m s 2 ) t l l i sp a p e rs h o ws o m en e wa l g o r i t h m sf o rt e d sa b o u ta d d i t i o na n d m u l t i p l i t i o n ，a n da n a l y s e st h ec o m p l e x i t i e so fa l g o r i t h m s i no r d e rt op r e s e n tt h e l o g i c a lb e h a v i a la n dt i m i n gi n f o r m a t i o no fc i r c u i t s ，t h i sp a p e rp r e n s e n t sa nn e w m o d u l e ，c a l l e dt i m e dt a y l o re x p a n s i o nd i a g r a m s ( t r e s s ) ，b a s i n g o n t e d s t i e d si sad i r e c te x t e n s i o nt o r e d sw i t ht i m i n gi n f o r m a t i o na n dp r e s e r v e s p r o p r i e t i e so f t e d s 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 d 也ec o n e c t n 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 st h e s i s 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 ls y m b o l i ca l g e b r a i c ；w g l s ； t e d s 1 1 1 哈尔滨工程大学 学位论文原创性声明 本人郑重声明：本论文的所有工作，是在导师的指导 下，由作者本人独立完成的。有关观点、方法、数据和文 献的引用已在文中指出，并与参考文献相对应。除文中己 注明引用的内容外，本论文不包含任何其他个人或集体已 经公开发表的作品成果。对本文的研究做出重要贡献的个 人和集体，均已在文中以明确方式标明。本人完全意识到 本声明的法律结果由本人承担。 作者( 签字) ：互至：玺基。 日期：z 幽绕侔月f 岁同 哈尔滨一l 科人学硕斗：学位论文 1 1e 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 o n ，e d a ) 的发展大致可 分为以下四个阶段“1 。 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 ) ，它是以交互式图形编辑和设计规则检查为特点，那时的逻辑图输入， 逻辑模拟，电路模拟与版图设计及版图验证是分别进行的，人们需要对两者 的结果进行多次的比较和修改才能得到正确的设计，它不能适应较大规模的 设计项目，而且设计周期长，费用高。 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 系统中更重要的是引入了版图和电路图之间的一致 性检查工具和“后模拟”，保证了设计的一次成功率，但是一致性检查和“后 模拟”仍是在设计的最后阶段才实施的，因而一旦发现错误，还需修改版图 或修改电路，仍需付出相当的代价。 进入9 0 年代，芯片设计的高复杂度使得单是依靠原理图输入方式已不堪 承受，采用硬件描述语言的设计方式就应运而生，设计工作从行为、功能级 开始，e d a 向设计的商层次发展，这就出现了第三代e d a 系统，其特点就是 堕玺堡土壁盔堂堡主堂垡堡塞 高层次设计的自动化。”1 。第三代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 dac h i p ) 和v d s m ( v e r yd e e ps u b m i c r o n ) 阶段，诸多新的问题摆在人们面前，这对设计自动化方法提出了新的 要求。 进入9 0 年代中期以后，集成电路发展到大规模、超大规模的水平。每片 门数达到几十万到几百万门，一个完整的电子系统可集成到一个芯片上，这 就是所谓的单片系统、片上系统或系统芯片( 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 j d l 、v e r i l o gh d l ) 混合应用来完成这一工作。在设计方 法上，采用可重用设计技术，其核心是i p ( i n t e l l e c t u a lp r o p e r t y ，知识产 权模块) ，它是一个高性能、可参数化、可综合、可供禊0 试的，用h d l 语言描 述而成，与具体实现工艺无关的“软核”( s o f tc o r e ) 。作为一种独立于工艺 的设计，可嵌入式地应用于各类片上系统中。可重用技术的应用不仅可以大 大缩短芯片的设计周期，而且还可以消除e s d a 与e d a 之间的衔接障碍，促进 e s d a 设计技术迅速发展和成熟起来。 1 2 课题研究的意义 本课题来源于国家自然科学基金项目基于多项式符号代数的系统芯片 d a 新方法研究( 项目编号：6 0 2 7 3 0 8 1 ) 。 2 i i i i i i i i i 高i i i ；i i i i i i i i ；i i ；i i i ；i i i i i 。_ 。 当今微电子学技术的发展，使得含有数千万的集成电路已经篚够大批量 地生成出来，真正的系统芯片( s o c ) 正在成为现实。但是如何正确地设计这些 超大规模集成电路的问题还没有解决。可以说集成电路的制造能力超过了集 成电路的设计能力“1 。为了充分发挥投资惊人的集成电路生产线的生产能力， 需要更多的设计者及时地提供大量复杂的设计。另外，计算机技术和通讯技 图1 1 数字系统自动设计的流程 的高速发展，使得数字系统渗透到整个社会的各个领域，特别是对于安全性 要求极高的很多关键场合，也大量地采用了嵌入式系统；同时各种数字硬件 的设计变得十分复杂，用传统的设计方法已经很难应付，这些都是对电路和 系统设计者的严峻挑战。 在数字系统设计的各个阶段都离不开验证，图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 。因此设计的正 确性验证成为设计的瓶颈，被称为“验证危机”。1 。 在软件设计中也具有类似的问题，即程序的正确性验证问题。在6 0 年代 末兴起的软件验证技术就反映了计算机科学家和数学家为解决“软件危机”， 即软件设计正确性问题所做的努力。他们用数学的理论和方法严格地证明程 序的正确性。这些努力在程序设计方法学方面做出了很大的贡献。然而一般 人认为软件验证技术在工业界的应用基本上是不成功的。8 0 年代初，人们把 类似的方法用来验证硬件，产生了硬件的形式化验证技术。目前普遍认为， 硬件验证技术在工业界的应用前景是十分乐观的。现在可以说，硬件形式化 验证技术的推广应用正在迅速展开。出现这种情况的原因之一是软件和硬件 在复杂度方面具有很大的差别。即使最复杂的硬件，比典型软件的复杂程度 也要小的多。这就使得对于硬件可以有效地应用基于状态空间法的工具如模 型验证程序进行验证。另一个重要的原因是软件验证和硬件验证在本质上具 有不同的特点。软件验证经常需要用户利用自己的知识和经验相当深入地指 导验证过程，但是硬件验证系统可以有效地利用自动状态穷举、语言包含和 符号重写等方法进行自动验证。由于硬件具有比软件更好的模块性，经常可 以把个大规模的验证问题分解为若干孤立的规模较小问题，然后用自动化 工具解决。 事实上，硬件验证理论和方法的研究和应用在近十几年来发展很快，特 别是最近几年，某些方面取得了突破性进展。前几年被认为没有什么前途的 硬件设计的形式化验证技术得到了工业界的普遍认可，特别是模型验证技术， 已经引起了e d a 产业的轰动和商业界的投资热潮。据统计，近几年在全世界 的主要e d a 公司都相继研制和推出了形式化验证软件。人们预料这项技术将 在电子设计领域得到更加广泛的应用。但是在国内，这种情况尚未引起广泛 重视，甚至很多人对于形式化验证感到陌生“1 。 在硬件设计领域，由于集成电路工艺的发展，需要人们设计包含几力门 4 哈尔滨工程人学硕士学位论文 的电路，总的趋势是要把整个系统设计在一个硅片( s o c ) 上。这时，软件和硬 件交织在一起，要进行软硬件协同设计( c o d e s i g n ) ：离散和连续的信息交互 作用，要研究混合系统的设计和验证方法。尽管出现了许多设计自动化工具 和系统，仍然难以保证设计的正确性。例如奔腾5 8 6 芯片中的除法运算错误 是在大量进入市场之后被一位用户发现的，虽然这种错误发生的概率为几亿 分之一，这个设计错误为i n t e l 公司造成四亿八千万美元的经济损失。因而 在硬件设计中为了增加设计正确性的信心和保证，寻求不同于传统的验证方 法是研究形式化方法的强大动力。 为解决设计验证这一难题，过去十多年中，人们发展了一种新方法一 形式化验证( 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 e i n t e g r a t i o n ) 设计验证的一种有希望的方法。形式化验证意味着验证过程是 数学化的，而不是如模拟那样，是试验性质的。数学化的验证克服了模拟的 不足，因为它对指定描述中所有可能的输入组合一次进行了验证，而不是仅 仅对其一个子集进行多次试验。 1 3 验证和确认 随着半导体设计技术走向0 1 5 微米以下，什么才是设计成功的保障呢? 刚刚在百万门级设计中突破0 1 5 微米设计障碍的工程师们已意识到，许多 i c 设计的基本习惯必须重新构建才能确保在新的设计水平上取得成功。在 0 1 5 微米以下设计中，设计人员发现了许多复杂的线路特性，这在过去只需 大致估计甚至可以忽略不记，但现在设计师必须立即寻找解决方案以应付一 种不断增加的需求，即在复杂程度增加的同时得到更为准确的设计结果。采 用建立在新型建模方式下的新方法和新设计工具，可以在0 1 5 微米及以下的 设计中得到一致准确的时序确认( s i g n o f f ) 。 芯片线路尺寸变小、密度增加后，设计师们要面临一大堆问题，使得获 取准确可靠的时序收敛更加复杂。芯片越小越密导致电容耦合增加，造成在 门延迟中通常起主要作用的线路延迟更加不确定。事实上，设计人员发现已 不能再在逻辑设计中消除物理设计的影响，相反却要处理逻辑和实际连线之 间复杂的相互作用。除此以外，随着芯片设计尺寸和布局复杂度增加，还会 哈尔滨j ：程人学硕十学位论文 i i i i i ；i i i i ；暑i i i i ；i i i i i i ；i i i i i i ；高i i i i i i i 罩i i i i i i i i i i i i i i - i i 引起整个芯片的温度、电压和功耗发生显著变化，使芯片设计又多了一层问 题。 设计的确认( v a l i d a t i o n ) 旧是所有系统设计中最重要的任务。设计确认 意味若确认系统所做的正是它应该做的，实质上是提供了系统运行的可信度。 而验证是对一个被接受的实体( 通常是一个高层次描述) 进行检查。在i c 设计中，验证分为两个主要部分：( 1 ) 说明的验证；( 2 ) 实现的验证。 说明的验证是验证系统设计从一个抽象层次向另一个层次的转换是否正 确，且两个模型是否一致。实现的验证是要检查在实际限制下，系统在实现 以后能否工作( 检查它是否按设计工作) 。验证与确认不同，确认的目的是证 明它正是在按预想的工作。 s o c 的设计确认可以看作是硬件操作的确认、软件操作的确认及软硬件 结合的系统操作的确认。它包括系统级功能和时序性能两方面。 在s o c 设计的初期阶段，在进行设计说明和r t 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 和功能模型确定之前，开发一系列良好的测试包和 测试实例( 包括实际的软件应用) 。有效的确认要依赖测试向量、测试平台的 完整、不同抽象级别的模型、e d a 工具及仿真环境。 设计验证的策略要随设计层次而变化。首先检查核级的模块以保证其自 身是正确的。在s o c 中，硬件设计包括使用核和设计一些胶接逻辑( 由于一 致性的原因，胶接逻辑可以看作另一种核) 。在检查了这些核的功能之后，检 查核之间的接口以保证执行类型和数据内容的正确。然后，在整个芯片的模 型上运行应用软件或等效的测试平台。因为一些应用项目只能通过实际执行 软件代码来验证，所以需要进行软硬件协同仿真。然后是模拟或用 a s i c ( a p p l i c a t i o ns p e c i f i c i n t e g r a t e dc i r c u i t ) 或f p g a ( f i e l d p r o g r a m m a b l eg a t ea r r a y ) 实现硬件原型。 表1 i 列出在不同的抽象级上核的设计和在每一级上可用的方法。核的 设计确认包括几个阶段，例如各个子模块的仿真测试、模块接口的验证和通 过运行应用软件完成整个核的确认。在这一过程中使用的基本测试类型是一 致性检测、极端情况测试( 其中包括复杂情况测试和最小最大情况测试) 、 随机测试、实际代码测试( 运行应用软件) 及回归( r e g r e s s i o n ) 测试。 6 哈尔滨二i ：程人学硕士学位论文 表i i 不同抽象级别下确认方法列表 抽象级别确认方法 核的设计说明用c 、c + + 仿真 行为级h d l系统仿真器、h d l 仿真器 寄存器传输级 l i d l 仿真器、代码覆盖、形式化验证 门级 形式验证、门级仿真、静态时序分析、硬件加速器、仿真器 物理设计 版图一原理图比较( l v s ) 、设计规则检查器( d r c ) 在这一过程中使用的工具包括基于事件的和基于周期的仿真器。基于事 件驱动盼仿真器适用于小规模设计和错误调试；基于周期的仿真器适于仿真 大规模设计，有利于项目管理时规划仿真时间。其他有用的工具是硬件建模 工具，这个工具在物理芯片和软件、评估系统和硬件原型之间建立接口。通 常，评估系统比较昂贵，且需要较长的编译时间；硬件原型更加昂贵，但它 可以实时地运行应用软件。 r t l 确认看起来正得到越来越多设计师的支援，这一先进概念是指主流 a s i c 设计师跳过合成和i 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 产业这 项意味深远的变革还需依赖新型工具的开发，尤其是所谓的能精确估计晶片 实现情沉的矽虚拟原型。 r t l 确认对i c 实现工具供应商来说是个“坏消息”，g a r t n e rd a t a q u e s t 公司e d a 分析师g a r ys m i t h 表示。随着设计师转而采用电子系统及设计工具 和r t l 确认，今天的r t l 和实体层设计工具的销售步伐将逐渐变得缓慢起来 【3 哪 但对于虚拟原型供应商来说，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 验证方法 i 4 1 模拟验证 所谓模拟验证( s i m u l a t i o nv e r i f i c a t i o n ) ，是指对实际数字系统加以抽 象，提取其模型，将其输入计算机。然后将外部激励信号旖加于此模型，通 过观察模型在外部激励信号作用下的反应判断该数字系统是否实现了预期的 功能。 模拟技术是当前数字系统验证的主要手段。它的局限性在于：模拟器的 功能仅是表现在某一组外部激励信号作用下该数字系统的行为，至于加什么 样的外部激威信号以及在该外部激励信号作用下系统反应的正确与否，完全 由设计者自己决定。 1 4 2 形式化验证 形式化验证是不同于模拟方法的对逻辑设计结果的另一种验证方法。在 自顶向下的设计过程中，在设计的各个阶段和级别，每一级设计都以上一级 的设计结果作为设计目标，得到本级的设计结果的结构描述，这是设计或者 综合的过程。验证的任务就是保证所得到的结果正确实现其设计要求。这里 通常包括两个方面： 1 ) 下一级所实现的功能与上一级的设计目标所要求的功能相一致，即 功能验证。 2 ) 下一级本身符合设计规则和条件制约，包括连接关系的限制、时间 关系的配合等。包括结构验证、时序验证和规则检查等。 逻辑模拟是验证的一种手段。逻辑模拟的技术已经比较成熟，获得了广 泛的应用。但是，用逻辑模拟来验证逻辑设计存在着一些难以解决的问题。 逻辑模拟的基本原理是对逻辑设计结果施加一定的输入数据( 对门和功 能级的逻辑电路则为一定的输入波形) ，在计算机上模拟执行，得到相应的输 出结果。通过分析其输出结果查找错误，判断设计是否正确。这里有三个问 题： 1 ) 输出数据要由用户给出，输入数据的好坏决定了所能查出错误的多 少。 8 哈尔滨： 程大学硕士学位论文 2 ) 输出结果的分析要由有经验的人来进行。 3 ) 由于输出数据难以穷举，尽管能查出许多错误，但刁i 能保证不再存 在错误。 随着数字系统规模的扩大，逻辑模拟的缺点变得越来越突出。尤其输入 激励波形的确定本身就是一个复杂的课题。事实上，一个电路设计结果正确 与否，是否具备所期望的功能，仅仅依赖于设计结果的结构。人们希望不要 指定激励波形，不要依赖行为的模拟，而是根据逻辑设计的功能和结构的描 述来证明逻辑设计的正确性。 形式化验证就是这样一种验证方法，它根据逻辑设计的功能和结构描述， 用类似定理证明的方法或数学的方法来证明逻辑设计的正确性。 逻辑设计的形式化验证研究是在7 0 年代中期开始的。这个时候，逻辑模 拟已广泛用于验证逻辑设计，并开始暴露其问题，同时软件程序正确性证明 已经提出了几个有效的方法。人们开始把软件程序证明的方法用在硬件设计 的验证上。在此之后，由于计算机工业的迅猛发展对设计的自动化的需要， 由于计算机结构和逻辑体系密切联系，形式化验证的研究也随之迅速发展。 近年来，陆续有许多有效的方法问世，并逐步向着实用化方向发展。 一般来说，形式化验证方法可以分为等价性验证( e q u i v a l e n c e c 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 。 1 5 形式化验证的现状 近十年，i c 技术和工艺不断改进，集成度已达几千万门，芯片频率超过 g h z ，出现了系统芯片s o c ，越来越复杂的系统都可以集成到一个芯片上实现。 i c 线宽已经降到现在的0 1 3 0 1pm ，实验室中正进行纳米技术的研究，然 而纳米技术在i c 中的实际应用尚需时臼。目前国际上的主流线宽是 0 1 8 0 1 3 pm ，我国的主流线宽是0 3 5 0 2 5 u m 。以v d s m 工艺和i p 重用 技术为支撑的s o c 技术是目前超大规模集成电路发展的趋势。s o c 的设计给 e d a 技术带来了新的挑战，迫切要求人们以系统设计的思想解决芯片设计的 9 问题、解决系统级描述与软硬件协同设计技术、有效的高层次综合技术、i p 重用技术、有效的形式化验证方法及由v d s m 工艺所带来的一系列关键技术。 复杂系统芯片体现了复杂开放系统的特征，需要在设计模型中体现出系 统论的思想，需要揭示出系统整体的一些本质特征，需要体现出逻辑与数学， 时间与空间的统一，需要从高层到低层设计的统一的理论模型。目前，芯片 设计的不同层次采用不同的结构模型和描述形式，这给高层次描述到低层次 实现( 综合) ，低层次实现结果与高层次描述的等价性验证以及不同抽象层次 的i p 部件描述和重用带来了很大的麻烦，同时也不利于考虑v d s m 效应的影 响。多项式符号代数支持对未赋值的变量表达式的多项式符号运算。运算对 象和过程允许存在非数值的符号变量，体现了任意精度的运算和推理过程。 在多年研究e d a 方法的实践中发现多项式符号代数的形式化模型能够体现复 杂系统的准全息特性，模型具有从高层到低层设计的统一性，从而可以无缝 地实现各阶段的模型融合，多项式符号代数在系统芯片设计中具有潜在的研 究价值和应用前景。 多年来，在复杂i c 综合中，实践证明真正有效的布尔函数的分解和替换 方法是代数分解，而不是布尔分解。人们是将逻辑表达式看作代数多项式， 施加一些限制来完成多项式的运算。因为多项式符号运算具有处理恩想相对 简单易实现的优点，且具有形式上的规范性。近两年，国外一些学者用多项 式代数方法描述电路行为，用字级( w o r dl e v e l ) 多项式模型形式建立起高层 数据通路的描述，进行了一些数据通路分配和匹配的工作，并于2 0 0 1 年实现 了一个基于符号代数的数据通路的有效综合算法“。他们的工作表明多项 式表达式能实现电路数据通路行为的紧凑、正则、无二义性的形式化描述， 而且在支持数据通路的单元匹配和部件重用方面很有效，显示出多项式符号 代数在复杂芯片设计领域的应用价值。用统一的字级多项式模型这种正则形式 可以实现从系统级到位级( b i tl e v e l ) 各个层次的模型描述以及不同抽象层 次的i p 部件的模型描述，消除系统级综合、高级综合、r t l 综合、逻辑综合 的描述差异，实现一个统一由系统描述到位级描述的、能充分利用i p 部件的 融合各设计层次的综合模型与算法。这种基于多项式符号代数的统一的综合 模型很容易与现有综合优化技术结合在一起，如优化调度、设计空间搜索、 时序凋整、资源共享技术等。现有的数学规划方法和基于演化程序的方法都 1 0 啥尔滨工捌犬学硕士学位论文 可以根据不同情况使用。目前的芯片设计要求设计高层应当考虑各种物理因 素( v d s m 效应) 的影响，能够进行i p 模块的早期定位和布局规划，并能对 互连延迟进行预估，而且要求实现低功耗的设计，并在设计前期就考虑芯片 功能与定时行为的可测性设计。通过在多项式符号模型中引入时间参数，建 立起时变多项式符号运算，亦可考虑引入功耗、面积等参数，扩充多项式符 号运算，建立起考虑v d s m 效应的多目标优化的综合方法。 目前人们在实践中采用各种形式的b d d ( b i n a r yd e e i s i o nd i a g r a m ) 啪作 为布尔函数的描述和运算工具来解决形式化验证问题。虽然在许多电路设计 实例中有效，但是随着输入个数的增加和功能复杂度的增加，b d d 的空间需 求指数增加太快，造成组合爆炸问题，大大限制了它的应用。而且b d d 不能 量化比较两个描述的相似或差异程度，致使形式化验证到现在也不能有效用 在复杂电路的设计中。 为提高形式化验证的效率，近两年人们又在探寻将模拟与b d d 模型验证 结合在一起进行电路验证的方法，但是效果并不理想“”。而且由于b d d 不能 描述位级以上的功能，对高层次的功能验证无能为力。后来人们又提出了 r o b d d ( r e d u c e do r d e r e db d d ) ，虽然能在一定程度上减小复杂度，但并不能 从根本上解决问题。b m d ( b i n a r ym o m e n td i a g r a m ) 可以用来产生字级表达式 验证线性电路的复杂功能，但是用在非线性电路中产生指数级的复杂度”1 。 其它的一些描述工具如固扩1 ( h y 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 ) 等也存在描述能力不足或是复杂度太高的问题。 字缀多项式符号模型可以实现由系统高层到低层的适应多设计层次的功 能验证模型，而且在将位描述转化成字描述时，随着输入位数的增加，它只 具有多项式的复杂度。虽然随着不连续状态数目的增加该描述会具有指数复 杂度，但是目前芯片的设计特点是要求强大的信号处理、数据通信能力、图 像、多媒体处理和运算能力，一般都具有紧凑的代数运算，不连续状态数目 并不大。因此字级多项式符号模型适于目前系统芯片的验证。而且多项式模 型可以进行误差的定量化控制，可以实现性能、精度和设计周期的折衷。研 制基于多项式符号运算的从系统级到位级的形式化验证方法是一个有意义的 课题。 从系统级描述到位级描述，多项式符号代数模型可以实现统一的描述， 各个阶段可以实现无缝的衔接，可以实现适应多设计层次的综合与验证模型， 并能便于考虑性能优化及物理因素，从而实现复杂高速芯片的高性能设计。 拓展和丰富多项式符号计算理论，使用这个数学工具描述和处理i c 设计自动 化，可以在e d a 领域建立创新的设计模型，提出适应新的设计环境和发展趋 势的新概念、新思路和新方法。 1 6 本文主要工作 本文研究了现在e d a 领域的关键技术形式化验证，形式化验证在电 路设计中越来越显示出其重要性。多项式符号代数理论在形式化验证方面的 应用进行了深入地研究。主要工作方面如下： 1 ) 基于w g l s “模型，给出了高层的数据通路的规格说明之间的等价性 验证算法，以及高层次描述与相应的电路实现的等价性验证算法。给出一个 完整的数据通路操作的指令集，能够在基于w g l s 的模型下进行等价性验证， 允许直接地把电路的h d l 描述转化为w g l s 。给出基于w g l s 的模运算和除法 运算的表示方法，但仅限于模2 6 和除2 “运算。这些操作是有效验证过程的核 心操作。通过对十进b c d 码与二进制之间相互转换的换器的验证来显示不同 的组件如何组合并实现了对此电路进行了自动验证。 2 ) 对w g l s 模型进行拓展，使其能够对含有字级和字节级变量的混合描 述进行表示，从而实现对含有字级和字节级变量的电路描述与具体实现之间 进行等价性验证。在高层次的描述中可以包含字级变量和字节级变量，新的 模型能够实现对上述情况的电路进行有效的表示。 3 ) 对泰勒展开图( t e d s ) “加法和乘法的算法进行改进，近而减少复杂 度，完全克服了由边权值的传播所引起的算法的指数复杂度。算法应用了函 数表达式的符号性质，通过运用m a p l e 求得两个函数的t e d s 之间操作的结果。 运用符号运算系统，从而减小了运算的复杂度。 4 ) 在t e d s 的基础上进行拓展，引入时序信息，称之为t t e d s ( t i m e d t a y l o re x p a n s i o nd i a g r a m s ) 。在保持t e d s 原有的规范基础上，t t e d s 给出 了带有时序信息的算术函数和布尔函数的统一的符号表示和操作。在t t e d s 中，为每一个节点给出个权值来表示时序信息，如同t b d d “”。并为每一条 1 2 哈尔滨j 二程人学硕士学位论文 边增加一个新的权值