(电路与系统专业论文)基于布尔可满足性的逻辑电路等价性验证和测试生成技术研究[电路与系统专业优秀论文].pdf_第1页
(电路与系统专业论文)基于布尔可满足性的逻辑电路等价性验证和测试生成技术研究[电路与系统专业优秀论文].pdf_第2页
(电路与系统专业论文)基于布尔可满足性的逻辑电路等价性验证和测试生成技术研究[电路与系统专业优秀论文].pdf_第3页
(电路与系统专业论文)基于布尔可满足性的逻辑电路等价性验证和测试生成技术研究[电路与系统专业优秀论文].pdf_第4页
(电路与系统专业论文)基于布尔可满足性的逻辑电路等价性验证和测试生成技术研究[电路与系统专业优秀论文].pdf_第5页
已阅读5页,还剩113页未读 继续免费阅读

(电路与系统专业论文)基于布尔可满足性的逻辑电路等价性验证和测试生成技术研究[电路与系统专业优秀论文].pdf.pdf 免费下载

版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领

文档简介

浙江大学博+ l 学位论文摘要 摘要 近些年在布尔可满足性( s a t ) 领域取得了较大进展,一系列基于 d p l l 框架的优化算法被提出,有效s a t 解算器诸如z c h a f f 等已可解决 很大规模的s a t 问题。s a t 作为一个优秀引擎在e d a 领域已广泛应用, 本论文的主要方向就是探索如何有效地将s a t 技术应用于等价性验证和 测试生成这两类重要问题中。 下面概括本论文的主要研究方向和创新点: 1 基于输出分组和电路s a t 的组合等价性验证技术。随着芯片设计 规模同益庞大复杂,功能验证成为现阶段i c 设计过程中的瓶颈环节,而 传统模拟技术已很难满足现时集成电路设计的要求。作为模拟技术的补 充,组合等价性验证工具在i c 功能验证中使用已日益普遍。本文提出一 种基于电路可满足性和输出分组技术的组合电路等价性验证算法。算法首 先使用与非图结构哈希技术来简化验证任务。对那些具有较多输出的复杂 电路,为共享结构信息从而提高验证速度,使用输出分组技术将那些共享 较多内部结点的输出转化为一个子问题,从而验证问题可转化为一系列验 证子问题。对每一个子问题,使用将电路s a t 和b d d 学习等技术结合的 验证算法来解决。实验结果表明该类方法可有效用于解决大规模电路的验 证问题。 2 结合不变量提取和时序s a t 的时序等价性验证技术。应用组合等 价性验证工具的重要的限制是两个待验证电路的触发器之间存在一一对 应关系。然而对一个复杂设计,通常在调用综合工具时会进行重定时等时 序优化,这些优化容易破坏综合前后设计触发器间对应关系。因此,验证 浙江大学博i :学位论文 摘要 这些类型设计就必须使用时序等价性验证技术。本文提出一种时序等价性 验证框架:为探索验证任务间结构相似性,算法使用不变量提取引擎来提 前识别电路中有效不变量;为减少不变量提取时的误判几率,提出了时间 帧扩展和动态选择候选集两种优化策略,同时提出了不变量提取过程中的 快速查找反例启发式方法。对使用不变量引擎后尚未解决任务,可进一步 使用完整的时序s a t 引擎来解决。从对部分i s c a s 8 9 电路和工业实例的 实验结果表明,提出技术对验证复杂时序电路提供了一种可能方案。 3 基于改进联接电路模型的时序自动测试生成技术。面向时序电路 的a t p g 问题是e d a 领域中具有高度计算复杂性问题之一,运行传统时 序a t p g 的观察发现大部分计算开销用于解决那些较难观测故障。针对使 用传统s a t 方法需要对每个故障构建一次联接电路的不足,本文中提出 了可同时注入多个候选故障的电路模型。使用该改进模型的关键好处在 于:( 1 ) 之前s a t 求解过程中获得的有用信息可在测试其他故障时完全 重用,这样可大大降低求解的计算开销;( 2 ) 当s a t 求解结果显示为不 可满足时,可以断定剩余所有故障是不可测试的,因此查找那些不可测故 障仅仅是s a t 求解的副产品。此外,将不变量提取、边界模型检验和时 序s a t 解算器结合并充分发挥各自引擎的优点,可进一步提高时序a t p g 求解的效率。实验表明,该算法是一种有效的算法,尤其适用于测试那些 常规方法无法解决的较难观测故障。 4 支持多故障和不同故障类型的诊断测试生成技术。时序a t p g 的 改进联接电路模型可扩展到诊断测试生成( d t p g ) 应用中,本文提出了 一种基于s a t 的d t p g 技术。基于扩展的模型技术,可共享求解不同故 浙江人学博 :学位论文摘要 障对d t p g 时获得的学习信息来极大地改进d t p g 搜索效率。进一步, 可将该模型扩展应用于区分多故障、不同故障类型间的d t p g 问题,这里 故障包括静态和动态故障。为减少产生的诊断矢量数目,文中提出一种探 索原始输入中无关值( d o n tc a r e ) 的诊断测试矢量压缩方法。将提出的 d t p g 技术与已有故障诊断结合起来,实验发现可以获得较好诊断精度和 获得更多故障信息。 关键词形式验证;等价性验证;二叉判决图;可满足性问题;不变量; 自动测试矢量生成;故障诊断; 浙江大学博l :学位论文 a b s t r a c t ab s t r a c t w i t ht h ed e v e l o p m e n to fm o d e ma n de f f i c i e n tb o o l e a ns a t i s f i a b i l i t y ( s a t ) a l g o r i t h m s i nr e c e n t y e a r s ,s a th a si n c r e a s i n g l ym a d eas i g n i f i c a n ti m p a c to n 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 ) a p p l i c a t i o n s i nt h i st h e s i sw ei n v e s t i g a t et h e a p p l i c a t i o no fm o d e ms a te n g i n e f o rt h ee q u i v a l e n c ec h e c k i n ga n dt e s tp a t t e r n g e n e r a t i o np r o b l e m s t h e o 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 ea sf o l l o w s : 1 e f f i c i e n tc 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 gu s i n go u t p u tg r o u p i n ga n d c i r c u i ts a t a st h e c h i p s i z ea n dc o m p l e x i t y d r a m a t i c a l l yg r o w s ,f u n c t i o n a l v e r i f i c a t i o nh a sb e c o m et h em a i nb o t t e m e c ki ni cd e s i g nf l o w s t o d a y sl a r g e , c o m p l e xd e s i g n so f t e nr e q u i r ea ni n o r d i n a t ea m o u n to ft i m ea n dc o m p u t a t i o nr e s o u r c e s t o v e r i f yu s i n gt r a d i t i o n a ls i m u l a t i o nt e c h n i q u ea l o n e a na l t e r n a t i v e f o rs o m e v e r i f i c a t i o nt a s k si st ou s ec 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 an e wc o m b i n a t i o n a l e q u i v a l e n c ec h e c k i n gt e c h n i q u ec o m b i n i n go u t p u tg r o u p i n ga n dc i r c u i ts a tw a s i n t r o d u c e di nt h et h e s i s a n d i n v e r t e rs t r u c t u r a lh a s h i n gt e c h n i q u ew a su s e dt os i m p l i f y t h em i t e rc i r c u i tf i r s t t h ea l g o r i t h mu s eo u rp r o p o s e dh e u r i s t i ct od oo u t p u tg r o u p i n g f o rc o m p l e xp r o b l e m s ,a n dt h u st h ee q u i v a l e n c ec h e c k i n gp r o b l e mc a nb ec o n v e r t e d i n t os o m ec i r c u i ts a tp r o b l e m s ,c i r c u i ts a ts o l v e rw a su s e dt os o l v et h e s e s u b - p r o b l e m s t or e d u c et h es e a r c hs p a c e ,u s e f u ll e a r n i n gi n f o r m a t i o no fs o m e s u b - p r o b l e mw a ss h a r e d e x p e r i m e n tr e s u l t sf o rs o m el a r g e rv e r i f i c a t i o n t a s k s d e m o n s t r a t et h ep r o p o s e da l g o r i t h m se f f i c i e n c y 2 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 gu s i n gi n v a r i a n te x t r a c t i o nt e c h n q i u ea n d s e q u e n t i a ls a ts o l v e r o n es i g n i f i c a n tl i m i t a t i o no fc o m b i n a t i o n a le q u i v a l e n c e c h e c k i n gi s i t sr e q u i r e m e n tt h a tt w od e s i g n su n d e rv e r i f i c a t i o nh a v ec o r r e s p o n d i n g f l i p f l o p s s y n t h e s i st o o l sm a y o f t e na p p l ys e q u e n t i a lo p t i m i z a t i o n ss u c ha sr e t i m i n gt o c o m p l e xd e s i g n sa n dh e n c ed e s t r o yt h ec o r r e s p o n d e n c eb e t w e e nf l i p f l o p si nb o t ht h e r e f e r e n c ea n di m p l e m e n t a t i o nd e s i g n s c h e c k i n gt h e e q u i v a l e n c eo fs u c hd e s i g n s s h o u l db ec a r r i e do u tu s i n gs 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 w ep r o p o s eas e q u e n t i a l e q u i v a l e n c ec h e c k i n gf r a m e w o r kb yi n t e g r a t i n gi n v a r i a n tc h e c k i n ga n ds e q u e n t i a ls a t a l t e r n a t e l y t oe x p l o r et h es t r u c t u r a ls i m i l a r i t y 。s o m ei n v a r i a n t si nt h em i t e rc i r c u i ta r e i d e n t i f i e di na d v a n c e ,a n dt h es e a r c hs p a c ec a nb ed r a m a t i c a l l yr e d u c e db yc o n s t r a i n i n g t h e s eg e n e r a t e di n v a r i a n t s a ne n h a n c e di n v a r i a n tc h e c k i n gm e t h o dt h a tc o m b i n e s t i m e f r a m ee x p a n s i o na n dd y n a m i cc a n d i d a t es e l e c t i o ns t r a t e g i e si sp r o p o s e d w h a t s 浙江人学博f j 学位论文 a b s t r a c t m o r e ,ah e u r i s t i cf o rq u i c k l yf i n d i n gc o u n t e r e x a m p l e so fi n - e q u i v a l e n tt a s k s i s i n t r o d u c e d ,i tc a ns o l v es o m eh a r d - t o d e t e c tp r o b l e m sw i t hl o n gs o l u t i o nl e n g t ht h a ta r e t y p i c a l l yf a i l e dw h e nb o u n d e dm o d e lc h e c k i n gt o o li su s e d t h ee f f i c i e n c yo ft h e a p p r o a c h i ss h o w nt h r o u g hi t sa p p l i c a t i o no nt h ei s c a s 8 9c i r c u i t sa n ds o m e h a r d t o - v e r i f yi n d u s t r i a lc i r c u i t s t h ee x p e r i m e n t a lr e s u l t ss h o wt h a tt h i sw o r kh o l d s p o t e n t i a lf o rs e q u e n t i a lv e r i f i c a t i o no fl a r g e - s c a l ec i r c u i t s 3 s e q u e n t i a la u t o m a t i ct e s tp a t t e r ng e n e r a t i o nu s i n ga ne n h a n c e dm i t e rm o d e l w h i c ha l l o w sr e u s eo fl e a r n e dc l a u s e sf o rd i f f e r e n tf a u l t s a u t o m a t et e s tp a t t e r n g e n e r a t i o n ( a t p g ) f o rs e q u e n t i a lc i r c u i t sr e m a i n so n eo ft h em o s tc o m p u t a t i o n a l l y d i f f i c u l tp r o b l e m si ne d aa r e a s i th a sb e e no b s e r v e dt h a tt h eh a r d t o d e t e c tf a u l t s o f t e nc o n s u m em o s to fc o m p u t a t i o n a lr e s o u r c e si nr u n n i n gat r a d i t i o n a ls e q u e n t i a l a t p gt 0 0 1 t h i st h e s i sp r e s e n t ss e v e r a li d e a so nm o r ee f f e c t i v ea p p l i c a t i o no fb o o l e a n s a t i s f i a b i l i t yt e c h n i q u e s t ot h es e q u e n t i a la t p g w ef i r s tp r o p o s ea ne n h a n c e d m i t e r b a s e d m o d e l ,w h i c h c a ni n c r e a s e r e u s a b i l i t y o fl e a r n e d c o m p u t a t i o n a l i n f o r m a t i o nb ys i m u l t a n e o u s l yi n j e c t i n gas e to ft a r g e tf a u l t si nas i n g l em i t e rc i r c u i t , i n s t e a do fb u i l d i n gas e p a r a t em i t e rc i r c u i tf o re a c hf a u l t t h eu s eo ft h i sm o d e l d r a m a t i c a l l yi m p r o v e st h ea t p ge f f i c i e n c yu s i n gas e q u e n t i a ls a t i s f i a b i l i t ys o l v e r f u r t h e r m o r e ,d e t e c t i n gu n t e s t a b l ef a u l t sn o wi so n l yab y p r o d u c to fs a ts o l v i n g s o m er e c e n tt e c h n i q u e sd e v e l o p e df o rs a t b a s e ds e q u e n t i a le q u i v a l e n c ev e r i f i c a t i o n c a l la l s ob em o d i f i e da n di n t e g r a t e dt of u r t h e ri m p r o v et h ee n g i n e se f f i c i e n c yf o r s e q u e n t i a la t p g t h ee x p e r i m e n t a lr e s u l t ss h o wt h a to u rm e t h o dc a ni m p r o v eb o t h f a u l tc o v e r a g ea n df a u l te f f i c i e n c y ,a n di t s e s p e c i a l l y u s e f u lf o rs o l v i n gt h o s e h a r d t o - d e t e c tf a u l t sw h i c ha b o r t e db yu s i n gt h et r a d i t i o n a ls e q u e n t i a la t p gt 0 0 1 4 d i a g n o s t i cp a t t e r ng e n e r a t i o nt h a ts u p p o r t sm u l t i p l ef a u l t sw i t hp o s s i b l y d i f f e r e n tf a u l tt y p e s w ea l s op r e s e n ta ne f f i c i e n td i a g n o s t i ct e s tp a t t e r ng e n e r a t i o n ( d t p g 、f r a m e w o r kb a s e du p o nab o o l e a ns a t i s f i a b i l i t ye n g i n e t h em o d e lu s e di n s e q u e n t i a la t p gi sf u r t h e re x t e n d e df o rd t p ga p p l i c a t i o n w i t ht h i sm o d e l i n g t e c h n i q u e ,l e a r n e di n f o r m a t i o nd u r i n gd t p gf o rd i f f e r e n tf a u l tp a i r sc a nt h e nb e n a t u r a l l ys h a r e dw i t h o u ta n yc o m p u t a t i o n a lo v e r h e a da n dt h u ss i g n i f i c a n t l yi m p r o v e t h ed t p gs e a r c he f f i c i e n c y w ea l s op r o p o s eam o d e lf o rd t p go fm u l t i p l ef a u l t s w i t hp o s s i b l yd i f f e r e n tf a u l tt y p e s ,i n c l u d i n gs t a t i ca n dd y n a m i cf a u l t s 。t or e d u c et h e d i a g n o s t i cp a t t e r nc o u n t ,w ef u r t h e ri n t r o d u c eac o m p a c t i o nh e u r i s t i cb ye x p l o r i n g “d o n tc a r e s ”a tt h ep r i m a r yi n p u t s w ed e m o n s t r a t ee x p e r i m e n t a lr e s u l t sw h i c h i n d i c a t et h a tt h ep r o p o s e dd t p gm o d e l sa n dm e t h o d sc a ns i g n i f i c a n t l ye n h a n e et h e v 浙江大学博 :学位论文 a b s t r a c t d i a g n o s i sr e s o l u t i o n k e y w o r d sf 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 ec h e c k i n g ;s a t ;b d d ;l n v a r i a n t ;a t p g ; f a u l td i a g n o s i s 浙江人学博f :学位论文 图日录 图目录 图1 1 功能验证分类2 图1 2i c 设计流程中的等价性验证4 图1 3 联接电路模型7 图2 1 霍夫曼时序电路模型1 2 图2 - 2 时i 日j 帧扩展模型1 2 图2 3b d d 简化规则1 4 图2 - 4 同一布尔函数采用不同变量次序构建b d d 1 6 图2 5d p l l 算法伪代码1 9 图2 6 简单电路2 4 图2 7 按拓扑结构求解策略2 4 图2 8 时间帧向后扩展策略2 5 图3 1 识别内部等价结点简化联接电路2 8 图3 2 割集引起误判情况2 9 图3 3 组合等价性验证算法流程3 0 图3 - 4a i g 表征3l 图3 5a i g 新结点构建伪代码3 2 图3 - 6a i o 简化举例3 3 图3 7 输出分组示意图3 4 图3 8 输出分组启发式算法伪代码3 5 图3 - 9b d d 学习策略举例3 7 图4 1 等价性验证系统流程4 l 图4 2 匹配模型电路4 2 图4 3 局部b d d 算法4 3 图4 4 匹配算法流程图4 5 图4 5 匹配时间比较4 6 图4 - 6 匹配精度比较结果4 7 图4 7 基于两个时间帧的验证原理图4 9 图4 8 时序等价性验证算法流程5 l 图4 - 9 状态空间s i 和r 间关系5 2 图4 1 0 时间帧扩展举例5 4 图4 1 1 三类不变量间关系5 5 图4 1 2 反例查找启发式方法伪代码5 6 浙江大学博十学位论文 图目录 图4 1 3s 3 8 5 8 4 反例查找时问比较5 7 图5 1 带扫描设计的时序电路6 3 图5 2 时序a t p g 分类6 4 图5 3 使用s a t 求解时序a t p g 6 5 图5 4 插入m u x 的故障注入技术6 7 图5 5 同时注入多个故障技术6 7 图5 - 6 同时观测多个故障的联接电路6 8 图5 7 基于改进模型a t p g 求解流程6 9 图5 8 基于s a t 的时序a t p g 算法流程7 l 图5 - 9 使用b m c 技术查找可测试故障7 3 图6 1 失效分析流程图路7 9 图6 2 基于s a t 的d t p g 技术流程8 2 图6 3 用于单故障的d t p g 模型8 3 图6 - 4 时序d t p g 电路模型8 5 图6 5 区别固定故障和桥接故障的电路模型。8 6 图6 - 6 求解s l o w t o r i s e 跳变故障的电路模型8 6 图6 7 区分桥接故障和跳变故障的电路模型8 8 图6 8 支持多故障d t p g 的额外电路8 8 图6 9 压缩诊断测试矢量举例9 0 图6 1 0 矢量列表更新规则9 l 图6 1 1 二阶段故障诊断技术流程9 2 图6 1 2 平均运行时间比较一9 3 图6 1 3 平均隐含次数比较9 3 图6 1 4 两阶段流程的诊断结果9 5 浙江人学博 :学位论文 表日录 表目录 表1 1 测试领域主要研究方向6 表2 1 常见布尔函数的b d d 复杂度1 5 表2 2 常用布尔运算的i t e 对应表示1 7 表2 3 常见逻辑门及其对应c n f 表示2 3 表3 1 验证i s c a s 8 5 优化前后电路实验结果3 8 表3 2 验证复杂电路实验结果3 9 表4 1 验证等价任务实验结果5 8 表4 2 验证不等价任务实验结果5 9 表5 1 基于时序s a t 的a t p g 实验结果6 6 表5 2 基于b m c 方法观测可测故障7 5 表5 3 应用结合多种技术的a t p g 工具求解实验结果7 7 表6 1 面向双固定故障的d t p g 结果9 4 表6 2 面向双跳变故障的d t p g 结果9 5 浙江大学博上学位论文 第l 章引言 第1 章引言 1 1 研究背景及意义 自从1 9 5 8 年德州仪器公司的j a c kk i l b y 等人发明了世界上第一块集成电路 ( 1 m e g r a t e dc i r c u i t s ,简写为i c ) 以来,电子工业进入了集成电路时代,集成电路 已经广泛地应用到国民经济和社会的一切领域。所谓集成电路,就是在一块单 晶硅片上,采用特殊制造工艺,将许多晶体管、各种元器件和互连线等集成在 同一基片上的微小型化电路。经过近5 0 年的飞速发展,集成电路已经从最初的 小规模集成电路( s s i ) 起步,先后经历了中规模( m s i ) 、大规模( l s i ) 、超 大规模( v l s i ) 、巨大规模( u l s i ) ,以至发展到今天的特大规模集成电路( g s i ) , 单个电路芯片中集成的元件数也从开始时的十几个发展到目前的几亿个乃至几 十亿个。比如,现阶段i n t e l 的微处理器芯片主频已高达2 g ,且每秒可执行上 百亿条指令。不难发现,集成电路发展的重要特征是器件特征尺寸不断缩小、 集成度不断提高、性价比不断降低。几十年来,集成电路发展一直遵循着所谓 的摩尔定律,即集成电路的规模和性能每1 8 个月翻一番,而价格减半。 以超深亚微米和i p 核复用技术为基础的系统级系统( s y s t e m o n c h i p ,简 写为s o c ) 技术将是未来集成电路产业主要发展方向。现在,能够符合s o c 芯片所需要的制造技术已经日益成熟,然而制造技术与芯片验证和测试之间, 却存在着较大的瓶颈。在集成电路设计验证与测试生成领域开展基础研究工作, 不仅本身具有重要的理论意义,而且对解决现阶段集成电路测试和验证中面临 各种挑战有现实意义。 1 1 1 功能验证技术 统计表明,现阶段集成电路设计验证过程消耗了整个设计周期的三分之二, 且设计组中验证工程师人数一般是硬件语言程序工程师人数的两倍。现今集成电 路产业发展一个重要特征是缩短产品进入市场时间,即”m ( t i m et om a r k e t ) , 因此如何提高验证的效率和减少验证所消耗成本,成为当前电路设计中个亟待 解决问题。 电路验证的任务是检验待验证电路即规格电路( s p e c i f i c a t i o nc i r c u i t ) 和设 计电路( i m p l e m e n t a t i o nc i r c u i t ) 在功能、时序、可测性、速度及功耗等方面是 否致。在以上这些验证指标中,其中以保证设计功能正确性的功能验证显得尤 浙江人学搏f :学位论文 第 章f i 寿 为重要,据统计从设计错误分布方面看功能缺陷占6 0 以上比率。目前大多数设 计者在功能验证中主要采用以模拟( s i m u l a t i o n ) 为基础的方法。基于模拟的验 证流程大致如下:( 1 ) 使用软件构造电路设计的模型,来编写测试程序 ( t e s t b e n c h e s ) ;( 2 ) 观察和比较模型的输入和输出以及内部状态,来判断设计 功能是否存在问题。随着芯片的规模日益庞大,目前基于模拟的方法主要存在以 下两个不足:第一,模拟方法是不完整的,它很难发现那些埋藏在设计深处的设 计错误设计测试程序,譬如一个经典的错误就是英特尔的奔腾浮点除法错误,这 个被预计每过2 万5 千年才能被用户碰到的错误,却给英特尔公司造成超过4 亿美元损失:第二,模拟方法是非常费时的,比如对大型复杂设计使用模拟验证 通常需要几天或更多的时间,导致费时的原因在于设计的高度复杂性,极大的损 害了模拟时的可控制性和可观察性。 图1 i 功能验证分类 为了克服传统基于模拟功能验证方法的不足,自从上世纪8 0 年代以来,国 内外学者们开始寻找其它验证技术,现已取得不少突破。现阶段常用功能验证方 法,如图1 - 1 所示,主要可分为模拟验证、硬件仿真( h a r d w a r ee m u l a t i o n ) 和 形式验证( f o r m a lv e r if ic a tio n ) 这三类。硬件仿真是将待验证电路设计下载到 f p g a 芯片中,通过f p g a 的运行来仿真实际i c 的运行,运行过程和模拟类似, 也需要激励矢量。基于硬件仿真技术可将模拟过程加速几个数量级,但不足主要 有:( 1 ) 仿真所用的硬件仿真器( e m u l a t o r ) 价格昂贵:( 2 ) 将验证设计和仿真 器匹配需消耗较长时间;( 3 ) 与模拟技术一样,硬件仿真技术不能达到1 0 0 的 验证覆盖率。作为模拟验证补充的形式验证技术,近些年已成为验证领域重要研 2 浙江大学博一i :学位论文 第i 章引言 究方向,并取得了长足进展且已应用于解决实际验证问题。形式验证技术即是用 形式化方法来证明一个设计的实现满足其规范 1 。为理解其概念,可从下面这 个例子来形象说明形式化方法与模拟方法的本质区别。比如需要证明( x + 1 ) 2 = x 2 + 2 x + l 中等式两边对所有可能输入均得到相同结果。基于模拟的方法是用x 具体数值逐次检验等式两边是否相等,比如对x 从o 一1 0 0 分别赋值,如发现两边 不等价,则表示该等式不成立;而如果对以上赋值两边相等则仍需继续对x 赋值 检验。而用形式化方法来证明等式两边等价时,主要使用交换律,分配律等来推 理得到两边完全相对。比较发现,模拟方法不能确定公式的正确性,因为它是枚 举的,目前主要应用模拟方法来发现反例;而形式化方法却完全验证其公式两边 等价,这也就是以上两种方法本质区别所在。 在功能验证中,形式验证方法可达到1 0 0 的验证覆盖率,且不需要任何测 试激励:而基于模拟方法可用于发现反例,但很难证明设计电路没有错误。因此, 与模拟方法相比,形式验证是一种完整的方法。然后,形式验证方法的主要不足 是完成验证任务时需要较大计算时间开销或内存开销,目前能满足的设计仍然有 限,且需要各种限制。 已有形式验证主要可分为三类:分别是等价性验证( 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 ) 。等价性 验证用于验证两个结构化的描述是否等价,一般是对优化及修改前后的两个待验 证电路间进行比较,因此等价性验证通常也叫做逻辑验证或布尔验证:模型检验 用于验证某些设计属性被满足,通常可用有限状态机( f i n i t es t a t em a c h i n e ) 表示待检验的系统,用某种时态逻辑来表示系统应该具有的性质,然后再检验这 些属性;定理证明则验证电路满足其规范,首先将原始设计和待验证的性质用基 于某种逻辑的形式化系统的公式表示出来,再根据该形式化系统的公理、推理规 则以及已经证明的定理,一步步地推导出表达系统性质的公式,从而证明原始设 计满足该性质 2 。 由于模型检验和定理证明涉及技术层面较广,且目前只支持较小规模的电 路,因此目前工业界使用的大多数形式验证工具基于等价性验证。目前e d a 市场 上常用等价性验证工具包括美国c a d e n c e 公司的c o n f o r m a ll e c ,s y n o p s y s 公 司的f o r m a lit y 和m e n t o rg r a p h i c 公司的f o r m a l p r o 等。这些工具主要是面向 浙江人学博i j 学位论文第1 章引苦 组合电路的等价性验证,因此要求待验证的任务通过触发器匹配可完全转化为组 合电路验证任务。在现阶段设计流程中,每当设计有所修改或优化后,工程人员 通常会同时使用等价性验证工具和模拟验证工具来发现并纠正每个设计阶段引 入的错误;图1 - 2 中描述等价性验证工具在设计流程中的角色 3 ,不管是使用 硬件描述语言( 如y e r i l o g ) 的寄存器行为级( r t l ) 电路,乃至经过综合优化后 的门级( g a t e l e v e l ) 电路设计,直到经过物理布局后得到的l a y o u t 电路,都 可以调用等价性验证工具来验证各个阶段间电路的功能等价性。 尽管等价性验证已经取得了广泛的应用,现有工具仍存在较大局限性,主要 不足可归纳为以下三点:其一、对那些对应触发器不能完全匹配的大型时序电路 设计验证,因需要遍历的状态空间过大,至今尚缺乏有效验证策略:其二、即使 是组合等价性验证任务,对某些经过多次优化前后复杂设计验证仍耗时很多,且 结合多种验证引擎技术仍不够鲁棒( r o b u s t ) ;其三、当发现验证电路间不一致 即存在错误时,如何找到错误位置并纠正错误,已有等价性验证工具仍然缺乏精 确的设计错误诊断技术。 高层抽象i 矽。鬻 毋层抽裂 图1 2i c 设计流程中的等价性验证 4 浙江大学博l :学位论文第1 章引言 本论文中的等价性验证部分讨论内容,就是主要围绕这三个问题展开。对前 两个问题,即较难的组合等价性验证和时序等价性验证:文中提出了一些改进的 验证技术,并实现了完整的等价性验证系统,具体细节将在第3 章和第4 章中加 以论述。对设计错误诊断问题,由于和故障诊断问题相类似,主要在故障诊断技 术上加以扩展。 1 1 2 电路测试技术 为了在当今激烈的市场保持竞争力,电子产品的生产厂家就必须保证产品 的可靠性。而为了保证产品质量,在生产过程中就需要采用各类测试技术进行 检测,以及时发现缺陷和故障并进行修复。随着电路规模同益扩大,线宽的不 断缩小,集成电路的测试问题也日益重要,测试开销在芯片总成本所占比重越 来越大,目前芯片的测试成本已约占芯片成本的二分之一。 集成电路的测试是为了检验制造得到芯片是否存在缺陷,测试的正确性和有 效性将直接影响产品的品质。一个好的测试过程,是在尽量减少缺陷芯片通过测 试几率( 即d e f e c tl e v e l ) 的同时减少正确芯片不能通过测试的几率( 即y i e l dl o s s ) 4 】。现阶段,测试过程通常可分为以下三个步骤【5 】:( 1 ) 测试矢量的生成( t e s t g e n e r a t i o n ) ,可通过在设计阶段使用软件方法来得到二进制测试矢量;( 2 ) 测试 矢量的应用( t e s t a p p l i c a t i o n ) ,通常指测试工程师在自动测试设备( a u t o m a t i c t e s t e q u i p m e n t 即a t e ) 上将测试矢量加到电路输入端,比较电路的相应和期望值来 判断测试电路是否正确,如果待比较值始终相等,可认为电路是好的;( 3 ) 故障 诊断( f a u l td i a g n o s i s ) ,如果器

温馨提示

  • 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
  • 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
  • 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
  • 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
  • 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
  • 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
  • 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。

评论

0/150

提交评论