（计算机系统结构专业论文）模拟验证中的激励产生与覆盖评估.pdf

1 摘要 集成电路设计验证是指在设计的过程中判别设计规范和实现之间是否一致。据统 计，目前在大规模集成电路的设计流程中，设计验证的时间已经占到整个设计周期的 一半以上。模拟验证作为一种重要的设计验证方法，其工作量通常会占据整个验证工 作量的4 0 n t 0 然而模拟验证中存在的激励生成质量不高、评估分析不力等问题仍 是目前困扰设计验证工程师的主要问题。针对这些问题，本文对模拟验证中的关键问 题：激励产生以及覆盖评估方法，进行了深入研究，取得了如下创新性成果： 1 提出了一种新的可观测性信息模型可观测性覆盖评估准则，是对传统覆盖 评估准则的增强。本文提出一种新的针对寄存器传输级( r e g i s t e rt r a n s f e rl e v e l ，简 称r t l ) 可观测性信息的抽象模型。本文采用增强型进程控制树( e n h a n c e dp r o c e s s c o n t r o l l i n gt r e e ，简称e p c t ) ，来表征每一时间帧代码的执行情况，以及截止到该 时间帧，代码的可观测性情况。同时，本文采用控制一观测链( c o n t r o l l i n g o b s e r v i n g c h a i n ，简称c o c ) 来记录在具体每一时间帧扩展过程中，代码的可观测性信息。本文 提出的表征方式结构简洁，它不仅可以清晰地表征截止到当前时间帧代码的可观测性 信息，同时可以清晰地表征在时间帧扩展过程中，代码的可观测性信息。基于该抽象 模型，可以很方便地完成各种操作 2 提出了一种新的可观测性覆盖分析方法该方法的实现主要包括两个阶段： ( 1 ) 向量模拟阶段；这是一个从输入到输出的“正向”过程，该阶段的主要工作是刷 新e p c t 中的相关域，并最终确定在该时间帧，每一个观测点的c o c ；( 2 ) 可观测性 分析阶段：这是一个从观测点出发，“反向”分析其所对应的c o c ，进而判断变量以 及语句的可观测性的过程。该方法具有以下特点：( 1 ) 采用了一种简洁合理的可观测 性信息模型；( 2 ) 采用变量的赋值和引用作为可观测性分析的基础，可以很容易地与 其它考虑可控制性的覆盖准则相结合基于上述思想，我们开发了相应的原型系统， 并进行了相关实验，实验结果说明：( 1 ) 可观测性语句覆盖评估准则增强了传统语句 覆盖评估准则的评估能力；( 2 ) 采用本文方法进行可观测性覆盖分析，时间开销仅 为1 0 9 7 ，远低于其他同类型算法 3 提出了种新的基于可观测性覆盖评估准则的激励生成方法。该方法具有以下 特点：( 1 ) 这是一种基于模拟的、无回溯的方法；( 2 ) 通过请求一响应过程，实现 了反向蕴涵与正向蕴涵；( 3 ) 在激励生成过程中以未观测代码的分布作为启发式信 息，指导激励生成；( 4 ) 在该方法的实现当中，采用了高效的覆盖分析算法最终我 们实现了相应的原型系统，并进行了相关实验。实验结果显示，采用本文方法所得到 的模拟激励的平均可观测性语句覆盖率为9 2 3 2 ，高于同类型其他算法，同时针对同 等规模电路的处理时间大大降低。 4 提出了一种新的基于混合遗传算法的r t l 激励生成方法该方法具有以下特 点：( 1 ) 以多种覆盖评估准则与r t l 故障模型作为激励生成目标，对模拟激励的评估 模拟验证中的激励产生与覆盖评估：摘要 更加全面；( 2 ) 针对基于模拟的激励生成问题的特点，采用合理的参数设置； ( 3 ) 结合遗传算法以及激励生成问题的特点，实现了一种全局一局域混合搜索机制。实验 结果显示采用该方法可以高效地产生具有较高语句覆盖率，分支覆盖率、r t l 传输故 障覆盖率，以及对应门级固定型故障覆盖率的模拟激励。 关键词：设计验证，模拟，激励生成，覆盖评估 r e s e a r c ho nv e c t o rg e n e r a t i o na n dc o v e r a g em e t r i c si n d e s i g nv e r i f i c a t i o nv i as i m u l a t i o n w e il u ( c o m p u t e ra r c h i t e c t u r e ) d i r e c t e db yp r o f x i a o w e il i a b s t r a c t d e s i g nv e r i f i c a t i o ni st h et a s ko fv e r i f y i n gt h a tag i v e nd e s i g n ，s p e c i f i e da tw h a t e v e r l e v e l ，h a sc e r t a i np r o p e r t i e sr e q u i r e db yas p e c i f i c a t i o n u s u a l l y , d e s i g nt e a m ss p e n dm o r e t h a n5 0 e f f o r to ft h ed e v e l o p m e n to nv e r i f i c a t i o nn o w a d a y s b yf a rs i m u l a t i o ni ss t i l l t h ep r i m a r yw o r k h o r s ef o rd e s i g nv e r i f i c a t i o na n d4 0 7 0 t i m es p e n ti nv e r i f i c a t i o nw i l l c o n s u m e dd u r i n gt h i sp r o c e s s w h i l et h e r ea r es t i l ls o m ep r o b l e m sb o r i n gt h ev e r i f i c a t i o n e n g i n e e r sd u r i n gd e s i g nv e r i f i c a t i o nv i as i m u l a t i o n o no n eh a n dt h eq u a l i t yo fp a t t e r n s c a n tb eg u a r a n t e e do f t e n ，a n do nt h eo t h e rh a n dc o v e r a g em e t r i c st a k i n go b s e r v a b i l i t y i n t oa c c o u n ta r en o tv e r ys a t i s f a c t o r y a i n l i n ga tt h e s ep r o b l e l n s ，t h i sd i s s e r t a t i o nc o v e r s t h ek e ya s p e c t so fs i m u l a t i o n ：s t i m u l ig e n e r a t i o na n dc o v e r a g ea n a l y s i s ，a n dt h eo r i g i n a l c o n t r i b u t i o n so ft h i sd i s s e r t a t i o na r ea sf o l l o w s 1 n e wr e p r e s e n t a t i o n st om o d e lo b s e r v a b i h t yi n f o r m a t i o na r ep r o p o s e d o b s e r v a b i l i t yc o v e r a g em e t r i ci sa l s oak i n do fb e h a v i o rc o v e r a g em e t r i c ，r e g a r d i n g a n o t h e ra b s t r a c tm o d e l ：o b s e r v a b i l i t y , a n di te n h a n c e st h et r a d i t i o n a lc o v e r a g em e t r i c s w i t h o u tt a k i n go b s e r v a b i l i t yi n t oa c c o u n t i nt h i sd i s s e r t a t i o n ，w ep r e s e n tp r e c i s ea n dc o n - c i s ea b s t r a c tr e p r e s e n t a t i o n sf r o mh d l ( 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 ) d e s c r i p t i o n s a tr t l ( r e g i s t e rt r a n s f e rl e v e l ) t om o d e lo b s e r v a b i l i t yi n f o r m a t i o n w eu s ee p c t ( e n h a n c e dp r o c e s sc o n t r o l l i n gt r e e s ) t or e p r e s e n tt h ea c t i v a t i o no fc o d e s i ns o m et i m e f r a m ea n dt h es t a t i s t i c si n f o r m a t i o na b o u to b s e r v a b i h t yu pt ot h ec u r r e n tt i m e 矗a l n e w e u s ec o c ( c o n t r o u i n g - o b s e r v i n gc h a i n s ) t or e p r e s e n tt h eo b s e r v a b i l i t yi n f o r m a t i o nd u r - i n gt i m ef r a m e se x p a n s i o n t h ep r o p o s e dr e p r e s e n t a t i o n sc o u l dd e n o t et h eo b s e r v a b i l i t y i n f o r m a t i o nc l e a r l ya n db a s e do nt h e s er e p r e s e n t a t i o n st h ea n a l y s i sa b o u to b s e r v a b i l i t y c o u l db ed o n ee a s i l y 2 an o v e lo b s e r v a b i h t ye v a l u a t i o nm e t h o di sp r o p o s e d t h eo b s e r v a b i l i t ya n a l y s i sp r o c e d u r ec o u l db ed i v i d e di n t ot w op h a s e s ：s i m u l a t i o n p h a s ea n da n a l y s i sp h a s e i nt h ef i r s tp h a s e ，w es i m u l a t ea v e c t o ra n dc o n s t r u c tt h e c o co fe a c ho d p ( o b s e r v e dp o i n t ) i nt h es e c o n dp h u s e ，w ea n a l y z et h ec o co fe a c h ，i，ii-l， 模拟验证中的激励产生与覆盖评估：英文摘要 o d pt od oo b s e r v a b i l i t ya n a l y s i s f i r s t l y , t h eo b s e r v a b i h t ym o d e l sw eu s e da r ec o n c i s e a n dp r e c i s e s e c o n d l y , t h ew o r ko fc o n s t r u c t i n gr t lm o d e l si sd o n ei np r e - s i m u l a t i o n p h a s e ，a n dt h e r el e a v e so n l ya n a l y s i so fw h i c hv a r i a b l e sa n ds t a t e m e n t sa r eo b s e r v a b l e d u r i n gs i m u l a t i o n t h e r e f o r et h ep r o p o s e dm e t h o di ss i g n i f i c a n t l ym o r ec o m p u t a t i o n a l l y e f f i c i e n tt h a np r i o re f f o r t st oa s s e s so b s e r v a b i l i t ya n di tc o u l db ei n t e g r a t e di n t oc o m - p i l e r sa n ds i m u l a t o r se a s i l y w ed e v e l o p e dt h ec o r r e s p o n d i n gp r o t o t y p et o o la n dd i d e x p e r i m e n t s t h er e s u l t ss h o wt h a to b s e r v a b i l i t ye v a l u a t i o ne n h a n c e st h ec a p a b i l i t yo f t r a d i t i o n a ls t a t e m e n tc o v e r a g em e t r i ca n dt h ea v e r a g et i m eo v e r h e a di s1 0 9 7 w h i c hi s l o w e rt h a nt h ec o r r e s p o n d i n ge x p e r i m e n t a lr e s u l t sg o tb yo t h e rm e t h o d s 3 an e wv e c t o rg e n e r a t i o nm e t h o dt a r g e t i n gt h eo b s e r v a b i l i t y - e a h a n c e ds t a t e m e n t c o v e r a g em e t r i ci sp r o p o s e d t h ep r o p o s e dm e t h o dh a st h ef o l l o w i n gc h a r a c t e r i s t i c s ( 1 ) t h i sm e t h o di s s i m u l a t i o n - b a s e da n db a c k - t r a c kf r e e ( 2 ) t h er e q u e s t e c h os t r a t e g yi su s e dt oa c h i e v e f o r w a r di m p l i c a t i o na n db a c k w a r di m p l i c a t i o n ( 3 ) t h ev e c t o rg e n e r a t i o np r o c e d u r ei s d r i v e nb yt h ed i s t r i b u t i o no fu n o b s e r v e dc o d e s ( 4 ) a ne f f i c i e n tc o v e r a g ea n a l y s i sa l g o - r i t h mi sa d o p t e di nt h i sm e t h o d a tl a s t ，t h em e t h o dp r o p o s e dh a sb e e ni m p l e m e n t e d a sap r o t o t y p et o o lf o rv h d l d e s i g n s 。a n dt h ee x p e r i m e n t a lr e s u l t so nb e n c h m a r k ss h o w t h a tt h o u g ht h ec i r c u m s t a n c e sa n db e n c h m a r k sa r ed i f f e r e n t ，t h ea v e r a g eo b s e r v a b i l i t y - e n h a n c e ds t a t e m e n tc o v e r a g ei s9 2 3 2 w h i c hi sh i g h e rt h a nt h ec o v e r a g eg o tb yo t h e r m e t h o d sa n dt h ec p ut i m ei ss h o r t e n e dg r e a t l y 4 an e wv e c t o rg e n e r a t i o nm e t h o da tr t lb a s e do nh y b r i dg e n e t i ca l g o r i t h m si s p r o p o s e d t h i sm e t h o dh a st h ef o l l o w i n gc h a r a c t e r i s t i c s f i r s t i v , m a n yc o v e r a g em e t r i c sa n d r t lf a u l tm o d e la r et a k e ni n t oa c c o u n tt oe v a l u a t ev e c t o r s s e c o n d l y , a i m i n ga tt h e c h a r a c t e r i s t i c so fv e c t o rg e n e r a t i o n ，w eu s ed y n a m i cp a r a m e t e rs e t t i n g st oe n h a n c et h e e f f i c i e n c yo ft h i sm e t h o d t h i r d l y , w ec o m b i n et h em e r i t so fg e n e t i ca l g o r i t h m sa n d 。t r a d i t i o n a ls e a r c ht e c h n i q u e st op r o p o s eag l o b a l - l o c a lh y b r i ds e a r c hm e c h a n i s m t h e e x p e r i m e n t a lr e s u l t ss h o wt h a tt h es y s t e mc o u l dg e n e r a t ev e c t o r se f f i c i e n t l yt oc o v e r m o s ts t a t e m e n t s ，b r a n c h e sa n dt r a n s f e rf a u l t so fr t ld e s c r i p t i o n s ，a n dt h e s ev e c t o r s c o u l da l s oc o v e rm o s ts t u c k - a tf a u l t si nt h ec o r r e s p o n d i n gn e tl i s t s k e yw o r d s ：d e s i g nv e r i f i c a t i o n ，s i m u l a t i o n ，v e c t o rg e n e r a t i o n ，c o v e r a g ea n a l y s i s 插图目录 1 - 1 模拟验证的简单模型 1 2 模拟验证流程 2 3 2 1 等价性检验在集成电路设计流程中的应用 2 - 2 积自动机( m i t e r ) 模型 2 - 3 有界模型检验示意图 2 4 设计验证与电路测试类比图【7 3 】 2 - 5 基于错误建模的验证流程。 2 6 层次化激励生成方法 2 7 存储器的行为模型 2 - 8 激励波形图 2 - 9 f s m 的结构【9 6 】 2 - 1 0 控制性与观测性示意图【4 4 】 3 - 1 h d l 中的串行语句与并行语句 3 - 2 进程的模拟周期。 3 - 3 组合进程p l 与其所对应的有向无环图 3 - 4 同步时序电路的一般模型 3 - 5 时钟进程中的阻塞赋值与非阻塞赋值 3 - 6 多条件分支语句转化为二条件分支语句 孓7 进程控制树节点结构 3 - 8 r t l 代码与其对应的抽象语句组以及p c t 结构 3 - 9 r t l 代码与其对应p c t 与d d g 结构 4 - l 逻辑框图 4 2 控制观测值计算示意图， 垂3 具有扇出分支的节点的可观测性值， 4 - 4 增强型进程控制树节点结构， 4 - 5 增强型进程控制树与数据流向图 4 6 可观测性分析图 5 _ 1 覆盖分析方法的整体框架 心j巧竭玲加孔幻弱疗 弘号勰“ 的鼹弱弱鼹 眈 模拟验证中的激励产生与覆盖评估：插图目录 进程的行为模拟算法 6 3 连续时钟周期的执行导致的数据流 6 3 可观测性覆盖分析算法6 4 确认目标过程中的回溯， 7 0 无回溯激励生成的理想框架 7 3 请求响应过程示意图 7 4 请求响应算法7 5 系统实现框架 7 6 激励生成算法7 8 遗传算法的一般结构 8 4 一段r t l 代码与所对应的扩充后的p c t 以及d d g 9 4 实现框架 9 5 传输故障信息的组织9 7 解释种群中基因设定原因的例子9 8 种群中的基因9 8 局部优化算法1 0 0 b 1 0 状态迁移图( 迁移条件省略) ，i 0 0 复位与停止判断算法1 0 1 弛粥弘 眈似晰 他他m”那w他加 表格目录 2 - l 逻辑门的真值表1 7 3 - l 数字系统的抽象级别与描述风格3 2 4 - 1 t a g 模拟对加法操作的运算表 5 4 5 1 电路特性与覆盖准则比较6 5 5 - 2 o c c o m 【4 4 】系统的时间开销 6 6 5 - 3 o c m _ s t a t i s t i c s 【4 6 】系统的时间开销 6 6 5 - 4 本文系统的时间开销6 7 6 - 1 本文系统与随机系统的运行比较8 0 6 - 2 文献f i o o l 的实验结果 8 0 7 - 1 遗传算法的主要应用领域8 4 2 参数设定表，9 9 7 - 3 电路特性与激励生成结果( 时间单位：秒)1 0 2 7 _ 4 不同系统效率比较( 时间单位：秒) 1 0 3 7 - 5 不同系统运行环境比较1 0 3 1 ： 毒 声明 本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得 的研究成果。就我所知，除了文中特别加以标注和致谢的地方外，论文中 不包含其他人已经发表或撰写过的研究成果。与我一同工作的同志对本研 究所做的任何贡献均已在论文中作了明确的说明并表示了谢意。 作者签名多氢勃 日期：乱咧牟l 毋陧日 关于论文使用授权的说明 中国科学院计算技术研究所有权处理、保留送交论文的复印件，允许 论文被查阅和借阅；并可以公布论文的全部或部分内容，可以采用影印、 缩印或其它复制手段保存该论文。 储签名锄翩勰例魄嘶1 日1 2 日 、l 1 1 研究背景 第一章引言 自从1 9 5 8 年美国德克萨斯仪器公司( t i ) 的基尔比( j k f l b y ) 等人研制发明了世 界上第一块集成电路以来，电子工业进入了集成电路( i c ) 的时代。在随后的4 0 多年 时间里，集成电路技术以惊人的速度，蓬勃发展起来。它不仅极大地改变了人们的生 活水平，同时也带动了信息技术、电子技术等相关领域的飞速发展。目前集成电路已 经从最初的小规模集成电路( s s i ) 起步，先后经历了中规模集成电路( m s i ) 、大规 模集成电路( l s i ) 、超大规模集成电路( v l s i ) 、巨大规模集成电路( u l s i ) ，发 展到目前的特大规模集成电路( g s i ) 和系统芯片( s o c ) ，单个电路芯片集成的元件 数目也从最初的十几个发展到目前的几亿个甚至几十、上百亿个。 伴随着集成电路的飞速发展，人们对电路产品可靠性的需求也与日俱增。如何确 保最终获得的集成电路芯片运行正确可靠? 这对任何涉足该领域的人来说都是个严 峻挑战。一方面，为了满足客户日益多样化的需求，芯片所要胜任的功能日新月异， 这就需要芯片的设计越来越复杂；另一方面，芯片设计制造厂商为了获取利润最大 化，就必须在众多竞争者中脱颖而出，达到早日上市的目标，这就迫使芯片的设计 制造周期足够短芯片的日益复杂以及设计制造周期的时间限制势必会对设计带来 挑战，就更有可能导致设计中的错误。b e n t l e y 在2 0 0 1 年设计自动化会议( d a c ) 上报 告，p e n t i u m i v 的设计中被检测出的“臭虫( b u g ) ”的数目，相比p e n t i u m p r o 增 长了3 5 0 【1 1 。同时目前硬件产品错误诊断与修复的代价非常昂贵，任何一个很小的设 计错误都可能给企业带来巨大的经济损失例如，1 9 9 4 年因为p e n t i u m 处理器浮点除 法部件设计的一个小“臭虫”，i n t e l 公司的损失达4 7 5 亿美元。 从设计流程的各个阶段到芯片的制造过程，每一个步骤都可能引入错误。例如不 正确的设计规范、设计工具本身的问题、设计者的疏漏或者版图的缺陷等都会导致最 终产品发生故障。为了保证产品的正确性，必须从概念到封装的每个步骤都进行严格 的验证与测试f 2 ，3 1 。 由于集成电路芯片设计规模的急剧增长，系统设计的功能验证正面临严峻的挑 战。事实上，目前在整个设计流程中，验证已经成为制约产品上市周期的瓶颈。目 前在大规模设计中，验证的工作量通常占整个设计流程的7 0 左右【4 】。2 0 0 3 年度的 国际半导体技术发展报告( i n t e r n a t i o n a lt e c h n o l o g yr o a d m a pf o rs e m i - c o n d u c t o r 简 称i t i t s 2 0 0 3 ) 更明确指出，目前验证已经成为集成电路设计流程中开销最大的工作。 在目前的工程项目中，验证工程师的数目超过了设计工程师，对于复杂的设计更是达 到t 2 ：l 或者3 ：1 的比率【5 】第三届v s i a ( v i r t u a ls o c k e ti n t e r f a c ea l l i a n c e ) 验证会议 得出的结论是“验证不仅仅是很难，而是非常，非常难。”验证的重要性与困难性， 由此可见一斑。 中国科学院博士学位论文：模拟验证中的激励产生与覆盖评估 集成电路设计流程包括许多步骤，在每一步骤，电路被表示成不同抽象层次的 模型，例如系统级、算法级、寄存器传输级( r e g i s t e rt r a n s f e rl e v e l ，简称r t l ) 、 逻辑级、电路级模型等。集成电路的设计流程实际上是一个对设计模型逐步“精化 ( r e f i n e ) ”的过程【3 ，6 ，7 】。在这个流程中，设计验证就是要保证每个阶段实现的正确 性，如功能、时序、性能及功耗等方面与设计规范的一致性。设计的最初阶段主要是 做需求分析，来确定芯片应该具有的功能或性能，它们往往不是形式化的，需要由其 用户和设计人员一起来确定，称之为概念设计；接下来，由芯片的设计人员将这种非 形式化的设计概念转换成形式化的设计规范( s p e c i f i c a t i o n ) ，这样的规范可以是由任 意形式语言来描述的【3 】；然后根据设计规范在寄存器传输级进行系统功能的设计，这 里一般是使用硬件描述语言( 如v h d l 、v e r i l o g 语言) 对各功能块及相互之间的关系 进行描述；下一步，利用综合工具将寄存器传输级模型转换成门级模型；再往底层进 行物理设计得到晶体管级模型直到版图；最后阶段进行芯片的加工，即基于芯片版图 的掩膜来制造出芯片的硅片并封装【8 】。在集成电路设计的每一步骤，部有可能引入错 误。因此，芯片从其需求开始，经过设计和生产，最终得到实际的芯片并投入应用， 其中的每一步都需要进行严格的验证或测试 设计验证发生在芯片的设计阶段，对设计的各种层次模型之间或它们与原始规范 之间的一致性进行检验，从而保证在设计流程的每一步骤没有引入错误3 ，9 1 。从传 统意义上讲，设计验证方法包括两大类：模拟的方法和形式化的方法。形式验证使用 严格的数学推理来证明一个系统满足全部或者部分规范 1 0 1 。这就要求设计方案的规 范和实现都有形式化的描述存在。常用的描述手段有谓词逻辑( p r e d i c a t el o g i c ) 、时 态逻辑( t e m p o r a ll o g i c ) ，以及各种硬件描述语言( 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 ) 。目前人们在形式验证方面已经提出了很多具体方法，并且在较低抽象层 次上非常适用，例如，验证门级与其寄存器传输级之问的一致性等。但是，对于大 规模的逻辑设计( 例如处理器) 来说，形式验证方法在其它层面上的应用仍然受到 相当大的局限目前有许多高度自动化的形式化方法，其所需的时间和易用性都与 模拟方法可以相提并论，但是其处理能力常常局限于“小”规模设计。同时处理能 力强大的形式化方法，又常常依赖于技术专家，并要耗费大量的时间。所以，在工 程领域，模拟仍然是主要的且不可或缺的验证方法，尽管我们通常不能穷尽模拟所 有可能的输入组合。在大型芯片的设计中，模拟验证的工作量通常会占据整个验证 图1 - 1 模拟验证的简单模型 第一童引言 工作量的4 0 到7 0 【1 l 】。图1 1 是对模拟验证过程的简单概括。其中，被验证的设计 称为“被测模型( m o d e lu n d e rt e s t ) ”，对应的正确电路称为“参考模型( r e f e r e n c e m o d e l ) ”。模拟验证就是根据设计或者规范，产生验证激励，通过模拟激励的施加与 比较，来确定在该激励下，设计是否有误在该过程中，验证激励是必需的。如何在 有限的时间内，产生高效率的验证激励，是模拟验证技术的关键问题。 我们可以在不同的抽象层次( 例如r t l 、逻辑级等) 对设计进行模拟，以期发现 设计的错误，或者通过一定数量激励的施加与比较来增强设计者对设计正确性的信 心。目前r t l 是一种最普遍、最流行的设计层次，在该层次进行大量模拟也是非常必 要的。 针对r t l 激励产生的研究工作主要包括对层次化( h i e r a r c h i c a i ) 的激励产生方 法的研究 1 2 ，1 3 】，以及对基于r r l 行为描述的激励产生方法的研究 1 4 ，1 5 ，1 6 1 。层次 化r t l 激励产生的一般做法是将大电路划分成若干小的功能模块，对每个功能模块产 生局部激励，然后将局部激励翻译成全局激励，从而达到从电路的原始输入测试各功 能模块的目的在基于r t l 行为描述的激励产生中，常采用的方法包括：将行为描述 转化成其他描述方式来进行激励产生【1 4 ，15 】：直接分析电路的硬件描述语言文件，从 中提取信息用于门级的激励产生【1 7 ，1 8 】以及基于模拟的随机选优方法【1 6 】，为了提 高执行效率，遗传算法常常在基于模拟的激励生成中被采用，用于对随机向量进行改 进与选择。 在模拟验证中，随着集成电路设计规模越来越大，穷尽模拟所有的输入组合是不 可行的。如何在占用合理的时间和计算资源的基础上达到最理想的模拟效果，是一个 具有实际意义的问题。通常的做法就是运用覆盖评估技术。在模拟验证中，覆盖评估 能够量化地度量模拟激励集的完备性。同时，覆盖评估技术能够诊断出对于当前的激 励集来说，哪部分设计尚未得到充分验证，这有助于后续的激励生成。一般的模拟验 证流程如图1 2 所示，覆盖评估是其中重要的环节。 常用的覆盖评估准则可分为两大类【5 1 ，一类是从行为的角度来度量【1 9 ，2 0 1 ，主要 包括：代码覆盖准则、电路结构覆盖准则、有限状态机覆盖准则等其中，代码覆盖 准则起源于软件测试【2 1 】，其覆盖评估主要以代码为对象，由于用硬件描述语言所完 成的设计也是一种软件，所以代码覆盖评估技术可以很容易地从软件测试领域移植到 硬件设计验证中来，代码覆盖准则主要包括：语句覆盖、分支覆盖、条件覆盖等电 路结构覆盖准则是从硬件电路的角度考虑，主要包括：信号线与寄存器的翻转覆盖以 设计信息 规范信息 图1 - 2 模拟验证流程 拟激励。手写向量集通常由设计者完成，其最关注的通常是设计的基本功能和重要 的边界情况采用这种方式的针对性极强，然而主观性也极强，通常要耗费大量的 时间针对具体的设计，也可以构造自动化的直接向量产生方法，如a l u - a o n 【2 2 等用 专家系统针对p o w e r p c 处理器特定的体系结构和指令集自动产生指令来进行验征。然 而，此类方法难以具备普遍意义 第二类是随机激励生成方法。如果采用完全的随机或者伪随机方法，所得到的激 励从功能验证的角度来看，很可能是无意义的因此普遍采用约束( c o n s t r a i n s ) 和 偏置( b i a s i n g ) 技术，以提高随机向量的质量：例如在体系结构级，通过对操作数的 取值集合、操作码的取值集合、指令序列的组合等内容做约束，可以限制随机生成的 指令，以此作为模拟激励。与完全随机生成的指令相比，约束化的随机指令生成可以 第一章引言 在更短时间内执行更大量的相关验证用例，并且达到高覆盖率工业界领先的验证工 具，例如v e r i s i t y 公司的s p e c m a ne l i t e 工具【2 3 ，2 4 1 ，便提供了很好的带约束的随机激励 生成机制。 以上两类激励生成方法，其优缺点十分明显。随机激励生成实现了自动化，但是 基本上没有考虑检测设计错误的能力，其激励的验证效果必须待模拟完成之后才能显 现；而直接激励生成通常还属于手工作业方式因此，目前对激励生成的研究工作常 集中在两个方面，一方面是如何对设计错误建模，另一方面是如何针对模型化错误自 动生成模拟激励。 目前，关于设计错误模型化的研究常常集中在较低的抽象层次。例如，l - a s a a d ，e t a l 【2 5 | 对门级组合电路定义了四类简单的错误模型，并将错误模型映射到单固定型故障 ( s i n g l es t u c k - a tf a u l t ，简称s s f ) 模型，以借助自动测试向量生成( a u t o m a t i ct e s t p a t t e r ng e n e r a t i o n ，简称a t p g ) 工具产生激励。c a m p e n h o u t ，e t 址 2 6 1 针对r t l 的 总线设计错误提出了更复杂的错误模型，但其激励生成尚未实现自动化 r t l 描述是目前应用最广泛的电路设计描述形式之一，几乎得到了所有电子设计 自动化( e l e c t r o n i cd e s i g na u t o m a t i o n ，简称e d a ) 厂商的大力支持和推广，其本身 也得到了很好的发展。在该设计层面的激励生成也是目前的一个研究热点i g h o s h 等 在文献【2 7 l 中，提出基于高级综合的赋值判决图( a d d ) 的激励生成方法。文献【1 4 】提 出了采用进程控制树( p c b ) 、数据流向图( d d g ) 等结构抽象r t l 代码的方法，在 此基础上，提出了传输故障模型以及一种基于该模型的激励生成方法。文献【2 8 】扩展 了f 1 4 l 中的数据模型，并提出了一种针对可观测性语句覆盖评估准则的激励生成方 法文献【2 9 】提出了一种面向h d l 描述的，基于路径覆盖的模拟矢量自动生成方法。 文献【3 0 ，3 1 】基于程序切片的思想，进行信息提取，在此基础上提出了针对v e r i l o g 语言 的r t l 描述的激励生成方法 此外，早在1 9 6 2 年，s e s h u 和f r e e m a n 就在文献3 2 1 6 b 提出了基于模拟的激励生成 方法其基本思路是通过故障模拟器，从大量随机产生的向量中选出那些能够增加 故障覆盖率的向量作为激励。与帧扩展方法相比，基于模拟的方法避免了庞大的搜 索空间不过，采用这类方法常常存在向量过多、故障覆盖率不高等问题，特别是 那些用简单的方式从随机向量中选优的方法。为此，遗传算法往往在基于模拟的激 励生成中被采用，用于对随机向量的改进与选择在基于模拟的激励生成领域中， 遗传算法的最早应用出现在文献【3 3 ，3 4 1 其中，文献【3 4 】仅针对组合电路。此后，文 献【3 5 ，3 6 ，3 7 ，3 8 ，3 9 ，4 0 】都是遗传算