（计算机科学与技术专业论文）x微处理器系统级验证平台的研究与实现.pdf

国防科学技术人学研究生院1 学位沦文 摘要 x 微处理嚣是一款异常复杂的微处理器，具有功能强大的总线接 ，支持总线流水 操作，突发操作以及锁操作等等，该微处理器还_ 支持虚存管理，中断和查询。要在系统 级对x 微处理器进行尽可能充分的功能验证，必须开发一个功能强大、高效易用的系统 级验证平台。 本论文深入研究了目前国际上系统级验证的一般方法及发展现状，深入研究了x 微 处理器系统级验证的具体需求，提出了x 微处理器的系统级验证解决方案，在此基础上 独立完成了支持这一解决方案的、完整的系统级验证平台的开发。该验证平台由平台核 心和辅助工具两部分组成。验证平台核心包括p - b u s 总线协议模型和初始化、内存、 0 、 中断、查询、特殊周期处理等各种外围模型。辅助工具包括格式转换工具、测试向量加 载程序、基于约束的随机测试向量生成工具等。采用该验证平台，用户可以很方便地运 行测试i 甸量并进行模拟结果的正确性判断。验证平台采用高级语言源程序作为输入，提 升了验证的抽象层次，减少了验证的工作量，提高了验证的生产力。为便于验证平台的 开发与调试本论文还开发了个简化的x 微处理器行为级功能模型。 本论文实现了基于事务的验证理念，并充分体现了自测试、因果测试、基于约束的 随机测试等先进的验证思想。 本论文还给出了实模式、保护模式以及虚拟8 0 8 6 模式下运行测试向量的具体实现 方法。 关键词系统级验证验证平台模拟验证自测试 因果测试事务 第1 负 国防科学技术人学研宄生院。产f _ 呛文 a b s t r a c t xm i c r o p r o c e s s o r i sa c o m p l e x o n e ，w h i c hh a s a p o w e r f u lp - b u s t h a t s u p p o r t s m u l t i p r o c e s s o rm o d e ，b u sc y c l ep i p e l i n i n g ，s i n g l e - t r a n s f e ra n d b u r s t t r a n s f e rc y c l e s ，a n ds oo n ， t h em i c r o p r o c e s s o ri sac i s co n ea n ds u p p o r t sv i r t u a lm e m o r ym a n a g e m e n t ，i n t e r r u p ta n d i n q u i r i n gc y c l e t ov e r i f y s u c hac o m p l i c a t e dm i c r o p r o c e s s o ra ts y s t e ml e v e l ，i ti s b a d l y n e e d e dt od e v e l o pav e r i f i c a t i o np l a t f o r mt h a ti sp o w e r f u l ，e f f i c i e n ta n de a s yt ou s e b a s e do nt h es t u d yo ft h es y s t e mv e r i f i c a t i o nm e t h o d sn e w l ya p p o s e di nt h ew o r l da n d a n a l y s i so f t h e i ra d v a n t a g e sa n dd i s a d v a n t a g e s ，a l s ob a s e do nt h er e q u i r e m e n t so ft h es y s t e m l e v e lv e r i f i c a t i o no fx m i c r o p r o c e s s o r as y s t e ml e v e l v e r i f i c a t i o ns c h e m ei s a p p o s e d t o s u p p o r tt h es c h e m e ，ac o m p l e t ev e r i f i c a t i o np l a t f o r mi sd e v e l o p e d ，w h i c hi sc o m p o s e do f a k e m e la n ds o m ea s s i s t a n tt o o l s t h ek e t u e lc o n s i s t so fap - b u sp r o t o c o lm o d e la n ds e v e r a l e x t e r n a lm o d e l ss u c ha sam e m o r ym o d e l ，a ni 0m o d e l ，a ni n t e r r u p tm o d e la n da ni n q u i r i n g m o d e l ，u s e r sc a nt u na n dd e b u gs i m u l a t i o n si nt h ep l a t f o r mv e r yc o n v e n i e n t l y u s i n gt h e p l a t f o r m ，a s e r sw r i t et e s t c a s e si nh i g h l e v e ll a n g u a g e ss u c ha sco ri na s s e m b l yl a n g u a g e s t h a ta r ep r o d u c t i v e f o rt h ep u r p o s eo fd e b u g g i n gt h ep l a t f o r m ，w ea l s od e v e l o pab e h a v i o r a l m o d e lo fx m i c r o p r o c e s s o l i nt h et h e s i s ，w ei m p l e m e n tt 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 ，s e l f - t e s t ，c a u s e a n d - e f f e c tt e s t ， a n dc o n s t r a i n t - b a s e dr a n d o mt e s t w ea l s og i v em e t h o d sf o rh o wt or u ns i m u l a t i o n si nr e a lm o d e p r o t e c tm o d ea n dv i r t u a l 8 0 8 6m o d eo f t h em i c r o d r o c e s s o l k e y w o r d s ：s y s t e m v 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 ，s o f t w a r es i m u l a t i o n s e l f - t e s t ，c a u s e a n d e f f e e tt e s t ，t r a n s a c t i o n 第1 i 页 独创性声明 本人声明所呈交的学位论文是我本人在导师指导下进行的研究工作及取得 的研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含 其他人已经发表和撰写过的研究成果，也不包台为获得国防科学技术大学或其它 教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任 何贡献均已在论文中作了明确的说明并表示谢意。 学位论文题目：! 邀矬理墨墨红丝坠堑垩鱼鲍堡峦量塞盟 学位论文作者签名 日期：训；年i ) 月如日 学位论文版权使用授权书 本人完全了解国防科学技术大学有关保留、使用学位论文的规定。本人授权 国防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子 文档，允许论文被查阅和借阆；可以将学位论文的全部或部分内容编入有关数据 库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。 ( 保密学位论文在解密后适用本授权书。) 学位论文题目：i 邀矬堡墨歪统熟坠堑壬垒啦互窥生塞理 学位论文作者签名：=! ! h曰期：如刁年t 2 ，月如日 作者指导教师签名： 坌雏日期：衫年月衫目 i 越 固防科学技术人学研究生院学 讧沦文 图目录 图卜1 芯片设计的瓶颈 图2 1 测试台， 图2 - 2 测试与验证的比较，。 图2 - 3b u g 发现过程 图2 4 验证进度管理， 图3 1x 微处理器设计的再收敛路径 图3 2 间接验证“修改”转换的汇确性 图3 - 3 验证平台核心的架构 图3 - 4 手工开发程序测试向量 图3 5 后处理时自动比较 图3 - 6 系统级验证平台总体结构 图4 一l 总线控制状态机。， 图4 2b f m 示例 图4 3 处理器发出的总线周期处理， 图4 - 4x 微处理器的存储层次 图4 - 5x 微处理器对不同宽度内存的寻址 图4 6x 微处理器与不同宽度内存的数据接口 图4 7 内存系统模型， 图4 8 内存读写b f m 图4 - 9 典型的查询周期 图4 1 0 $ r e a d m e m h 的语法 图5 1 实模式下l m 内存示意图、 图52b u r s t 读操作的时序比较， ：0 8他心垢m肌巧n鲍弘弘明鹅坦印娩 国防车： 学技术人学研究，上院学位沦文 国防科学技术人学研究生院学位论文 第一章绪论 微处理器是知识经济时代的灵魂，是信息社会的制高点。研制具有自主知识产权的 微处理器对于我国的经济现代化建设，国防建设以及信息安全具有举足轻重的作用“_ “。 目前，作者所在的教研室正在进行几款高性能微处理器的研制。随着芯片复杂度的上升， 验证工作的复杂度和工作量呈指数上升。实现部分的r t l 代码每多一倍，验证的工作量 往往要增加到4 倍甚至更大。相对上世纪末几十万门的芯片系统，目前动辄上千万门的 芯片的验证工作量已无可避免的成为芯片设计的大部分工作。目前，复杂芯片的整个设 计团队往往是验证人员占到大部分，然而芯片系统的t t ( t i m et om a r k e t ) 的重担， 每每仍然都落在项目中的验证阶段。验证的工作量已经占到整个芯片设计工作量的 5 0 一8 0 ，芯片系统要尽快推向市场，目前可以认为验证已经成为极重要的一环，甚至是 最重要的环。对于高性能微处理器的设计而言，验证是一项极具挑战性的工作，尤其 是系统级验汪，对验证人员提出了更高的要求。丌发一个高效、易用的系统级验证平台， 对系统级验证的成功起着至关重要的作用。 1 1 课题的研究背景 随着v l s i 设计的日益复杂，验证的复杂度也连带地以指数倍增的方式不断增加 也就是说，当设计的大小增加为两倍时，耗费在验证上的努力，可能就要增加为四倍。 我们作如下的计算：对于单个的f f ( f l i p f l o p ) ，有两种状态，对其进行完全的验证需 要4 种测试图样。对于z 8 0 微处理器，大约有5 k 门，有2 0 8 个寄存器位和1 3 个主要的 输入，可能的状态转换为2 “，以每秒钟l 百万条指令的速度，需要1 0 5 3 年模拟所有的转 换! 更何况，当前芯片的复杂度远远超过5 k 门! 而且，规模的增大使得功能正确性的保证越来越困难，人们耗费大量的心血对设计 进行各种各样的验证，最终也很难保证芯片1 0 0 正确。i n t e l 公司p e n t i u m 微处理器的 浮点除b u g ，就是一个典型的例子。 p e n t i u m 是i n t e l 的主流微处理器，具有3 1 0 万个晶体管。p e n t i u m 的早期版本存 在浮点除b u g ，漏掉了5 个晶体管，通过对一个“掩膜”进行重新设计而得到修复。i n t e l 公司在“投片”之前对p e n t i u m 进行了标准的验证步骤，包括在高级( h i g hl e v e l ) 软 件模型上进行大量的模拟，对最终逻辑设计进行模拟、仿真，其中硬件仿真器耗资数百 万美元，对整个芯片进行了i o o h z 下的仿真验证，对第一批产品进行了大量的测试，输 入的测试向量高达1 0 ”之多，但是依然漏掉了浮点除错误，这说明，对于如此复杂的系 统，验证做到面面俱到是十分困难的。i n t e l 公司的浮点除b u g 之所以存在，并不是工n t e i 公司为了提前上市而“省略”了验证的某些步骤。这也从另一个方面表明，验证只能指 第l 页 国防科学技术人学研究，卫院学何论文 出设计存在错误而不能保证设计不存在缺陷。 但是，尽管验证如此之复杂，难度是如此之犬，人们也不得不挖空心思尽量保证没 计的f 确性，因为芯片重制的代价实在太大了。以i n t e l 的浮点除h u g 为例，i n t el 最 终收回了所有存在h u g 的处理器，造成直接经济损失4 7 5 亿美元。 在电子产业的过去十年问，是由e d a 厂商领军，他们将努力的重点，放在布局靠线 以及逻辑综合的自动化上同时也获得了相当大的成功。不过在这段期间罩，设计功能 的验证，相对地就比较受到大家的忽视。由于现今a s i c 和系统设计的复杂度只渐提高， 功能验证已经成为整个系统设计的主要瓶颈( 见文献 3 - 5 ) 。据报导指出，设计团队通 常必须将其设计时间与设计资源的5 0 8 0 ，耗费在功能验证上，如图i - l 。 1 9 9 6 3 0 万门 2 0 0 0 i 百万门 代码验证综合 p & r 3 0 4 0 5 0 8 0 代码验证综合 p a r 图卜l 芯片设计的瓶颈 验证的主要任务是保证设计与其功能描述相符合，在设计流片之前找到并排除设计 中的错误。 验证追求的主要目标是效率和品质。所谓效率是从验证工程师的工作量这个角度 来谎的，可以用验证工程师为完成某个特定的验证计划而付出的劳动来衡量。采用尽量 少的测试码覆盖尽量多的功能是i c 验证工程师们永恒的追求。提高验证的效率可以缩短 整体验证时间，从而保证产品的上市时间，提高产品的最终获利能力。所谓品质，是从 验证所达到的效果这个角度来说的，验证的品质主要用功能覆盖来衡量。为了提高产品 的一次流片成功率，从而降低昂贵的芯片重制风险以及由此带来的经济损失，必须使功 能覆盖率尽量趋近 0 0 。 验证技术己经落后于设计和制造能力，形成了一个验证鸿沟，而且这个鸿沟还在不 断扩大，为了解决验证鸿沟问题，为了获得更好的验证效率和更高的验证品质，人们付 出了很大的努力，提出了各种各样的验证方法。在功能验证领域，全球各大e d a 厂商都 提出了自己的解决方案，包括c a d e n c e 的i n c is i v e 验证平台、s y n o p s y s 的d i s c o v e r y 验证平台、m e n t o rg r a p h i c s 公司的基于平台的设计与验证、v e t is i t y 公司以e 语言和 s p e c m a ne n t e 为基础的功能验证解决方案，等等。 虽然人们在如何提高验证效率和品质方面观点不尽相同，但最基本和最重要的几点 却是大家公认的。第一，若要改善大型化复杂设计的功能验证效率，最重要的一步，就 是提升验证环境的抽象化程度，抽象化程度越高，验证工程师所付出的劳动就会越少， 第2 页 国防科学技术人学研究生院学位沦文 验汪效率也就会越高。第二，除了提升抽象层次之外，还必须将一些繁琐、重复而耗时 的工作自动化，这包括测试程序的生成、输出结果的检查，等等。第三，为了避免对某 些功能的一而再、再而三的重复验证，必须采用一种行之有效的评测功能覆盖率的方法。 第四，为了减少重复的劳动，还必须重视重用，包括单个设计内的重用、设计间的重用 甚至不同设计团队之间的重用。 目前，作者所在的课题组正在进行一款微处理器芯片( 在后面的叙述中称为“x 微 处理器”) 的研制。x 微处理器芯片是一款与i n t e l 公司p e n t i u m m m x 微处理器兼容的芯 片，其晶体管数达4 5 0 万之多，对于如此复杂的一个芯片，其验证的难度已经达到了一 个相当的高度。为了对x 微处理器芯片进行充分的验证，为了获得较高的验证效率和验 证品质，采用传统开发测试程序的方法已经显得力不从心，必须将丌发测试程序的抽象 级别提高到可执行程序级。为此，本课题开发了x 微处理器的系统级验证平台，在该平 台下，可以很方便地加载测试程序和进行模拟结果的分析。根据x 微处理器芯片的设计 实际，模块级的验证很难做充分，这就对系统级的验证提出了更高的要求。作者认为，x 微处理器芯片的验证对于系统级验证平台的需求十分迫切。 1 2 课题研究的主要内容 为了建立一个简单、易用而可靠的系统级验证平台，以便对x 微处理器芯片进行充 分的验证，同时达到高效和高品质两个验证目的，本课题在如下几个方面展开研究。 一、x 微处理器系统级验证解决方案 x 微处理器是一款相当复杂的芯片，对其进行系统级验证具有很高的难度，这些难 度包括复杂的总线协议，存储管理，多任务等等。作者在对x 微处理器j 占片所面临的验 证问题进行详细分析的基础上，提出了系统级验证的总体解决方案。 二、系统级验证平台的开发 对于高性能微处理器的设计而言，验证是一项极具挑战性的工作，尤其是系统级验 证对验证人员提出了更高的要求。开发一个高效、易用的系统级验证平台，对系统级 验证的成功起着至关重要的作用。开发系统级验证平台的主要工作是验证环境的建立， 包括平台核心的p - b u s 总线协议、内存系统、i o 系统、中断系统和查询系统等部分的 建模工作以及各种辅助工具的开发。 三、利用验证平台进行x 微处理器系统级验证的实现方法 在验证平台开发的基础上，作者研究了利用该平台进行实际的x 徽处理器系统级验 证的实现方法，包括：如何进行初始化测试，如何在实模式、保护模式以及虚拟8 0 8 6 模式下运行测试向量等等。 四、x 微处理器行为级功能模型 本课题的研究与x 微处理器芯片的逻辑设计是并行开展的，在作者进行系统级验证 第3 页 国防科。学技术人等：研究生院学位论文 平台的研究时，x 微处理器芯片的逻辑设计还没有全部完成。为了检验验证平台本身的 讵确性，作者开发了一个简化的x 微处理器行为级功能模型，利用该模型与验证平台进 行联调。另外在进行实际的系统级验证时，还可以利用该功能模型产生期望结果。 五、离效验证的进一步研究 最后，为了进一步达到高效和高品质两个验证目的，作者研究了目前国际上比较先 进的系统级验证方法，将其中先进的验证思想运用到x 微处理器的系统级验汪中，这些 先进思想主要包括基于事务的验证、自测试、因果测试、基于约束的随机测试、基于功 能覆盖的验证等。 1 _ 3 论文的结构 论文首先在第二章对系统级验证加以简要介绍，主要包括功能验证的基本实现方 法国际上系统级验证和功能验证的研究现状，并由此总结出系统级验证的发展趋势。 接下来在第三章介绍x 微处理器系统级验证的总体解决方案，在第四章介绍系统级验证 平台的_ 【= 发，在第五章介绍如何利用本课题开发的系统级验证平台运行测试向量，这三 章构成本论文的主体部分。最后，在第六章对本论文的工作进行了总结，并根据作者的 亲身经历和体会，提出未来工作展望。 1 4 本论文的研究成果 本论文对微处理器的系统级验证进行了研究和探讨，提出了x 微处理器的系统级验 证解决方案，并开发了一个用于支持该方案的系统级验证平台，包括平台核心和几个辅 助工具。本论文开发的验证平台实现了基于事务的验证理念，并充分体现了自测试、因 果测试以及基于约束的随机测试等先进的验证思想。以第一作者在第八届计算机工程 与工艺全国学术年会上发表文章一篇( 见本文附录) 。 第4 页 国防科学技术人学研究生院学侮论文 第二章系统级验证概述 2 1引言 验证是判断设计是否满足功能描述要求的一项技术。根据验证层次的不同，可以将 验证分为模块级、子系统级以及系统级验证。 在模块级验证阶段，设计人员的关注重点是功能和时序的细节验证，保证这些模块 达到技术规范的要求，没有明显问题存在。其目标是尽可能多地发现设计错误，因为模 块级验证是发现并纠正这些错误成本最低和最有效的阶段。h d l 仿真器是这一阶段理想 的工具，因为它易于使用而且纠错能力强。对于有模拟混合信号模块的系统，这些模块 也必须象数字电路的功能验证一样执行类似的验证。目前，已经有较好的针对模拟混合 信号模块验证的专用商业工具，例如，m e n t o r 公司的a d v a n c em s 验证套件工具便是其 中之一。通过该套件工具，m o d e i s i m 为模拟m d l 行为仿真以及模拟模块的s p i c e 仿真提 供了平滑的接口界面。该界面允许在同一个纠错环境中对数字和模拟事件的仿真进程进 行同步处理和查看。a d v a n c em s 模拟器针对复杂模拟混合信号设计的验证工作提供了 单一内核的验证环境。 对所有模块完成充分验证之后，将进入模块集成阶段，多个模块组成更高层次的模 块即构成子系统。在子系统验证阶段，模块间通信、控制、时序和协议实现对确保子 系统的功能正确性都是非常重要的“：因此，通过执行协议检查或采用断言来验证总线 数据交换的工具都是非常有用的。硬件加速仿真工具或仿效验证工具可以在这一阶段配 合使用。 系统级验证涉及各个模块的进一步集成以及设计流程的其余部分，例如设计的嵌入 式软件和物理实现的过程。在设计人员将较小模块集成进越来越大的模块过程中，需要 仿真的内容越来越多，运行时闻越来越长，设计验证要求开展更多仿真工作，提出了多 项验证任务的需求，比如芯片和系统的功能测试，设计综合后与布线后结果的验证。在 这一验证层次，也可以使用等效检查、硬件仿真器阵列或仿效验证工具，确保整个设计 在后端处理过程中没有改变设计的任何特性，这些通常被称作回归测试。采用硬件仿真 器阵列可以为用户提供比较高的数据吞吐能力，对规模较小的测试向量测试提供完备的 解决方案。对于规模较大的测试向量测试则可以采用仿效验证工具( 如v s t a t i o n ) ，因为 它拥有验证大规模芯片设计的能力和容量。硬件仿真器阵列和仿真验证工具是互为补充 的解决方案，可以在不同的应用环境中加以有效使用。 根据是否可以对内部信号进行直接控制和观测的不同，可以将功能验证分为黑盒 子、灰盒子以及自盒子验证( 见文献 7 ) 。 第5 页 国防科学技术人1 学研究生院学f t 论文 采用黑盒子进行功能验证，验证工程师不知道设计的任何实现细节。所有的验证都 必须通过接口完成，不能对内部的状态进行直接访问，对内部的结构和实现没有太多了 解。这个方法有一个明显的缺陷，那就是可观测性和可控性比较差。采用黑盒子验证， 通常比较难于没置一组感兴趣的内部状态，对某些功能进行分离也比较困难。对输入的 响应进行观察以及对错误的定位也同样比较困难。这种困难来源于错误发生的时刻和在 待验证设计( d e s i g nu n d e rv e r i f i c a t i o n ，简称d u v ) 的输出接口上检测到错误的时刻 之间存在比较跃的延迟。黑盒子验证的优势在于它不依赖于任何特定的实现。无论设计 是用单个的a s i c 、多个f p g a 还是电路板或者用纯软件实现，都没有影响。黑盒子验证 是一种真正的一致性验证，可用于验证一个特定的设计实现了描述的功能，而不管设计 是如何实现的。在非常巨大和复杂的设计中，黑盒子验证需要对设计进行某些不影n 向功 能的修改，以便增加可观测性和可控性。这方面的例子包括：设置一组软件可访问的寄 存器( 这些寄存器不用于“正常”的操作) ，用于方便观察和控制内部状态；修改被处理 数据的长度以便使验证时间最小化。它们通常在第一次原型系统的集成阶段颇有价值。 在三种方法中，黑盒子是唯一一种能够使功能验证与设汁实现并行进行的方法。 自盒子的方法对待验证设计的内部结构和实现完全可见，也具有完全可控性。这种 方法的优点在于能够快速地设置感兴趣的状态和输入组合，或者分离特定的功能。白盒 子验证可以很容易地在验证的过程中对结果进行观察并在输出与期望结果不致时立即 报告错误。然而，这种方法与特定的实现紧密相关，并且不能用于不同的实现或者将来 的二次设计。白盒子验证还需要验证工程师对设计实现的细节有相当的了解，以便正确 生成有意义的条件以及合理地确定对什么结果进行观测。白盒子验证是黑盒子验证的有 益补充。该方法可以保证与实现有关的特性的正确性。 灰盒子验证是介于黑盒子验证和白盒子验证之间的一种折中方案。黑盒子的方法可 能不能验证设计的所有部分，而白盒子验证不具备可移植性。与黑盒子验证一样，灰盒 子验证通过最顶层接口对设计进行观测和控制。但是，一般而言，采用灰盒子的方法最 主要是验证与特定实现有关的重要特征。虽然对于不同实现下均相同的验证，也可以采 用灰盒子验证但这种方法不会比黑盒子的方法来得更有效。 从具体实现的角度，又可以将验证分为模拟、仿真以及形式化验证三种方法。 软件模拟是采用e d a 软件( 模拟器) 对设计进行验证的方法，是在设计验证过程中 使用最为广泛的种方法“1 “。软件模拟可以用于从电路级到行为级甚至系统级的所有 设计层次，在各个层次都有e d a 工具支持。软件模拟的最大优点是易于使用且纠错能力 强。软件模拟不能保证设计1 0 0 的正确性，因为对设计运行所有可能的激励是不现实 的”1 ，但通过充分的模拟，可以尽量多地找出b u g ，提高对设计的信，t i 。 硬件仿真可以使目标设计在真实的系统环境( 如实际的操作系统和应用软件) 下运 行，并且具有速度快的优点。然而，硬件仿真不能用于设计的所有层次，只有当设计流 程到达逻辑门一级时才能实现，而逻辑网表只有在设计流程的后期才能获得。另外，硬 第6 页 国防科学技术人。学训究_ ：院学位论文 件仿真不具备友好的故障诊断与调试接口，只能确定测试是否通过，而不能指明错误自i 一 具体位置，因此，当初期错误较多时，不利于使用仿真的方法m 。与软件模拟一样，硬 件仿真亦不能保证设计1 0 0 的正确性。 形式化验汪可以保证设计i o o 的正确性，弥补了软件模拟和硬件仿真的不足，但 遗憾的是t 形式化验证存在状态空间爆炸性问题】，只适合处理比较小的设计或者进行 模块级的验证，对于大型的芯片或者系统，目前形式化验证仍然无能为力。在现今的芯 片验汪领域形式化验证还只是一种辅助手段，仅在少数情况下使用( 如i n t e l 公司对 p e n t i u m4 微处理器的浮点执行单元和指令译码逻辑的验证便使用了形式验证的方法， 见文献 9 ) a 值得说明的是，在有些情况下，采用形式验证的方法相当有效，如时钟树 生成莳后或者缓冲器插入前后逻辑一致性的检查”1 。形式化验证分为等价性检查和模型 检查两种。等价性检查最常见的应用是对两个网表进行比较，保证对网表的某些后处理， 如扫描链的插入、时钟树的综合以及人工修改等，没有改变电路原有的功能。等价性检 查的另一种应用是检查r t l 代码与门级网表的一致性。如果人们完全相信综合工具的能 力，则这种检查是不必要的。然而，综合工具是一个大型的软件系统，它依赖于算法和 库信息的正确性。历史表明，这种软件是必然存在b u g 的。在综合工具出现b u g 时，等 价性检查可用来发现这种错误。少数情况下，等价性检查被用来检查两个r t l 描述的逻 辑等价性。有时，人们为了得到更好的综合结果，对设计进行了少量的修改，但并没有 改变设计的功能，这时，就可以利用等价性检查保证两个r t l 描述在功能上是等价的。 例如，数字设备公司( d e c ) 的工程师们利用等价性检查发现了一个由综合引起的错误。 被验证的设计采用了一个合成操作符，该操作符在对4 8 位以上的数据进行处理时将产生 错误的结果，在文档中已经明确地说明了这一点。由于综合工具不知道文档所描述的信 息，从而产生了无效的逻辑。采用等价性检查很快发现了这个错误，如果采用门级模拟， 浚错误将很难被发现。模型检查是形式化验证技术较新的一种应用。利用模型检查，可 以形式化地证明或者反驳一个设计的断言或者特征。例如，模型检查可以判断设计中所 有状态机的不可达或者分离的状态，更强的模型检查可以判断是否发生死锁。接口是另 一类能够被形式化验证的断言。采用形式化的描述语言，可以描述有关接口的断言，然 后用工具证明或者反驳之。模型检查技术的最大困难在于通过对设计描述的解释，确定 对何种断言进行证明a 在所有的断言中，仅有一个子集能够被切实有效地证明。当前的 设计还不能证明高层次的断言，以确保复杂的功能已经被正确地实现。人们希望，给定 特定的寄存器设置，一组a t m ( 异步传输模式) 单元将产生某种形式的输出结果。遗憾 的是，模型检查技术还没有到达那个层次。 另外，验证与测试台( t e s t b e n c h ) 以及测试是有区别的。 验证与测试台具有紧密的联系，但是验证不仅仅是一个测试台，或者说是一组测试 台，而是一个论证某个设计之功能正确性的过程。在这里，我们强调的是过程，也就是 说，为验证某个设计之功能正确性所付出的全部努力，部包括在验证的范畴之内。而测 第7 页 一 国防科学技术人学研究生院学化沦文 试台通常指的是为某个设计产生输入序列( 激励) 的一段代码。该代码一般用v e t il o g 或v h d l 实现，还可能包括外部的数据文件或c 例程。测试台为待验证设计提供输入并监 视其输出( 如图2 一1 ) 。 图2 一l 钡0 试台 测试是容易与验证混淆的一个概念。测试的目的是检查制造的正确性，而验证的目 的是保证设计与其功能描述相符合，如图2 2 。在测试阶段，检查芯片与用于制造的网 表的一致性。测试通过测试向量完成。这些测试向量的目标不是检验设计的功能，而是 检验设计中的各个物理位置能否从0 变到1 以及从l 变到0 。已测试的物理位置和总共 需要测试的物理位置的比值被称为测试覆盖。为了使测试覆盖最大化，测试向量通常自 动生成并辅以一个被称作a t p g ( a u t o m a t i ct e s tp a t t e r r lg e n e r a t i o n ) 的过程使测试 向量最小化。测试和测试覆盖依赖于将内部物理位置设置为1 或者0 ( 可控性) 并随后 观察它们是否被正确设置( 可观测性) 的能力。某些设计具有很少的输入和输出，但却 具有大量的可能状态，这就需要一个较长的过程对所有内部物理位置进行观察和控制。 典型的例子就是电子手表，只有3 或者4 个输入以及很少的输出。但是，如果该手表具 有日历功能，它将有数以亿计的可能状态，为使该设计遍历其所有状态，将耗费数百年! 硬件设计制造 验证测试 图2 - 2 测试与验证的比较 2 2 系统级验证的发展概况 大规模集成电路设计已经逐渐进入s o c ( s y s t e mo nac h i p ) 的时代，为了解决越 来越复杂的系统级验证问题，全球各大e d a 厂商都在加紧系统级验证方面的研究，各自 第8 页 国防科学技术人学研究生院学位论文 都提出了自己的系统级验证解决方案。 、c a d e n c e 的i n c is jv e 验证平台 c a d e n c e 的i n c i s iv e 验证平台是系统级验证解决方案的典型代表。根据c a d e n c e 对 当今系统级验证的理解，即：项目的各个部分之间、项目之间和设计链之间的脱离是导 致低效率的验证方法的根本原因，c a d e n c e 提出了统一的验证方法学。c a d e n c e 认为，统 一的验证方法学解决了目前验证所面临的绝大部分挑战，同时使整体验证速度和效率达 到最优。 c a d e n c e 公司的i n c i s i v e 验证平台，是专为纳米尺寸设计而推出的单内核验证平台， 它是嵌入式软件、控制、数据通路和模拟混合信号以及r f 设计的统一平台。这种统一 的设计方法学可以使验证平台的开发时间、验证运行时间和调试时问大大缩短，从而使 整个的设计验证时间缩短5 0 以上。 i n e is i r e 平台内建支持v e r i l o g 、v h d l 、s y s t e m c 、s y s t e m c 验证库、规范语言 p s l s u g a r 、算法开发和模拟混合信号( a m s ) 。它实现了十分强大的设计功能集成。 c a d e n c e 的验证方法学的核心是f v p ( f u n c t 【o n a lv ir t u a i p r o t o t y p e ) 的建立和 应用，f v p 是一个事务级的功能虚拟原型，在整个验证过程中起着不可或缺的作用，f v p 的运行速度非常快，从而使结构级性能分析、早期嵌入式软件验证都变得非常理想。f v p 还为模块级验证提供了快速的全芯片环境。c a d e n c e 提出的统一的验证方法学不仅可以 用于验证流程的各个阶段，而且适用于各种设计领域。统一的验证方法学着重于s o c 设 计的验证，同时也适用于单个的子系统。统一的验证方法学在用于完全自顶向下的设计 时，将取得最大的好处。在甩于自顶向下与自底向上相结合的设计时，统一的验证方法 学也是可行的，只是获得的好处不如完全的自顶向下设计那么明显。为了帮助验证团队 从当前使用的验证方法学逐步转向统一的验证方法学，c a d e n c e 还提供了在同一验证团 队中使用多种验证方法学的标准。 二、s y n o p s y s 的d i s c o v e r y 验证平台 s y n o p s y s 公司也推出了d i s c o v e r y 验证平台作为自己针对系统级验证的解决方案。 s y n o p s y s 公司的d i s c o v e r y 验证平台，是一个提供高性能和在所有平台组件之间高效交 互使用的统一环境，这些组件包括混合h d l 模拟、混合信号、系统级验证、断言、验证 i p 、代码覆盖、功能覆盖、测试台和形式分析。d i s c o v e r y 验证平台包括s y n o p s y s 的v c s h d l 模拟器、v c sm x 混合h d l 模拟器、用于系统级验证的c o c e n t r i cs y s t e ms t u d i o 、 l e d a 可编程r t l 检查器、v e r a 测试台自动工具、m a g e l l a nh y b r i dr t l 形式化验证、 d e s i g n w a r e 验汪i p 、形式等价性检查、用于混合信号仿真的n a n o s i m 和h s p i c e 。 s y n o p s y s 公司还大力支持a c c e i l e r as y s t e m v e r i l o g 语言，以实现更先进的可验证 设计( d e s i g nf o rv e r i f i c a t i o n ，简称d f v ) 方法。d i s c o v e r y 验证平台中先进的验证 技术与s y s t e m v e r il o g 的结合，可以解决更为复杂的验证。s y n o p s y s 的可验证设计方法 能够帮助工程师极大地提高设计能力。这种新的方法使用改进后的设计规范驱动验证( 其 第9 页 国防科学技术人学研究生院学f 论文 中含有断言。功能、简明编码和层次化芯片验证等技术) ，确保将验证贯穿于设计之中，降 低因功能错误而进行高成本再流片的风险。 三、m e n t o rg r a p h i c s 的验证解决方案 m e n t o tg r a p h i c s 提出的验证解决方案包括了v s a t i o n 仿真系统、一流的咨询服务 以及先进的硬件加速仿真策略知识。高性能v sr a t i o n 硬件加速仿真系统能为各种复杂设 计提供全面的功能强大的验证环境，并通过在单个平台上提供的多次引用模式，实现对 多个异步时钟同时建模。v s t a t i o n 仿真器独特的协同建模技术还可在几百k h z 范围内提 供高性能仿真加速，与软件模拟相比，其性能提高了近一万倍。 m e n t o t 公司还提出了s e a m l e s sc v e 嵌入式系统软硬件协同验证解决方案。通常， 嵌入式软件的开发会滞后于硬件开发，特别是软硬件的集成调试，必须等到物理原型生 产出来以后，所以无法在设计的早期发现软硬件接口之间的问题。一旦硬件原型有错， 修改后还必须重新生产，然后再进行调试。整个设计过程排错困难，周期长，投入高。 s e a m l e s sc v e 将嵌入式软件开发工具和逻辑仿真器结合起来，使项目丌发小组在物理原 型( 电路板或芯片) 生产出来之前，就能够使用同一个系统模型进行高性能的软硬件协 同验证，使软件和硬件开发成为并行的过程，从而及早发现并改正软硬件接口中的错误， 缩短设计周期，减少投入。s e a m le s sc v e 还可以按照用户的配置来运行，使设计人员既 能在需要时观测到所有的软硬件交互细节，又能通过不同的优化策略来加速软件代码的 执行，提高协同验证的效率。其主要特点包括： ( 1 ) 缩短嵌入式系统( 板上系统和片上系统) 的开发周期： ( 2 ) 减少硬件原型的设计反复次数： ( 3 ) 加速设备驱动程序和硬件诊断程序的调试； ( 4 ) 无须更改软硬件设计； ( 5 ) 一致性存储器服务器和动态优化技术能够提供最佳的协同验证性能； ( 6 ) 支持业界主要的微处理器和控制器模型： ( 7 ) 接口开放，能够集成第三方的设计和验证工具。 四、v e t i s i t y 的验证方案 作为功能验证自动化的领导厂商，、e r i s i t y 公司的验证方案主要是e r m ( er e u s e j e t h o d o o g y ) 技术，该技术能够运用于可重复使用、高品质的验证组件开发工作上。通 过e r m 技术的协助，v e r i s i t y 公司为e v e ( ev e t i f ic a t i o nc o m p o n e n t ) 的开发工作， 提供全面性的指导方针。e r m 技术提升所有e v c 的生产力，并确保其可交互运用性。 e 剐技术可以大幅提升功能验证的产出能力，尤其对先进的a s i c 、s o c 以及处理器 而言，其效果更是显著。e r m 技术囊括了各种e v e 开发工作的最佳范例并憋其整合成 一套完整的方法论。e r m 提供一个可共享的e v c 运用模型，不论和e r m 兼容的所有e v c 来源为何，皆可以确保其完美地进行交互运用。 通过e r m 技术建立可重复使用的验证环境，可以使验证作业被重复使用，可直接提 第l o 页 凼防科学技术人学缈 究生院学1 口硷文 供更高的生产力，并可提升芯片的品质，以及整体的验证投资。 e r m 技术包含了3 项主要的要素在内： ( i ) e v e 丌发作业的晟佳范例v e “s t y 和他的客户与伙伴进行合作，整合了各 项开发作业上的标准，以提升e v c 的一致性、可重复使用性，以及可交互运用 性。这些标准，和e v c 的架构、命名方式、编码方式、安装、配置、文件分割， 以及包装组合等方式有关。 ( 2 ) 新的s p e c m a ne l i t e 功能可以让和e r m 兼容的e v c 使用新的s e q u e n c e s 功能，产生复杂的多重化处理方案( m u l t i t r a n s a c t i o ns c e n a r i o s ) ，并将其 同步化。 ( 3 ) 知识的转移v e r i s i t y 可以为客户及e v c 的开发厂商，提供e r m 培训课程、 3 个”黄金版e v c ”( 理想化的编码范例) ，以及许多的相关文件。v e t is i t y 也可以提供开发厂商模板，以作为e v c 的使用者指南与训练课程。这些模板， 能够以最正确的方式，将相关信息传达给e v c 的使用者。 另外，e r m 具有较好的兼容性。为确保e v c 能够和e r m 确实兼容，v e r i s i t y 提供 了一份e 黼检查表。检查表内详述了为达到e r m 兼容的状态丌发厂商必须完成的重要项 目。和e r m 相容的e v c 必须在组件本身之内，包含e r m 检查表报告。这样，就可以让 使用者评估每一个e v c 在其验证环境内的可交互运用能力。 纵观国际上关于系统级验证方法的研究，到目前为止，人们还没有达成很好的一致 意见。验证领域可谓是一个八仙过海，各显神通的领域。对于具体的设计，人们还必须 根据具体的情况选择合适的验证方法。而且，在实际的工程实践中，往往需要采用一系 列的技术和方法，以期尽可能多地发现设计中的错误1 1 ”。从各种五花八门的方法中，本 课题总结出系统级验证的未来发展方向。 、统一的验证方法学 验证方法学的统一包括设计环境的统一和数据库的统一。在整个设计与验证流程 中，采用统一的数据库与设计环境，不仅可以减少各种转换引入错误的可能性，而且可 以减少学习成本。 二、