（电路与系统专业论文）面向微处理器验证的分层随机激励技术的设计研究[电路与系统专业优秀论文].pdf

浙江大学硕士学位论文摘要 摘要 随着嵌入式系统功能日益增强，设计复杂度和上市时间( t t m ) 之 间的矛盾逐渐突出，提高功能测试验证的效率和覆盖率是当前数字集成 电路研究的热门领域。本文以嵌入式c p u 的验证为背景，探索数字集成 电路功能验证的激励产生方法，提出一种基于层次化架构的受限约束随 机激励产生方法，可增强激励产生的目的性和提升覆盖率，从而提高处 理器的验证效率。主要研究内容和创新点包括： 1 层次化的随机约束技术。在分层架构下将直接激励针对性强和普 通受限随机激励测试方便的优点相结合，实现从底层处理器信号级到高 层处理器系统级随机激励的逐层抽象，提高测试激励的质量和有效性。 该技术通过测试层、场景层、功能层和指令层，提供灵活的约束参数配 置接口，解决嵌入式c p u 验证中传统受限随机激励方法所面临的参数配 置复杂度高和针对性低的问题，实现随机测试激励在不同粒度范围的高 效可控，缩减测试激励搜索空间，加快验证的收敛速度。 2 可配置功能库技术。通过抽象处理器内部逻辑和外部通信功能， 以处理器功能单元为随机激励的构建基础，产生基于指令和通信接口行 为操作的测试序列流。该技术利用处理器计算与通信的正交性原则，构 建复杂的处理器模拟运行环境，扩大测试覆盖空间。功能库将测试案例 的约束编写与具体的处理器功能实现方法相分离，减少随机测试向量数 目，并可重用于系列处理器验证过程中，显著提高处理器验证效率。 该分层随机激励产生技术成功应用于c k c o r e 微处理器的功能验证 平台。实验结果表明：该方法与创痛受限随机激励相比，在功能覆盖率 浙江大学硕士学位论文摘要 相同的情况下，激励编写量减少6 0 ；在仿真时间相同的情况下，功能 和代码覆盖率分别改善1 0 和5 以上，有效提高处理器验证的质量和 效率。 本文提出的分层随机激励技术对于加快微处理器的功能验证和提高 微处理器的功能覆盖率等方面有一定的参考意义。 关键词分层；随机；激励；微处理器；功能；验证；约束 浙江大学硕士论文 a b s t r a c t a b s t r a c t w i t h i n c r e a s i n gc o m p l e x i t y a n ds h o r t e r p r o d u c t i n gt i m e ，f u n c t i o n a l v e r i f i c a t i o no ft h e l a r g ed i g i t a ld e s i g n ，e s p e c i a l l ym i c r o p r o c e s s o r ， i sa c h a n l l e n g i n gp r o b l e mw h i c hw i l lc o s tl a r g ea m o u n t so fe f f o r t o n eo ft h em a i n r e s e a r c hd i r e c t i o n si se x p l o r i n gt h es i m u l a t i o n b a s e dv e r i f i c a t i o nm e t h o d t h i s t h e s i sp r e s e n t e dan e wm u l t i p l e l a y e rc o n s t r a i n tr a n d o ms t i m u l a t i o ng e n e r a t i o n t e c h n i q u et oi n c r e a s ef u n c t i o nc o v e r a g ea n ds t i m u l u sv a l i d a t i o na n di m p r o v et h e e f f i c i e n c yo fp r o c e s s o rv e r i f i c a t i o n t h eo r i g i n a lc o n t r i b u t i o n so ft h i st h e s i sa r e a sf o l l o w s ： 1 l a y e r e dc o n s t r a i n tr a n d o mt e c h n i q u e i tc o m b i n e dt h ea d v a n t a g e so f s t r o n gt a r g e t e di nd i r e c t e ds t i m u l u sa n dt h ec o n v e n i e n c ei ng e n e r a lr a n d o m s t i m u l u st h r o u g ht h el a y e r e da r c h i t e c t u r e i ta l s or e a l i z e dt h ea b s t r a c t i o nf r o m b o t t o mp h y s i c a ll a y e rt ot o ps y s t e ml a y e rt oi m p r o v et h eq u a l i t ya n de f f e c t i v e n e s s o fs t i m u l u s m u l t i l a y e rc o n s t r a i n t sf r o mf o u rl a y e r s ，t e s t ，s c e n a r i o ，f u n c t i o na n d c o m m a n d ，c a ns t r e n g t h e nt h ec o n t r o l l a b i l i t yo nr a n d o ms t i m u l u sg e n e r a t i o ni n d i f f e r e n tg r a n u l a r i t i e s ，a n dr e f i n et h es t i m u l u ss p a c et os p e e du pt h ew h o l e v e r i f i c a t i o nw o r k 2 c o n f i g u r a b l ef u n c t i o nl i b r a r yt e c h n i q u e b a s e do nt h o s ef u n d a m e n t a l f u n c t i o n a lb e h a v i o ru n i t so fm i c r o p r o c e s s o r , an e wc o n f i g u r a b l ef u n c t i o nl i b r a r y w a sp r o p o s e dt og e n e r a t et w ok i n d so fr a n d o ms t i m u l u sf o ri n t e r n a ll o g i c f u n c t i o na n de x t e r n a lc o m m u n i c a t i o ni n t e r f a c e r e s p e c t i v e l y i te n s u r e dt h e o r t h o g o n a l i t yo fp r o c e s s o rc o m p u t i n ga n dc o m m u n i c a t i n gf u n c t i o n st ob u i l dt h e 浙江大学硕士论文 a b s t r a c t a c t u r a lp r o c e s s o ra p p l i c a t i o ne n v i r o n m e n ta n de x p a n dt h et e s ts p a c e f u n c t i o n l i b r a r ys e p a r a t e df u n c t i o nr e a l i z a t i o nf r o mt e s tc a s ew h i c hr e d u c e dt h en u m b e r o ft e s tv e c t o r sa n d h a db e t t e rr e u s a b i l i t yf o rs e r i e sp r o c e s s o rv e r i f i c a t i o n t h em u l t i l a y e rc o n s t r a i n tr a n d o ms t i m u l a t i o ng e n e r a t i o nt e c h n i q u eh a sb e e n s u c c e s s f u l l ya p p l i e dt oc k c o r em i c r o p r o c e s s o rv e r i f i c a t i o np l a t f o r m a ss h o w n i nc k c o r em i c r o p r o c e s s o rv e r i f i c a t i o ne x p e r i m e n t s ，c o m p a r e dw i t ht r a d i t i o n a l c o n s t r a i n tr a n d o ms t i m u l u sg e n e r a t i o n ，t h ep r o p o s e ds t r a t e g yc a l l e f f e c t i v e l y i m p r o v et h eq u a l i t ya n de f f i c i e n c yo fm i c r o p r o c e s s o rv e r i f i c a t i o n ，w i t h6 0 s t i m u l u sc o d i n gr e d u c t i o n ，w h i l em o r et h a n10 a n d5 f u n c t i o na n dc o d e c o v e r a g ei n c r e a s e t e c h n i q u e sp r o p o s e di nt h i st h e s i sh a dp o s i t i v ee f f e c t so ni m p r o v i n gt h e e f f i c e n c ya n df u n c t i o nc o v e r a g eo fm i c r o p r o c e s s o rv e r i f i c a t i o n k e y w o r d sm u l t i l a y e r ；r a n d o m ；s t i m u l u s ；m i c r o p r o c e s s o r ；f u n c t i o n ；c o n s t r a i n t 浙江大学硕士学位论文图表目录 图目录 图1 1 设计与验证的鸿沟1 图1 2s o c 逻辑设计复杂性2 图1 3 处理器m i p s 性能指标增长曲线。4 图1 4i n t e li a 3 2 系列芯片逻辑b u g 数5 图1 5a l p h a 2 1 2 6 4 激励产生流程9 图1 6g e n e s y s p r o 随机测试发生器的总架构图1 0 图1 7h l t g 激励产生和测试流程1 0 图1 8s t r e s s t e s t 激励产生流程示意图1 1 图1 - 9c k 6 1 0 处理器的流水线基本结构1 1 图2 1 激励产生示意图1 5 图2 。2 验证环境不同层次的测试激励1 5 图2 3 分层随机激励的分层架构1 6 图2 - 4 测试层对各层的约束1 7 图2 5 场景层的配置范围1 8 图2 - 6 分层随机激励的功能流组成1 9 图3 1 分层随机激励的约束组成2 1 图3 2 分层随机激励的约束范围配置2 3 图3 3 功能层的静态约束方式2 4 图3 4 功能层的动态约束方式2 4 图4 1 分层随机激励的功能库机制2 6 图4 2 功能库的转化与驱动2 7 图4 3 内部逻辑功能库的组成2 8 图4 4 功能转换库的转移概率图2 9 图5 1v m me n v 的测试用例执行流程3 4 图5 2s y s t e m v e r i l o g 的常数约束随机3 5 图5 3s y s t e m v e r i l o g 的变量约束随机3 5 图5 4s y s t e m v e r i l o g 的权重约束随机3 6 图5 5s y s t e m v e r i l o g 的数组约束随机3 6 图5 6s y s t e m v e r i l o g 的条件约束随机3 7 图6 1c k c o r e 微处理器的验证环境3 8 图6 2c k c o r e 微处理器的验证技术4 0 浙江大学硕士学位论文图表目录 图6 3c k c o r e 微处理器的三种测试激励4 l 图6 4c k c o r e 微处理器验证平台的分层激励发生器4 3 图6 5 处理器定制示意图4 4 图6 - 6 测试案例的总体实现架构4 5 图6 7 测试案例示意图4 5 图6 8 场景流的信息组织形式4 6 图6 - 9 场景流的产生流程一4 8 图6 10 功能流的产生流程4 8 图6 1 l 功能库管理4 9 图6 1 2 功能库构建示例4 9 图6 1 3 功能库的内部逻辑功能转换示例5 0 图6 1 4 功能库的外部通信功能转换示例5 0 图6 1 5 分层随机激励的文件组织结构5 1 图6 1 6 测试代码的编写量比较5 3 图6 1 7 覆盖率的实验结果5 4 图6 1 8 分层随机激励的约束效用评估5 5 图6 1 9 不同验证方案的b u g 曲线对比图5 6 浙江大学硕士学位论文图表目录 表目录 表1 1 验证的种类和使用范围7 表6 1 处理器定制的配置参数4 3 表6 2 场景层的配置组信息4 6 表6 3 分层随机激励的文件结构和功能5 1 表6 4 受限随机和分层随机的激励比较5 2 表6 5 测试激励的代码重用度比较5 4 浙江大学硕士学位论文 浙江大学研究生学位论文独创性声明 浙江大学研究生学位论文独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工作及取 得的研究成果。除了文中特别加以标注和致谢的地方外，论文中不包含其他 人已经发表或撰写过的研究成果，也不包含为获得逝婆盘堂或其他教育 机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任 何贡献均已在论文中作了明确的说明并表示谢意。 学位论文作者签名：乡长酝凡 签字日期：年月日 学位论文版权使用授权书 本学位论文作者完全了解逝姿盘堂有权保留并向国家有关部门或 机构送交本论文的复印件和磁盘，允许论文被查阅和借阅。本人授权迸江 盟可以将学位论文的全部或部分内容编入有关数据库进行检索和传播， 可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后适用本授权书) 学位论文作者签名： 弓掺取扎 签字日期：年月日缈月 钇何 事物年 名 乳 戳 瑚 燃 阳 翮 解 浙江大学硕士学位论文致谢 致谢 研究生的学习生涯已到尾声，回首这三年，最应该感谢的就是我的 导师谭年熊教授，感谢谭老师对我的悉心指导和深切关注。谭老师治学 严谨，为人谦逊，一直是我学习的榜样。同时，非常感谢严晓浪教授为 我们超大所提供了良好的学习科研环境，以及言传身教，实事求是的科 研态度，这是我取得进步的物质基础和精神支柱。 我也要感谢葛海通老师多年来对我在学习和生活上的关心，以及在 工程项目上的悉心指导和预见性建议。还要感谢浙江大学超大规模集成 电路设计研究所的吴晓波、史峥、沈海斌、何乐年、王国雄、王维维、 竺红卫、罗小华、张培勇、赵梦恋等老师给予我的指导和帮助。 同时也非常感谢黄凯和孟建熠两位师兄在我研究生学习阶段对我的 热情指导和帮助，他们严谨的工作作风，渊博的科学知识，乐观的生活 态度让我十分敬佩，终身受益。感谢李春强和刘兵两位师兄在嵌入式软 件方面对我的指导和帮助。另外，感谢参与c k 6 1 0 设计验证的所有人员， 在完成艰巨任务的同时帮助我顺利完成面向微处理器的分层随机激励技 术的设计研究工作。还要感谢在中天微系统公司一起学习和工作的同学 和同事：黄凯、孟建熠、李春强、丁永林、殷燎、刘兵、陈志坚、冯炯、 彭信民、莫鹏飞、龚帅帅、徐鸿明、傅可威、沙子岩、林锋毅、刘智力、 陈晨、郑丹丹、黄雪维、卢永江、敬擎、王达、廖志宾、项晓燕，刘磊 等。此外，还要感谢黄凯和孟建熠师兄对我研究生论文相关研究工作的 大力支持和无私帮助。 还要感谢浙江大学对我七年的培育，浙江大学的深厚文化底蕴是内 心深处的归宿，浙江大学的求是精神是陪伴左右的座右铭。 还要感谢我的父母二十多年的培养和关怀，一直以来你们对我的关 浙江大学硕士学位论文致谢 心和信任是我积极进取的动力和信念。 最后由衷的感谢在求学生涯中所有帮助过我的老师、同学和朋友们。 张欣 2 0 1 0 1 2 4 浙江大学硕士学位论文 第1 章绪论 1 1 课题背景与研究意义 第1 章绪论 随着集成电路工艺技术的发展，设计的复杂度指数级增加，市场对产品 的上市时间和要求更为严格。它们需要有完备强大的功能，敏锐的反应速度， 高质量低功耗等，这使得系统芯片集成的功能日益复杂，电路规模e t 益增大， 验证的难度日益突出，工作量显著增加，成为整个设计的瓶颈所在。验证在 芯片研发中所占的比例越来越重，在很多情况验证一直到近几年才变得成熟， 从普遍的简单仿真的误解到到对设计全面验证的具体步骤的了解，演化到验 证方法学等，都显示了验证技术的进步之快【1 1 。图1 1 表明了设计与验证的 鸿沟【2 1 。设计生产力的增长持续低于复杂度的增长但是验证生产力依旧低下， 比设计需要投入更多的人力和时间。芯片的验证方法在保持技术更新步伐的 同时，依然是s o c 和i p 模块设计面临的巨大挑战【3 j 。 图1 - 1 设计与验证的鸿沟 在使用高级的抽象的设计方法时，在最终转换映射到产品时不可能做到 没有任何的信息丢失和误解。比如在综合阶段需要将硬件设计语言( h d l ) 层次的设计转换为门级设计时，我们需要用验证来保证转换的正确性，以及 设计意图没有丢失或被更改；在提高抽象层次时，同时给验证带来在仿真时 无法正确解释设计代码的含义等问题【2 1 。在异构设计主导的今天，多数设计 都是软硬件共存，数字模拟共存的。这也是更高系统可靠性带给验证的任务： 浙大学碗士学位论文 第1 章绪论 在芯片级缺陷具有倍增效应时，保证芯片级功能在系统环境中运作良好，为 了提高验证效率，业界提出用高层抽象来解决验证的瓶颈问题比如在 v c r i l o g 、v h d l 中潘加一些高层语言结构，包括任务，线程，控制等。这些 语言不能综合，但能够在验证功能边角问题上发挥作用另外也出现新的验 证语言来提高抽象层次来应对复杂性持续增长的设计等。 1 1 1 验证面临的挑战 功能验证( f u n c t i o n v e r i f i c a t i o n ，f v ) 是当今复杂数字设计的发晨的必要 步骤。硬件复杂度的增长遵循摩尔定律( 1 9 8 5 ) 【1 i ，但验证的复杂性更具挑 战。它在理论上将随着硬件复杂度的翻倍而指数型增长功能验证被广发的 认为是硬件设计的瓶颈所在，高达7 0 的时间耗费。争年的调查研究( 图1 - 2 ) 表明s o c 设计的统计数据，表明设计复杂度( l o g i c g a t e s ) ，设计时间( e n g i n e e r y e a r s ) 和验证的复杂度( s i m u l a t i o nv e c t o r s ) 三者的关系。研究表明了对于 复杂s o c 系统而言，以激励为基础的测试将面临着巨大的挑战，预计在2 0 0 7 年，验证方面的研究在今年的会议和芯片设计公司，e d a 厂商变得炙手可热 2 0 0 0 g ：2 0 0 2 击2 0 t _ o g i eg a k 5 图1 - 2s o c 逻辑设计复杂性 验证工程师将面临四大主要的挑战： 状态空间的处理：状态空间的衡量是面性的第一个挑战。为了在最 大程度上验证芯片的功能正确，验证工程师需要检查每一个可能的 状奄和每一个可能的输入组合以及正确的下一个状态。为了应对状 态空间的爆炸式增长，验证人员将难题分解完成【4 】。验证小组将不 t k 一 浙江大学硕士学位论文第1 章绪论 一次验证整个芯片，而是划分子设计并单独验证，设计变小，难度 降低，验证可管理。最后验证小组再将子设计放到一起验证，确认 各自的工作。 错误行为的检测：第二个挑战就是检查设计在违反预期行为或规格 制定的情况。随着所有可能的传输状态( 一个状态到另一个状态) ， 验证工程师必须确认被测设计的行为在当前状态和输入下正确无误 2 1 。对于验证工程师来讲，验证重点并不是每个硬件的可能的状态， 而是更高的抽象层次，包括将输入分为有效命令集合和数据集合， 关注被测设计在具有功能意义上的输入后出的行为。 缺乏黄金参考模型；缺乏一个黄金参考模型是逻辑b u g 产生的重要 因素之一。在r t l 级有很多的规格模型，包括功能模型、时序模型、 验证模型等。这些模型都是处于对黄金参考模型的考虑。 缺乏全面的功能覆盖度量。缺乏功能覆盖的评估也是导致逻辑b u g 产生的重要因素。功能覆盖评估是用来权衡微体系架构功能特征的 覆盖情况，也就是功能测试的质量。目前的集中覆盖标准和设计的 功能没有直接的联系。比如在流水线的处理器设计中，覆盖标准不 会是所有可能的冲突、停顿和异常，以及其交叉情况全部被验证到【4 1 。 1 1 2 处理器验证的重要性 在集成电路进入s o c 时代后，处理器在生活的各个角落都得到了广泛的 应用。在处理器的硬件设计中，由于芯片的规模扩大【5 1 ( 图1 3 ) 和功能的 扩展繁复，这都导致处理器的验证地位愈发重要，能否发现设计中存在的错 误保证设计正确性也成为关注焦点。所以，处理器的功能验证尤为重要。 浙江大学硕士学位论文 第1 章绪论 图1 3 处理器m i p s 性能指标增长曲线 1 2 国内外研究现状和关键技术 目前的微处理器一般采用超标量，指令预取，跳转预测，乱序执行等先 进技术来提高性能，这样让处理器的结构更为复杂，处理器的功能验证面临 更多的挑战【6 1 ： 巨大的验证空间 处理器的指令集通常包括很多上百条指令，处理器在处理指令流的状态 千变万化，同时不同的操作数以及处理器的外部信号的输入( 比如中断，调 试请求等) 都会改变指令流的处理方式和执行过程，这使得理论上的验证空 间趋于无穷大。如何构建完备的指令产生空间并产生测试案例是面临的难题 之一。 验证高效性的保证 传统的测试案例的解决途径能够应付单个设计特性的验证，对于百万门 级规模的处理器验证必然效率低下。如何提高验证效率，需找不同的解决途 径也是关注的焦点之一【7 1 。 验证充分性的评估 目前，通过功能覆盖率【8 ，9 1 ，代码覆盖率等多种手段来保证验证的充分性。 在验证过程中确定被测对象的正确性，对验证的全面性等进行合理的评估从 进一步指导验证工作，提高验证收敛速度也是验证人员追求的目标。图1 4 总结了i n t e li a 3 2 系列芯片的研究成果【2 1 ，该趋势说明了逻辑错误b u g 指数级 的增长趋势，每代芯片都以3 0 0 4 0 0 的幅度增长。 浙江大学硕士学位论文第l 章绪论 么昌i ：。_ 旦二 图i _ 4 i n t e l1 a 3 2 系列芯片逻辑b u g 数 1 2 1 处理器验证技术的研究现状 目前处理器的功能验证技术主要采用模拟验证( s i m u l a t i o n v e r i f i c a t i o n ) 、 硬件加速验证( h a r d w a r e e m u l a t i o n v e r i f i c a t i o n ) 和形式化验证( f o r m a l v e r i f i c a t i o n ) 。 一、模拟验证( s i m u l a t i o nv e r i f i c a t i o n ) 模拟仿真仍然是最主要的验证手段【1 0 - 2 0 1 它的基本方法是将实际的数 字系统进行抽象，提取模型，施加外部激励信号，观察数字系统的行为来判 断是否实现预期功能，保证设计的正确性模拟验证方式通常分为基于时钟 周期( c y c l e ) 的模拟和基于事件( e v e n t ) 的模拟两种方式事件驱动的模 拟工具有s y n o p s y s 公司的v c s ，m e n t o rg r a p h i c s 公司的m o d e l s i m 等吐 模拟验证的效果主要取决于剥试澈励的有效性，仿真结果的判断和覆盖 率评估这三个方面高层语言搭建的行为模型由于是对设计的抽象描述，所 以仿真速度比比r t l 模型快。在实际应用中，抽象层次随着行为级r t l 级、 门级、开关级的逐级降低，其使仿真速度逐级下降模拟仿真重要组成部分 是澈励的产生，监视器和覆盖率评估 匕如剥试语言s y s t e m v e r i l o g ，v e r a ， e 语言等都支持仿真测试平台的定义等。验证语言并不是可综合的，所以在 形式验证或者硬件仿真中这些测试案例和测试平台不能直接被使用口”。 对于激励而言，产生激励的方式通常有以下三种：直接教励，随机教励 和受限约束激励( 业界多采用该方法) 。对于监视器而言，它的主要任务就是 浙江大学硕士学位论文第1 章绪论 观察模拟仿真是否结束，相应的事件是否发生，标志位是否置起等。一个事 件可以是布尔信号的组合或者是一系列有时间标签的时间组合。对于事件的 组合可以采用断言实现，比如o v a ，s v a ，p s l 等。对于覆盖率而言，它是 衡量模拟仿真的完成情况。目前有很多种方式，比如代码覆盖率( c o d e c o v e r a g e ) ，状态机覆盖率( f s mc o v e r a g e ) 。当然用户可以根据内部信号和 初始状态的设定来进行模拟情况的覆盖。 目前以覆盖率为导向的验证方法【2 2 ，2 3 1 和基于断言的验证方法都是模拟 验证中的热门研究方向。 二、硬件加速验证( h a r d w a r ee m u l a t i o nv e r i f i c a t i o n ) 硬件加速仿真给人的直观印象就是模拟仿真将速度提升了数千倍。所以 对于硬件加速仿真来讲，模拟速度不存在瓶颈，而验证人员编写测试向量的 速度成为速度限制的首要原因2 。在硬件加速验证中，验证工程师可以进行 全片验证，比如移植u n i x 操作系统等。 微处理器的硬件加速验证除了采用商业的硬件加速器外通常采用f p g a 验证被测设计的逻辑功能。f p g a 仿真将逻辑设计转换为编程数据并下载到 f p g a 期间，再利用测试向量( 或目标系统) 产生激励进行验证【2 4 1 。尽管f p g a 能够提供相当于芯片功能的硬件仿真环境，但是错误定位和调试比较困难， 所以验证人员一般在被测设计的基本逻辑设计正确的前提下才进行硬件加速 仿真，这样可以在流片之前移植操作系统和应用程序，评估处理器性能。 三、形式化验证( f o r m a lv e r i f i c a t i o n ) 形式化验证功能强大，通常分为三类：等效性验证( e q u i v a l e n c e c 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 i n g ) 。 形式化验证在处理器的验证领域已经有所成就 2 5 , 2 6 】，其中的定理证明方法由 于需要公式和定理来证明系统的正确性，根据规范抽象属性通过数学逻辑公 式验证等，在学术研究阶段，只适合小规模的设计，所以不做讨论。 等效性验证( e q u i v a l e n c ec h e c k i n g ) 是最成功的形式化验证技术，通常 用在r t l 级到门级的整合，最熟悉的就是前端到后端的功能等价性验证等。 商用的等价性工具有d e s i g nv e r i f y e r 和f o r m a l i t y t 2 7 1 。 浙江大学硕士学位论文第l 章绪论 模型验证( m o d e lc h e c k i n g ) 即设计属性检查工具。模型验证需要完全 的分析被测设计2 8 1 。当模型检查器检测属性失败时，需要产生错误的激励： 从初始状态开始的一系列操作。当模型检查器发现属性正确时，能够确保初 始状态的任何有效输入都不能使该属性检测失败。这就决定了模型检查器无 法很好的处理大型设计。模型验证的重要组成部分包括：被测设计，初始态 集合，需要验证的属性，被测设计所处的环境四个部分。形式化断言验证工 具发展迅速，包括二元判决图( b d d ) ，布尔可满足性( s a t ) ，自动测试产 生算法( a t p g ) 等等。 形式化验证主要用于小规模设计和收敛性的验证【2 9 1 ，目前成功实例都是 局部逻辑功能的正确性验证【2 6 ，3 0 1 。硬件仿真加速的仿真速度快，但错误定位 和调试十分困难。而模拟仿真更适合电路拓扑结合和状态机复杂的功能验证， 可以综合使用各种方法是验证达到要求的结果，在处理器验证中处于主导地 位。下表【3 1 1 列出了主要的测试方式的应用领域。作为模拟仿真的核心技术， 激励产生方法的探索是当前处理器验证的主要研究方向之一 表1 1 验证的种类和使用范围 类型描述设计阶段目标 模拟验证对抽象的数字系统模型施加外设计完成初期功能正确 部激励信号，判断数字系统的行完备 为正确性。 硬件加速验证保证基本逻辑设计正确的前提设计稳定期流片前的 下运行大型的应用程序，比如操最后验证 作系统等。 形式化验证利用定理证明和推导的方法来收敛性设计小规模设 验证设计结果的正确性。 计 1 2 2 处理器验证的激励产生技术 当前处理器的激励产生方法主要有直接激励和随机激励两种【2 7 1 。 一、直接激励 直接激励是在测试中最早使用的方法，需要验证小组书写测试计划和测 试平台文档，保证是对产品规格书的单独释义【3 2 1 。测试计划通常是验证工程 师用黑盒测试的思想对被测设计的理解。该文档的目标就是将产品规格书中 浙江大学硕士学位论文 第l 章绪论 所提到的功能点全部测试完成。直接测试激励就是该测试计划的实现。测试 计划的书写过程可以发现产品规格书的二义性或漏洞。而测试平台文档将着 重描述测试平台的功能特征，比如可以完全使用到所有的被测设计的功能。 两文档将被设计和验证小组同时审阅。 当直接测试激励完成并运行后，通常引入第三方的覆盖率评估标准。比 如行覆盖率，分支覆盖率和t o g g l e 覆盖率。这些覆盖目标是必需但非有效的。 如果没有达到目标，能肯定测试不完全。但是达到目标，却并不意味这测试 完全。经验表明利用黑盒思想的测试计划通常达不到该覆盖目标，需要通过 白盒思想的牢i 、充测试案例才能完成。补充测试案例通产用来覆盖一些特定的 传输序列来保证覆盖率。在成熟的直接激励的测试计划中，通常是用灰盒思 想完成的，既包括被测设计的功能点，又包括设计中的关键逻辑。总的来说， 直接激励测试针对性强，但代码编写工作量大，验证充分性不能保证。 二、随机激励 随机激励则是把激励限定在一定的范围，比如某一范围的指令，或者临 界状态的数据集合等，然后随机产生。随机激励测试代码生成快，测试空间 大，但测试程序随机性强，目的不明确，导致功能覆盖少。其中约束随机激 励，是随机激励的先进形式，它可以指定更为确定的约束范围和约束方式。 随机激励的优点包括：1 有效缩短验证代码的长度，减少验证时间和人力的 投入；2 容易覆盖到边角情况，使验证的覆盖率增大。 约束随机激励在随机激励的基础上增加约束限制，使激励更容易覆盖到 被测功能点。约束激励发生方法根据不同的用户需求产生具有一定针对性的 测试激励，但随机参数配置随着设计复杂性增加而日趋复杂，需要通过较长 的验证时间来获得较高的功能覆盖率1 9 ，3 3 1 。基于覆盖率的随机测试也是重要 研究方向之一，它对验证的自动化具有推进作用【3 4 ，3 5 1 。 1 2 3 激励产生技术的发展现状 目前业界主要通过伪随机激励方法来生成处理器指令流，实现处理器高 效验证。 a l p h a 2 1 2 6 4 t 1 0 1 的测试策略包括四个阶段：p r e i n t e g r a t i o n 阶段、 r 浙江大学硕士学位论文第l 章绪论 t r y a n y t h i n g 阶段、t e s t p l a n n i n g 阶段、s t r u c t u r e dc o m p l e t i o n 阶段。它的测试 环境是经典的处理器测试平台，其中的方法在大量的处理器验证中都会使用。 包括汇编代码的获取方式：手工编写，c 代码产生，工具产生等；包括对环 境的配置和事件的模拟；通过汇编器和链接器得到可执行的二进制代码，下 载到可执行镜像中，运行测试平台，通过被测设计和参考模型的比较得到测 试结果。同时被测设计可以通过断言等手段进行自检查等。通过被测设计在 运行中的信号反馈，得到覆盖率分析，通过自动或手工的方式实现汇编代码 的修改和再次生成。 图1 - 5a l p h a 21 2 6 4 激励产生流程 g e n e s y s p r o 1 1 1 是业界领先地位的处理器和多核处理器的功能验证的测 试程序生成器。凭借测试工具在2 0 多年的发展和经验积累，该工具可应用在 p o w e r p c 架构和非p o w e r 架构的设计上。g e n e s y s p r o 通过按照激励模板编写 测试案例，指令建模和约束求解生成测试指令流。g e n e s y s p r o 利用激励模板 使测试案例可读性变强，可以根据需要配置参数；它可以进行高层处理器架 构建模产生所指定的处理器；它具有自己的约束求解引擎，能够促进测试程 序的高质量。但是它对于繁多的随机约束参数的配置上交代不多，这方面存 在效率不高的问题。 浙江大学硕士学位论文 第1 章绪论 m o d e l i n g e n gu n e e r v e r i f i c a t i o n e n g n n e e r 图1 - 6g e n e s y s p r o 随机测试发生器的总架构图 h l t g 1 4 1 在应用层面关注高层有效激励的产生，是基于功能的测试向量， 主要针对处理器的特殊应用，忽略处理器的硬件细节，没有对处理器运行的 真实系统环境的模拟。 i n s t r u c t i o ns e t：p r o c e s s o r i n p u t e x t r a c t i o n c o n f i g u r a t i o n g e n e r a t i o n 图1 - 7h l t g 激励产生和测试流程 s t r e s s t e s t ”】在马尔可夫模型基础上，根据监视器的反馈信息动态调整激 励产生得到测试激励，具有简单的功能划分，但对处理器所处的运行状态没 有提及，缺乏对激励产生空间的保证。该激励产生方法都侧重于基于指令的 随机测试向量，没有考虑处理器外部行为对处理器内部功能的影响，同时缺 乏对激励受限参数缺乏有效的管理。 浙江大学硕士学位论文第l 章绪论 图1 - 8s t r e s s t e s t 激励产生流程示意图 1 3 论文的研究基础 本课题的研究基础是c k c o r e 嵌入式系列处理器【3 6 ，37 1 ，该系列处理器经 历了第一代单发射七级流水的c k 5 1 0 系列处理器的开发到成熟阶段后，进行 第二代双发射八级流水的o k 6 1 0 系列处理( 图1 - 9 ) 的研发。c k 5 1 0 系列微 处理器验证是基于直接测试的验证方法，而对于c k 6 1 0 的双发射结构允许多 条质量在同一个时钟周期发射，执行，回写等。这使得直接测试方法的已跟 不上复杂的硬件设计的发展速度，故需要新的处理器测试方法。 图1 - 9c k 6 1 0 处理器的流水线基本结构 浙江大学硕士学位论文 第1 章绪论 1 4 论文的研究内容 本文着重研究全面提升微处理器验证效率的关键技术，主要集中在如何 有效地产生微处理器的激励。包括研究构建完备的指令状态空间，解决处理 器理论验证空间不收敛的问题；研究提高处理器激励产生的有效性，从处理 器配置到指令序列上通过随机参数和约束来提高验证效率；研究通过反馈实 现测试自动化和提高验证收敛速度；研究通过功能覆盖率来保证验证的充分 性。 本课题在充分研究国内外处理器激励产生方法和的基础上，提出一种基 于分层思想( m u l t i 1 a y e r ) 的受限随机激励产生方法，该方法的提出和设计 在处理器激励产生的研究中具有较强的创新性和实用性，并将其应用于 c k c o r e 系列处理器的验证平台，研究内容和创新点主要包括以下方面： 通过分层架构的产生方式，精炼处理器的状态激励空间。通过分 层结构实现从高层处理器系统级到底层处理器信号级随机激励的逐 步细化，通过测试层、场景层、功能层，指令层和物理层逐层产生 激励，使处理器的测试激励空间得到精简提炼。该产生方式在随着 测试粒度的增加能够解决指令空间大导致覆盖完整性不够的问题， 在一定程度上能够提高功能覆盖率。 约束参数的灵活配置，提高激励质量。约束是随机验证流程中控 制激励产生的指导框架，处理器的随机约束一般分为软件约束和硬 件约束，该分层受限随机激励方法将软硬件约束与激励的层次化框 架结合起来，有效产生激励流。分层架构下的约束参数配置十分灵 活，设计规模的庞大并不影响约束参数的有序管理。 将基于指令的测试流抽象为处理器操作功能的测试流，实现激励 可控性。在通常的处理器激励产生方法中是以指令集为基本单位来 产生测试序列，在分层随机激励的产生中，将指令层抽象到功能层， 通过定义高层次的功能操作抽象来实现处理器功能的提取，使验证 工程师更注重处理器各个功能之间的协同工作。 提出逻辑功能和通信接口相结合的随机机制，使功能覆盖更完 浙江大学硕士学位论文第1 章绪论 备。在普通的处理器激励产生方法中，指令集构建的逻辑功能测试 序列的技术非常成熟，但是将处理器的硬件环境状态纳入考虑范围 却很少，或者是两者没有联系来考虑。该分层随机激励方法将处理 器的逻辑功能和通信接口结合起来，保证计算与通信分离的正交性， 构建真实的处理器运行环境。 提出功能库的概念，实现同体系架构的处理器验证复用。分层随 机激励产生方法的重要保证是完善的功能库。功能库( f u n c t i o n l i b r a r y ) 是分层随机激励引入的新概念。它是处理器功能操作的具 体实现。功能库将测试案例编写的约束与处理器功能实现相分离， 验证工程师在功能库构建时考虑细节，在测试案例编写时关注激励 约束和流程，有利于实现高质量激励。功能库在同微体系架构的系 列处理器验证中可以实现最大程度的复用，避免重复代码。 1 5 论文的组织结构 本文的组织结构如下： 第一章为绪论，本章首先讨论微处理器验证的背景和研究意义，以及微 处理器功能验证所面临的挑战。接着论述了微处理器验证技术的研究方向， 特别是对其中的微处理器激励的产生技术和发展趋势。同时，