（微电子学与固体电子学专业论文）基于specman+elite验证平台的garfield+Ⅲ功能验证.pdf

摘要 摘要 在人们已经对系统芯片( s o c ) 开发的成本和最终的上市时间引起足够的重视之后，芯 片的一次性硅流片成功成为了s o c 设计的一个基本要求。一次性硅流片成功需要一个综合 的技术来验证芯片的功能、时序、数字，模拟信号接口。在这些验证内容中，功能验证尤其 重要。但是，验证设计功能的过程在目前显得相对有点不够重视，对验证方法学和技术的改 善也大都集中在仿真器的速度上，而不是给出一个完整的自动验汪方法学。i - j 时，由于s o c 不断增加的规模和越来越复杂的功能，使得功能验证越来越成为s o c 设计的一个重要障碍， 设计团队中要花费多达5 0 7 0 的人力和资源用到功能验证上束。这些跟功能验证方法学 联系在一起的问题主要是缺少一种有效的自动机制来解决功能验证过程中的验证环境的搭 建、测试激励的生成、对测试质量的评估以及调试和纠错等原本都是手工操作的过程。 本课题研究的对象就是s o c 中功能验证。首先，它将介绍验证方法学和技术的演变史， 分析它们的优缺点；接着，它将介绍v e r i s i t y 公司提出的基于s p e c m a ne l i t e 的验证平台和它 的支撑验证语言e ；然后它将以g a r f i e l d i l l 系统芯片为例子介绍怎样用e 语言搭建验证 环境和使用以覆盖率驱动的验证技术。最后，它分析实验结果并提出s o c 功能验证中别的 需要研究的课题。 关键词：功能验证测试自动生成自动检查功能覆盖率e v ce r m 东南大学硕上论文 a b s t r a c t w i t ht h ei n c r e a s e de m p h a s i so nt r i m m i n gp r o d u c t i o nc o s t sa n dt i m et om a r k e t ，f i r s t p a s s s i l i c o ns n c c e s sh a sb e c o m eaf u n d a m e n t a lr e q u i r e m e n tf o rs y s t e m o n a - c h i p ( s o c ) d e s i g n s f i r s t p a s s s i l i c o ns u c c e s sc a no n l yb ea c h i e v e dt h r o u g hac o m p r e h e n s i v em e t h o d o l o g yf o r v e r i f y i n gt h ef u n c t i o n a l ，t i m i n g ，a n da n a l o g d i g i t a ls i g n a li n t e r f a c eo fad e s i g na m o n gt h o s e ， f u n c t i o n a lv e r i f i c a t i o ni sd o m i n a t i n g h o w e v e r ，t h ep r o c e s so fv e r i f y i n gd e s i g nf u n c t i o n a l i t yh a s r e m a i n e dr e l a t i v e l yn e g l e c t e dd u n n gt h i st i m e a d v a n c e si nv e r i f i c a t i o nh a v ec e n t e r e dp r i m a r i l y o ni n c r e a s i n gt h es p e e do fs i m u l a t i o n ，n o to na u t o m a t i n gt h ev e r i f i c a t i o nm e t h o d o l o g ya saw h o l e a tt h es a m et i m e ，d u et ot h ei n c r e a s i n gc o m p l e x i t yo ft o d a y 。ss o c s ，f u n c t i o n a lv e r i f i c a t i o nh a s b e c o m eam a j o rb o t t l e n e c ki nt h ed e s i g np r o c e s s d e s i g nt e a m sr e p o r t e d l ys p e n da sm u c ha s5 0t o 7 0p e r c e n to ft h e i rt i m ea n dr e s o u r c e so nt h ef u n c t i o n a lv e r i f i c a t i o ne f f o r t m o s to ft h ep r o b l e m s a s s o c i a t e dw i t hf u n c t i o n a lv e r i f i c a t i o n m e t h o d o l o g i e st o d a ys t e mf r o mt h el a c k o fe f f e c t i v e a u t o m a t i o nt oc o p ew i t ht h ed a u n t i n gg r o w t hi n d e s i g n s i z ea n dc o m p l e x i t y t h i sm a k e s d e v e l o p i n gt e s te n v i r o n m e n t s ，t o o l sf o rt e s tg e n e r a t i o n ，a n dd e t e r m i n i s t i ct e s t sa ni n t e n s i v em a n u a l e f f o r t c h e c k i n ga n dd e b u g g i n g t e s tr e s u l t si sa l s op r e d o m i n a n t l yam a n u a lp r o c e s s t h i sp a p e ra d d r e s s e st h es o cf u n c t i o n a lv e r i f i c a t i o ni s s u e f i r s t l y , i tw i l li n t r o d u c et h e e v o l u t i o no ft h ev e r i f i c a t i o nm e t h o d o l o g ya n dt e c h n i q u e sa n da n a l y z et h e i rp r o sa n dc o n s ，a n d t h e n d e p i c t t h en e wv e r i f i c a t i o n m e t h o d o l o g ya n dt e c h n i q u e sf e a t u r e s e c o n d l y , i t w i l l r e c o m m e n dt h ec o m p l e t ea u t o m a t i o nv e r i f i c a t i o ns y s t e ma d v o c a t e db yv e r i s i t yd e s i g n ，l n c a n d i t ss p e c i a lv e r i f i c a t i o nl a n g u a g e e t h i r d l y , i tw i l ld e m o n s t r a t eh o wt ou s eel a n g u a g et o c o n s t r u c tg a r f i e l di i ic h i p sv e r i f i c a t i o ne n v i r o n m e n t f o u r t h l y , i tw i l la d o p tt w oc o m m o n l yu s e d v e r i f i c a t i o n t e c h n i q u e s ：c o d ec o v e r a g e d r i v e n a n df u n c t i o n a l c o v e r a g e d r i v e n v e r i f i c a t i o n t e c h n i q u e st ov e r i f yg a r f i e l di i i f i n a l l y , i tw i l lg i v et h ee x p e r i m e n tr e s u l ta n dp u tf o r w a r ds o m e o t h e ri s s u e si nv e r i f y i n gs o cf u n c t i o n a l i t y k e yw o r d s ： f u n c t i o n a lv e r i f i c a t i o n ，t e s ta u t o m a t i o n g e n e r a t i o n ，s e l f - c h e c k i n g ，f u n c t i o n a l c o v e r a g e ，ev e r i f i c a t i o nc o m p o n e n t ( e v c ) ，er e u s a b i l i t ym e t h o d o l o g y ( e r m ) i t 东南大学学位论文独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究成果。 尽我所知，除了文中特另j j j h 以标注和致谢的地方外，论文中不包含其他人已经发表或撰写过 的研究成果，也不包含为获得东南大学或其它教育机构的学位或证书而使用过的材料。与我 一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示了谢意。 研究生签名：拯塑至日期：之竺苎：! - 7 东南大学学位论文使用授权声明 东南大学、中国科学技术信息研究所、国家图书馆有权保留本人所送交学位论文的复印 件和电子文档，可以采用影印、缩印或其他复制手段保存论文。本人电子文档的内容和纸质 论文的内容相一致。除在保密期内的保密论文外，允许论文被查阅和借阅，可以公布( 包括 刊登) 论文的全部或部分内容。论文的公布( 包括刊登) 授权东南大学研究生院办理。 一虢她一：非日期 0 1 课题的研究背景 f i u 昌 在设计规模变得越来越大，功能变得越来越复杂，性能要求越来越高，工艺变得越来 越先进等情况下，有两个非常棘手的问题时刻困扰着集成电路( i c ) 设计： 夺如何确保芯片在流片之前没有逻辑性设计错误 夺如何确保芯片在流片之后没有物理性制造错误 对于这两个问题已经有两种方法学在研究解决，它们分别是功能验证( f u n c t i o n a l v e r i f i c a t i o n ) 和测试( t e s t ) 。简而言之，功能验证就是核实芯片是否是按照它的设计规范 ( s p e c i f i c a t i o n ) 来实现的，并满足了指定的功能，从而确保芯片在流片之前没有逻辑性错 误。测试的目的是为了核实芯片有没有被正确地制造出来”j 。验证工作在测试工作之前。图 o - - 1 描述了这两种概念和它们之间的顺序： 设计规范 硬件设计 物理制造 图o 一1 功能验证与测试示意图 测试 芯片 功能验证只能证明设计中的错误存在性，而不能证明设计中的错误不存在性。本课题 的研究内容就是s o c 中功能验证问题。 o 2 功能验证的重要性 在芯片规模变得越来越大、功能变得越来越复杂、系统芯片( s o c ) 的i p 复用等新情 况的出现使功能验证这一工作变得更重要、更艰巨，在现代i c 设计中，大约有5 0 一7 0 的 设计周期被用在了功能验证上【 4j ，而且随着s o c 规模的不断扩大，其比例还会不断增加。 同时，如果在行为和功能调试时忽视这个过程，就很难在后面的物理设计阶段发现逻辑性错 误，而只能在流片之后才会被测试出来，这就导致了设计的高成本以及会耽搁芯片的最终上 市时间( t i m e t o m a r k e t ) 。从成本( c o s t ) 和上市时间的角度来考虑，通过功能验证发现逻 辑性错误，将会极大地降低整个设计的成本，同时还可以把对上市时间的影响降低到最低点。 罗碴 网表 东南大学硕士论文 0 3 本课题研究的主要内容和论文结构 本课题的主要研究内容是s o c 芯片设计中的功能验证，介绍其模块级和芯片级的功能 验证方法和侧重点。在本文的第一章简单介绍了目前用于功能验证的一些方法学和技术。第 二章分析传统动态验证方法学中的不足，介绍新的新的验证方法学和一种新的验证语言。第 三章介绍介绍怎样用e 语言搭建g a r f i e l d 芯片的验证环境。第四章详细介绍本课题的功能验 证方法一基于覆盖率驱动的验证方法。第五章给出实验的具体数据，并分析这些数据所说 明的问题。第六章是总结和展望。 第一章功能验证方法学简介 第一章功能验证方法学简介 1 1 功能验证的危机 伴随着设计能力特别是i p 复用技术的快速发展与成熟、综合技术、布局布线技术 以及工艺水平的不断提高，上千万门规模的系统芯片( s o c ) 都已经变成了可能，并且其生 产周期已经缩短到了1 2 个月左右。但是美中不足的是许多验证工程师都希望用过去对付低 于百万门规模的设计的e d a 工具和方法学来验证现在巨大的、复杂的用硬件描述语言 ( h a r d w a r ed e s c r i p t i o nl a n g u a g e ，h d l ) 描述的s o c 他们往往都是无功而返。在很多情 况下，他们对这些设计的功能验证都显得力不从心，为什么呢? 这都是由于s o c 芯片显示 出了与以往普通a s i c 芯片许多不同的特点”j ： s o c 芯片规模更大、功能更加复杂 s o c 芯片需要更短的上市时间 s o c 芯片设计团队的规模更小 s o c 芯片更倾向于由可重用的( r e u s a b l e ) i p 模块组成 s o c 芯片需要集成更多的微处理器和数字信号处理器( d s p ) s o c 芯片需要更大的片上存储体 s o c 芯片需要更加复杂的软件来支持 s o c ：苍片需要集成一定规模的模拟电路，比如a d 、d a s o c 芯片比以往的a s i c 芯片更加接近微型的计算机系统、功能更加强大，当然其管 理就更加复杂了，但是它们却是由规模更小的设计团体和在更短的设计周期内完成。这就在 客观上造成了验证工程师对设计不能够进行深刻的理解，同时验证工程师对特定的设计没有 足够的资源来开发出合适的验证工具。于是验证工程师( 验证团队) 只能依靠现有的工具和 技术，结合一些通用的验汪方法学，对它们只做一些小的变动便应用在特定的设计上，这种 有点迁就味道的做法必然会影响最终的验证质量。虽然在i p 复用的技术问题上，大家都已经 达成了共识它能大大地解放设计能力，缩短s o c 的设计刷期，从而加快s o c 的上市时间， 但同时它也给验证工作带来了前所未有的挑战，由于i p 呈给验证工程师的是一个整体黑 盒子机理，他们很难知道它内部的工作机制，在某些应用场景下，它就可能没办法得到验证， 更重要的是验证工程师很难给系统集成工程师( s y s t e mi n t e g r a t o r ) 提供具有建设性意义的帮 助，提示系统集成工程师去解决或弥补模块的功能不健壮l “。 在过去的十年多中，业界提出了许多新的方法和技术来解决设计问题的瓶颈，但是正 如前面所提到的问题，在设计能力不断快速发展的同时，又h 现了另个s o c 发展过程中 的瓶颈功能验证，而在这方面由于没能引起业界足够的重视，使它严重滞后于设计能力。 功能验证的重要性还体现在它能降低芯片开发过程中的费用，从图1 一l 中可以看出， 错误发现的越晚，用于纠错的费用就会越高“j 。 可能在孵出一个创意( i d e a ) 的时候，如果出现了不妥的地方系统设计人员只需要 重新考虑一下方案，它只会稍微耽搁一下芯片的开发进程，对开发费用的影响是微乎其微的； 当在芯片级或系统级发现了一个错误的时候，验证工程师和系统设计人员要做的事情可能要 更多一些，过程更复杂一些：需要更多的错误隔离时间、更复杂的纠错过程，甚至反复同样 的工作，更为严重的是系统设计工程师可能要重新考虑芯片的实现算法，这将会严重影响芯 片的开发进度，有时可能还需要重新制作系统验证的电路印刷板子( p c b ) 。如果在客户端 发现了错误，结果是致命的，那可能要重新设计芯片了，同时可能还会给芯片生产商的信誉 带来负面影响! 东南大学硕士论文 1 9 9 6 年a r i a n e5 火箭爆炸就是因为当6 4 位浮点数转换成1 6 位整数时的失败造成的以 及早期p e n t i u m 芯片的失败就是因为其乘法表的不健全性造成的，它们都是由于功能验证失 败导致的吲。 错 误 的 数 量 意 级 范 级 计 级 统 级 阁i l 错误数量、错误级别和发现错误的关系 面对功能验证这又一个s o c 发展中的瓶颈，传统的e d a 工具与方法学已经显得力不 从心了，必须寻求新的功能验证方法学和开发新的e d a 功能验证工具，来同步功能验证工 作。 1 2 功能验证的概念 功能验证，简而言之，就是核实经过人工翻译或工具翻译后的设计跟翻译前的设计规 范( 设计属性) 是否一致凹。图1 2 是功能验证示意图。 一一一一、 设一 一一7 图l 一2 功能验征示意图 但是，在4 ；同的设计层次，验证工作所需要做的具体工作是不同的。图l 一3 简单地介 绍了s o c 设计流程，j i ：标出功能验证在其中所处的层次1 0 】。 4 第一章功能验证方法学简介 系统。l 义 i i w 州分引 一 卜 飘 习表螗l f _ 1 1 1 ws w 舒= i = | | tt 7 胛h 1 “，r ， 、 卜 ：_一卜 糕。_ = 硅f - - 轼” 轴lr 卜 ，台m 局布线 ， ， n n 【： j - - 0 _ i 1 口q t 女 t 一赢丢 图卜3s o c 设计流程 1 3 功能验证工作的组成 一般的功能验汪工作由三个部分组成：激励的生成、数据和时序的检查以及覆盖率分 析和评估。 激励的生成主要是通过随机的、约束的和半随机的等策略生成测试所需的各种数据以 及数据的序列；数据和时序的检查则是为了榆查设计的输出和接口上的时序是否正确；覆盖 率的分析和评估则是帮助验证工程师( 验证团队) 估量验证工作的进程和验证工作的质量 1 4 功能验证的错误来源 功能验证过程中的错误来源有曲类：一是设计本身的错误：二是验证环境的错误。 s o c 设计是一个非常复杂和耗时的过程，这其中不刈避免的会有许多因素会让s o c 的 功能不能正常表现出来2 1 。首先是系统定义的错误，这步的功能验证就是验证设计人员 所制定的定义是否和系统定义一致。在这步检盎通过之后，硬件设计工程师就会按照系统 、 ：| z ， 僦 东南大学硕士论文 定义好了的规范去用硬件描述语言来实现，然后再用e d a 综合工具把它翻译成门级网表， 由于这一步过多地掺进了人工劳动利工具的处理，最有可能引起很大的功能错误。 同时，功能验证的失败还有可能是由验证环境本身的错误造成的，主要是由于设计规 范模棱两可，或验证工程师对设计规范的理解不够。由于搭建的验证环境的质量不高，把一 些非设计错误报告出来，误导验证工程师的验证工作。 验证工程师的职责就是找出设计本身的错误，避免产生验汪环境的错误。 1 , 5 功能验证方法学的分类 面对s o c 的又一个瓶颈功能验证，、i k 界电提出了几种功能验证方法学。它们分别 介绍如下： 1 5 1 静态功能验证形式验证 形式验证是一种静态的功能验证方法学， 的规范是否相一致的，也有些人把它定义为是 征的过程1 3 , 1 4 1 。 它通过数学的方法来证明设计的实现跟设计 一种检查所实现的设计是否满足某些属性特 在很多时候，一些对形式验证方法学不甚了解的工程师，认为形式验证的强大优势在 于它不需要写任何测试矢量，其实这种认识有点片面! 形式验证的巨大优势在于它能够在功 能验证之后，保证刚才的验证能够达到1 0 0 的功能覆盖率! 但是它的缺点亦是很明显的： 它的容量、它的应用范围，以及它对硬件环境要求的苛刻都使它不适宜进行系统级的功能验 证，在目前，它还主要应用于模块级和单元级设计的功能验证”1 。 形式验证有三个不同的类型： 夺等价证明，相似检查( 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 e n ) 下面简单一下三种方法的原理及应用的范围。 1 5 1 1 等价证明，相似检查 通过比较两个结构来检查它们是否等价，或通过数学证明的方法来证明两者逻辑上的 等价性。 它一般应用在设计的后期，设计形式比较低的层面，主要是从r t l 到门级( 综合后) 的过程中验证两者的一致性嘲。图1 4 是等价证明的示意图。 6 第一章功能验证方法学简舟 一一、 r t l 悯面嗍雕 一一一7 1 5 1 2 模型检查 图1 4 等价证明示意图 模型检查是通过形式上的检查来认可或否决模型的特征。模型检查一般用来检查一般 的，非特殊的问题或检查用户定义的设计行为的行为是否违规了，它通常应用在设计的高级 阶段，同时那些被检查的特征一般从设计规范中演推而来，检查的过程中常常会引入一个状 态机m 1 。图l 一5 是原型检查的示意图。 设计规范 r t l 编码 属性 ( 断言语句) 图1 5 原型检查示意图 r t l 代码 但是这种形式验证方法学却很不成熟，具体表现在：知道那些特性需要检查和怎样去 表达这种需要需要很大的技巧，一般需要这类型的验证工程师有很高的数学修养；很少有友 好用户界面的e d a 工具；现存的这类型的工具其应用的容量很有限。 1 _ 5 1 3 定理证明 定理证明是用形式逻辑同时去描述设计的实现和设汁的规范，然后用理论证明的方法 东南大学硕士论文 来验证两者在逻辑上是适宜地相关，相似。 这是形式验证方法学中最早的一个方法，它的优点是形式的证点n 丁以机械地检查，它 的缺点是推演出这些形式的原型和证点非常繁琐，不过目前它还只是在学术上进行研究。 1 5 2 动态功能验证 1 5 2 1 仿真 它是通过对实现的设计施加测试矢量，然后检查实现的设计的行为是否按照它的设计 规范而运作的。 这种方法的优点是它简单、易操作并且它的适用范围比较广，不受设计规模的影响， 但它的缺点亦是明显的：难开发出比较健全的测试案例，特别是一些边缘测试案例：其次难 以分析、判断它的功能覆盖率和测试的完备性；更有可能一些未被定义的行为会被当作设计 错误报告出来；对于检查工作仅能局限在一些给定的范围之内” 。 1 5 2 2 基于断言的验证方法 通过在r t l 代码中插入断言语句，然后在动态仿真的过程中由这些断言语句来判断实 现的设计是否跟设计的规范相一致”。 使用断言验证方法学能够帮助验证工程师理解实现的设计，如果实现的设计有不正确 的地方，还能够帮助验证工程师定位出错误的地点。但是，使用断言验证方法需要首先学会 一种断言验证方法的验证语言，用它来描述d u v 的预期应发生的以及预期不应发生的行为。 在以后的设计中插入断言语句将会变为一种趋势! 这对于i p 开发商和系统集成工程师 都是一种必要”o w 。 本章小结 本章详细论述了功能验证在现代i c 设计中的重要性，并简单介绍了它的概念和它的 验证对象，在最后一节简单介绍了目前一些正在应用的功能验证方法。在这些方法中，由于 形式验证技术还不能应用于大的设计，特别是对于规模大，瓜且功能又很复杂的s o c 芯片， 所以动态功能验证方法学依然是r t l 设计的主要验证技术。 在实际的功能验证过程中，本章介绍的任何一种验证方法都不可能解决验证过程中遇 到的所有问题! 但是把它们杂糅在一起，取长补短，能够加速验证工作的进度和提高验证工 作的质量。 第二章一种新的功能验证方法学和新的验证语言e 第二章一种新的功能验证方法学和新的验证语言e 由于静态形式验证的容量和性能都不能满足规模大、功能复杂的s o c 的验证要求，所 以动态功能验证依然是s o c 验证，特别是系统级验证的主要手段。本章将要介绍的功能验 证方法以动态功能验证方法为主，但又集成了静态形式验证的一些优点。 2 1 剖析传统动态功能验证方法学的不足 2 1 1 动态验证方法的演变 本节介绍验证方法的演变。图2 1 是验证方法演变的示意图。 下面分别详细地介绍它们。 图2 1 验证方法演变图 2 1 1 1 基于h d l 任务策略的验证方法 随着引入硬件描述语言h d l ，它被用米同时描述硬件设计和硬件验证。这种基于任务 策略用h d l 搭建的验汪环境一般具有下面两个特色： l 用h d l 捕述的向d u v 中写数据和从d u v 中读数据的任务。 2 这些手工选择输入到d u v 的激励并检查相应的结果的测试矢量是专指向于设计某 一个特定的属性。 一。一+一。一 东南大学硕士论文 图2 2 是这种方法的一个基本流程示意图。这种方法的缺点是： 夺 写测试矢量非常累人、繁琐和耗时 夺测试矢量非常难读和难维护 夺 需要开发很多的边缘测试案例 夺 基于这种策略的验证环境很难创建和维护，因为它只能提供微乎其微的可共享的 代码一h d l 语言不能提供强大的能够用于搭建复杂环境的功能 豳雾j 圈j 2 1 1 2 面向对象的验证方法 图2 2h d l 任务验证策略 为了使验证环境具有更大的可重用性和可读性，许多验证工程师转而使用面向对象的 高级编程语言，比如c c + + 来开发测试向量和搭建验证环境。这种方法能够降低开发测试向 量的工作量，因为这种而向对象的编程方法能够提高输入数据和输出数据的抽象层次。验证 工程师只需要创建抽象数据的模型，而验证环境会自动创建这些抽象数据模型的比特级 ( b i t 1 e v e l ) 形式。 虽然这种方法在创建测试向量上大大节省了工作量，但是用在别的验证工作上的时间 又上升了。由于运用了新的应用，验证环境变得更加复杂了比如在验证环境中需要添加仿 真器的接口。这种花在验证环境构建上的时间有时可能会抵消在创建测试向量上节省的时 间，所以这种方法在对付设计的复杂性上面不能明显地提高生产力。 2 1 1 3 随机激励生成验证方法 面向对象的验证工作量已经基本稳定了，但验证工程师又同时发现有必要去减少创建 确定性的测试向量的工作量，因为创建这些确定性的测试向量非常累人、耗时，且难以维护。 因此验证工程师开始使用一种随机算法的激励生成器来自动地选择那些输入激励。通过写。 个简单的测试环境，用不同的种子( s e e d ) 跑多次测试，验证工程师实际上用这样的验证环 境创建好几种测试向量。 但是，这种完全随机的测试产生会产牛许多非法的激励。为了避免一些无意义或冗余 的测试向量，因此需要一种定制的激励生成器。创建和维护一个定制的激励生成器已经被证 明了是一项非常有挑战性的工作。 除此之外，这种随机算法发激励生成又带来了一些新的问题： 夺 检查测试结果变得很困难了因为每次仿真的时候这些输入激励都是不同的， 那么每次在仿真之前清楚地定义那些输出结果就变得很困难了。 夺 必须提供功能测试覆盖率冈为验证工程师要是没有分析测试向量看那些输 入激励被应用了，就没办法知道测试向量验证了设计的哪一个属性。 虽然相比较前阿种方法，它在牛产力方面有了不小的进步，但是它还没有达到验证复 杂设计的能力。 1 0 第二章一种新的功能验证方法学和新的验证语言e 2 1 1 4t e s t b e n c h 工具 在经历了各种方法之后，有一种强烈的动机就是要减少创建验证环境中新的应用的时 间，比如仿真器的接口和定制激励生成器。这些新的应用比较典型的是在验证过程中当设计 规范变动时难以维护。在不同的仿真器或不同版本的设计之间移动时需要不菲劳动量的验证 环境重建工作。 通常，这种t e s t b e n c h 工具能够减少搭建验证的工作量，但是，t e s t b e n c h 工具往往不能 提供复杂的约束架构和语言层的能力以帮助测试向量开发人员在某一个抽象层面指定测试 向量，而不需要知道验证环境的具体架构。此外，这种t e s t b e n c h 的方法还不能提供一种方 法，用于描述时序概念，因此对于一些复杂的检查工作和复杂的覆盖率场景工作还是显得力 不从心。 2 1 1 5 完整的t e s t b e n c h 自动验证系统 在分析了传统的动态验证方法弊端之后，对将来的验证方法就有了一个清晰的目标。 这就是需要一个完整的自动的t e s t b e n c h 系统。它需要包含f 面这些特色： 夺提供一种语言能够帮助验证环境中的对象进行某一个方向的拓展，而4 ：是继承， 这样可以降低很大的劳动量 夺 能够有一种语言表达验汪环境中的约束条件，因为基于约束的方法对于t e s t b e n c h 的描述更加强大。同时，需要一个复杂的约束解决者和激励生成器，能解析这些 约束信息 夺 一个覆盖率引擎能够定义复杂测试场景的覆盖率目标 夺 一个时态的引擎能够用一种简洁、宣言式的格式捕捉协议规则 2 1 2 重用性 传统的验证方法学很少关注验证环境的重用性，这是由其自身的原因决定的：一是， 传统的验证环境跟被验证的设计的实现形式休戚相关，只要被验证的设计一有改动，验证环 境就得跟着改动；二是，没有一个很好的验证支撑语言，使用这样的语言搭建的验证环境具 有很大的灵活性。 验证环境的重用性对于现代的大规模、复杂的验证工作是必须的，它能够减轻验证工 程师( 验证团队) 的工作量，司时还能够提高验证工作的质量，因为那些能被重用的验证环 境都是已经被论证过是健壮的”1 。 2 2 介绍新的功能验证方法学 面对各种验证压力和要求，业界又提出了一种新的功能验证方法学半形式动态验 证方法( s e m i f o r m a l ) 。这种方法以动态验证方法为主，以静态验证为辅，吸收形式验证和 仿真验证两者的优点，运用形式验证的思想来提高仿真的覆盖率和运用仿真方法学来加强形 式验证方法的仿真功能“7 1 。具体表现为： 审 运用形式验证的方法贯穿设计的抽象层面，然后产生测试矢量 夺 用静态分析的方法挖掘出边缘测试矢量 东南大学硕士论文 夺 运用仿真的方法接近所有感兴趣的状态以观察设计的行为 v e r i s i t ye d a 公司走在了这个领域的前沿，并开发出了相应的验证平台s p e c m a n e l i t e 和它的支撑验证语言e 。它能够提高构建验证环境的生产力和维护验证环境的生产 力，能够让验证工程师用比较短的时间就能搭建出验证环境，减少验证工程师的工作量，同 时还能让这种验证环境具有很大的灵活性，能够在新的验证环境中被重用。其次，它还能够 提高构建的验证环境的质量，提高验证工作的效果，加速验证工作的进程和提高验证工作的 可信度。 2 2 1s p e c m a ne l i t e 及e 验证语言简介 1 e 验证语言的提出与特征 当今，一个项目队伍中在一个典型的开发周期中需要花费大约4 0 一7 0 的资源来构建 巨大的验证环境。因为一个典型的验证环境需要一个同步机制来控制把通信数据流送到 d u v 的输入端e lr ，然后再在d u v 的输出端e l 突出检查数据的一致性。传统上v e r i l o g 和 v h d l 等硬件描述语言都被同时用来构建验证环境，但是不足的是对于复杂的验证环境和问 题，这些语言缺少足够的建模架构来有效地搭建验证环境。于是，很多的设计队伍转向使用 更高级的语言，比如c 和c + + ，来更有效地搭建验证环境。同样不足的是，这些通用的 语言都没有内嵌的架构来描述一些硬件概念，典型的比如同步机制、仿真过程的操作和管理 不同的比特宽度的测试向量。没有这些架构，处理这些跟硬件相关的需求：控制交通数据流 之问的同步机制、检杏真确的时序关系和检查真确的数据流格式就显得力1 i 从心，而且相当 的费时。有些设计团队经常把这两种语言混合起来使用以解决以上的问题，但却又增添了一 个新的问题如何解决好两种语言之间的接口问题“。 此外，更加先进的验证方法学需要t e s t b e n c h 和t e s t b e n c h 构建语言来实现高级的概念， 比如生成测试案例的约束条件、断言以及定义功能覆盖点和功能覆盖率分析。 综合起来，新的验证语言需要具备以下这些特色： 夺 能够用跟设计规范中同样的方式指定数据流量和数据流量中一些控制参数 夺能够自动产生这些数据流，同时能够仿真出设计的边缘应用案例 夺 能够存储和检查一些突出事务处理 夺 能够检查协议的一致性 夺 能够收集激励和d u v 的功能的反馈 夺能够在d u v 仿真的过程中自动响应来自d u v 的反馈 有了这些特色，那么验证工程师就不需要再花再多的时间去考虑怎样去实现验证而只 需要知道要验证什么就行了。 e 验证语言是v e r i s i t y 公司开发的，专门用于s p e c m a ne l i t e 之上，能够更好地服务于 最新的功能验证技术和方法学。这门语言最重要的一个需求就是它能够保证验证环境的重用 咀提高验证生产力。这门语言除了继承了传统的面向对象的、能够清理垃圾的软件编程方法 之外，它还显示出了自己的特色“： 夺 宣称式的约束帮助产生测试场景 夺 一个完整的协议，断言语言 夺 覆盖率规范定义 夺 支持面向而的编程方式 夺 同时支持叙述式和过程式的编码风格，包括定义新的叙述式的架构 夺 能够描述时序和同步关系，能提供直接跟h d l 语言、低级文件和字符操作的接 第二章一种新的功能验证方法学和新的验证语言e 2 s p e c m a ne l i t e 简介 s p e c m a ne l i t e 提出了一个全面的包含了验证方方面面的验证环境：自动的功能测试向 量生成、数据的真确性检查及时序正确性检查和功能点覆盖率分析，甚至h d l 仿真控制。 它具有以下的特征”“： 1 能够自动捕捉可执行的设计规范e 作为一个强大的验证语言能够从设计规范 中捕捉到设计规则或要求，然后提交给s p e c m a ne l i t e 自动产生测试案例。s p e c m a n e l i t e 能够减轻验证工程师对设计规范的深入理解。 2 基于约束条件的测试案例自动生成通过指定一些约束条件，能够快而容易地 让激励生成器产生验证工程师功能验证计划中期望的任何测试场景。这些测试场 景甚至能够根据d u v 当前的状态动态地产生，这样就更有可能产生那些很难碰到 的边缘案例。 3 自动完成数据和时序关系的检查强大的时序构架引擎能够让验证工程师很快 地捕捉到需要检查的协议规范。动态地数据产生和检查能够让验汪工程师得到特 定环境下- 的期望值。当然了，验证工程师还可以随便运用灰白黑盒子方法或它们 的随机组合来加快调试过程。 4 能够自动进行功能覆盖率分析个可执行的( 运作的) 功能测试计划能评估 验证的质量。功能分析能够自动地找出测试覆盖中的漏洞，验证调度机制会变得 更加的具有可预测性，因为功能覆盖率是个非常有意义的指标，它能够指导验 证工程师完整地验证设计。 5 支持软硬件协同验汪更早地集成和调试软硬件系统将会发现更多的软硬件协 同工作时的错误，提前纠错工作，缩短整个系统的上市时间。 6 提供跟所有主流的v e f i l o g 和v h d l 仿真器的接口_ s p e c m a ne l i t e 中集成了所 有当今业界中先进的v e r i l o g 和v h d l 的仿真器的接u 。它能够对d u v 内部的信 号进行随时采样和驱动。它对h d l 代码具有1 0 0 的可控性和观察透明度，在仿 真过程中s p e c m a ne l i t e 的引擎能够完全跟踪d u v 内部信号。 2 2 2v e r i s i t y 的基于s p e e m a ne l i t e 验证平台 基于s p e c m a ne l i t e 的功能验证方法学能够发现一些验汪工程师可能想都没想到的没 计错误，这些基本上都是由于设计规范写的过于模棱两町，或一些期望不被运用的行为而被 使用了。 图2 3 是v e r i s i t y 提出的基于s p e c m a ne l i t e 的验汪解决方案。首先根据设计规范， 特别是接口设计规范制定出验证计划，然后根据这些验证计划用e 语言措建验证环境，这 些验证环境包括带有约束的激励生成器，数据、时序检查器和功能覆盖率模型，s p e c m a ne l i t e 会根据这些生成合适的激励并能自动去做数据、时序检查以及功能覆盖率的分析。 3 东南大学硕士论文 e x t e r n a l 库 l 蘑圈 圈霾圈 一i _ s p e c m a ne l i t e 藤 i i c l e c k l 。、8 l 图2 3 基于s p e c m a ne l i t e 的功能验证平台 从图2 3 可以看出，这种验证平台包括以下几个部分： 1 s p e c m a ne l i t e 整个验证环境都是用e 语言来建模的。验证环境包括d r i v e r 、 c h e c k e r s 和c o v e r a g e 组件以及数据结构。所有的e 语言代码都是在s p e c m a ne l i t e 下 编译和仿真。 2 e x t e r n a l 库它包括所有用c ，c + + 或别的语言建立的合法的模型，这些模型都可 以从e 语言代码中激活( 调用) 。比如，一个用c + + 编写的m p e g ( m o t i o np i c t u r e e x p e r t sg r o u p ) 解码器算法，可以在e 语言中被调用去跟期望的帧数据进行比较来 检查d u v 的功能。 3 ，d u v 待验证的整个设计。 4 各色各样的仿真文件它主要指用h d l 语言建立的各种仿真模型，比如，p l l 的仿真模型，各种b f m 模型。 5 t o p 文件它例示d u v 和各式各样的仿真文件，有时它还可能包括驱动d u v 输 入的寄存器和从d u v 输出接受数据的线的定义，以及时钟的产生机制( c l o c k g e n e r a t i o n ) 。 6 s t u b s 文件这是一个特殊的v e r i l o g 或v h d l 代码，它是验证工程师在s p e c m a n e l i t e 工具，r 发m 个特殊的命令后自动产生。这个文件有着特殊的作用，它在仿真 过程中起着s p e c m a ne l i t e 和仿真器之问的通信通道。但是，这个文件在产生之后， 还要接受仿真器的编译，这样才能被仿真器接受。 7 仿真器它用来仿真v e r u o g 或v h d l 代码，跟s p e c m a ne l i t e 同步运行。仿真器 的作用是编译所有的h d l 代码，并仿真它们。 图2 - - 4 是基于s p e c m a ne l i t e 的功能验证平台的仿真流程，介绍如下： 1 s p e c m a ne l i t e 和仿真器同时被调用。s p e c m a ne l i t e 掌握控制权，而仿真器停在仿 真时问t - - o 时刻，当s p e c m a ne l i t e 完成必要的预指定任务之后，把控制权传递给 仿真器，仿真开始了。 1 4 第二章一种新的功能验证方法学和新的验证语言e 2 仿真器继续运行，当它到达一个由s p e c m a ne l i t e 设置的触发点( 仿真器某个变量 发生了变化) 时，或称之为回收点时。仿真器把控制权交还给s p e c m a n e l i t e 。 3 s p e c m a ne l i t e 收回控制权之后，进行必要数据计算和事务处理。在这个期间，仿 真器处于非激活状态，所以仿真时间是不会流逝的。 4 当s p e c m a ne l i t e 处理完事务以后，把控制权再交给仿真器。然后仿真器接着中断 的仿真时间继续运行直到下一个被s p e c m a ne l i t e 设置的回收点，接着重复2 ，3 两步。 5 这种通过控制权在s p e c m a ne l i t e 和仿真器之间来回不断的传递，推动着仿真1 i 断 向前深入，直到s p e c m a ne l i t e 内部一个特殊的过程调用，要求停止当前的仿真活 动。 6 结果分析。根据分析新一轮仿真又可以开始r 。 工程师发出 t e s t 命令 匪牌罄豳 本章小结 图2 - - 4 基于s p e c m a ne l i t e 验证平台的工作流程 本章首先分析了传统的t e s t b e n c h 验证方法在现代i c 设计中在生产力和质量方面存在 的1 i 足，然后提出了新的验证方法的要求，接着简单介绍了v e r i s i t y 公司提出的验证解