（微电子学与固体电子学专业论文）基于断言的功能验证方法研究.pdf

摘要 摘要 目前我们采取的基于受限随机矢量生成机制的验证方法流程，是系统根据设计人员所规定的约 束条件生成外部激励并输入到待验证模块，然后根据输出结果分析功能正确性。这种方法的优点是 可以方便的覆盖巨大的验证空间；通过多次输入不同的激励，可以逐步覆盖边缘情况。然而实际应 用中，这种方法依然存在着一些不足：例如仅仅分析仿真波形，无法快速定位设计错误；时间开销 较大，验证周期过长；边缘情况的覆盖比较困难，需要不断地修正约束激励：产生的激励冗余度过 大，验证时间过长等等。 针对目前验证流稃中的不足，本文主要研究了基于断言验证方法的实现。基于断言的验证方法 是目前验证方法学上的新趋势，它的优点在于：能够增加验证过程的可观察性和可控制性；在设计 周期中能更早的发现设计缺陷，促进错误的诊断；可以减少多余仿真周期，降低设计错误不被发现 的风险；断言模块有很强的独立性，可以与设计模块很好的分开，可重用性强，验证效率较高；支 持第三方的模块；能更好的利_ i j 形式以及半形式验证。 本文首先介绍了当前主流的功能验证方法，分析了目前验证流稃中所存在的不足和困难，针对 目前存在的困难提出基于断言的验证方法。用断言验证的长处弥补随机矢量验证的不足，增强验证 的可观测性和可控性；通过断言库的建设，提高了验证环境的可重用性。随后本文进一步分析了几 种主要断言验证语言的优缺点，通过比较决定采用s y s e m v e d l o ga s s e r t i o n 作为研究- t 具。分析了利 h j 它实现验证环境的构建的具体过程。针对g a r f i e l d 芯片中的a h b 模块l c d c ( 液晶显示控制器) 和a p b 模块s d ( 安全数码p 控制器) ，本文分别构建了不同的验证环境。根据两者各自的特点，添 加了新的断言监视器。为了提高插入断言的效率，本文采用了一种自动插入断言的接口，对自动插 入断言的要求提出了具体的规范，并且利用p e r l 实现了这一接口。利用断言插入程序可以方便高效 地实现断言的自动插入。 最后本文对验让的结果进行了分析，并对设计工作指出了改进的要点。通过分析总结实验数据， 指出利用断言验证的方法比原来单纯利用受限随机矢晕的验证方法人大缩短了验证时间，目前最多 可比原来方法节约时间7 1 2 4 。 关键词：功能验证断言验证自动插入接口可重用性 东南大学顾士论文 a b s t r a c t a sas o c g a r f i e l dh a ss o l mt y p i c a lc h a r a c t e r s ni sb a s e do na m b ap r o t o c o l sa n dt h e r ea r om a n y f u n c t i o n a lm o d e l si ng a r f i e l dc h i p t h e s ec h a r a c t e r sb r i n gm a n yc h a l l e n g e s f u n c t i o n a lv e r i f i c a t i o ni so i l e o ft h ec h a l l e n g e s i th a sb e c o m eam a j o rb o t t l e n e c ki nt h ei cd e s i g np r o c e s s n em o s td i f f i c u l t i e so f i c f u n c t i o n a lv e r i f i c a t i o na r ea sf o l l o w s ：t h eb u i l d i n go ft e s t b e n c h ，t h er e u s a b i l i t yo fv e r i f i c a t i o ne n v i r o n m e n t 。 t h eo b s e r v a b i l i t ya n dt h ec o n t r o l l a b i l i t yo fv e r i f i c a t i o np r o c e s s c u r r e n t l y , w eu s et h ec o n s t r a i n t - r a n d o mm e t h o dt ov e i l f vo u rf u n c t i o n a lm o d e l n ev e r i f i c a t i o ne n g i n e e r s m a k et h ec o n s t r a i n ta c c o r d i n gt ot h es y s t e ms p e c i f i c a t i o n ，i n p u tt h es t i m u l u st od u va n dc h e c kt h er e s u l t i nt h eo u t p u lt h ea d v a n t a g eo ft h i sm e t h o di st h a ts t i m u l u sc o u l db eg e n e r a t e de a s i l ya n dq u i c k l y h o w e v e r , t h e ma r es t i l ls o m es h u t o u t si nt h i sm e t h o d ：c o s t i n gs i m u l a t i o nt i m e s f i n d i n gb u g se f f e c t i v e l e s s l y a n dp o o ro b s e r v a l i l i t y s ow ei n t r o d u c et h ea s s e r t i o nb a s e dv e r i f i c a t i o nt oi m p r o v eo u rw o r km e t h o d f i r s t l y , w ei n t r o d u c et h e p r i m a r yf u n c t i o n a lv e r i f i c a t i o nm e t h o d sa n da n a l y s et h ea d v a n t a g e sa n dd i s a d e v a n t a g a so ft h e s em e t h o d s s e c o n d l yw ed i s c u s st h ep r o c e s so fa s s e r t i o nb a s e dv e r i f i c a t i o ni nd e t a i l a saf r e s hm e t h o d m a n y o r g a n i z a t i o n sa n dc o r p sd e v e l o p e dl a n g u a g e st os u p p o r ti t i nt h i sp a p e r , w eu s et h es y s t e m v e r i l o g a s s e r t i o nt oi m p l e m e n ti tb e c a u s eo fi t sc o n v e n i e n c ea n du s e f u l n e s s t h e nw eu s et h ec o n s t r a i n t - r a n d o m m e t h o da n da s s e r t i o nb a s e dm e t h o dt o g e t h e rt ov e r i f yt h eg a r f i e l dc h i p t h r o u g ht h i sw a y , w em a k et h e v e r i f i c a t i o ne n v i r o n m e n tm o r er e n s 曲l e t h eo b s e r v a b i l i t ya n dt h ec o n t r o l l a b i l i t yh a v er e s t r i c t e dt h e e f f i c i e n c yo ff u n c t i o n a lv e r i f i c a t i o n t oi m p r o v i n gt h ev e r i f i c a t i o ns p e e l i ，w ei n t r o d u c eaa u t o - a s s e r t i o n i n t e r f a c ea n dt h ea s s e r t i o nm o n i t o r sc o u l db ea d d e di nr t lc o d i n g sa u t o m a t i c a l l y t h ea u t o - a s s e r t i o n i n t e r f a c es p e e d su pt h ew h o l ev e r i f i c a t i o np r o c e s s f i n a l l yw er e c o r dt h ev e r i f i c a t i o nr e s u l t sa n da n l y s et h eb u g sa n dv e r i f i c a t i o nt i m e s i ts h o w st h a tm a n y b u g sa g ef o u n db yu s i n gt h ec o n b i n e dm e t h o dt h i sp a p e rd i s c u s s e d i ta l s os h o w st h a to u rm e t h o di sq u i t e s a v et i m ei nt h ei cd e s i g nf l o w k e yw o r d s ：f u n c t i o n a lv e r i l f i c a t i o n ；a s s e r t i o nb a s e dv e r i f i c a t i o n ；a u t o - a s s e r ti n t e r f a c e ；r e u s a b i l i t y 学位论文独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究 成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发 表或撰写过的研究成果，也不包含为获得东南大学或其它教育机构的学位或证书而使用 过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明 并表示了谢意。 研究生签名：蔓翌兰坠日期：三生兰兰 关于学位论文使用授权的说明 东南大学、中国科学技术信息研究所、国家图书馆有权保留本人所送交学位论文的 复印件和电子文档，可以采用影印、缩印或其他复制手段保存论文。本人电子文档的内 容和纸质论文的内容相一致。除在保密期内的保密论文外，允许论文被查阅和借阅，可 以公布( 包括刊登) 论文的全部或部分内容。论文的公布( 包括刊登) 授权东南大学研 究生院办理。 研究生签名：吾堑! b 师签名：- 二邀日 期： 第一章绪论 1 1 课题的研究背景 第一章绪论 随着集成电路制造工艺不断进步，芯片的生产能力正在不断地提高，设计能力已经落后于生产 能力，并且两者见的著距仍在逐步加丈( 见图1 1 ) 与此同时，单个芯片上的集成度不断提高， t _ ”雄l 螂 脚4 御 ， 图1 一l 设计能力与制造能力间的差距 数字系统的功能也变得越来越复杂，使得功能验证工作变得日益凼难。目前的芯片开发小组中，功 能验证所消耗的资 ! 泉已占整个开发资源的7 0 甚至9 0 ，其中r t l 级的验证t 作约占箍个验证开销 的5 2 ，因此，r t l 级及高层验证已经成为整个设计过程的瓶颈，并存在于设计流程的各个层次1 2 3 ； 从图i 2 可以看到设计缝隙和验让缝隙正逐步扩大并且验让缝隙比设计缝隙还要巨大，验证方法已 经远远落后于设计和生产能力。i c a s i cd e s i g nt e a m si nn o r t ha m e r i c a 针对i c a s i c 功能性验 证的研究报告显示，目前i c 设计上的错误主要仍来自设计本身，大约5 0 以上的芯片需要超过一 次以上的r e - s p i n s ( 重制) 对这些r e - s p i n s 的芯片进行分析，会发现年大约有7 1 的错误原因是 来自于自身的功能实现( 2 0 0 1 年数据) ；剑了2 0 0 3 年逻辑功能错误导致重新流片的比例达到了7 5 ， 请参考图1 3 1 5 1 。 图1 2 验证的能力远远不能满足设计和市场的需求( b r i a nb a i l e ym e n t o rg r a p h i c sc o r p o r a t i o n ) 东南大学颀士论史 这就更体现了现今对于良好功能性验证的迫切需要所以随着设计越来越复杂，我们的确1 f 常迫切 需要一种更好的验证方法。 事实上，设计验证应当和系统定义是同步的，验证计划是系统定义的一个组成部分，系统设计 图1 3c o l l e t ti n t e r n a t i o n a l2 0 0 3 规范决定了验证策略。图i 一4 表明了s o c 设计中的验证方法学，指出在s o c 设计的各个阶段的验 证工作嘲。 图1 4 s o c 设计中的验证流程 2 第一章绪论 可以看出，s o c 设计中包括多个层次的验证。系统定义规定需要的时钟频率、输入输出时序、 面积、功耗、各个子模块功能的划分等；系统级验证主要验证系统功能、评估各种设计方案，从而 对系统结构进行最优化分析。硬件描述语言( h a r d w a r ed e s c r i p t i l a n g u a g e ，即h d l ) 描述系统行 为；功能验证则主要验证r t l 代码功能的正确性，本文将重点讨论功能验证的有关问题( 下文提剑 的验让若不加特别声明，都将指功能验证) 。在此之后，由综合工具将h d l 描述转换为j 级网表； 网表验证确保由r t l 代码综合得剑的i j 级网表和r t l 代码在逻辑上是一致的。最后在布局、布线 完成后还要进行物理验证，确保没有物理设计错误，主要包括d r c ( 设计规则检查) 、l v s ( 原理 图与版图检查) 等。 1 2 功能验证的重要性 在逻辑设计阶段，如果没有进行充分的功能验证，设计中存在的逻辑性错误就很难在后面的物 理设计阶段被发现，而只能在流片之后才会被测试出来，这就导致设计成本的攀升和芯片上市时间 ( t i m e - t o - m a r k e t ) 的延迟。从成本和上市时间的角度来考虑，通过功能验证发现逻辑性错误在整个 设计流稃中至关重要。在整个设计流程中设计错误发现得越晚，用于修改错误的代价就越高。在规 划阶段修改错误只需修正设计方案，其代价是稍微延迟芯片开发进程，而对开发费用几乎没有影响； 而在芯片级或系统级发现设计错误，用于修改错误的代价会人幅提高：需要更多的错误隔离时间、 更复杂的纠错过程，严重时甚至需要系统设计人员重新设计芯片的实现算法，从而严重影响芯片开 发进度；在客户端发现设计错误，后果是灾难性的，可能要重新设计芯片，同时还会给芯片生产商 的信誉带来负砸影响。 1 3s o c 设计中的验证方法和困难 为什么验证一个系统的正确性会如此困难呢? 让我们首先来了解一下主要的验证方法。 我们这里主要讨论的是功能验证。功能验证就是核实设计单元和设计规范在功能上的一致性， 它主要验证硬件的h d l 描述是否符合设计的功能描述。目前，功能验证大体上分为静态功能验证 和动态功能验证，分别有如f 几种比较主流的方法： 静态功能验证是指通过数学方法检查所实现的设计是否满足某些属性，从而证明实现的设计和 设计规范是否一致的验证方法”m 。目前，静态功能验证的主要手段是形式验证。 形式化验证方法使_ h j 数学方法形式化地证明设计实现部分或全部满足系统描述要求，形式验证 的优势不仅在于不需要写任何测试矢罩，更重要的是它能保证达到1 0 0 的覆盖率。但是它也存在着 明显的缺点，它在容量、应用范同以及对硬件环境方面的苛刻要求使它不适官进行系统级的功能验 证1 9 1 。目前，形式验证主要应用丁模块级和i 单元级设计的功能验证，它主要包括：等价性验证、模 型检验、定理证明以及符号轨迹求解等方法。 等价性验证( e q u i v a l e n c ec h e c k i n g ) 用于比较设计的两种实现是否一致，验证两个结构的描述等 价或着通过数学证明的方法来证明两者逻辑上的等价性。它一般用来证明r t l 和i j 级网表的一致性 ”，图1 5 是等价证明的示意图。该方法又可分为组合等价性检查( c o m b i n a t i o n a le q u i v a l e n c e c h e c k i n g ) 和时序等价性检杏( s e q u e n t i a le q u i v a l e n c ec h e c k i n g ) ，组合等价性检查的目的是检卉两个组 合电路在给定的输入下是否等价。时序等价性检查应用包括：比较r t l 级设计在综合前后的等价性； 检查逻辑级设计及其版图实现间的等价性；对设计进行性能优化前后电路的等价性证明等。时序等 价性检壳的问题是需要一个参考模璀作为描述，而设计参考模犁也是一个很重的任务。 模型检测( m o d e lc h e c k i n g ) 是指根据设计规范建立具有一般性特征的模型，通过形式上的检查来 证明模型特祉的止确与否。它通常应用在设计的高级阶段，用来检查具有普遍性的问题，同时验证 3 东南丈学颤士论义 设计人员的设计行为是否违规1 1 2 1 ，这种形式验证方法目前很不成熟，具体表现在：从设计规范 综合 等价形式验证 表 圈i 5 等价性证明图示 中提取特征从而检查这些特征需要很高的技巧和深厚的数学功底，缺少成熟工具的支持。 设计规范 r t l 编码 属性 图1 6 模犁检查示意图 定理证明( t h e o r e mp r o v i n g ) 用形式逻辑同时去描述设计的实现和设计规范，然后用理论证明的 方法来验证两者在逻辑上的相关性和相似性。在定理证明中，系统及其需满足的属性都用数理逻辑 的形式化语言描述。一个形式化描述的系统包括一组公理莆i 演绎规! l ! i i 。这是形式验证方法学中发展 最甲的一个方法，该方法需要一个设计行为的形式化描述”“。通过严格的数学证明，比较h d l 描 述的设计和系统的形式化描述在所有可能输入下是否一致。这种方法存在的问题是，通常h d l 描 述就是第一个形式化描述，即便有一个更高层次的形式化描述，还需要保证该描述的正确性，才能 和h d l 描述进行一致性比较。形式化描述和h d l 描述的致性证明很难进行，推演出这些形式的 原璋l 和证点非常繁琐。通常需要假设很多条件，以简化比较证明，而要证明这些假设本身也是很凼 难的 1 4 】。另一个土要问题是不能完全自动化。其优点是形式的证点可以机械地检查，目前它还只是 在学术上进行研究。 动态功能验证主要指仿真。 仿真是通过对d u v ( d e s i g nu n d e rv e r i f i c a t i o n ，待验证的设计) 施加测试矢量，然后检查其行 为是否按照设计规范运作。仿真是目前功能验证的主要手段。这种方法的优点是简单、易操作、适 用范嗣比较广且不受设计规模的影响。但它也有明显的缺点：难以开发出完全彻底的测试案例，特 别是一些边缘测试案例；难以分析，判断它的功能覆盖率和测试的完备性；一些未被定义的行为可 能会被当作设计错误报告出来：检查丁二作局限在一些给定的范围之内。 基于断言的验证是仿真的一个新发展，它是通过在r t l 代码中插入断言语句，然后在动态仿真 4 第一章绪论 的过程中由这些断言语句来判断实现的设计是否跟设计的规范相一致“，j 。使j j 基于断言的验证方法 的优点是：验证人员能够很好地理解实现的设计；能够精确定位设计中出现错误的位置。但是，使 用基于断言的验证方法首先需要学会一种基于断言的验证语言，用它来描述d u v 的预期应发生以 及不应发生的行为采用基于断言的验证方法是i c 设计的新趋势“o j 。 以上介磐f 了目前使用的一些功能验证方法。在这些方法中，形式验证技术能解决验证完备性问 题，但在较小规模的设计上才能达到速度要求，还不能应用于大规模的设计，特别是功能复朵的s o c 芯片。动态功能验证方法依然是i c 设计的主要验证技术。它将激励信号施加于设计，进行计算并观 察输出结果，并判断该结果是否与预期一致其主要缺点是非完备性，即只能证明有错而不能让明 无错。另外它还依赖丁测试向争的选取，而合理而充分地选取测试向量，达到高覆盖率是一个十分 艰巨的课题。由丁二设计者不能预测所有错误的可能模式，所以尚未发现某个最好的覆盖率度鼍。即 使选定了某个覆盖率度量，验证时间也是一个瓶径。需要指出的是，在实际功能验证过程中，以上 介纠的任何一种验证方法都不可能解决验证过干旱中遇到的所有问题，必须综合使用各种手段加速验 证工作的进度，提高验证工作的质量。 通过上面分析目前的设计、验证形势然后结合当前的验证能力和验证方法，回答为什么验证问 题如此之难就比较容易理解了。困难来自于以f 几个方面： 系统复杂度的不断增大。一直在遵循m o o r e 定律的i c 制造技术使得设计者在单个芯片上集成 了更多的m 核、内存、总线等，构成非常复杂的系统。与此鲜明对照，验证技术的发展落后于i c 制造能力。这使现有的验证工具越来越不能胜任验让需求。对于功能验证，发现隐含错误本来就是 它的弱项，而系统越复杂，隐含错误就越多。 上市时间的不断缩短。目前电子产品的更新换代之快反映了对设计周期不断缩短的市场竞争要 求。验证过稃所耗费的时间一般占总设计周期的三分之二，甚至达到8 0 以上。冈此，对验证的合 理要求就是：尽草提高速度以溶入设计流程中。尤其在设计甲期，在高层次发现设计错误，可以极 大地降低设计返j 二的成本。 单一的验证都有各自的缺陷。形式验证往往局限丁理论，实际应用时存在建模困难，系统开销 巨大等问题；而功能验证义存在着c o r l l e rc a s e ( 边缘怙况) 完全覆盖困难，找到的错误无法快速定 位等问题。 这就要求我们一方面要设计出性能优异，功能强大的芯片，另一方面又要努力缩短设计和验证 的时间，而这两者在现实中往往是矛盾的。为此我们必须要在设计和验证方法上不断地加以改进， 以缓和矛盾，尽量满足上述的要求。 1 4 本课题研究的主要内容和论文结构 本课题的主要研究内容是i c 设计中的功能验证，以传统的基于仿真的验证方法为基础，针对其 存在的缺点，提出一种能够提高验证质阜和效率的验证方案从而进一步地解决j 二程上的验证问题。 以g a r f i e l d 芯片中的l c d c 和s d 模块为例，详细讨论采用这种方案进行模块级功能验证的方法和 侧重点。 本文的论题基于s y s t e m v e r i l o g a s s e r t i o n 的功能验证。本文共分为五章：第一章是绪论。第 二章介纠断言验证技术以及s y s t e m v e d l o g a s s e r t i o n 的实现结构。第三章研究验证环境中断言的具体 实现以及如何实现自动添加断言的接口。第四章研究可重用验证环境的构建以及具体实验数据分析。 第五章对全文总结并对后续验证工作提出规划性建议。 5 东南大学硕士论文 第二章断言验证技术 由于编写能把设计错误传播到输出端口的向晕具有较大难度，本章在分析这个问题的基础上， 提出使用断言验让技术来解决这个问题，然后简要论述断言验证技术，最后对主流的几种断言验证 进行比较，确定以s v a 为论文的研究方向。 2 1 断言验证技术及影响 所亨( a s s e r t i o n ) 用来对设计对象的属性特性或行为特性进行描述。它并不是一个全新的概念， 在软件设计中断言早已得到了广泛的应用。它的最早的使坩，也许可以追溯到1 9 4 9 年 l u r i n g 在高 速自动记算机器( h i g hs p e e da u t o m a t i cc a l c u l a t i n gm a c h i n e s ) 会议论文所提及的一段叙述1 。见图 2 一l 。因此断言最简单的解释，就是一种检查器( c h e c k e r ) 、一种监视器( m o n i t o r ) ；更确切的来说， 断言是一段叙述，用米描述被预期的特定性质( p r o p e r t y ) 在v e f i l o g 代码验证中，也存在着基丁二断 言思想的验证方法，其目的也是尽可能快的找出硬件设计中的缺陷。 i no r d e rt h a tt h em a l lw h oc h e c k sm a yn o th a v et o od i f f i c u l tat a s k ，t h ep r o g r a m m e rs h o u l dm a k e an u m b e ro fd e f i n i t ea s s e r t i o n sw h i c hc a l lb ec h e c k e di n d i v i d u a l l y ，a n df r o mw h i c ht h ec o r r e c t n e s s o ft h ew h o l ep r o g r a me a s i l yf l o w s a l a nt u r i n g 图2 一l t u r i n g 在其会议论文c h e c k i n gala r g er o u t i n e 里对断言所作的叙述 硬件设计的断言可用很多方式来描述，包括埘传统的硬件描述语言，甚至v h d l 里也有关键字 a s s e r l 。硬件的断言包括只检查单一事件j 以及r 多个事件所组成的情况j ，后者就是去检查一段 时间内的硬件行为。比如说检查一个队列( q u e u e ) 是否溢出( 如图2 2 ) ，是只检查单一事件；而 检查g r a n t 信号总是发生在r e q u e s t 信号发出之后的数个时钟周期之内，则属于检查一段时间内的硬 件行为。而更广泛的来说，断言也可以是设计的约束( e o n s t r a i n 0 ，合成_ i ：具可以透过这样的设计约 束来实现符合设计者预期的结果，如s y n o p s y s 合成器常用的“f u l l _ c a s c ”与“p a r a l l e l _ c a s e ”等 图2 2 断言在v e r i l o g 里的例子：检查q u e u e 是否o v e r f l o w 断言的插入点可以被认为具有和软件内部测试点类似的概念，它在验证过稗中不停地监视着设 计的预期行为，并且不断的为设计工稃师和验证工群师提供各种相关信息。例如当在某一个插入点 存在设计缺陷时，相关的缺陷报告就会被打印出来。通过这种验证方法，设计j 二程师和验证上稃师 可以节省大晕的时间和精力。使用传统的基于仿真的验证方法时，验证工拌师必须手1 编写测试向 量，并且要花费大茸时间精力来思考什么样的测试向量才会使设计内部的错误能传播到输出端口上。 仿真完成后，分析波形和日志文件也是一个费时费力的过程。这种方法的验证效率低下，而且往往 不能找出设计的内部缺陷。断言验证方法可以作为传统验证的有效补充，改善了传统验证方法中的 6 第一章断自验计技术 很多问题，具体优点描述如下： 1 断言改善了传统验让方法的验证质量 仿真验证方法的仿真j ：作通常在芯片级进行，模块级的仿真有很多的限制。因此，很多的设 计缺陷是在项目设计的最后阶段才被发现，并且很难确定这些缺陷的位置。在模块级的代码 开发时，就在h d l 代码中插入断言，不仅可以减少设计人员手工编写模块级测试向龟的工 作量，而且可以在项目进程的早期就开始验证j 二作，有助于较早的发现设计错误。 2 断言验证提高了设计的可观察性和可控性 使用仿真验证查找设计错误时，必须通过分析波形和日志文件，来检查设计中是否存在错误 而断言验证需要了解设计模块的实现结构，当断言监视到设计中有违反断言描述的行为特性 时，它就会报告出设计缺陷的相关信息，大大提高了设计的可观察性。内嵌在硬件描述语言 里的断言，不但可以用来增加可观察性( o b s e r v a b i l i t y ) 以方便侦测错误，还可以用来表达设 计者的设计意图与叙述设计里的要点。而当整合多个模块时，断言也可以_ j 来隔绝与抓住问 题的所在。 表2 1 是d e c ( d i g i t a le q u i p m e n tc o r p o r a t i o n ) 在d e ca l p h a2 1 2 6 4 微处理器设计里使用的各种 错误侦测机制所找剑错误的比例。由该表可知断言检查器( a s s e r t i o nc h e c k e r ) 对a l p h a 2 1 2 6 4 微 处理器设计的错误侦测上有很人的贡献“。另一方面m m 在以色列海法( 8 a i f a ) 研究中心 的经验显示在其执行过的数个计划中包括g i g a h e r t z 微处理器等，使用其f o e s ( f o r m a l c h e c k e r s ) 技术可以减少5 0 的验证工作鼍”9 j 。相较丁二传统验证方式需要复杂的输入序列 才能达剑电路设计的某些状态，断言可以由形式验证或半形式验证的技术来增加验证时的可 控制性( e o n t r o l l a b i l i t y ) ，以找到平常不易发现的错误( c o r n e r - c a s eb u g ) 。 表2 - 1d e c l 9 9 8 年使用在d e ca l p h a2 1 2 6 4 微处理器设计里的错误侦测机制 b u gd e t e c t i o nm e c h a n i s m s o f t o t a lb u g s a s s e r t i o nc h e c k e r2 5 r e g i s t e rm i s c o m p a r e 2 2 s i m u l a t i o n n op r o g r e s s 1 5 p cm i s c o m p a r e 1 4 m e m o r ys t a t em i s c o m p a r e 8 m a n u a li n s p e c t i o n6 s e l f - c h e c k i n gt e s t 5 c a c h ec o h e r e n c yc h e c k3 s a v e sc h e c k2 3 断言增加了模块间的协调性 断言一般插入在模块中，也可以插入在设计的输入输出接口，监视设计的接口行为特征。现 代的i c 设计一般是由多名设计者合作完成，每名设计者设计不同的模块，在晟后的系统集 成时，用断言来监视各个模块的接口行为是必须的，因此断言可以验证多个模块能否协调工 作。 4 断言具有可重用性 专门为了对某个模块进行验证而编写的测试向鼍一般不能用来验证其它功能模块，但是同一 个断言可以使用在不同模块的验证上作中，这样就保证了先前i ：作的有效性。 使用断言描述设计的属性特性或行为特性要比自然语言更为优越，这是因为断言不存在模棱两 可的特点，并且可以被执行，它的明确性来自于其定义明确的语法，这个特点能够使我们清楚的定 义任何属性特征。 断言验证给验证方法学带来一些重要的影响，j j = 1 纳起来，这些影响主要包括以下几个方面： 7 东南丈学硕士论文 设计功能的验证已经成为复杂设计中的主要任务，尤其是复杂设计中不同子模块之问的接 口很容易带来潜在的错误。断言语言允许验证工稃师在较高的描述层次上对设计属性进行 定义，这种定义比硬件描述语言的描述要简洁和自然 用断言语言描述的设计属性具有重用性。由于断言描述与具体的实现不相关，用户可以方 便地在不同的设计中重用已有的属性定义，例如。对p c i 、a m b a 等所定义的设计属性描 述可在不同的设计中_ l = i 于功能仿真o 。 传统的验证覆盖率分析是基于代码覆盖的覆盖率分析，例如，代码行覆盖率、条件分支覆 盖率，信号翻转覆盖率等。由于断言定义了设计的属性( 或可认为是功能) ，通过对断言的 覆盖率统计我们可以将传统的代码覆盖率分析提升到功能覆盖率分析功能覆盖率分析对 于设计的功能检查具有更加直接的意义 基于断言的验证方法是现阶段具有先进理念的验证方法学之一，也是功能验证发展的一个重要 分支。现阶段有几种不同的断言验证语言，例如i b m 公司开发的s u g a r 语言，s y n o p s y s 公司开发的 o v a ( o p c nv e m ) 语言，a c c e l l e r a 组织提出的s v a ( s y s t e m v e r i l o ga s s e r t i o n ) 库和标准属性规范语言 ( p r o p e r t ys p e c i f i c a t i o nl a n g u a g e ，即p s l ，已被i e e e 采纳为断言验证语言的标准) 2 2 断言技术在传统验流程证中的作用 2 2 1 传统验证流程缺陷分析 基丁测试向晕验证的基本原理就是把测试向每作用与d u v 的输入端，在d u v 的输出端收集数 据，再根据一定的规则对收集的数据进行时序或者数据分析，达到查找设计缺陷的目的。这种流程 根本上是属于覆盖率驱动的验证流程，如图2 3 所示。 图2 3 覆盖率驱动的验证流程 暑 第一章断；验自f 技术 测试激励实际上可以理解成d u v 的所有输入的集合，我们称这样的集合为d u v 的输入验证空 间。它的定义如下：假设某个d u v 有n 个输入信号，那么该d u v 的输入空间对应一个n 维空间， 这个空间有2 “个离散的点构成。仿真过程和时间密切相关，即验证过稃是时间的函数，因此，d u v 输入空间的维数实际上是n + i 维，所有的针对该d u v 的输入向量都在这个n + i 维空间中旺“。如果 仿真能够遍历所有的输入空间，那么可以说这样的验证工作是完备的。但是，仿真时间受到设计规 模的制约，当设计规模超过一千万门时，要遍历整个输入验证空间，软件仿真消耗的时间将会达到 数十年。因此，要完全遍历大规模芯片所有输入的全部组合，理论上是不可能实现的。 覆盖率驱动的验证流稃的做法是对验证计划中感兴趣的测试场景进行验证，它从输入空间中选 择部分有效的子集，这个子集中的所有输入向晕在逻辑上相互关联，它可以验证到设计中期望的测 试场景，如果这个测试场景存在设计错误，验证工程师就会把它查找出来。这种实际上是通过描述 约束条件定义的。它在整个输入验证空间中定义了一系列子空间，在这些子空间中随机生成激励。 不同的测试子空间对应于不同的测试场景。但是，要把测试场景中设计缺陷完全的找出来，需要验 证工程师的经验和智慧。 同一个测试场景可以用不止一个的验证子空间对其进行验证，但是，并不是每一个设计缺陷都 会被检查出来，即测试向荤存在着验证盲点这是由于覆盖率驱动验证流程的自身缺点造成的，下 面用图2 4 来说明这个问题。 o o b u g b u g ( b ) o e n v i r e n m e n t c h e c k e r b ug ( b ) 0n 1y c o u l db ef o u n d b ys t i m u l u sb 图2 4 测试盲点说明圈 假设遁过添加约束条件，针对测试场景n 在输入验证空间中定义了三个验证子空间a 、b 和c ， 这些输入子空间内可以随机产生测试激励，并且各自拥有不同的向晕集。在测试场景中存在一个设 计缺陷，验证输入子空间a 、b 、c 都可以检查剑b u g 的存在，覆盖率驱动的验证需要在分析输出 端口收集的数据，才能确定b u g 的存在。但是，对于这个测试场景中的设计缺陷米说，只有验证输 入子空间b 才能使它传播到输出端口，验证输入子空间a 和c 虽然也能检卉剑b u g 的存在，但是， 它们对于覆盖率驱动的验证工作却意义不犬，因为验证工程是无法用它们查找剑测试场景n 中的设 计缺陷( b u gb ) ，也就是说这种向量集存在着测试盲点( b l i n ds p o t ) 。为了克服这个问题，就使得 工稃师不必花费人母的精力去考虑编写什么样的测试向量才能消除测试盲点，或者描述约束条件随 机生成没有盲点的测试向量，必须考虑如何才能使设计错误传播刘硬件设计的输出端口。同时，即 使设计缺陷能传播剑输出端口，验证丁稃师也要花费大量的时间去查看波形和分析日志文件。 从上面的分析中，可以看出基于覆盖率驱动的验证方法存在着不足之处，其主要的缺点： 1 使用测试向鼍查找设计中的缺陷，不能保证测试向鼍能清晰显示设计缺陷。通常需要运行多个 验证矢量，才能找出设计错误，浪费了宝贵的仿真时间，不利于t i m e - t o m a r k e t ，是i c 设计团 队面临的主要压力之一 2 验证t 稃师需要通过分析波形和日志文件，来检查设计中是否存在错误以及确定错误产生的位 置，设计错误的定位比较困难，整个验证过程耗时耗力，同样不利于设计的顺利进行。 9 东南人学坝十论文 2 2 2 使用断言技术改进传统验证流程 通过上面的分析，我们可以看出覆盖率驱动的验证流稃仍然存在着一定的缺陷，导致验证资源 的浪费，不能获得最佳的验证效果。针对这个问题，现在对图2 3 所示的验证流程做部分改进，提 出了采用断言验证方法来改善覆盖率驱动的验证流稃。 这个流程本质上还是覆盖率驱动，但是为了增加验证过程的可观察性和可控制性，我们根据原 来的设计规范单独定义设计的属性，再使_ h j 断言对其进行监视。当测试向晕能诊断出设计中的错误 时，断言就打印出报告信息，这样验证t 稗师在设计测试向鼍生成时，不需要考虑如何把错误传播 到输出端口，只要把精力放在如何编写针对测试场景的测试向量就可以了，图2 - 5 表明了这一流程。 图2 - 5 覆盖率驱动验证流程的改进 经过改进以后的验证流程如下： 1 根据设计规范，制订验证计划。验证计划中包含设计所有的功能点，所有感兴趣的测试 场景，所有的状态机的转变。 2 根据制订的验证计划，用e 语言建立设计的验证环境，这个环境中需要描述要覆盖的 设计功能点。 3 从验证计划的测试场景中抽象出设计的特性，再将断言插入到设计中，监视设计的行为。 4 运行测试向母进行仿真，确保尽可能多的测试场景都被测试到，通过这一步的验证，应 该找出大量容易被发现的错误。 l o 第一章断占验计技术 5 6 7 分析覆盖率报表和断言的执行情况，评估设计中哪些功能点已经被覆盖，哪些断言被执 行，找出尚未被覆盖和断言还朱执行的地方。 再次生成测试向量，针对难以被测试到的边缘情况，重新编写测试向量并运行仿真，再 次对覆盖率币i 断言执行率进行评估。 多次重复第5 步和第6 步，直至测试到所有的测试场景 从上面的流程可以看出，断言机制从一开始就参与整个验证流程，它增加了验证过程的可控制 性和可观察性，并提高了验证效率。 改进后的验证流程和改进前相比较，其优点主要体现在如下几个方面： 1 断言机制在验证前期就参加了验证流程，在向龌仿真时，针对同一个测试场景的设计错误，任 何一个相应的验证输入子空间都可以诊断出来，不一定非要把设计错误传播到设计的输出端口， 减少了仿真时间。a c c e l l e r a 组织曾进行过统计，在设计中插入断言，对于相同数目的测试向晕 来说，仿真时间会有所增加，但是，对于整个验证流程来说，可以降低1 5 左右的时间，而改 进前的验证流程是很难达到的j 。 2 在改进前的验证流稃中，验证工程师需要分析冗长的波形和日志文件，这也是一个费时费力的 过程，即使查剑错误的存在，也不太容易确定其位置。改进后的流程可以自动打印出报告信息， 给出设计错误的位置。 断言和功能覆盖率犹如一个硬币的两面，在一个砌几的设计中，两者都提供了详尽的可观察点。 断言提供了功能止确与否的信息，而功能覆盖率则显示出对设计行为的监测。两者都代表了对设计 意图的描述，它们以仿真或形式验证的方式来确认田】。断言运用于r t l 为主的侦错中，在确认错误 及使错误区域化的方面有显著的效删。除此之外，它还可以缩短整个设计周期，使除错更为便利。 如果能有效地利用断言与功能覆盖率，将这西种功能结合在一起，可以省去许多时间与精力。 2 2 3 几种断言验证技术的比较 目前在i c 设计中获得广泛应用的断言验证语言有开放验证库( 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 ys p e c i f i c a t i o nl a n g u a g e 即p s l ) 和s y s t e m v e r i l o ga s s e n i 0 1 1 。 s y s t e m v e r i l o g 目前由a c c e l l e r a 组织所制订，但是技术来源则主要是由各家公司所贡献。a c c e l l e r a 下的s y s t e m v e f i l o g 委员会的会员来自模拟