（电路与系统专业论文）系统芯片设计中基于开放验证库的dma控制器功能验证.pdf

摘要 摘要 g a r f i e l d 是一款典型的集成了多个功能模块的系统芯片，模块之间要进行数据传输，存储器直 接存取控制器( d i r e c tm e m o r ya c c e s sc o n t r o l l e r ，简称d m a c ) 在数据传输中起着重要作用，它 的错误有可能导致整个系统的崩溃，因此要对其进行充分的功能验i f ( f u n c t i o n a lv e r i f i c a t i o n ) 。功能 验证是现代i c 设计中最主要的挑战之一，它己成为芯片没计中的瓶颈。功能验证的难点主要体现在 以下三个方面：测试向鼍的生成、验证环境的可重用性、验证过程的可观察性和可控制性。 本文通过定性分析传统激励生成机制和受限随机( d i r e c t e d - r a n d o m ) 向量生成机制的优缺点，选 择了受限随机向量生成机制作为搭建d m a c 验证环境的激励生成机制。可重用性能够降低验证工作 的难度，论文采用模块化组件构建d m a c 的验证环境，把测试文件、待验证设计( d e s i g nu n d e r v e r i f i c a t i o n ，简称d i n ) 的行为属性特征从验证环境中分离出来，并且把对d i n 行为的描述和对 d u v 行为实现方式的描述独立开米，通过这些方法，搭建了d b l a c 的可重用性验证环境。验证过程的 可观察性和可控制性制约着验证丁作的效率，论文在搭建d m a c 验证环境时，提出使用断言技术对其 进行改进。通过比较评估几种典型断言验证方法的性能和成本，本文选择了开放验证库( o p e n v e r i f i c a t i o nl i b r a r y ，即o v l ) 来改进验证过程的可控制性和可观察性，o v l 由3 1 个断言监视器 ( a s s e r t i o nm o n i t o r ) 组成，论文详细讨论了其实现方式和使用方法原则。根据d m a c 设计规范， 提取山5 7 个行为属性，并在验证环境中插入断言监视器对其进行监视，其中5 3 个属性获得验证。 实验结果表明，采用本文提出的功能验证方案可以高效率的查找错误，增加了设计成功的信心 为流片成功提供了有效的保证。 关键词：功能验证测试向量可重用性断言验证开放验证库 尔南大学领十学位沦文 a b s t r a c t g a r f i e l di sat y p i c a ls o c - b a s e do na m b ar u l e s t h e r ea r em a n yf 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 em o d e l st r a n s f e ral o to fd a t u me a c ho t h e r d m a c 巾i r e c tm e m o r ya c c e s sc o n t r o l l e r ) i sv e r y i m p o r t a n ti ni t t h e r e f o r e ，d m a cm u s tb ev e r i f i e dc o m p l e t e l y f u n c t i o n a lv e r i f i c a t i o ni so n eo ft h e c h a l l e n g e si nm o d e mi cd e s i g n 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 t h em o s t d i f f i c u l t i e so fi cf u n c t i o n a lv e r i f i c a t i o na l 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 f v 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 n t h e r ea l et w om e t h o d si nt h eb u i l d i n go ft e s t b e n c h o n ei st h ec o n v e n t i o n a ls t i m u l u sb u i l d i n g m e c h a n i s m , a n dt h eo t h e ri st h ec o n s t r a i n t - r a n d o mm e t h e d i nt h i sp a p e r ，w 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 dt oc r e a t es t i m u l u s t h er e u s a b i l i t yo ft h ev e r i f i c a t i o ne n v i r o n m e n ti sv e r yi m p o r t a n t 1 ti sa ne f f e c t i v em e t h o dt od e c r e a s et h ed i f f i c u l t yo fv e r i f i c a t i o n i ta l s ok e e p st h ev a l u eo ft h ec u r r e n t w o r k t h ep a p e ru s e st h em o d u l a r i z a t i o nm o d u l et om a k et h ev e r i f i c a t i o ne n v i r o n m e n to fd m ac o n t r o l l e r ， s e p a r a t e st h et e s tf i l e sa n dt h ep r o p e r t yo fd u v f r o mt h ev e r i f i c a t i o ne n v i r o n m e n t t h r o u g ht h e s em e t h o d s ， t h ep a p e rm a k e st h ev 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 u s a b 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 e r e s t r i c t e dt h ee 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 h ep a p e ru s e st h ea s s e r t i o nt e c h n o l o g yt oi m p r o v et h i s p r o b l e m i nt h i sp a p e r ，o p e nv e r i f i c a t i o nl i b r a r y ( o v l ) i su s e dt oi m p r o v et h eo b s e r v a b i l i t ya n dt h e c o n t r o l l a b i l i t y o v li n c l u d e s3 1a s s e r t i o nm o n i t o r s t h ep a p e rd i s c u s s e st h er e a l i z a t i o na n dt h ea p p l i c a t i o n o fo v l a c c o r d i n gt ot h es p e c i f i c a t i o no fd m a c ，5 7p r o p e n i e sa r ea b s t r a c t e d t h e r e f o r e ，m a n ya s s e r t i o n m o n i t o r sa r eu s e dt om o n i t o rt h e s ep r o p e r t i e s f i n a l l y ，5 3p r o p e r t i e sa r ev e r i f i e d t h ef u n c t i o nv e r i f i c a t i o nd i s c u s s e di nt h i sp a p e ri sm o r ee f f e c t i v et of o u n dd e s i g ne r r o r s ，a n dc a n e n s u r et h es u c c e s so fi cd e s i g n k e yw o r d ：f u n c t i o n a lv e r i f i c a t i o n t e s t b e n c h r e u s a b i l i t y a s s e r t i o n b a s e dv e r i f i c a t i o n o p e nv e r i f i c a t i o nl i b r a r y i i 学位论文独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究成 果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表 或撰写过的研究成果，也不包含为获得东南大学或其它教育机构的学位或证书而使用过 的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并 表示了谢意。 研究生签名：型釜i日期：塾! 生幽垄旦 关于学位论文使用授权的说明 东南大学、中国科学技术信息研究所、国家图书馆有权保留本人所送交的学位论文 的复印件和电子文档，可以采用影印、缩印或其他复制手段保存论文。本人电子文档的 内容和纸质论文的内容相一致。除在保密期内的保密论文外，允许论文被查询和借阅， 可以公布( 包括刊登) 论文的全部或部分内容。论文的公布( 包括刊登) 授权东南大学 研究生院办理。 研究生签名：丝垒耋 导师签名： 艇 第一章绪论 1 1 论文的研究背景 第一章绪论 现代集成电路( i n t e g r a t e dc i r c u h ，即i c ) 设计一般都采用自上而下( t o p - d o w n ) 的设计方法， 先从规格定义开始规定需要的时钟频率、输入输出时序、功能、面积、功率、信噪比等，第二 步进行丁艺和架构选择，然后用硬件描述语言( 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 ) 描述系统 行为，为了保证设计的r t l 代码正确性，还要进行功能验证，在此之后，由综合工具将h d l 描述 转换为门级网表，为了获得更高的性能和更小的面积，通常要对逻辑进行优化，然后经过库单元映 射和版图设计，最后完成流片生产。图1 - 1 给山了典型的t o p - d o w n 的设计流程。 确定实现电路的具 体库名，并指定综 合生成的网表类型 规格定义 r t l 级描述 ( v h d l 或者v e r il o g ) 磊蕊i 掣 至 综合j = 具k 一 逻辑优化t 具 工艺库卜剖布局布线工艺 布线后门级仿真 l 满足要求 1 投片生产l 要求 图1 - 1i c 的典型设计流程图 随着集成电路制造工艺不断进步，在单个芯片上的集成度不断提高，现代数字系统的功能也变 得越来越复杂，这使得功能验证工作变得十分困难。目前的芯片开发小组中，功能验证人员的数目 是设计人员的2 倍，功能验证所消耗的资源己占整个开发资源的7 0 到8 0 ，其中，r t l 级的验证 工作整个验证开销的5 2 。因此，r t l 级及高层验证已经成为整个设计过程的瓶颈1 、2 】。 东南大学硕十学位论文 设计验证要保证项目初期开发的h d l 描述的正确性，并且保证在每一设计层次间的设计转换过 程不会带米新的错误。在项目开发过程中，设计错误越甲被发现就越容易被改正，并且修改错误所 花费的成本就越小。如果设计错误在流片之后才被发现，那么就不得不重新进行昂贵的投片，而且 对其进行的修正将会涉及到项目开发的各个层次，这样的错误将会增加巨人的开发成本，图1 2 说 明了设计错误发现时期和修止错误成本之间的关系。 项目开授进度 图1 - 2 项目进度和错误修正成本的关系图 芯片规模变得越来越大、m 核获得广泛使用等新情况f ，使得功能验证工作变得更重要、更艰 巨，在现代i c 设计中，随着系统芯片( s y s t e mo nac h i p ，即s o c ) 规模的不断扩大，功能验证所占 用的开发资源的比例还会不断增加。同时，如果在行为和功能调试时忽视这个过程，就很难在后面 的物理设计阶段发现逻辑性错误而只能在流片之后才会被测试出来这就导致设计成本的增加， 同时也会耽搁产品的上市时间( t i m e t o m a r k e t ) 。因此，功能验证土要集中在h d l 描述的r t l 级 设计，图1 - 2 也要求我们要尽甲发现设计错误，这也是整个项目后续设计层次获得成功的主要保证。 通过功能验证发现逻辑性错误，可以极大地降低整个项目开发的成本，同时还可以加速产品的上市 时间从而为企业带来更为丰厚的利润。 1 2 功能验证方法学概述 图1 3 给出了传统的功能验证流程，这张图仅仅是从验证的角度进行说明从中可以看出传统 的验证流程主要包含以下步骤： 1定义设计的规格，制定其的体系结构； 2根据设计规格，拟订一个功能验证计划； 3 针对待验证模块( d e s i g nu n d e rv e r i f i c a t i o n ，即d u v ) 开发山测试向量 4把d u v 放在仿真器中进行仿真； 5分析日志文件和波形文件： 2 第一章绪论 6 得到结果，并判断设计是否达到要求的性能。 图1 3 传统的验证流程 功能验证就是要确保设计功能的止确性，简而言之，就是核实经过人工翻译或工具翻译f f 斤的设 计跟翻译前的设计规范( 设计属性) 是否一致1 3 1 。它主要验证硬件的h d l 描述是否符合设计的功能 描述。现阶段获得广泛应t h j 的功能验证方法主要有三种：软件仿真验证、形式化验证和基于断言的 验证，下面就分别给予简要介绍。 1 软件仿真验证方法 仿真验证一般用于运行v e d l o gh d l 的设计，它通过对d u v 施加测试矢量，然后检查其行为是 否按照它的设计规范米运作。软件仿真运行在普通计算机或者服务器上，它读入v e r i l o gh d l 代码 并且在软件仿真器中仿真其行为。 这种方法的优点是它简单、易操作，并且它的适用范围比较广泛，但是它的缺点也很明显：在 很大的程度上受到设计规模的影响，当设计规模超过一百万门时软件仿真消耗的时间开始呈指数 上升，并且难以开发出比较健全的测试向量，特别是一些边缘测试案例( c o m e rc a s e ) 和边缘条什 ( b o u n d a r yc o n d i t i o n ) ；其次这种验证方法要手工编写测试向量这会导致测试向量的产量和质量 都很低r ，并且花费巨大精力编写的测试向量还不具有重用性，对于那些不同的硬件模块，还需要 重新开发测试向量；再次需要分析冗长的日志文件和波形文件，这个过程也十分地消耗时间和精力， 而且效率低下；更有可能一些未被定义的行为会被当作设计错误报告出来：对于检查工作也仅能覆 盖很少一部分的状态空间。因此，这种验证方法具有很大的局限性”1 。 2 形式化验证方法 3 东南大学硕士学位论文 形式化验证方法使削数学方法形式化地证明设计实现是否部分或者全部满足系统规范所描述的 要求，它是一种静态的功能验证方法学，因此也可以把形式验证定义为是一种检查所实现的设计是 否满足设计规格定义的某些属性，特征的过程”1 6 j 。形式验证方法学的强大优势不在于它不需要写任何 测试矢量而在丁它能够在功能验证之后，保证刚才的验证能够达到1 0 0 的功能覆盖率! 图l - 4 展示了形式化验证j 二具的验证流程，它通过试探操纵设计的所有可能t 作路径来证明设 计属性是否正确，这种以穷尽的方式搜索一个设计的验证思想造成的最大缺点是：它只能用来验证 设计规模有限的设计。 图1 - 4 形式化验证流程 目前形式化验证方法的容量、应用范围有很大的局限性，它对硬件环境要求也很苛刻，因此， 它不适宜进行系统级的功能验证，在现代i c 设计中，形式化验证还主要应削于模块级和单元级设计 的功能验证。 形式化验证有三个不同的类型： 等价证明，相似检查( e q u i v a l e n c ec h e c k i n g ) 等价证明的目的是用数学的方法来证明两 个电路在逻辑上的等价性，即检查两个电路在给定的输入下是否等价。它般麻用在设计 的后期，土要检查r t l 代码在综合前和综合后的的一致性1 。 模型检查( m o d e lc h e c k i n g ) - - - 模型检查用于检测某个具有有限状态集合的系统是否有其 描述所规定的属性。目前，这种方法只能处理小规模的设计。 定理证明( t h e o r e mp r o v e n ) 定理证明是用形式逻辑同时去描述设计的实现和设计的规 范，然后用理论证明的方法来验证两者在逻辑上是适宜地相关，相似。 3 基于断言的验证方法 设计者或者验证工程师在硬件设计的r t l 代码中插入断言语句，然后再使用动态仿真进行验 证，在这一过程中通过这些断言语句来判断实现的硬件设计是否和设计的规范相一致例。 基于断言的验证方法能够帮助设计工程师理解设计的规范描述，在使用断言的过程中其本身 4 第一章绪论 就减少了b u g 存在可能性。如果在设计中发现设计中缺陷，该验证方法还能够定位出错误的位置。 但是，使_ h j 断言验证方法需要首先学会一种断言验证方法的验证语肓，这增加了设计和验证工程师 的学习开销，相应的也增加了项目的开发成本。 为了减少断言验证的不便，本论文主要讨论如何使用o v l ( o p e nv e r i f i c a t i o nl i b r a r y ) 来达到 降低学习开销和开发成本的目的，这将在后续章节进行详细的讨论。 以上简要介绍了目前正在使用的部分验证方法。其中形式验证不能用于大规模设计，动态仿真 验证方法是现代i c 设计的主要验证技术，但它也存在测试向量难以开发、可观察性和可控制性筹等 缺点。在实际验证过程中，上述的任何一种验证方法都不可能解决验证的所有问题，必须综合使用 各种验证方法，取长补短，加速验证t 作的进度和提高验证工作的质量。 1 3 论文的主要研究内容和结构 本课题的主要研究内容是i c 设计中的功能验证，以传统的基丁| 仿真的验证方法为基础，针对其 存在的缺点提出一种能够提高验证质量和效率的验证方案。以自主设计的d m a c 控制器为例，详 细讨论采用这种方案进行模块级功能验证的方法和侧重点。 本文的论题基于e 语言和o v l 方案的d m a c 功能验证。 论文第二章研究如何利崩可重用验证口核搭建可自动生成测试向量的验证环境。第三章在分析 覆盖率驱动验证流程的缺陷基础上，重点探讨如何使用断言验证技术改进这些缺陷。第四章具体讨 论o v l 序的使用方法和原则，并对需要插入o v l 的案例进行总结。第五章对具体实验数据进行分 析。第六章是总结和展望。 东南大学硕士学伉论文 第二章基于s p e c m a n 平台架构的d m a c 验证环境构建 本章以g a r f i e l d 系统芯片中d 胜c 为验证对象，主要研究基于e 语言的测试向量自动生成技术 在此基础上，讨论如何使用e v c 米加速验证环境的搭建工作。 2 1 验证环境的测试向量生成机制 2 1 1 手工编写向量生成机制 当使用传统方式进行验证工作的时候，验证工程师不得不自己去编写测试向量，硬什描述语言 h d l 不仅被用米描述硬件设计，同时它也被用来进行硬什验证，这种基于任务策略用h d l 搭建的 验证环境一般具有下面两个特色： 1 用h d l 描述的t e s t b e n c h 向d u v 中写数据和从d u v 中读数据； 2 这些手工编写的、具有选择性的t e s t b e n c h 是验证工程师专指向于设计中感兴趣的测试 场景中某一个特定的属性； 人工编写的输入激励不可能穷尽设计的所有运行情况，随着设计规模的变大，输入激励的编写 变得更加的困难，编写测试向量费时、费力，而且花费巨大精力编的测试向量又非常难读和难以维 护，因此这种方法从根本上限制了测试向量的产董和质量。 对手工编写向量生成机制的缺点总结如下： 写测试矢量非常累人、繁琐霸慌时 测试矢量非常难读和难维护 需要开发很多的边缘测试案例 基于这种策略的验证环境很难创建和维护，而且搭建的验证环境的可重用性很差，也就是 说当前的工作几乎没有什么后续价值。 2 1 2 受限随机向量生成机制 为了克服手j 二编写向量生成机制的缺点，验证工程师使用基于约束条件的测试矢量自动生成机 制，通过描述约束条件随机产生向量来验证计划中期望的验证场景。这种向量生成方式可以根据约 束条件自动地选择输入激励，通过写一个简单的测试环境，用不同的种子( s e e d ) 跑多次测试，实 际上就对d u v 进行了多次验证。这种基于随机算法的测试向量生成机制带来了新的问题，首先，每 次仿真使用的输入激励个不相同，那么要在仿真完成后，耍弄清楚输入和输山的一一对应关系就变 得非常困难，其次，由于向量随机产生验证工程师很难定量分析测试向量，在这种情况下，要确 定那些设计的行为特征，属性被测试到，哪些没有，具有相当大的难度。 6 第一章基于s p e c m a n 平台架构的d s a c 验自 环境构建 仅仅做到测试向量自动生成，还不能满足当前验证工作的需要，因为验证环境的重用性对于现 代的大规模、复杂的验证工作是必须的，它能够减轻验证t 程师( 验证团队) 的工作量，同时还能 够提高验证t 作的质量，因为那些能被重用的验证环境都是已经被论证过是健壮的。 通过上面的分析后，我们应该清楚基于约束的随机向量生成机制只能是验证环境的一部分，这 种完全自动化的验证系统必须具备一些条仲： 必须具备可重用的验证机制，能够对验证环境中的对象进行某一个方向的拓展，这样就可 以有效的降低劳动量； 需要提供一种支撑语言来表达验证环境中的约束条件，同时，需要一个复杂的约束和激励 生成引擎，这可以使验证环境有能力解析这些约束信息并生成完善的测试向量： 一个覆盖率引擎能够定义复杂测试场景的覆盖率目标： 一个时态的引擎能够用一种简洁、宣言式的格式捕捉协议规则； v e r i s i t ye d a 公司开发的验证e d at 具一s p e c m a ne l i t e 和它的支撑验证语言e 完全具 有上述条件，它是一个完善的支持受限随机向量生成机制的验证平台。能够提高构建验证环境的生 产力和维护验证环境的生产力，能够让验证工程师用比较短的时间就能搭建出验证环境，减少验证 j 二程师的上作量，同时这种验证环境还具有很大的灵活性，能够在新的验证环境中被重用。 2 2 s p e e m a ne l i t e 验证平台架构 2 2 1 s p e e m a ne l i t e 和e 语言简介 v e r i s i t ye d a 公司开发的功能验证平台工具s p e c m a ne l i t e 和它的支撑验证语言_ e 语言 向验证丁程师提供了一个全新的验证方案，该上具具备以下这些特征： 自动检查完全确保设计正确性； 可以自动进行分析功能覆盖率； 支持软硬件协同验证； 提供跟所有主流的v e r i l o g 和v h d l 仿真器的接1 2 1 ： 随机产生测试向量大大缩短产品开发周期、提高产品质量 功能覆盖清楚再现项目进度； s p e e m a ne l i t e 的支撑验证语言e 语言是一种高级验证语言，它提供了简单而有效的语法， 完全把验证工程师从编写测试向量中解放出来，使其把大部分精力放在对功能模块的特征，特性的理 解上，这样可以大大提高验证效率，它具备以下特色： 能够自动捕捉可执行的设计规范； 支持完整的协谢断言语言； 继承了传统的面向对象的编程风格 可以使验证丁作具有可重用性； 7 东南大学颁士学位论文 2 2 2 基于s p e c m a ne l i t e 的平台架构 v e r i s i t y 公司的验证工具s p e c m a n 和e 语言是为验证t 作量身定做的验证平台，该验证平台架构包 括以下部分： s p e c r n a ne l i t e 软件和e 语言代码待验证设计的验证环境用el a n g u a g e 建模，s p e c m a n e l i t e ：用来编译利运行el a n g u a g e f , 码。 待验证设计模块设计人员根据设计规范文档编写的功能模块，它是功能验证的对象。 t o p 文件它是h d l 编写的仿真文件，包含了验证环境中的各种信号、其它仿真文件和 d u v 例化。 s t u b s 文什这是一个特殊的v e r i l o g 或v h d l 代码，它是验证工程师在s p e c m a ne l i t e t 具 上发出一个特殊的命令后自动产生。这个文件有着特殊的作用，它在仿真过程中起着 s p e c m a ne l i t e l 仿真器之间的通信通道。 仿真器s p e c m a n e l i t e 可以单独运行，但是在更多的情况下，使崩仿真器和其链调，仿 真器编译h d l 代码，并把测试向量j j i 到d u v 的输出输入信号上。 其它的仿真文件和相关库。 v e r i s i t y 提出的基于s p e c m a n e l i t e 验证平台的的架构示意图如图2 i 所 图2 一ls p e c m a ne l i t e 验证平台的架构示意图 2 3 搭建d m a c 的可重用验证环境 东南大学a s i c 系统工程技术研究中心针对a m b a 总线规范开发了一款代号g a r f i e l d 的嵌入式 微处理器。此微处理器除采用a r m 。公司a r m 7 t d m i t m p , j 核的硬口外，其余模块采用了自己开发 的软口。现以d m a c 为验证对象，论述如何使用e 语言搭建功能验证环境。本章节的内容包括以 8 第二章摧于s p e c m a n 平台架构的 m a c 验证环境构建 下几个部分：a h b 总线概述、d m a c 设计规范、d m a c 模块的验证计划、用可重用验证i p 核搭建 验证环境。 2 3 1 可重用验证环境 d m a 控制器的早期版本的验证工作是基于a r m 开发平台，采用传统激励生成机制产生测试向量。 这种方案的一个重要缺点就是缺乏对验证环境可重用性方面的考虑，这是由其自身的原因决定的： 第一，传统验证环境和d i n 的实现紧密联系，如果改动d u v ，则验证环境就必须改动；第二，验证 语言缺乏建立可重用验证环境的灵活性。 为了建立可重爿j 验证环境，本文提出了几点改进原则，描述如f ： 原则一：采用模块化设计的方法构建验证环境。 验证环境由激励生成模块、总线功能模块、数据和时序的检查模块、覆盖率分析和评估评估模 块四个部分组成，这四个模块要独立设计，如图2 2 所示。 劁2 - 2 可重用验证模块框图 图中a c t i v ea g e n t 是激励生成模块，它负责生成验证所需的各种数据以及数据的序列：b f m 组 件负责把激励驱动到d u v 的输入端口上；c h e c k e ru n i t 组件负责数据正确性的检查，m o n i t o ru n i t 组件协议时序检查数，c h e c k e r 和m o n i t o r 组件构成数据和时序的检查模块：c o v e ru n i t 负责覆盖 率的分析和评估，并打印出响应的报告。 采用模块化构建的验证环境可以根据需要添加和删减这样就保证了验证环境的灵活性和可重 用性。 原则二：把测试文件从验证环境中分离出来 验证环境是整个验证工作的基础，对于d u v 来说，它是一个稳定平台，用来验证d u v 一般性的 特征。如数据结构、芯片接口、协议规则等，由激励生成模块、总线功能模块、数据和时序检查模 块、覆盖率分析和评估模块组成。测试文件用来验证某个感兴趣的验证场景的描述。所以要把测试 文件从验证环境中分离出来，如图2 3 所示。 9 东南大学硕士学位论文 图2 - 3 验证环境和测试文件分离 把测试文件从验证e 环境中分离对可重用性具有重要的意义，主要体现在以下两点： 1 验证环境用来验证d a i ( 控制器一般属性，具有相对稳定性，可以减少大量的重复劳动。 同时验证环境采用模块化设计，容易维护。 2 测试文件主要针对感兴趣的验证场景，它根源于设计规范，它的特点是非常的灵活，描 述能力强，并且修改设计时，也不会测试文件的工作产生影响。 原则三：把d u y 的行为属性特征从设计规范中提取出来 建立验证环境是整个d u v 验证工作的基础，增加验证过程的可观察性和可控制性也是重用验证 环境的要求，图2 - 4 体现了这个改进原则。 图2 - 4 从设计规范中提取行为属性，特征 d i n 的行为属性特征根源于设计规范，验证环境工作时也要这些属性特征传播到设计的输出 端口，这个传播过程的可控制性和可观察性很差，从设计规范中提取出属性特征，在辅助以其它技 术，对于增加验证环境的可重用性具有很大意义。 可重用验证环境还具有其它方面的一些原则，但是无论如何都必须有一种功能强大的支撑语言 来支持这种环境的搭建。e 语言就具有这种强大的能力，使用它开发的可重用验证组件称为可重用 1 0 第二章基十s p e c m a n 平台架构的蹦a c 验证环境构建 验证i p 核。e 语言的可重用性使得v e r i s i t y 拥有大量的可重用的e 语言验证组件( e v c ) ，用户可 用这些验证口来加速验证工作，e 语言验证组什就是针对某一协议或结构( 如a h b 、p c i 、u s b ) 开发的口核，使用者可以直接对其进行配置，搭建相应的验证环境。 a h be v c 验证组件就是一个可重用验证i p 核，它是针对a m b a 的a h b 协议开发的、可以直 接进行配置的、具有可扩展性的验证环境。使用e v c 能够验证典型的a h b 设备，图2 - 5 是其结构 框图。 图2 - 5a h be v c 的结构框图 2 3 2 d m a c 控制器的设计规范 本课题组2 0 0 2 年启动了称为g a r f i e l d 的嵌入式处理器开发项目。该款s o c 芯片支持显示器件 接口、存储控制器、通讯控制器和多媒体应用等。本文研究的对象就是g a r f i l e d 芯片中直接内存访 问控制器( d m a c ) 的功能验证j 二作。 图2 - 6g a r f i e l d 芯片结构 g a f f i l e a l 体系结构如图2 - 6 所示，它包括c p u 内核、片上总线和其他的外设。内核采用的a r m 公司提供的a r m 7 t d m i ，其余模块采用了自己开发的i p 核。选择a m b a 2 0 的标准作为g a r f i e l d 的 东南大学硕士学位论文 片上总线，a m b a 包含高速总线a h b 和低速总线a p b ，a h b 是为高速、高性能的外设设计的骨干 总线，g a r f i e l d 通过a h b 把存储子系统控制器e m l 、内核、片上s r a m 、显示控制器l c d c 、多媒 体加速引擎m m a 和d m a c 等模块连接起来。a p b 是为低速、低功耗的外设设计的，它不提供b u r s t 传输，所有其他不需要高数据带宽的外设都通过a p b 连接。在a h b 和a p b 之间则通过一个桥 ( b r i d g e ) 连接。 d m a c 模块在g a r f i l e d 芯片中位置见图2 - 3 ，它作为a h b 的土设备，同时也是a h b 的从设备， 并且具有a m b a 的b r i d g e 功能，提供a p b 的接v i 信号。具有6 个d m a 通道，均可支持烈向传输 具有硬件d m a 通道优先级，d m a c 结构框图见图2 7 。 2 3 3 d m a c 模块的验证计划 图2 7d m a c 结构框图 从前几章节我们可以知道，高级验证语言el a n g u a g e 的最大特色就是实现了验证工作的重用性 完全把验证工程师从编写测试向量中解放出来，大大提高了验证的效率。 2 3 3 1 d m a c 模块的验证方案 搭建d m a c 模块的验证环境的总体方窠如下 1 在验证环境中使用到的工具有：s p e c m a ne l i t e 软件、v c s 仿真工具、a h be v c 验证组件、 d m a c 功能模块； 2 使用基于约束条件的受限随机向量生成机制件生成验证所需的测试向量： 3 通过监控d m a c 控制器和a h b 、d m a c 、外设接口信号来验证时序的正确性； 1 2 第二章基于s p e c m a n ：严台架构的i ) w a c 验证环境构建 4 d m a c 的数据、时序的检查采用自动检查机制。数据正确性采用记分板( s c o r e b o a r d ) 的方 式来进行检杏。 5 验证质量评估机制覆盖率是评估验证j 二作的重要方面，本文采用了功能覆盖率米评估验证 质量。在此基础上，再采片i 其它验证方法对其进行补充( 详见第三章和第四章) 。 2 3 3 2 使用a h be v c 搭建验证环境 a h be v c 验证组件是用来验证基于a h b 总线规范的功能模块，前面叙述的d m a c 功能模块的 接口正是基于这一总线规范，它既是主设备，义是从设备因此使用a 皿e v c 验证组件可以方便 的对d m a c 模块进行功能验证。根据a h be v c 验证组件的结构和使用原则，搭建的d m a c 模块 验证环境的具体架构见圈2 - 8 。 图2 - 8d m a c 验证环境架构图 从d m a c 的验证环境架构图中可以看到，在此环境中配置了一个a c t i v ea r b i t e r ，一个a c t i v e d e c o d e r , 两个主动的主设备m 2 和m 3 ，两个主动的从设备s 2 和s 3 ，一个被动的主设备m l ，两个被动 的从设备s 0 和s 1 。这些代理组件( a g e n t ) 构成了d m a c 的验证环境，住这些a g e n t 中，s 0 和s 1 用来监控d a m c 模块作为a h b 从设备的行为，m 1 用来监控d m a c 模块作为主设备的行为，s 2 和 s 3 仿真a h b 从设备的行为，通过a r b i t e f 和d e c o d e r 与d m a c 模块通信，对d m a c 模块的总线传 输作出响应，m 2 和m 1 仿真l i b 主设备的行为，对d m a c 进行设置操作，a r b i t e r 和d e c o d e r 主要 用来模拟a h b 总线行为。 2 3 3 3 配置a h be v c 配置文件 从前面的章节中可以知道，a h be v c 支持基丁a h b 总线规范的各种类型的d u v 功能验证， 这些d u v 总体上分为两类，a h b 主设备和a h b 从设备。根据使用a h be v c 对a h b 设备进行验 东南大学硕士学位论文 证的一般步骤，第一步要做的就是根据待验证d u v 的验证计划来配置a h be v c 的验证环境。对 a h be v c 的配置文件进行配置，一般可采用两种方式，随机配置和直接配置。d m a c 既是主设备， 义是从设备，因此必须同时配置主设各和从设备与它通信。针对d m a c 模块对a h be v c 验证组件 的配制文件进行的配置情况见表2 一l 。 表2 - 1 验证环境设置 属性描述 h a sc h e c k s 在验证环境中嵌入检查器。 h a s _ a c t i v e _ m a s t e r s在验证环境中为d a m c 模块配置主动的主代理组件 ( a c t i v em a s t e r ) ，当对d m a c 模块进行配置时，此时 d m a c 作为a h b 从设备，需要使用a c t i v em a s t e r 对其进 行读写操作。 h a s _ p a s s i v e _ m a s t e r s 在验证环境中为d m a c 模块配置被动的主代理组件 ( p a s s i v em a s t e r ) ，当d m a c 模块作为主设备与a h b 总 线进行通信时p a s s i v em a s t e r 用来监视a h b 总线上各种总 线行为和各种总线操作的覆盖情况。 h a s a c t i v e _ s l a v e s在验证环境中为d a m c 模块配置主动的从代理组件 ( a c t i v es l a v e ) ，d m a c 模块配置完成后，此时d m a c 作为a h b 主设备，需要有从设备相应其在a h b 总线上发 出的各种总线行为。 h a s _ p a s s i v e s l a v e s在验证环境中为d m a c 模块配置被动的从代理组件 ( p a s s i v es l a v e ) ，当d m a c 模块作为从设备与a h b 总线 进行通信时，p a s s i v es l a v e 用来监视从设备响应a h b 总线 的各种总线行为和各种行为的覆盖情况。 h a s _ a c t i v e _ a r b i t e在a h be v c 的配置文件中为d m a c 验证环境配置一个仲 裁器( a c t i v ea r b i t e r ) ，a c t i v ea r b i t e r 可用于仿真a h b 总 线中仲裁器的各种行为。 h a s _ a c t i v e _ d e c o d e r在a h be v c 的配置文件中为d m a c 验证环境配置一个解 码器( a c t i v ed e c o d e r ) ，a c t i v ed e c o d e r 可片j 于仿真a r b 总线中解码器的各种行为。 h u m _ o f _ a c t i v e _ m a s t e r s = = = 2在d m a c 模块的验证环境中为其配置两个主动的主代理组 件( a c t i v em a s t e r ) 。 n u m _ o f _ a c t i v e _ s l a v e s 一2 在d m a c 模块的验证环境中为其配置两个主动的从代理组 件( a c t i v es l a v e ) 。 n u m _ o f _ p a s s i v e _ m a s t e r s = = 1 在d m a c 模块的验证环境中为其配置一个从动的土代理组 件( p a s s i v em a s t e r ) 。 n u m _ o fp a s s i v e _ s l a v e s = = 2在d m a c 模块的验证环境中为其配置两个从动的从代理组 件( p a s s i v es l a v e ) 。 1 4 第二章基十s p e c 的n 平台架构的d m a c 验证环境构建 a c t i v e _ m a s t e r _ n a m e s = = m 2 ；m 3 在d m a c 验证环境中配置的两个主动的主代理组件的名称 为m 2 和m 3 。 a c t i v e s l a v e n a m e s 一 s 2 ；s 3 】 在d m a c 验证环境中配置的两个土动的从代理组件的名称 为s 2 和s 3 。 p a s s i v e _ m a s t e r _ n a m e s = = m 11 在d m a c 验证环境中配置的一个从动的主代理组件的名称 为m i 。 p a s s i v es l a v en a m e s = = s 0 ；s 1 ) 在d m a c 验证环境中配置的两个从动的从代理组件的名称 为s 0 和s 1 。 2 3 3 4 配置a h be v e 序列库 在使用可重用验证口核验证硬件设计模块时，产生测试激励的最好办法是使用e v c 中的序列 ( s e q u e n c e ) ，a h be v c 中集成了多个序列，使用时只需要配置相关序列就可以产生需要的激励。 表2 2 列出了搭建d m a c 验证环境所使用的a h be v c 中序列的配置情况。 表2 - 2a i t be v c 序列库配置 s