（电子科学与技术专业论文）基于约束求解的微处理器功能验证程序自动生成技术研究.pdf

国防科学技术大学研究生院学位论文 a 。b s t r a c t t o d a y ，w i t ht h em i c r o p r o c e s s o rb e i n gm o r ea n dm o r ec o m p l e x i t y ，f u n c t i o n a lv e r i f i c a t i o ni s w i d e l ya c k n o w l e d g e d a st h eb o t t l e n e c ko f m i c r o p r o c e s s o rd e s i g n a r c h i t e c t u r e l e v e lv e r i f i c a t i o n c a nf i n df a i l u r e si nd e s i g nf l o we a r l y 。w h i c hc a ng r e a t l yr e d u c el o s s s i m u l a t i o ni ss t i l lt h em a i n v e h i c l ef o ra r c h i t e c t u r e l e v e lf u n c t i o n a lv e r i f i c a t i o n b u tt h eg e n e r a t i o no ft e s tp r o g r a mf o r s i m u l a t i o nb yh a n d si sv e r yl o we f f i c i e n t ，a n di t sf a i l u r ep r o b a b i l i t yi sh i g h t h e r e f o r e ，t h e a u t o m a t i c g e n e r a t i o no ft e s tp r o g r a mp l a y s a m a j o rr o l e i nt h ev e r i f i c a t i o no fm o d e m m i c r o p r o c e s s o r s e x i s t i n gt e s tp r o g r a mg e n e r a t o r sc a l l tv e i l f yt h ew h o l ed e s i g n t h e i rm e t h o d sf o rm a k i n g a r c h i t e c t u r em o d e la r ec o m p l e x w h a t sm o r e ，m o s to ft h e mc a l lb ei n t r i n s i c a l l yr a n k e d a u t o m a t i cr a n d o mt e s tp r o g r a mg e n e r a t o r ，w h i c hr e s u l t si nl o wv e r i f i c a t i o ne f f i c i e n c y b a s e do no u ro w nf r a m e w o r kf o rm i c r o p r o c e s s o ra r c h i t e c t u r e l e v e lt e s tp r o g r a mg e n e r a t i o n ， t h et h e s i sc o m p l e t e st h ef o l l o w i n gw o r k ： f i r s t l y ，w ed e s i g nac o n s t r a i n td e s c r i p t i o nl a n g u a g ew i t hs i m p l es y n t a xa n de a s ye x p r e s s i o n s a n di m p l e m e n tt h ec o m p i l e r a i m i n ga ta l lk i n d so fc o n s t r a i n ti n s t a n c e si na r c h i t e c t u r el e v e l f u n c t i o n a lt e s t ，i tc a nd e s c r i b et h ec o n s t r a i n tr e q u i r e m e n tc l e a r l y a tt h es a l _ n et i m e ，w e i m p l e m e n tac o m p i l e rf o r t h ec o n s t r a i n td e s c r i p t i o nl a n g u a g e ，w h i c hi si n d e p e n d e n to f a r c h i t e c t u r ev a r i a t i o n w i t hc o n s t r a i n t sd e s c r i p t i o na n di n s t r u c t i o nm o d e ll i b r a r y ，t h ec o m p i l e r g e n e r a t e sc h c o d e sf o rc o n s t r a i n ts o l v i n g a f t e rc o m p i l i n ga n de x e c u t i n gt h eg e n e r a t e dc + + c o d e s ，i tw i l lf i n a l l yg e n e r a t et e s tp r o g r a m sf o ra r c h i t e c t u r el e v e lv e r i f i c a t i o n s e c o n d l y ，w er e s e a r c ht h es t r a t e g i e so fi n s t r u c t i o ng e n e r a t i o na n di n t e g r a t ea l lt h es t r a t e g i e s i n t ot h ec o n s t r a i n ts o l v e r f o rf u n c t i o n a lv e r i f i c a t i o nr e q u i r e m e n t ，w ed e s i g nt h es t r a t e g i e so f i n s t r u c t i o ng e n e r a t i o n ，i n c l u d i n g ：a b s t r a c t i n gc o n s t r a i n tf r o mi n s t r u c t i o ns e t ，m o d e l i n gt h e c o n s t r a i n tn e t ，m o d e l i n gt h ec o n t r o lh a z a r d ，a v o i d i n gt h ei n f i n i t yl o o p ，m o d e l i n ge x c e p t i o n ， m o d e l i n gm e m o r y t h i r d l y ，w er e s e a r c ht h ep i p e l i n es t a t ec o v e r a g ea n di m p l e m e n ti t sa r i t h m e t i c p i p e l i n es t a t e c o v e r a g er e d u c e dt e s tp r o g r a ms i z e s t h em o d e lo fp i p e l i n es t a t ec o v e r a g ei sp r e s e n t e di nt h i s p a p e r f o u r t h l y ，w er e s e a r c ht h ea r c h i t e c t u r el e v e lt e s tp r o g r a mg e n e r a t i o no fd l x a n dl e o n 2 p r o c e s s o r i nt h i sc a s e ，w ep l a nt h ev e r i f i c a t i o nu s i n gc o n s t r a i n td e s c r i p t i o nl a n g u a g et ot e s t c o v e r a g ea n dd i s c o v e re r r o r sw h i c h w ei n t r o d u c e d t h ep r o t o t y p es y s t e m m a 2 t gc a nn o to n l yg e n e r a t et e s tp r o g r a mr a n d o m l y ，b u ta l s o g e n e r a t es p e c i f i ct e s tp r o g r a m i th a sb e e ns u c c e s s f u l l ya p p l i e dt ot h ev e r i f i c a t i o no fd l x a n d l e o n 2 p r o c e s s o r ，a n dt h ee x p e r i m e n tr e s u l t sh a v ep r o v e dt h ev a l i d i t yo f o u rm e t h o d k e y w o r d s ：u s e rc o n s t r a i n td e s c r i p t i o nl a n g u a g e ，c o n s t r a i n t s a t i s f a c t i o np r o b l e m ， s t r a t e g yo fi n s t r u c t i o ng e n e r a t i o n ，p i p e l i n es t a t ec o v e r a g e 国防科学技术大学研究生院学位论文 图目录 图1 1 数字设计流程中的抽象级别图 图1 2 芯片设计的瓶颈 图1 3 微处理器体系结构级验证框架。， 图2 1 覆盖率驱动的验证流程 图2 2 验证进度管理 图2 3s p e c m , a n 验证框架 图3 1 约束编译程序结构 图3 2 约束求精过程 图3 3 通用指令格式 图3 4 分解约束的规则树。 图3 5 约束指令分组示意图 图3 6 字符识别状态转换图 图4 1 数据相关示例 图4 2 组相联c a c h e 示意图 图4 3 生成的部分测试程序 图4 4 资源锁定示意， 图4 5 流水线覆盖率示意 图5 1 验证框架 图5 2s u p e r s c a l a rd l x 处理器框图 图5 3 主存储器结构 图5 4 随机生成系统与m a 2 t g 系统的覆盖率曲线 图5 5 无覆盖率反馈方法与有反馈方法的覆盖率曲线 图5 6 流水线状态覆盖率曲线 图5 7d l x 处理器的代码覆盖率， 图5 8l e o n 2 体系结构， 1 0 1 1 1 6 1 8 1 8 2 2 2 2 2 6 4 2 4 3 4 5 4 6 ，4 7 4 9 5 0 5 1 5 2 5 3 5 3 5 4 5 4 国防科学技术大学研究生院学位论文 表目录 表3 1 约束描述语言单词符号及其种别值2 5 表3 2 变量表3 2 表3 3 范围表，3 2 表3 ，4 指令说明表，。，3 2 表3 5 操作数关系说明表，3 3 表4 1 部分异常列表 表4 2 测试程序的指令分布 表5 1a d d 指令的覆盖率 表5 2 引入错误比较 4 4 5 2 5 5 独创性声明 本人声明所呈交的学位论文是我本人在导师指导下进行的研究工作及取得 的研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含 其他人已经发表和撰写过的研究成果，也不包含为获得国防科学技术大学或其它 教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任 何贡献均已在论文中作了明确的说明并表示谢意。 学位论文题目：基土丝塞盛鲤鲍邀丛理墨功篷坠适焦庄自边生盛擅苤盟壅 学位论文作者签名：堡& 日期：卫一严年l l 月；f 日 学位论文版权使用授权书 本人完全了解国防科学技术大学有关保留、使用学位论文的规定。本人授权 国防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子 文档，允许论文被查阅和借阅；可以将学位论文的全部或部分内容编入有关数据 库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。 ( 保密学位论文在解密后适用本授权书。) 学位论文题目：基王约塞垄篮鲍邀缝堡墨边丝坠适堡庄自边垒盛垫查盟壅 学位论文作者签名：鎏 作者指导教师签名叠垫 日期：p ) 年i 。月，f 日 日期：2 。吖年j 工月，j 日 国防科学技术大学研究生院学位论文 第一章绪论 1 i 课题背景 以微处理器为核心的现代军用电子信息技术已成为当今武器装备中竞争最激烈、发展 最迅速的领域，其发展规模和技术水平己成为衡量一个国家军事地位和综合国力的重要标 志。在微处理器设计中，为了保证芯片设计的正确性和加快芯片上市时间，需要对各层次 设计描述进行详细全面的验证。图1 1 显示了数字设计流程中的抽象级别。在设计层次中， 高层设计的验证比低层验证更容易发现设计错误，算法实现开销更小，对设计周期的影响 更大，对整个设计的正确性影响也更大。芯片出现错误的代价是不可想象的，以i n t e l 公 司1 9 9 3 年推出的p e n t i u m 处理器为例，由于浮点除的b u g ，i n t e l 最终收回了所有存在b u g 的处理器，造成直接经济损失4 7 5 亿美元。 图i 1 数字设计流程中的抽象级别图 国防科学技术大学研究生院学位论文 随着现代微处理器规模和复杂度的不断增大，设计验证变得越来越困难。研究和设计 实践表明，目前的芯片设计队伍结构中，验证人员一般是设计人员的2 倍，验证所花的时 间和精力已占整个设计过程的7 0 n8 0 ，其中，r t l 级及高层验证占整个验证开销的 5 2 1 。如图1 2 所示，验证尤其是r t l 级及高层验证已经成为整个设计过程的瓶颈。 1 9 9 6 3 0 万门 2 0 0 0 l 百万门 代码 验证综合 p r 3 0 _ 4 册 5 0 _ 8 0 代码验证综合 p k r 图1 2 芯片设计的瓶颈 微处理器功能验证主要采取模拟方法和形式验证方法。形式验证方法如等价性检查、 模型检验和定理证明，处理规模有限，不能满足大规模复杂设计的需求。模拟验证仍然是 目前验证的主要手段。它通过在验证对象上模拟大量测试程序来验证尽可能多的体系结构 功能。在模拟验证中，完备的模拟矢量集可以在最短的时间内最大可能地发现错误。对于 高性能微处理器这种大型设计，模拟所需的时间特别长。为了确保模拟的完备，需要大量 的模拟矢量来对设计进行详尽的测试，而手工编写模拟矢量是一个很漫长的过程。测试程 序的生成和质量成为模拟方法的瓶颈。 体系结构级模拟验证的质量和周期极大地依赖于体系结构级验证程序的生成。目前主 要有人工生成、伪随机生成和半形式化生成方法。人工生成的速度慢、工作量大，并且不 一定能验证各种可能的情况。伪随机生成则包含大量的冗余指令，而且不容易产生针对特 殊要求的测试程序。半形式化生成主要处理流水线及控制逻辑等部件，处理范围比较窄， 规模也比较小。目前国外微处理器设计公司的主要设计验证方法是结合模拟和形式化验证 方法，以模拟方法为主。对部分电路采用形式化方法进行验证，对大部分设计采用半形式 化验证方法，即结合模拟矢量自动生成方法、模拟覆盖率分析方法，来加快设计验证。这 种方法在i n t e l 、i b m 、s u n 、s g i 、m o t o r o l a 等公司已经成为主流方法。 1 2 研究内容 在体系结构级验证微处理器，主要考虑验证其功能的正确性。在验证过程中，首先， 必须提升验证的抽象层次，抽象层次越高，验证效率也就越高。其次，必须将一些繁琐、 重复、耗时的工作自动化，这包括测试程序的生成、输出结果的检查等。第三，为了避免 对某些功能的重复验证，必须采用一种有效的评钡4 覆盖率的方法。指令集结构是对微处理 器功能的直接描述，根据指令集结构的信息来产生测试程序是一种可行的方法。为了能够 产尘适应于不同体系结构的测试程序，必须不依赖于具体的指令集，而是动态地建立指令 第2 页 国防科学技术大学研究生院学位论文 模型。对于模拟验汪束说，最重要的应该是测试程序的大小和功能覆盖率，测试程序越小， 覆盖的功能越多，那么该测试程序的质量就越高。因此，我们希望能找到一种理想的生成 方法，它可以根据验证者的要求生成功能覆盏率高、代码量小的测试程序。这种生成方法 应该以满足指令集固有的约束和验证者的需求为宗旨。 d l 描述 a d l 编译器 体系结构 特性文件 约束规则 描述文件 翮i 竺登翠兰兰h 鳖菱萎模板库ll _ t jl 垩；型旦 菝募卜叫约束求解器卜叫r t l 级设计 比较器 图1 3 微处理器体系结构级验证框架 基于上面几点考虑，针对已有的各种自动测试程序生成方法存在的缺点，课题组提出 了系统级的覆盖率驱动的验证方法的框架( 如图l i3 所示) 。提出了如下的构想：用该框 架进行体系结构级验证时，首先编译目标微处理器的a d l 描述，根据它的体系结构特征信 息自动生成体系结构特征配置文件和指令模板库。体系结构特征配置文件中保存的是用于 配置约束编译器的体系结构信息，以保证编译器建立的约束模型适用于目标微处理器。指 令模板库包含的是根据目标处理器体系结构特征为验证问题建立的固有约束模型。所谓固 有约束是指于用户所提出的约束需求无关的那部分约束，它们是因目标微处理器的体系结 构特征而异的。约束编译器经过体系结构特征配置文件配置以后对约束需求文件进行编 译，该文件是用户向系统提交验证需求的唯一手段。约束编译器在后端为测试程序建立约 束模型。约束模型与指令模板库和约束求解库链接执行之后就可以生成满足约束条件的测 试程序。生成的测试程序可供体系结构模拟器使用，也可供r t l 级h d l 模拟器使用。最后 将两个模拟结果作比较即可。对模拟结果进行功能覆盖率分析后，可以人工编写约束验证 来覆盖设计，也可自动分析覆盖率分析结果，自动生成约束描述，作为下一次测试程序生 成的输入。课题组的目标是基于图1 3 提出的框架，研究其中的关键技术，设计出一种新 的体系结构级测试程序自动生成的原型系统一微处理器体系结构级自动测试程序生成系 统( m i c r o p r o c e s s o ra r c h i t e c t u r e l e v e la u t o m a t i ct e s tg e n e r a t o r ，姒2 t g ) ，并将该 原型系统应用到d i x 2 、l e o n 2 3 等体系结构的验证当中，以证明浚方法的有效性和有用 性。 第3 页 国防科学技术大学研究生院学位论文 本课题来源于国家自然科学基金项目“微处理器高层功能验证测试程序自动生成的理 论与方法”。本文的研究工作是基于上述框架，深入研究其中的约束编译器、约束求解器 和功能覆盖率的驱动技术，并完成原型系统中相应部件的设计和实现，是整个课题组研究 的重要组成部分。 1 3 本文工作 本文具体的研究和设计工作如下： l 、用户约束描述语言的设计和约束编译器的实现 课题对微处理器的功能验证需求进行了广泛的研究和分析，根据用户可能提出的验证 需求特性，定义了一种结构清晰、语法简洁、使用简单的体系结构级约束规则描述语言， 制订出该语言相关的描述说明和使用规则，并实现了其编译器。 2 、指令生成策略的研究并将其集成到约束求解器中 针对功能验证的需求，制订了相应产生测试程序的约束求解策略，其中解决的关键技 术包括：指令集结构中固有约束的提取与求解模型的建立、各种数据冲突约束网络的建立、 控制相关约束模型的建立、避免产生不合法测试程序的策略( 例如：无限循环的避免) 、 触发各种异常的约束模型的建立、验证存储层次正确性的指令组合约束模型的建立等。 3 、流水线状态覆盖率的研究和实现 深入研究了流水线状态覆盖率技术，建立了流水线状态覆盖率模型，研究了流水线状 态覆盖率驱动的指令生成算法和评测标准，以提高生成程序的覆盖率，减小生成程序规模。 4 、i ) l x 和l e o n 2 处理器的实例研究 针对d l x 和l e o n 2 处理器的体系结构级和r t l 级代码的验证，使用约束描述语言，制 订了比较全面的实验方案，进行覆盖率测试和错误捕捉，并根据该环境对m a 2 t g 系统进行 了性能评价。 1 4 论文结构 本文共分为六章： 第一章，绪论。首先介绍了课题的研究背景，然后提出了本文的研究目标，并给出了 课题研究丌发的淞2 t g 系统所基于的测试程序自动生成框架，最后概述了本文的主要工作。 第二章，功能验证方法与程序自动生成技术。综述了微处理器功能验证技术、测试程 序自动生成技术、覆盖率分析技术和硬件验证语言，分别总结各类技术的代表性理论和工 具，归纳了它们的优缺点，从而为分析系统需求打下了孥实的理论基础。 第三章，约束描述语言的设计与实现。根据解决约束满足问题的一般思路，对用，o 验 第4 页 国防科学技术大学研究生院学位论文 证需求进行了归类分析，提出了指令模型及其约束网络的建模方法，设计了体系结构级约 束描述语言，最后实例介绍了约束编译器的具体实现： 第四章，指令生成策略及流水线覆盖率。在c s p 求解算法的基础上，研究了对用户描 述的约束网络进行建模和求解的具体策略，分类讲解了各类建模策略的过程，并结合具体 的例子进行了分析。为了减小测试程序规模，进一步深入研究了流水线状态覆盖率的模型 和生成算法。 第五章，功能验证程序自动生成的实例研究。首先提出了验证的框架，在此基础上， 介绍了d l x 和l e o n 2 两种处理器的体系结构，然后分别进行覆盖率测试和错误捕捉实验。 最后根据实验结果对m a 2 t g 系统进行了性能评价。 第六章，结束语。总结了论文的主要工作，并对后续工作进行分析和展望a 甭了页一 国防科学技术大学研究生院学位论文 第二章功能验证方法与验证程序自动生成技术 设计验证要保证设计初始的h d l 描述是正确的，并且每一设计层次间的设计转换过程 不会带来错误。由于r t l 级h d l 描述是后续设计层次设计功能验证的主要参照系，因此， 功能验证主要集中在h d l 描述的r t l ( r e g i s t e rt r a n s i s t o rl e v e l ) 级设计，以确保尽早 发现设计错误。这种保证设计功能正确性的验证被称为功能验证( f u n c t i o n a l v e r i f i c a t i o n ) 。 2 i 功能验证技术 功能验证方法主要有三种：形式化验证方法、模拟验证方法和覆盖率驱动的验证方法。 2 i 1 形式化验证方法 形式化验证方法使用数学方法形式化地证明设计实现部分或全部满足系统描述要求。 目前形式化验证方法种类较多。模型检验( m o d e lc h e c k i n g ) 是一种检测设计是否具有所 需属性的方法；等价性检查( e q u i v a l e n c ec h e c k i n g ) 用于比较设计的两种实现是否一致， 该方法又可分为组合等价性检查i ( c o m b i n a t i o n a le q u i v a l e n c ec h e c k i n g ) 和时序等价性 检查( s e q u e n t i a le q u i v a l e n c ec h e c k i n g ) 。其它的方法还包括定理证明( t h e o r e mp r o v i n g ) 和符号轨迹求解( s y m b o l i ct r a j e c t o r ye v a l u a t i o n ，s t e ) 等。 在形式化验证方法中，通常使用k r i p k e 结构来描述反应式系统，描述这种系统的状 态变化。k r i p k e 结构m 被定义为一个三元组m2 ( s ，氐，m ，其中s 是一个有限状态集合， 6 0e s 是仞始状态集合，r 量s x s 是状态变迁关系。 l 、模型检验 模型检验用于检测某个具有有限状态集合的系统是否有其描述所规定的属性 4 。描 述通常用时态逻辑表示，例如计算树时态逻辑( c o m p u t a t i o nt r e el o g i c ，c t l ) 5 和线 性时态逻辑( l i n e a rt e m p o r a ll o g i c ，l t l ) 6 ，而系统被建模为k r i p k e 结构。早期的 模型检验方法是显式状态搜索方法 7 ，该方法的缺点是状态爆炸问题。m c m i l l a n 等 8 提出了基于化简有序二分决策图( r e d u c e do r d e r e db i n a r yd e c i s i o nd i a g r a m ，r o b d d ) 9 的隐式状态搜索检测方法，称为符号模型检验。虽然符号模型检验方法已经能处理有 几百个状态寄存器的设计 1 0 ，但是现代设计常常带有成千上万个状态寄存器，因此，目 前模型检验还只能处理小规模的设计。虽然该方法可以直接基于h d l 描述进行，证明【id 【 万百百r 国防科学技术大学研究生院学位论文 描述在所有输入下满足某些正确性属性。但这些属性通常由设计者给出要求对设计功能 需求有很全面的了解才能给出这些属性，并且只能证明设计满足属性要求，而不能证明设 计的正确性。 2 、定理证明 在定理证明中，系统及其需满足的属性都用数理逻辑的形式化语言描述，一个形式化 描述的系统包括一组公理和演绎规则，从系统的公理找到对属性的证明的过程就被称为定 理证明 1 1 。与模型检验不同，定理证明能在无限状态空间上进行推理。 目前有很多定理证明工具用于解决硬件验证问题，例如h o l 系统 1 2 ，p v s 系统 1 3 和a c l 2 系统 1 4 等，并且都有成功应用案例。m o o r e 等人 1 5 验证了a m d s k 8 6 芯片的除法 算法的微码，b r o c k 等 1 4 验汪了m o t o r o l a 的c a p 处理器，c l a r k 等 1 6 验证了s r t 除法 算法。 该方法需要一个设计行为的形式化描述，通过严格的数学证明，比较h d l 描述的设计 和系统的形式化描述在所有可能输入下是否一致。该方法存在的问题是，通常h d l 描述就 是第一个形式化描述，即便有一个更高层次的形式化描述，还需要保证该描述的正确性， 才能和h d l 描述进行一致性比较；形式化描述和h d l 描述的一致性证明很难进行，通常需 要假设很多条件，以简化比较证明，而要证明这些假设本身也是很困难的。另一个主要问 题是不能完全自动化。 3 、组合等价性检查 组合等价性检查的目的是检查两个组合电路在给定的输入下是否等价。组合等价性检 查属于c o n p 问题 1 7 ，但在实际应用中，要比较的两个电路往往差别很小，结构相似性 很大。该方法已在工业界得到广泛应用。该方法采用的标识等价点和利用两个电路间的隐 喻关系的方法能加快检查进程，实际实现时采用了多种布尔求解引擎，如b d d 、a t p g 、s a t 等 1 8 ，1 9 ，使其能获得较高的性能。 4 、时序等价性检查 时序等价性检查分为两种应用场景，第一种应用中两个时序电路有对应的状态寄存 器，例如，两个电路的状态编码相同，此时，时序等价性检查就变成了组合等价性检查。 该类应用包括：比较r t l 级设计在综合前后的等价性：检查逻辑级设计及其版图实现间的 等价性：对设计进行性能优化前后电路的等价性证明等。第二种情况是两个时序电路状态 编码不同，例如，检查电路在r e t i m i n g 后的正确性；比较电路的流水化设计和非流水设 计等。解决该问题的一种简单的方法是构造两个时序电路的乘积状态机，通过遍历乘积状 念机的状态空间来检测是否等价，显然该方法不能处理大型的设计。 针对不同的应用情况，现有研究提出了各种有效检查流水和非流水设计的等价性的方 法。例如，b u c h 和d i l l 2 0 建立了基于u n i n t e r p r e t e d 函数进行抽象验证流水微处理器 控制的基础。r i t t e r 等 2 1 基于i n t e r p r e t e d 函数和c a s e 划分检查两个h d l 描述的可计 算性等价。这些方法都不是基于状态空问遍历的，而是通过验证设计的实现和描述间检查 点( c h e c k p o i n t ) 的等价性来进行验证的。 时序等价性检查的问题是需要个参考模型作为描述，而设计参考模型也是一个很重 的任务。 5 、符号轨迹求解 符号轨迹求解 2 2 ，2 3 是一种受限形式的模型检验方法，它提供了符号轨迹公式来描 述设计说明。符号轨迹公式由布尔表达式和时态逻辑的“下一时刻”操作符x 构成，属性 的定义形式是【hj o j ，其中a 是由输入和经过一定时钟周期后的系统状态组成的序列，c 是该序列可能的结果行为。例如，反相器可被描述为 抽2 j x ( o u t2 一o ) 1 。检测是通过 基于二叉决策图( b i n a r yd e c i s i o nd i a g r a m ，b d d ) 的三元符号模拟进行的。出于每个结 点有三种状态( 0 ，1 ，x ) ，需要用一对变量来表示b d d 中的一个结点。在符号模拟时，与 要验证的属性无关的初始输入和系统状态都被赋值为“x ”，这使得s t e 比其它模型检验 方法有优势，因为其计算复杂度是由属性决定的，而不需要检查整个状态空问。s t e 方法 已在逻辑级数据通路设计验证中获得成功应用 2 4 ，2 5 。 s t e 的缺点是轨迹公式不能描述“负”和“或”，只支持一种时态逻辑操作符( x ) ， 因此s t e 方法的表达能力有限；其次，s t e 使用b d d 进行符号模拟，同样存在状态空间爆 炸问题。 2 1 2 模拟验证方法 该方法使用用户给定的输入激励，直接模拟运行h d l 描述，根据模拟结果判断设计是 否满足功能描述要求。根据检查模拟结果的方法，该方法又被分为联合模拟和自检查模拟。 l 、联合模拟 在该模拟框架下，除了r t l 级描述，还需要一个称为黄金模型的比r t l 级层次高的系 统模型。模拟时，使用同一组输入运行两个模型，并比较两个模型的输出以判断r t l 模型 是否有错。该方法对输入激励要求较低，不需要输入激励提供预定输出。随机和伪随机模 拟矢量自动生成方法适用于这种模拟框架 2 6 ，2 7 ，2 8 。该模拟框架存在的问题是，编写 黄金模型的工作量大，而且保证黄金模型的正确性也是一个很难解决的问题；只能保证r t l 级模型与黄金模型一致，而无法证明r t l 级描述是无错的；另一个问题是由于两个模型的 抽蒙程度不同，同步两个模型的执行以进行比较也是一项复杂的工作。该方法主要用于系 列产品的微处理器设计中。 2 、自检查模拟 该模拟框架中，需要设计者自己检查模拟输出，或者提供的输入激励耍带预期输出结 第8 页 国防科学技术大学研究生院学位论文 果，以进行自检查。相比于联合模拟框架，该方法只需要一个r t l 级模型，建立模拟环境 比较容易，是一种使用得比较普遍的模拟验证方法。但在该方法中，准备模拟激励以及自 动生成模拟矢量成为方法的瓶颈。 除了上述两种模拟验证方法各自存在的问题，模拟验证存在的另一个问题是如何度量 模拟验证的程度，即何时可以停止模拟。这往往依赖于设计者和验证工程师个人的判断。 随着设计复杂度的增大，将会产生大量冗余的模拟矢量来增强模拟验证的可信度。 2 1 3 覆盖率驱动的验证方法 待测模型抽取卜+ 一r t l 级描述卜+ 一d e b u g 调试 未覆盖信息 覆盖率目标是否达到 卫 完成 是 图2 1 覆盖率驱动的验证流程 形式化验证和模拟验证方法各有优缺点，单独使用一种方法都难以高效地完成整个功 能验证任务，这两种方法是互为补充的。因此，结合了形式化验证和模拟验证方法优点的 覆盖率驱动的验证方法从一提出来，就迅速成为功能验证的流行方法。图2 1 是覆盖率驱 动的验证方法的框架图。该方法根据所提供的模拟覆盖率测度，检查模拟输出，判断r t l 级描述的哪些部分被模拟过，哪些部分未被模拟过，并为未被模拟过的部分生成使其被激 活的模拟矢量。覆盖率驱动的验证有很多优点。覆盖率分析报告可以指明设计的哪些部分 已经得到验证，哪些区域还需要进一步验证。通过去除不必要的冗余代码可以优化回归测 试，尽量少地利用模拟资源。为签出( s i g n o f f ) 提供一个定量的准则。总的原则是使用 更少的模拟激励进行了更多的验证。 第9 页 国防科学技术大学研究生院学位论文 1 0 0 水 基 丑 采 聒 目 蜊 廿 时阃 图2 2 验证进度管理 图2 2 为传统方法与基于覆盖的方法b u g 发现过程的比较。尽管1 0 0 的覆盖率并不能 保证设计1 0 0 无错误，但该方法提供了一种更系统化的方法来度量模拟验证的程度，并且 结合了形式化验证技术进行模拟矢量自动生成。 2 。2 微处理器功能验证程序自动生成技术 功能验证程序自动生成技术主要分为伪随机生成和半形式化生成两类。 2 2 1 伪随机生成 在微处理器验证过程中，通过伪随机生成的模拟程序所发现的设计错误是最多的，通 常占错误总数的7 0 以上 2 9 ，应用非常广泛。 o b s i d i a n 公司的r a v e n 是一个随机生成的商用解决方案。通过图形化的界面输入，用 户选择操作码、寄存器、存储地址以及机器状态( 比如操作模式、存储器中的内容、c a c h e 状态等) 的偏倚( b i a s ) 值来随机生成测试。同时使用定向测试技术使结果在指定功能空 间中更为密集。用户使用t c l 作为描述语言写几百个测试模板交给机器，就可以生成大量 的测试程序。定向生成作为补充，主要是手写的覆盖边界条件的测试程序和由覆盖率反馈 所驱动的针对未覆盖逻辑区域生成的测试程序。作为商用工具其支持的处理器类型很多， 配置灵活，也支持多处理器的验证程序自动生成。但是出于指令序列主要由用户指定的偏 倚( b i a s ) 值生成，对用户编制测试模板要求较高，并且会有大量的冗余测试程序生成， 覆盖率也不够高。 i b mh a i f a 实验室将约束求解方法用于伪随机指令自动生成系统中，在指令建模时给 予一定的约束限制，通过求解一个约束满足问题( c o n s t r a i n ts a t i s f yp r o b l e m ，c s p ) ， 第1 0 页 国防科学技术大学研究生院学位论文 生成符合要求的测试程序。g e n e s y s 系统 3 0 用c c + + 语言描述微处理器的体系结构、指 令集等信息，通过用户指定运行环境( 如c a c h e 状态等) ，利用测试知识库，在一组约束 的指导下生成模拟程序。对于每条指令来说，约束主要是指该指令的操作数列表、体系结 构级资源( 存储器、寄存器) 的读写和它的行为表达。这样，每条指令的模型就描述了一 个由指令的读写所修改的变化的操作数和资源所组成的约束网络。该系统已经戏功地用于 p o w e r p c 、x 8 6 和一个d s p 芯片的设计验证流程中，功能覆盖率可达8 0 。该系统的缺陷 是描述语言较为难用，需要手工使用c + + 语言为微处理器建模，建模周期长，容易出错。 p i p a r a z z i 系统 3 1 进一步深入对微体系结构进行建模，如超标量、乱序、流水线等机制， 将其描述为基本单元。指令生成同时对体系结构和微体系结构模型求解。约束求解算法主 要是基于m a c ( m a i n t a i n i n ga r cc o n s i s t e n c y 3 2 ) ，多条指令在一个约束网络中计算。 该系统已经用于p o w e r p c 处理器和z s e r i e s 处理器的验证。对目标处理器的微系统结构 建模后，由用户制定生成的规则，覆盖率比g e n e s y s 高约1 2 ，可以达到9 2 左右。但是 其建模难度更大，要求用户对系统有深刻的理解。 接口描述功能骏迁计划原有代码 ( e 语言)( e 语言)( c 语言) d 乡岜多土弓 s p e c 淞n 约束驱动的测试数据和逻辑功能覆盖率 向量生成时态检查分忻 ；彳fi p h d l 模拟器 彳f h d l 模型原有代 5 ( h d l ) 图2 3s p e c m a n 验证框架 v e r i s i t y 公司的基于s p e c i f ic a t i o n 和约束求解的生成方法通常由三部分组成：系统 描述、模拟矢量生成约束、约束求解器。s p e c m a n 3 3 提供了e 语言描述系统的功能和接 口行为，主要是指令体系结构的描述。测试计划则描述对此次生成的模拟矢量的约束，包 括要生成的指令、指令顺序，以及在什么情况下生成这种指令。最后使用s p e c m a n 的约束 求解器生成模拟矢量。图2 3 是其验证的框架。s p e c m a n 基于随机基础之上进行向量产生， 同时施加监督机制，使之产生确实有用的、能发现b u g 的测试向量，这种监督机制大大提 高验证效率；同时让机器自动产生测试向量，也大大提高了单位时间内测试向量的数量。 v e r i s i t y 提供的监督机制具体表现就是“功能覆盖”，而非传统的“代码覆盖”，这样便 可很好地量度整个验证过程。对于随机测试向量产生，须有自动的设计正确性检查机制。 国防科学技术大学研究生院学位论文 这种检查分两种：数据检查和硬件协议检查。对于数据检查，s p e c m a n 使用记分牌方式进 行，在特定时间点上，对设计输出的数据的正确性进行检查。对于硬件协议检查，v e r i s i t y 的e 语言提供简单有效的高级语法来支持断言( 即最接近自然语言的方式) ，而非传统使 用的状态机。这样，一个复杂的协议，e 语言用一两行语句就可表述出来，简单的描述也 极大地保证了描述的正确性。到2 0 0 3 年，v e r i s i t y 占功链验证领域的市场份额达6 5 以 上。在国外的功能验证领域，所有知名设计公司都将v e r i s i t y 的验证方法和系统s p e c m a n 作为标准验证平台。 2 2 2 半形式化生成 半形式化生成方法主要针对流水线及控制逻辑等部件。对流水线或控制部件建立有限 状态机，通过遍历状态机生成测试程序，这样理论上对流水线行为可以取得1 0 0 的状态 覆盖率。为了用尽可能少的模拟程序来覆盖尽可能多的设计，f s m 状态空间遍历方法可以 用图论中求解欧拉环游和中国邮递员问题的算法，也可以使用b d d 表示f s m ，使用模型检 测方法中计算所有可达状态的算法。由于固有的状态空制爆炸的问题，要为所有信号建立