（计算机系统结构专业论文）基于vmm的硬件验证技术研究及应用.pdf

ad i s s e r t a t i o nf o rt h ed e g r e eo fm e n g r e s e a r c ha n d a p p l i c a t i o n o fh a r d w a r e v e r i f i c a t i o nt e c h n o l o g yb a s e do nv m m c a l l d i d a t e ： s u p e r v i s o r ： a c a d e m i cd e g r e ea p p l i e df o r ： s p e c i a l t y ： d a t eo fs u b m i s s i o n ： d a t eo fo r a le x a m i n a t i o n ： u n i v e r s i t y ： l ih o n g x i a n g p r o f z h a n gg u o y i n m a s t e ro fe n g i n e e r i n g c o m p u t e r a r c h i t e c t u r e f e b r u a r y , 2 0 1 0 m a r c h ，2 0 1 0 h a r b i ne n g i n e e r i n gu n i v e r s i t y 哈尔滨工程大学 学位论文原创性声明 本人郑重声明：本论文的所有工作，是在导师的指导下，由 作者本人独立完成的。有关观点、方法、数据和文献的引用已在 文中指出，并与参考文献相对应。除文中己注明引用的内容外， 本论文不包含任何其他个人或集体已经公开发表的作品成果。对 本文的研究做出重要贡献的个人和集体，均已在文中以明确方式 标明。本人完全意识到本声明的法律结果由本人承担。 作者( 签字) ：绝鸦秘吖 u1 日期：劲f d 年乏月i1 日 哈尔滨工程大学 学位论文授权使用声明 本人完全了解学校保护知识产权的有关规定，即研究生在校 攻读学位期间论文工作的知识产权属于哈尔滨工程大学。哈尔滨 工程大学有权保留并向国家有关部门或机构送交论文的复印件。 本人允许哈尔滨工程大学将论文的部分或全部内容编入有关数据 库进行检索，可采用影印、缩印或扫描等复制手段保存和汇编本 学位论文，可以公布论文的全部内容。同时本人保证毕业后结合 学位论文研究课题再撰写的论文一律注明作者第一署名单位为哈 尔滨工程大学。涉密学位论文待解密后适用本声明。 本论文( g 在授予学位后即可口在授予学位1 2 个月后 口 解密后) 由哈尔滨工程大学送交有关部门进行保存、汇编等。 作者( 签字) ：鹰：鹇酗文导师( 签字) ：彦硼双卜p 日期：如【o 年z 月一日历年j 月，汨 低。因此在产品上市之前，提供高效率可重用的验证平台对产品进行充分的 验证是必要的。本文以多功能车辆总线控制器m v b c 的验证项目为引导，研 究基于验证方法学v m m 的硬件验证技术，具有理论和实际的重要意义。 本文深入研究了三种基于仿真的验证技术( 基于事务的验证技术、覆盖 率驱动的验证技术以及基于断言的验证技术) ，分析其技术特点，总结其优缺 点；然后在验证方法学的指导下，将三种技术融合在层次化的验证平台中； 其次研究了基于有限状态自动机( f s m ) 模型化理论，对硬件电路进行f s m 建模，从中提取待验证的功能点然后转化为事务级模型，并且基于硬件描述 与验证语言s y s t e m v e r i l o g 实现该验证平台。 最后在验证平台上完成对m v b c 中曼彻斯特编解码模块的验证，并在仿 真软件v c s 上运行，对验证结果的分析表明，该验证平台能够保证较快的验 证速度，提高验证的效率，并且保持了层次化验证平台模块化可复用的优点， 同时应用f s m 模型化理论使得提取的功能覆盖点更为完整。 关键词：功能验证；验证平台；验证方法学；多功能车辆总线控制器 哈尔滨工程大学硕士学位论文 a b s t r a c t h a r d w a r ev e r i f i c a f i o nt e c h n o l o g yh a sb e c o m et h eb o t t l e n e c ko ft h eh a r d w a r e c i r c u i td e s i g n ，v e r i f c a t i o nt h r o u g h o u tt h ep r o d u c td e v e l o p m e n tp r o c e s st og a i n t h eh u m a nr e s o u r c e sa n dt i m er e s o u r c e sb e c o m em o r ea m b i t i o u s ，b u tt h e e f f i c i e n c ya n dr e u s a b i l i t yo ft h ev e r i f i c a t i o ni sv e r yl o w t h e r e f o r e ，p r i o rt o m a r k e t ，h o wt op r o v i d ea ne f f i c i e n ta n dr e u s a b l ev e r i f i c a t i o np l a t f o r m sa n daf u l l v e r i f i c a t i o no ft h ep r o d u c ti sn e c e s s a r y i nt h i st h e s i s ，w eu s em u l t i f u n c t i o n v e h i c l eb u sc o n t r o l l e rt o g u i d et h e v e r i f i c a t i o np r o j e c t ，s t u d yv m m - b a s e d h a r d w a r ev e r i f i c a t i o nt e c h n o l o g y ；i th a st h e o r e t i c a la n dp r a c t i c a li m p o r t a n c e t h i st h e s i si n d e p t hs t u d i e st h r e ek i n d so fs i m u l a t i o n b a s e dv e r i f i c a t i o n t e c h n i q u e s ( t r a n s a c t i o n b a s e dv e r i f i c a t i o n ，c o v e r a g e d r i v e nv e r i f i c a t i o na n d a s s e r t i o n b a s e dv e r i f i c a t i o nt e c h n o l o g y ) ，a n a l y s i so ft h e i rt e c h n i c a lc h a r a c t e r i s t i c s ， s u mu pt h e i r s t r e n g t h s a n dw e a k n e s s e s ；a n dt h e nm e r g et h et h r e ek i n d so f t e c h n o l o g yt o g e t h e ra tt h el e v e lo fv e r i f i c a t i o np l a t f o r mu n d e rt h eg u i d a n c eo f v e r i f i c a t i o nm e t h o d o l o g y ；s e c o n ds t u d i e st h em o d e lt h e o 匆t h a tb a s e do nf i n i t e s t a t em a c h i n e ( f s m ) ，u s et h eh a r d w a r ec i r c u i tf s mm o d e lt oe x t r a c tf e a t u r e p o i n t st ob ev e r i f i e da n dt h e nc o n v e r ti tt ot r a n s a c t i o n 1 e v e lm o d e l ，a n dt h e n a c h i e v et h ev e r i f i c a t i o n p l a t f o r mb a s e do nt h e h a r d w a r ed e s c r i p t i o na n d v e r i f i c a t i o nl a n g u a g es y s t e m v e r i l o g f i n a l l y , w eu s et h ev e r i f i c a t i o np l a t f o r mt oc o m p l e t et h ev e r i f i c a t i o no ft h e m a n c h e s t e re n c o d i n ga n dd e c o d i n gm o d u l e si n m v b c ，a n dr u ni to nt h e s i m u l a t i o ns o f t w a r ev c s t h ea n a l y s i so ft h er e s u l t ss h o w st h a tt h ev e r i f i c a t i o n p l a t f o r mc a ng u a r a n t e e af a s t e rv e r i f i c a t i o ns p e e d ，i m p r o v et h e e f f i c i e n c yo f v e r i f i c a t i o n ，a n dm a i n t a i n e dah i e r a r c h i c a lv e r i f i c a t i o np l a t f o r mw i t ht h e a d v a n t a g e so fm o d u l a ra n dr e u s a b l e ，w h i l ea p p l i c a t i o no ff s mm o d e lt h e o r y m a k e st h ee x t r a c t i o nm o r ec o m p l e t ef u n c t i o n a lc o v e r a g ep o i n t s k e y w 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 ；v e r i f i c a t i o np l a t f o r m ；v m m ；m v b c lirl 目录 第1 章绪论1 1 1 研究背景及意义1 1 2 验证技术分类2 1 2 1 形式化验证技术3 1 2 2 基于仿真的验证技术4 1 2 3 静态分析技术5 1 3 研究现状及发展趋势6 1 4 论文的主要研究内容8 1 5 论文的组织结构8 第2 章基于仿真的功能验证技术1 0 2 1 基于仿真的功能验证技术一1 0 2 1 1 基于事务的验证技术1 0 2 1 2 覆盖率驱动的验证技术1 2 2 1 3 基于断言的验证技术1 4 2 2 硬件描述与验证语言s y s t e m v e r i l o g 17 2 2 1 s y s t e m v e r i l o g 特性1 7 2 2 2 s y s t e m v e r i l o g 断言技术1 8 2 3 s y s t e m v e r i l o g 功能验证实例1 9 2 4 本章小结2 1 第3 章多功能车辆总线控制器的验证方案2 2 3 1 列车通信网络概述2 2 3 2m c 各模块功能2 3 3 3 传统的验证平台架构2 5 3 3 1 验证平台概述2 5 3 3 2 传统验证平台的缺陷2 6 3 4 基于v m m 的验证平台设计一2 6 3 4 1 基于v m m 的验证平台架构2 6 3 4 2 基于v m m 验证平台的不足2 8 3 5 多功能车辆总线控制器的验证方案。2 8 3 5 1基于有限状态机提取模型的完备性理论2 9 3 5 2 引入模型的层次化验证平台3 2 3 6 本章小结3 3 第4 章m v b c 的模块级验证及结果分析3 4 4 1曼彻斯特编解码模块功能描述3 4 4 2 编解码器的验证3 6 4 2 1验证计划3 6 4 2 2 曼彻斯特编解码模块的f s m 建模。3 8 4 2 3 事务产生器与驱动器的实现4 0 4 2 4 监视器与比较器的实现4 3 4 2 5 计分板与参考模型的实现4 5 4 2 6 顶层环境与覆盖模块的实现4 6 4 2 7 s y s t e m v e r i l o g 断言技术的实现。4 7 4 3 验证环境的搭建4 8 4 3 1v c s 安装及设置4 8 4 3 2 版本控制软件c v s 的配置4 9 4 4 仿真结果及分析5 0 4 4 - 1事务产生结果报告5 0 4 4 2 覆盖率结果报告5 1 4 4 3仿真结果分析5 4 4 5 本章小结。5 5 结j 沧5 6 参考文献5 8 攻读硕士学位期间发表的论文及取得的科研成果6 2 致谢6 3 哈尔滨工程大学硕士学位论文 1 1 研究背景及意义 第1 章绪论 随着半导体产业的快速发展，集成电路i c ( i n t e g r a t e dc i r c u i t ) 设计技术 也进入到了一个新的时代，从最初的电子管和晶体管发展到现在的超大规模 集成电路以及特定功能的专用集成电路a s i c ( a p p l i c a t i o ns p e c i f i e di n t e g r a t e d c i r c u i t ) 【l 】。根据摩尔定律，单片芯片上的晶体管数量每1 8 个月将会翻一番。 目前半导体工艺水平已经达到6 5 纳米甚至4 5 纳米的水平，芯片的集成度越 来越高，规模也愈加庞大，百万门级的设计也逐渐普遍化。由此带来的生产 能力、设计能力和验证能力上的不协调愈加严重，即设计鸿沟与验证鸿沟都 有明显增大的趋势，设计鸿沟就是指设计能力与生产能力上的差距，验证鸿 沟就是指验证能力与设计能力上的差距【2 】。 芯片性能大幅提升的同时也带来了巨大的挑战。a s i c 设计的风险性主要 在于：在开发过程中由于设计者理解偏差等原因导致的芯片不符合规格。而 验证就是尽可能的保证芯片在投产时符合设计的意图。验证在a s i c 开发中 的地位逐渐加重，甚至成为了a s i c 设计的瓶颈。对于大规模以及超大规模 的设计来说，验证人员的数量将达到设计人员的2 倍，验证工作要占用整个 开发过程中6 0 7 0 的时间，并且其中寄存器传输级r t l ( r e g i s t e r t r a n s f e r l e v e l ) 验证还大约占整个验证工作的5 2 t 3 卅。设计工程师通常是依据设计规 范的典型事例进行设计，而验证工程师却要对设计的所有实例进行验证，工 作量繁重，容易漏掉错误，所以对于一块中等复杂的芯片，即使在验证上投 入了大量的资源，在投产收益之前通常也要经历多次的流片( t a p e o u t ) i s 。 集成电路的快速发展对验证技术提出了巨大的挑战。以往的设计过程中， 人们对设计流程中其他步骤比如逻辑综合和布局布线等关注较多，而没有对 哈尔滨工程大学硕士学位论文 m li i i i 验证投入过多的精力，这也导致验证成为当前的瓶颈。本项目中的待验证的 对象m v b c ( m u l t i f u n c t i o nv e h i c l eb u sc o n t r o l l e r ) 硬件设计十分复杂，芯片 要求的功能点较多并且时序要求也非常严格，所以如何提供快速的、高效率 的并且可重用的验证平台对m v b c 进行验证是本课题的研究重点。 典型的a s i c 设计与验证流程如图1 1 所示。 图1 1a s i c 设计与验证流程 j a n i c kb e r g e r o n 定义验证是证明一个设计的功能是否正确的过程【6 】。验证 工作贯穿整个设计流程中，从行为级到h d l 设计一直到芯片设计定案之前都 需要做足够多的验证工作。验证的过程实际上就是要保证设计的功能时序等 要满足设计相关文档的需求。典型的验证包括：系统级验证、r t l 级功能验 证以及综合布局布线后的网表级验证， 不同层次关注的验证对象也不尽相同， 也包括静态的时序分析以及后仿真。 系统级验证以整个系统为验证对象， 侧重系统整体的性能与行为；r t l 级功能验证关注寄存器传输级的功能模型， 侧重验证r t l 级模型的功能：门级仿真主要验证综合后功能是否发生变化； 后仿真物理级验证主要是在实际物理器件上进行验证。本课题重点研究其中 r t l 级功能验证。 1 2 验证技术分类 当前的功能验证主要分为静态的功能验证和动态的功能验证两种。静态 的功能验证以形式化验证为主要手段，动态的功能验证以基于仿真的验证为 主要手段。 l-ii-r 哈尔滨工程大学硕士学位论文 1 2 1 形式化验证技术 形式化验证技术是指利用数学的概念、方法和工具来解决设计的正确性 问题。一般来讲，即用具有形式语义的记号和工具明确的描述所要设计的系 统的要求，给出系统规范( s p e c i f i c a t i o n ) ，并且根据系统规范用上述记号和 工具对系统具有的性质和最终实现的正确性进行严格的证明。典型的形式化 验证包括以下几种方法：等价性检验、模型检验以及基于定理的证明【7 - s 1 。 形式化验证首先要抽象出数学模型，然后利用严格的数学推理来证明设 计是正确的。形式化验证技术可以在早期检测出某些缺陷，并且验证中不需 要验证平台与测试激励向量，在理论上也可以保证较快的验证速度和较高的 覆盖率，甚至达到1 0 0 的覆盖率。但是形式化验证技术在应用范围和对硬 件环境的要求也有一定的局限性，不适合进行系统级验证。形式验证的典型 流程如图1 2 所示【9 】。 性 质 错 误 图1 2 形式验证的流程图 等价性检验主要用于一个设计经过变换的情况，即要证明设计的变化没 有产生功能上的变化。这里所说的设计的变化包括门级、r t l 级和网表级互 相间的转换，也包括f p g a 到a s i c 的转换等【1 0 1 。 不需要用户提供输入。当利用等价性检验的工具检测到两个模型间存在差异 时，系统便显示一个反例及引起这个差异的原始输入，以便于设计者进行分 析。可满足性算法( s a t ) 为常用的等价性检验算法。 模型检验是由e m c l a r k e 等人提出的，它主要是基于一种分支时态逻辑 即计算树逻辑( c t l ) 和有限状态机( f s m ) 理论的，其基本思想是用c t l 公式表达电路的时序性质，用f s m 表示电路的状态转移的抽象结构，通过对 f s m 进行遍历来检验时态逻辑公式的正确性。r k u r s h a n 在1 9 8 7 年提出“同 态化简”的方法，简化数据结构和控制序列；8 0 年代末又发展了二叉判定图 技术和符号模型检验技术【1 0 】。 模型检验是完全自动化的，与等价性检验一致，当检查出系统不满足给 定的性质时，同样会给出反例提示。近年来模型检验已经应用于验证大规模 设计中，包括奔腾微处理器的浮点运算单元、i e e e 标准验证和各种协议验证 等。模型检验的缺点是随着电路规模的增大，遍历f s m 时状态空间会呈现指 数型增长，也就是组合爆炸问题，它将使得模型检验无法在可容忍的时间内 完成。通过“同态化简”等技术已经缓解组合爆炸的问题，但是却无法从根 本上解决该问题。 定理证明的方法允许用户使用定理去构造对待测设计行为的证明，并以 此来表明设计对象满足一定的功能要求。这种方法还仅仅处于理论研究阶段， 并没有实际应用【1 0 】。 c 1 2 2 基于仿真的验证技术 动态的功能验证主要是指利用仿真器对待测设计进行仿真来判断待测设 计的功能是否正确的一种手段。通过在待测设计施加测试激励，检查其执行 过程，判断其是否按照相应的规范来运行。基于仿真的验证的典型流程如图 1 3 所示嘲。 4 一。i 哈尔滨1 二程大学硕士学位论文 图1 3 基于仿真的验证流程图 基于仿真的验证主要包括两种：基于事件驱动的方式和基于周期的方式 1 。事件指的是电路中的特点节点发生电平的逻辑值改变，当事件发生时， 电路中的节点逻辑值重新进行计算并逐级传递。而基于周期的方式中是在每 一个周期内都对电路中的节点逻辑值重新进行计算，这里的周期经常使用的 就是系统的时钟周期。基于周期的方式加快了处理速度，但是不能进行时序 分析，所以仅限于应用在同步电路设计中。 在实际应用中，通常是将两种方式结合起来使用，比如：在初始的同步 设计中，采用基于周期的方式，然后在随后的验证过程中，使用事件驱动的 方式对电路进行验证。 1 2 3 静态分析技术 静态分析技术不需要验证平台与测试激励向量。通常包含两种方法：代 码静态检查与时序验证。 代码静态检查主要是应用检查工具如l 硫对待测设计对象的源代码做静 态检查，验证其在语法上的正确性。在设计的早期进行检查可以避免代码中 的简单错误，如变量未初始化、端口不匹配等，同时避免了使用高级的仿真 个输入信号可能有多个输入源，时序会根据电路的运行而发生变化。时序验 证的目的是保证设计满足时序要求，即s e t u p h o l dt i m e 符合要求，以便数据 能被正确的采样。时序验证的主要方法包括s t a ( s t a t i ct i m i n g a n a l y s i s ) 和 后仿真i 2 】。由于本课题的验证对象是使用f p g a 进行设计，在设计时已经基 本保证r t l 级代码在综合结果和功能仿真结果的一致性，只要综合布局布线 后的静态时序报告没有违反时序约束的警告，就可以进行板级调试了。 1 3 研究现状及发展趋势 形式化验证技术中以模型检验与等价性分析应用较为广泛，一般应用在 中小型设计中，并且该设计便于用数学符号进行描述。而定理证明技术仅仅 处于起步研究阶段，并没有实际应用。形式化验证方法主要存在以下两个问 题i lo 】： ( 1 ) 模型的准确性 形式化验证的证明中，要利用对象的各种模型，而如何保证这些模型的 正确性和准确性，这对于解决的问题的质量和效率是很重要的。 ( 2 ) 证明的正确性 形式化验证要利用定理证明设计正确，但是却无法保证证明过程中的正 确性，所以它也无法保证设计是完全正确的。 基于仿真的验证技术广泛应用于各种场合，仿真操作比较简单，运行速 度较快，但是对于测试激励难以保证完全覆盖，检查工作只能局限在一个特 定的范围之内，无法在整体上保证验证的完整性，因此不适用于对验证要求 较高的设计中。 静态分析技术是以上两种技术的重要辅助手段，尤其在s o c 设计及a s i c 6 哈尔滨工程大学硕士学位论文 设计中进行静态时序分析是必要的，但是静态分析技术需要验证人员手工分 析时序关系，较为费时和繁琐。 形式化验证技术与基于仿真的验证技术各有优势，前者偏重于部分设计， 而后者侧重于整体设计；从验证目标来看，前者主要针对功能进行验证，而 后者还可以对电路的时延性能等做出精确仿真；从验证结果来看，前者只能 给出设计是否正确的判断，而后者在验证过程中可以准确定位错误，方便修 改设计。未来的发展趋势是如何整合各种验证方法的优势，既能够提供完整 的覆盖方法，并且保证快速的、自动化程度较高的以及可复用的验证技术。 在本课题中主要采用基于仿真的验证方法，并适当借鉴形式化验证的验证方 法的优势。 传统的验证技术关注的更多集中在信号层次，而随着集成电路复杂度增 大、设计的抽象层次不断提高，这种传统的验证方法已经不在适用。造成验 证技术成为瓶颈的原因主要有以下几点- 1 ： ( 1 ) 集成电路集成度快速增加，设计抽象级别越来越高，设计的产品功 能愈加复杂，导致验证的工作量呈几何数量级增长。 ( 2 ) 现代设计中许多领域对系统的可靠性要求增加，这也对验证工作提 出更高的要求。 ( 3 ) 在设计过程中，高抽象级别的设计会产生一定的信息丢失，或者由 于系统规范具有二义性导致设计人员理解错误，这些问题就需要验证人员在 验证中要辅助设计人员，以确保设计的各个步骤间的正确转换，同时也要确 保产品完全体现了设计者的目的。 ( 4 ) 传统的验证技术中不容易验证到边角情况，并且对于模拟电路与数 字电路进行交互的情况以及复杂的协议也不容易验证。 为了解决以上问题，现代的验证技术也朝着几个方向去发展： ( 1 ) 验证工作量的指数级别增加使得手工去编写每一个测试用例变得不 现实，那么采用自动化的测试激励产生方式变得很重要。 ( 2 ) 设计的抽象层次越来越高，使得验证也不能只停留在信号级层次上， 7 哈尔滨工程大学硕士学位论文 如何提高验证的抽象层次也是当前验证技术重要的研究问题。 ( 3 ) 为了减少在验证平台开发过程中的重复工作，那么如何构建一个高 度可重用的验证平台也变得十分重要。 1 4 论文的主要研究内容 本论文的主要研究内容如下： ( 1 ) 通过对验证流程的分析，重点研究功能验证的验证效率问题以及验 证过程中的自动化程度问题。通过研究当前主流的验证技术解决以上问题， 包括基于事务的验证技术、覆盖率导向的验证技术、基于断言的验证技术、 可重用的验证架构以及基于专门验证语言的验证平台技术。 ( 2 ) 研究自动机模型化理论，分析自动机模型完备性理论，并利用该理 论进行事务级功能模型抽取，以此来保证功能模型的完备性。 ( 3 ) 用硬件描述与验证语言s y s t e m v e r i l o g 具体实现一个基于事务级别， 可重用的采用模块化思想的验证平台，使得验证在比较高的一个抽象级别上 进行，在修改激励向量的时候不需要对验证平台代码进行修改。 ( 4 ) 利用该验证平台完成对列车通信网络中的m v b c 进行验证，并对 验证结果进行分析和总结。 1 5 论文的组织结构 本文首先介绍验证技术的现状与发展，分析功能验证的流程与技术，总 结其优缺点，分析并比较验证技术发展过程中存在的问题。其次研究基于状 态机模型完备性理论抽取事务级功能模型的方法，以此来保证事务功能模型 的完整性。在验证方法学的指导下基于s y s t e m v e r i l o g 语言设计并实现层次化 模块化的功能验证平台，最后阐述应用该验证平台对m v b c 模块进行实际验 证的过程，并对验证结果进行分析和总结。论文组织结构如下： 第2 章：重点研究基于仿真的功能验证方法，并对当前主流的验证技术 ( 基于事务的功能验证方法、基于断言的功能验证方法和覆盖率驱动的验证 方法) 进行研究和比较，总结其优缺点；简要介绍设计与验证语言 s y s t e m v e r i l o g 的特性以及选用s y s t e m v e r i l o g 的原因。 第3 章：首先简单介绍列车通信网络中的m v b c ，重点介绍m v b c 各 模块及其功能；然后对验证平台框架进行分析，将自动机模型理论引入层次 化验证平台，提出多功能车辆总线控制的验证方案。 第4 章：利用上一章的验证平台实现m v b c 中的曼彻斯特编解码模块的 验证过程，搭建仿真所需的硬件及软件环境，对验证的结果进行分析，对整 体验证平台进行分析和总结。 9 验证要保证待测设计的功能和时序满足规格说明书中的要求。为了尽量 缩小设计与验证之间的鸿沟，业界也产生了各种各样的验证技术，大体上分 为以下几种：基于仿真的验证技术、形式化验证技术、静态分析技术以及物 理验证技术。本章主要研究本项目中使用的基于仿真的验证技术。 2 1 基于仿真的功能验证技术 基于仿真( s i m u l a t i o n ) 的验证技术是指利用仿真器对待测对象进行模拟 并监测待测设计的响应。基于仿真的验证技术主要分为：基于事务的验证技 术、覆盖率驱动的验证技术以及基于断言的验证技术等。 2 1 1 基于事务的验证技术 基于事务的验证是在1 9 9 8 年首次提出来的，现在已经广泛应用在了集成 电路的验证中 i s 3 。传统的验证方法中，验证是在信号级的层次上，即测试平 台直接通过端口与待测设计d u t ( d e s i g nu n d e rt e s t ) 连接，也就是使用直 接激励的方式来驱动待测设计，然后通过检查端口上信号的逻辑值变化以达 到验证设计的功能是否正确的目的。显然这种方式的抽象级别非常低，测试 激励与设计的端口协议紧密相连，如果待测设计在输入和输出引脚上有大的 改变，那么原来的测试激励就失效了，所以传统的验证方式可重用性较差。 与传统的验证方式不同，通过事务可以一次性完成对一组信号的操作，这里 的事务实际上是对待测设计功能的一种高层次抽象的描述。事务 ( t r a n s a c t i o n ) 是指测试平台与待测设计之间通过设计的特定接口( i n t e r f a c e ) 进行的高层次的数据或者控制信号的传输。事务可以用起始时间、结束时间 1 0 和属性来描述ij 6 。这里的属性主要指设计中数据的变化与流向，控制信号的 动作等。简单的事务可以是一次对存储单元的访问，复杂的事务可以是一次 通讯中数据包或者报文的传送。 基于事务的验证技术对底层信号进行了封装，使得验证工作可以在一个 较高的抽象级别上进行，减轻了验证人员的压力，使得验证人员可以更多的 关注事务级的验证而不去过分的关注信号级的时序关系，极大的提高了验证 效率。基于事务的验证使得测试激励的可重用性变为现实，比如网络中一次 报文的传输就可以定义为事务以便复用到不同的项目中。 在基于事务的验证中，需要将事务层与信号进行连接，通常使用事务验 证模型t v m ( t r a n s a c t i o nv e r i f i c a t i o nm o d e l ) ，t v m 将事务级别的激励按照 协议的规定转换成周期精确的信号输入待测设计【1 。】。 典型的基于事务的验证框架【1 9 2 0 】如图2 1 所示： t e s t硎 图2 1 基于事务的验证框架 整个框架的核心部分是t v m ，在底层t v m 通过信号与待测设计相连， 在高层t v m 通过事务与t e s t 进行连接，这里的t e s t 定义了验证中所需要 的事务的组合序列，这里知道需要哪些事务产生激励并且是一个怎么样的顺 序就可以了，而不需要详细的了解设计的接口协议。t v m 中将高层次的事务 转化成d u t 能够接受的信号级时序的二进制信号。这里传递事务需要用到接 口的概念，与传统设计中端口的概念不同，端口在以往的设计中是一对一绑 定的关系，一旦确定之后就无法更改，而接口是指一组信号线的传送，在传 送到不同的模块时，只需要指定每根信号线的传送方向即可，也具有高度复 基于事务的功能验证流程如图2 2 所示1 2 l 】： 图2 2 基于事务的验证流程图 2 1 2 覆盖率驱动的验证技术 覆盖率的概念来源于软件测试中，在测试软件程序时，测试人员要看每 条语句和每个分支是否都执行到，并以此来衡量测试的完备程度。现在的集 成电路设计大多采用硬件描述语言，所以在硬件验证中，覆盖率也自然的成 为验证的重要参考指标。传统的覆盖率主要包括：语句覆盖、分支覆盖和条 件覆盖等。由于硬件描述语言的一些特性，导致在硬件验证中的覆盖率除了 传统的软件程序覆盖率之外，还包含一些特殊的参数：如状态机覆盖、断言 覆盖以及功能覆盖等。代码的覆盖在仿真过程中仿真器可以自动统计，主要 检查哪些代码没有执行，使用代码覆盖率能够检查是否存在冗余代码。功能 覆盖是仿真器根据验证定义的功能覆盖点进行统计，通过功能覆盖能够检查 验证平台的功能是否完整阎。 覆盖率驱动的验证中需要定义覆盖率参数，并以此作为评价验证是否完 备的标准，当未到达此参数时，重新产生测试向量进行验证，只有达到预期 1 2 的覆盖率时才会停止验证。覆盖率驱动的验证流程如图2 3 所昶：，】： 图2 3 覆盖率驱动的验证沉程图 传统的验证方法中，验证的开始完全依赖于待测设计的规格说明书，即 根据功能来进行验证，并且在产生激励的过程中更多的是动手编写测试激励， 同时验证响应的过程也是直接的，即手动计算出每个测试激励的响应，再与 仿真得到的结果进行比较，效率较为低下。覆盖率主要针对代码进行覆盖， 覆盖点不够全面。 而覆盖率驱动的验证中，所有其他的验证过程都要以覆盖率指标作为参 考标准，并以此衡量验证是否结束。验证中的测试激励可以通过带约束的随 机激励产生，通过修改约束产生不同的测试激励以便达到更好的覆盖率；验 证响应的过程中，由于测试激励是随机产生的，也无法去计算每一个测试激 励的预期响应，这里使用与黄金模型( g o l d e nm o d e l ) 进行对比的方法，所 谓的黄金模型即根据测试激励可以产生正确输出的一个模型，一般用高级语 言进行描述。以上几方面极大的提高了验证效率。覆盖率驱动中更重要的是 1 3 哈尔滨工程大学硕士学位论文 功能覆盖率，它更加贴近实际的设计意图。 覆盖率驱动的验证中，最重要的是对于覆盖点的定义，尤其是功能覆盖 点，需要仔细分析待测设计的规格说明书，然后编写功能验证说明书，详细 指明其中的覆盖点。 ( 1 ) 如果代码和功能覆盖率均很低，则说明产生的测试激励较少，需要 重新产生随机种子，并增加测试激励的数量。 ( 2 ) 如果功能覆盖率明显低于代码覆盖率，则可以有以下两种原因： 测试激励较为集中，没有激发待测设计的相关功能；验证人员根据设计提 取的覆盖功能点有误，如提取了某些待测设计无法完成的功能。 ( 3 ) 如果代码覆盖率明显低于功能覆盖率，则可能有以下两种原因： 设计中存在冗余代码导致代码覆盖率低下；验证人员对于待测设计的功能 提取不够全面和完整。 ( 4 ) 代码和功能覆盖率都较高，但均未达到预期规定，此时可以更改种 子，产生新的激励，另外也可以手动加入直接测试激励来弥补未产生的部分。 在实际的验证中，可以根据以上的方面适当进行调整，使得覆盖率满足 预先的期望值【2 4 】。 覆盖率驱动的验证使验证过程更加系统化和结构化，能够极大的提高验 证的效率，具有一定的可重用性，在项目中具有实际的应用意义。 2 1 3 基于断言的验证技术 这里的断言和软件设计中的断言概念是一致的，都是用来描述待测设计 的属性特性和行为特性的。断言最早的使用可以追溯到t u r i n 9 1 9 4 9 年在高速 自动计算机器会议论文中的论述【2 5 】。 “i no r d e rt h a tt h em a nw 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 e p r o g r a m m e rs h o u l dm a k ean 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 d i n d i v i d u a l l y , a n df r o mw h i c ht h ec o i t e c t l l e s so 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 n t u r i n g 1 4 键的时序部分以及设计的主要特征和属性点插入断言，在整个验证过程中就 会一直监视该特征是否出现，可以同时为开发人员和验证人员提供有效的信 息。 基于断言的验证技术的优点： ( 1 ) 在传统的基于仿真的验证中，验证人员在完成仿真过程中，还需要 去分析波形和日志文件来判断验证过程是否正确，不仅耗时耗力效率低下， 还很容易导致验证的不准确性。使用断言可以在设计开始的初期就考虑到设 计中关键部分的属性与特征，如果断言失败会自动产生错误提示，比较容易 定位问题。 ( 2 ) 在传统的基于仿真的验证中，许多错误要在芯片级的验证中才能发 现，许多缺陷都到了项目的后期才被发现，并且难以定位；在模块级的验证 中使用断言，尽早的进行验证工作，有助于较早的发现设计中的错误，减少 项目的损失。 ( 3 ) 用断言描述的属性和特征具有一定的重用性；在验证过程中，可以 自动收集断言的覆盖率；使用断言减少了验证相关代码的复杂度并且提高了 验证效率。 基于断言的验证技术的缺点： 断言内嵌于设计代码，只能用于检查内部设计的属性；断言的检查是基 于时钟驱动的，所以不适用于检验计算类的和数据转换等错误。 基于断言的验证流程如图2 4 所示【2 6 】： 1 5 哈尔滨工程大学硕士学位论文 图2 4 基于断言的验证沉程图 首先从详细设计说明书中整理验证计划，然后从中抽取出待断言的属性 与特征，接下来在设计代码中插入相应的断言，根据编写的测试向量开始验 证过程，最后根据插入的断言是否全部执行完来判断验证工作是否结束。 当前主流的断言验证技术： ( 1 ) 开发验证库( o p e nv e r i f i c a t i o nl i b r a r y ，即o v l ) 。与名字相同， o v l 是被定义为库的格式，其中预定义了部分模块，使用时直接实例化到设 计代码中就可以使用，使用中不能直接进行扩展，只能通过增加参数和新的 端口来实现【2 7 】。 ( 2 ) 特性规范语言( 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 ) 。p s l 是 从s u g a r 基础上发展出来的断言验证语言，它的验证功能比o v l 强大，p s l 1 6 可以直接在r t l 代码中使用，但是学习起来却需要一定的时间开销嗍。 ( 3 ) o p e n v e r a a s s e r t i o n ( o v a ) 是广泛使用的断言描述语言，o p e n v e r a 是s y n o p s y s 公司开发的，o v a 是在o p e n v e r a 基础上，由s y n o p s y s 和i n t e r 公司将i n t e r 的f o r s p e c 语言融合的结果，目前被s y n o p s y s 公司捐献给 a c c e l l e r a 委员会，成为了s y s t e m v e r i l o g 语言的一部分【2 9 】。 ( 4 ) s y s t e m v e r i l o g 断言( s y s t e m v e r i l o ga s s e r t i o n 即s v a ) 。s v a 是属于 s y s t e m v e r i l o g 语言的一部分，本课题选择的也是s y s t e m v e r i l o g 语言，它是建 立在v e r i l o g 语言基础上的，学习起来较为容易，并且它是兼具有强大的设计 与验证能力的语言( h a r d w a r ed e s i g na n dv e r i f i c a t i o nl a n g u a g e ，h d v l ) ，具 有广泛的应用前景【3 0 】。s y s t e m v e r i l o g 的详细特性将在下一节介绍。 2 2 硬件描述与验证语言