（电路与系统专业论文）集成电路的逻辑等价性验证研究[电路与系统专业优秀论文].pdf

浙江大学博士学位论史 摘要 摘要 集成电路规模的快速增长使得验征的难度越来越大，传统的模拟和 仿真不但需要花费大量的时间，而且不能保证完全的验证覆盖率，已经 不能满足现时集成电路设计的要求。形式验证利用数学的方法隐式遍历 所有可能的情况，能保证完全的验证覆盖率，所需要的验证时间也大幅 减少，是克服验证瓶颈的可行途径。等价性验证作为一种实用化的形式 验证方法，常被用于综合后和人工修改后电路的功能验证，本论文围绕 等价性验证在以下三个方面展开了有价值的研究： 1 在验证组合电路的等价性时，直接构建原始输出的b d d 并进 行比较的方法已经不再适用，需要发掘出两个待验证电路中等价的内部 结点，利用这些结点组成割集，将原有的验证问题分割成一系列小而简 单的子问题。针对割集在组合等价性验证中的运用，本文创新性地提出 了结合通用割集和专用割集的验证方法，针对由割集引起的误判，本文 提出了一种注重消除高层次结点间依赖关系的处理策略。基于i s c a s 8 5 电路的实验结果表明本文中的方法r 叮以有效加快组合电路的等价性验 证。 2 在验证时序电路的等价性时，常需要通过前时间帧计算 f p r e i m a g ec o m p u t a t i o n ) 半4 断某个状态是否由初始状态可达，它占用了全 部验证时间中的很大一部分，针对这种情况，本文创新性地提出了一种 利用状态缓存的时序验证方法，将模拟过程中到达的状态缓存为达状 态，同时缓存验证过程中被确认为不可达的状态，利用它们避免重复的 前时间帧计算，基于m c n c 9 1 的实验结果表明了本方法的有效性。 3 可满足性问题是近十多年来的一个研究热点，它已经超越了单 纯数学问题的范畴，被广泛应用于e d a 设计的各个方面。基于s a t 的 等价性验证方法更适于发掘电路中的不等价结点，对于实际等价结点的 验证，b d d 在内存占用刁i 是很高时具有更高的效率，本文提出了一种结 浙江大学博+ 学位论文 摘要 合b d d 和s a t 两种引擎的时序验证方法，首先运用b d d 引擎对结点进 行验证，如果验证过程中超过了设定的限制，再调i s a t 引擎，这样能 充分发挥它们各自的优点，对i s c a s 8 9 电路的实验结果表明，两种引擎 的结合可以有效地减少验证所需的时间。 关键词集成电路；形式验证：等价性验证；二叉判定图；可满足性问 题 浙江大学博士论文 a b s t r a c t a st h es i z eo fi n t e g r a t e dc i r c u i t si n c r e a s e sr a p i d l y ，t h e i rv e r i f i c a t i o n b e c o m e sm o r ea n dm o r ed i f f i c u l t t r a d i t i o n a ls i m u l a t i o na n de m u l a t i o nn o to n l y r e q u i r em u c ht i m e ，b u ta l s oc a n n o tg u a r a n t e ef u l lv e r i f i c a t i o nc o v e r a g e , i naw o r d ， t h e yc a n n o ts a t i s f yt o d a y sr e q u i r e m e n ti nt h ev e r i f i c a t i o no fi n t e g r a t e dc i r c u i t s f o r m a lv e r i f i c a t i o nu s e sm a t h e m a t i c a lm e t h o d st oe n u m e r a t ea l lp o s s i b l e c o n d i t i o n si m p l i c i t l y ，i tc a ng u a r a n t e ef u l lv e r i f i c a t i o nc o v e r a g ea n dn e e d sm u c h l e s st i m e ，i t saf e a s i b l ew a yt oo v e r c o m ev e r i f i c a t i o nb o t t l e n e c k a sb e i n ga p r a c t i c a lf o r m a lv e r i f i c a t i o nm e t h o d ，e q u i v a l e n c ec h e c k i n g i sa l w a y su s e dt o v e r i f yc i r c u i t s f u n c t i o n a l i t ya f t e rs y n t h e s i sa n dm a n u a lm o d i f i c a t i o n t h em a i n f o c u so ft h i st h e s i si se q u i v a l e n c ec h e c k i n ga n di tw a se x p l o r e di nt h ef o l l o w i n g t h r e ea s p e c t s ： 1 w h e nv e r i l y i n gc o m b i n a t i o n a lc i r c u i t s f u n c t i o n a l i t y ，i t sn o tf e a s i b l et o b u i l db d d sf o rp r i m a r yo u t p u t sd i r e c t l y t h ei n t e r n a le q u i v a l e n tn o d e ss h o u l db e d i s c o v e r e dt of o r mc u t s ，w h i c hc a nb eu s e dt os e p a r a t et h eo r i g i n a lv e r i f i c a t i o n p r o b l e mi n t o as e r i e so f s m a l la n de a s yp r o b l e m s a i m sa tu s i n g c u t si n 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 ，an e wm e t h o dc o m b i n i n gu n i v e r s a lc u ta n d s p e c i a lc u tw a sp r o p o s e d ；a i m sa tt h ef a l s en e g a t i v e sc a u s e db yc u t ，as t r a t e g y w h i c hp a i dm o r ea t t e n t i o no nr e m o v i n gd e p e n d e n c i e sa m o n gh i g hl e v e ln o d e s w a sp r o p o s e d e x p e r i m e n t a lr e s u l t sb a s e do ni s c a s 8 5s h o wt h a tt h em e t h o dc a n i n c r e a s ev e r i f i c a t i o ns p e e do fc o m b i n a t i o n a lc i r c u i t se f f i c i e n t l y 2 w h e nv e r i f y i n gt h ee q u i v a l e n c eo fs e q u e n t i a lc i r c u i t s ，al o to ft i m ei s s p e n to np r e i m a g ec o m p u t a t i o n ，w h i c hi su s e dt oj u d g ew h e t h e ra s t a t ec a nb e r e a c h e df r o mt h ei n i t i a ls t a t e an e wm e t h o du s i n gc a c h e ds t a t e sw a sp r o p o s e di n t h i st h e s i s s t a t e st h a tc a nb er e a c h e df r o mt h ei n i t i a ls t a t ei ns i m u l a t i o nw e r e c o l l e c t e da sr e a c h a b l es t a t e s ，s t a t e st h a tc a n n o tb er e a c h e df r o mt h ei n i t i a ls t a t ei n 浙江大学博上学位论义 a b s t r a c t v e r i f i c a t i o nw e r ec o l l e c t e da su n r e a c h a b l es t a t e s ，a n dt h e yw e r eu s e dt oa v o i d r e p e a t e dp r e - i m a g ec o m p u t a t i o n e x p e r i m e n t a lr e s u l t sb a s e do nm c n c 9 1s h o w t h ee f f i c i e n c yo ft h i sm e t h o d 3 s a t i s f i a b i l i t yi st h eh o t s p o to fr e s e a r c hi nr e c e n tt e ny e a r s ；i t sm o r e t h a na p u r em a t h e m a t i c a lp r o b l e m ，b u ti s u s e dw i d e l yi ne d ad o m a i n s a ti sm o r e e f f i c i e n ti nf i n d i n gn o d e st h a ta r en o te q u i v a l e n t ，w h i l eb d di sm o r ee f f i c i e n ti n p r o v i n gn o d e s e q u i v a l e n c e t h i st h e s i sp r o p o s e dan e wm e t h o dt h a tc o m b i n e d b d da n ds a ti ns 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 ，b d de n g i n ew a su s e df i r s tt o v e r i f yt h ee q u i v a l e n c eo fn o d e s ，i ft h el i m i tw a se x c e e d e d ，s a te n g i n ew a su s e d i n s t e a d ，i nt h i sw a y , b o t ho ft h e i rs t r e n g t hc a nb ee x e r t e d e x p e r i m e n t a lr e s u l t s b a s e do ni s c a s 8 9s h o wt h a tt h ec o m b i n a t i o no ft h e s et w oe n g i n e sc a nr e d u c e v e r i f i c a t i o nt i m ee f f i c i e n t l y k e y w o r d si n t e g r a t e dc i r c u i t ；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 ec h e c k i n g ；b i n a r y d e c i s i o nd i a g r a m ；s a t i s f i a b i l i y 浙江大学博士学位论文 图目录 图目录 图1 1 验证工具适用范围3 图1 2 层次化的电路设计4 图2 1 测试平台1 0 图2 2 模拟与形式验证在输出空间上的区别。1 2 图2 3 形式验证的分类13 图2 - 4 性质检验的过程1 4 图3 1 香农分解与二叉判定图一2 0 图3 2 布尔函数f = a b + c 在相同变量排序下的不同表示2 1 图3 3 对有序二叉判定图的简化：。2 2 图3 - 4 用二叉判定图表示电路。2 4 图3 5 不同变量排序对二叉判定图大小的影响2 8 图3 - 6 二叉判定图里的层互换3 0 图4 1 通过等价的内部结点对联接电路进行简化。3 5 图4 2 对规模较大的电路进行分割3 6 图4 3 基于割集构建局部b d d 3 7 图4 - 4 割集引起误判的发生3 8 图4 5 电路结点取值的学习过程。3 9 图4 - 6 基于转换的结构性验证流程图。4 0 图4 7 结合通用割集和专用割集的验证流程4 2 图4 8 通用割集和专用割集4 4 图5 1 时序电路的简单表示。5 1 图5 2 时序电路的联接电路m i t e r 5 2 图5 3 一个有限状态机的状态转移图5 3 图5 4 集合对应的真值表和b d d 5 4 图5 5 关系对应的特征函数和b d d 5 5 图5 - 6 利用状态缓存的时序验证流程。6 1 图5 7 状态转移图6 3 图6 1 典型的分支决策过程7 2 图6 2 添加学习的子句及非同步回溯7 6 图6 3 二输入与门的c n f 转换过程7 7 图6 - 4 二输入或门的c n f 转换过程7 7 图6 5 一个简单电路的c n f 格式表示7 9 i v 浙江大学博士学位论文 图目录 图6 - 6 时序电路的时间帧展开8 0 图6 7 基于时间帧展开的s a t 求解过程。8 1 图6 8 结合b d d 和s a t 的时序验证流程8 2 图6 - 9 同时验证所有原始输出的等价性8 3 v 浙江大学博士学位论文 表目录 表目录 表3 1i t e 运算表2 6 表3 2 常见布尔函数的b d d 复杂度2 9 表4 1 运用通用割集和专用割集验证组合电路的结果4 7 表4 2 传统依赖性处理策略和本文依赖性处理策略的比较4 8 表5 1 有限状态机的状态遍历过程一5 3 表5 2 利用状态缓存的时序等价性验证结果6 6 表6 1 常见逻辑门的c n f 格式表示7 8 表6 2 对经过s c r i p t r u g g e d 优化后电路的验证8 4 表6 3 对经过r e t i m e _ n 优化后电路的验证i 8 6 表6 - 4 对s c r i p t r u g g e d + r e t i m e 一1 1 优化后电路的验证8 7 v i 1 1 论文背景及意义 第1 章绪论 自从第一块集成电路于1 9 5 8 年在德州仪器公司问世，集成电路的发展一 直基本遵循着摩尔定律每隔1 8 个月，集成电路的集成度和性能就会翻一 番，而价格下降一倍。随着集成电路的规模很快从小规模集成电路( s s i ，门 数 1 0 8 ) ，电路的功能也越来越复杂。 集成电路设计是一项十分复杂的工程，任何微小的失误都可能造成巨大 的损失。1 9 9 4 年i n t c l 公司的p c n t i u m 芯片在上市后被发现存在浮点除法错误， 虽然这种错误发生的概率只有几亿分之一，但它仍给i n t c l 公司造成了4 7 5 亿美元的经济损失和难以估量的形象损失。1 9 9 6 年6 月4 日，欧洲航天局研 制的阿里亚娜五型火箭在发射后不到4 0 秒就爆炸坠毁，事后调查发现，错误 发生于当一个很大的6 4 位浮点数转换为1 6 位带符号整数时出现异常，细微 的错误导致数十年的努力毁于一旦。因此，验证对于一个成功的集成电路是 非常重要的，随着电路规模的不断增大，电路验证的难度也随之增加。从时 间花费、硬件投入以及人工投入来看，验证已经是很多实际设计过程中最主 要的一部分，套用i t r s 2 0 0 6 1 1 的说法，设计规划与实现正在逐渐成为验证 过程的前奏。据统计，在很多复杂的集成电路设计中，验证过程消耗了整个 设计周期的三分之二，设计过程中专门的验证工程师的人数一般是h d l 代 码编写人员的两倍，在设计完成时，模拟测试程序构成全部设计代码的 8 0 2 】。 造成这种局面的原因有两个，一是设计规模的增大引起了验证难度的增 新江大学博士学位论文：集成电路的逻辑等价性验证研究 加：二是历史上设计过程的重点被放在了其他诸如逻辑综合、布局布线以及 测试向量生成等方面并取得了很多突破，这也导致验证越来越成为设计过程 的瓶颈。如果再不能在验证方面取得大的突破，验证将成为半导体工业继续 前进最大的障碍，因此对集成电路的验证技术进行研究是十分必要的，这主 要有两方面的意义： ( 1 ) 对于产品设计本身而言，必须通过验证确保设计功能的正确性， 才能避免制造出错误的系统，避免造成时间、金钱和人力等各方 面的浪费； ( 2 ) 对于产品设计周期而言，为了能让产品更早的面市，占据市场的 先机，赚取最大的商业利润，必须在保证设计正确性的基础上， 用尽量少的时间完成验证的过程。 今天工业界主流的验证方法是不断重复的建立模型，选择一些特定的向 量进行模拟【3 】，【4 】，如果能碰巧发现错误，那就进行修改。但是这种测试方 法的覆盖率是很低的，哪怕在模拟上花费了数月的时间，也丝毫不能增加设 计者对于设计成功的信心；即使碰巧发现了错误，错误定位与分析也将是一 个耗时且令人生厌的过程。这种测试方法还有一个缺点，需要设计者很多人 工干预，模拟器不知道设计的哪个部分更关键，需要设计者指明方向以进行 更多的模拟；如果测试的覆盖率很低，需要设计者对设计进行深入的分析并 调整模拟的策略。 要使验证赶上设计的步伐，必须将集成电路的验证技术从特定向量的模 拟发展到形式化的验证方法。形式化的验i 正 4 1 【1 3 】是指用数学方法表达系统 的规范和性质，根据数学理论证明所设计的系统满足规范或具有期望的性质， 在不能满足规范或期望的性质时，则必然存在设计错误。形式化的方法具有 完全的验证覆盖率，但目前能处理的设计规模有限，不能验证规模很大的设 计，如图1 1 所示。传统的模拟方法虽然在设计规模很小时也能达到比较高 的验证覆盖率，而且也能被用于规模很大的电路的验证，但对于这些规模很 大的电路，模拟的验证覆盖率是很低的。半形式化验证方法 1 4 1 - 【1 6 】在两者 之间取了折中，它牺牲了一部分验证覆盖率以换取验证大规模设计的能力 【1 7 】。 验证覆盖率 设计规模 图1 1 验证工具适用范围 形式化验证方法和半形式化验证方法虽然具有比较高的验证覆盖率，但 现阶段在工业界的应用并不多，这里有两方面的原因，除了它们能处理的设 计规模有限这个原因外，另一个原因就是模拟这种验证方法已经“深入人心” ( 其实这是惯性的力量，因为工程师们都已经习惯用模拟的方法去验证设计， 并且过去很多年来一直如此) ，想要改变它或换用其他验证方法需要付出很高 的代价。 集成电路的验证是指检验电路实现是否达到设计规范的要求，它包括很 多方面，比如功能验证、时序验证、布图验证和电学验证等【4 】，本论文主要 研究功能验证。自顶向下的设计方法通常可以分成系统级、行为级、r t l 级、 浙江大学博士学位论文：集成电路的逻辑等价性验证研究 逻辑门级和版图级，如图1 2 所示。对电路的系统级、行为级描述，需要检 验它们是否与设计者的设想一致，这种验证又被称为设计验证( d e s i g n v e r i f i c a t i o n ) 1 8 1 ，因为设计者的设想常常没有用形式化的语言准确地描述下 来，因此很难将设计的所有方面都验证到，设计验证带有实验的性质就不足 奇怪了。设计验证一般可以通过定理证明和模型检验来完成，第2 章里将有 关于这两种方法的进一步说明。 高抽象层次 低抽象层次 满足规范? 满足规范? 功能等价? 功能等价? 功能等价? 图1 - 2 层次化的电路设计 除了设计验证，设计者还需要检验电路在行为级、r t l 级、逻辑门级、 版图级之间转化时是否保持功能的一致，这种验证也被分别称为实现验证 ( i m p l e m e n t a t i o nv e r i g c a t i o n ) 1 8 1 。电路在不同层次之间的转化一般是通过综 合工具来实现的，或许很多人会认为综合的理论基础是正确的，而且综合工 具的正确性已经被很多设计实例所验证，综合后的结果应该与综合前的保持 一致，但事实却并非如此【1 9 】，1 2 0 】。造成这种结果的原因有多个：综合算法 的复杂性以及综合过程本身会引入错误；综合过程中各种优化选项的加入会 使综合结果偏离设计者的设想；综合后的结果没有设计者设想的那么好( 如 关键路径过长) ，设计者需要对综合结果人工修改。实现验证一般可以通过等 绪论 价性验证来完成，对等价性验证方法和工具的研究可以： ( 1 ) 确保综合前后电路功能的一致性，避免由于优化选项的加入和综 合工具本身的原因而导致综合后的电路发生功能错误； ( 2 ) 确保人工修改前后电路功能的一致性，人工修改的目的是改进电 路的性能，如减小关键路径的长度、减少面积等，如果修改导致 了功能错误，性能的改进将毫无意义。 1 2 论文的主要工作与创新点 论文在分析集成电路验证方法的基础上，对等价性验证进行了详细深入 的研究。二叉判定图( b i n a r yd e c i s i o nd i a g r a m ，b d d ) 2 1 i 可以被用于正则的表 达布尔函数，是现在等价性验证中用得最多的引擎，本文基于b d d 开展了 下面两个方面的研究工作： ( 1 ) 基于b d d 的组合等价性验证：组合电路是一切电路的基础，从组 合电路入手可以更容易理解等价性验证的本质，也更容易开发出 实用的验证工具，对于两个组合电路，组合等价性验证就是判断 对于所有可能的输入，它们是否都有相同的输出； ( 2 ) 基于b d d 的时序等价性验证：实际产品中的电路一般不会是完全 的组合电路，对时序电路的等价性验证进行研究将更有实用价值， 时序电路比组合电路多出了时序元件( 如寄存器、锁存器等) ，因 而也就比组合电路多出了状态，相比组合电路，它的验证难度大 为增加，对于从初始状态出发的两个时序电路，时序等价性验证 就是判断对于所有可能的输入，它们在所有的状态上是否都有相 同的输出。 可满足性问题( s a t i s f i a b i l i t y , s a t ) 2 2 是近十多年来的一个研究热点，它 已经不仅仅是一个数学问题，而是被广泛应用于等价性验证、模型检验、自 动测试向量生成等e d a 设计的各个方面，本文基于s a t 开展了下面的研究 浙江大学博士学位论文：集成电路的逻辑等价性验证研究 工作： ( 3 ) 基于b d d 和s a t 的时序等价性验证：由于时序电路的状态数目 随着状态变量数目的增加而指数级增长，而且b d d 本身容易受到 内存爆炸的影响，而s a t 本身并不保存电路的状态或电路结点的 功能信息，不容易受内存爆炸的影响，将两者结合在验证过程中 将可以增大时序电路的验证规模，提高验证的速度。 论文在以下几个方面做出了创新： ( 1 ) 提出了结合通用割集和专用割集的组合等价性验证方法：通用割 集可以被用于所有c e p 的验证，通过它可以使中间结点的b d d 得 到重复利用，专用割集只被用于某一对c e p 的验证，通过它可以 避免在验证过程中占用过多内存，两者的结合既可以避免内存爆 炸的出现，还可以提高验证速度； ( 2 ) 提出了注重消除高层次结点间依赖关系的依赖性处理策略：因为 高层次结点间的依赖关系更容易引起误判，而且消除高层次结点 间的依赖关系需要付出的代价更小，这种策略能在消除依赖性与 付出的代价之间达到最佳的平衡； ( 3 ) 提出了利用状态缓存的时序等价性验证方法：在时序电路的等价 性验证过程中，为了判断一对结点或寄存器是否确实不等价，需 要判断状态是否由初始状态可达，这就是前时间帧计算，本文中 的方法缓存了模拟时的可达状态和验证过程中的不可达状态，利 用它们避免了重复的前时间帧计算。 ( 4 ) 提出了结合b d d 和s a t 的时序等价性验证方法：s a t 不容易受到 内存爆炸的困扰，适于发掘电路中的不等价结点，但对于实际等 价结点的验证，b d d 在内存占用不是很高时效率更高，文中的方 法结合了b d d 和s a t ，可以发挥它们各自在验证等价结点和不等 6 价结点时的优势，使验证速度更快，内存占用更少。 1 3 论文的组织结构 论文的组织结构安排如下： 第一章首先介绍了论文的背景及研究形式验证的意义。随着集成电路规 模的快速增加，传统的模拟已经不能满足要求，形式化验证方法通过数学手 段来完成验证，不需要测试向量，能达到完全的验证覆盖率，能好地弥补模 拟方法的不足。接着介绍了论文的主要工作以及在等价性验证中取得的创新， 最后是论文的组织结构安排。 第二章对常见的电路验证技术作了简单的分类，并比较它们各自的优缺 点。针对形式验证，介绍了常见的形式验证方法及它们各自适用的集成电路 设计的不同阶段，本论文主要关注等价性验证，它被广泛用于综合前后及人 工修改前后电路的验证。 第三章介绍了形式验证中最常见的数据结构二叉判定图。为了将其 用于电路的形式验证，还必须引入精简的有序二叉判定图。还介绍了二叉判 定图的性质及如何将它用于电路的验证中，二叉判定图的运算和变量排序是 本章介绍的重点。 第四章介绍了组合电路的等价性验证。常见的组合等价性验证分为功能 性验证方法和结构性验证方法，结构性验证方法可以使复杂的电路验证问题 简单化，本文对结构性验证方法中的割集和误判进行了详细的研究，在此基 础上提出了结合通用割集和专用割集的验证方法，针对割集引起的误判，提 出了注重消除高层次结点间依赖关系的依赖性处理策略。 第五章介绍了时序电路的等价性验证。常见的时序等价性验证方法是状 态遍历，对于规模越来越大的时序电路，这种方法已经不再适用，必须从时 序电路间的等价信息入手将时序验证问题组合化，这就是基于寄存器匹配的 时序验证方法。为了判断状态是否由初始状态可达，必须进行前时间帧计算， 浙江大学博士学位论文：集成电路的逻辑等价性验证研究 针对其中大量的重复计算，本文提出了利用状态缓存的时序验证方法。 第六章介绍了基于b d d 和s a t 的时序等价性验证。s a t 不像b d d 那样 容易受到内存爆炸的影响，近年来对它的研究越来越多，首先介绍了s a t 这 种数据结构的定义及常见的求解可满足性问题的算法d p l l 算法，针对 电路问题，如果能利用好电路的结构信息，将显著提高s a t 算法的效率。b d d 在证明结点的等价性方面具有优势，而s a t 在发掘电路内的不等价信息方面 具有优势，本文提出了一种结构b d d 和s a t 的验证方法，并将其用于时序 电路的等价性验证。 第七章首先对论文作了总结，然后对论文的下一步工作做了展望。 集成电路设计验证综述 第2 章集成电路设计验证综述 2 1 验证方法分类 为了确保电路功能的正确性，必须对设计后的电路进行功能验证，验证 有很多种方法，也有很多种实用的工具，如s y n o p s y s 公司有v c s 和f o r m a l i t y ， c a d e n c e 公司有n c v e r i l o g 、n c v h d l 以及f o r m a l c h e e k ，m e n t o r 公司有 m o d e l s i m 和f o r m a l p r o ，但它们基本都可以划分为两类：基于模拟的验证方 法和形式化的验证方法( f o r m a lv e r i f i c a t i o n ) 1 ， 2 】，【4 】， 5 1 ，它们之间的主要区 别在于前者需要测试向量，而后者不需要。还可以从另外一个角度区分它们： 模拟方法是面向输入的，因为设计者需要给定输入向量进行测试，而形式验 证是面向输出的，设计者需要提供待测试的输出特性【4 】。近年来还发展了一 种混合型的验证方法，它结合了基于模拟的验证方法和形式化的验证方法， 被称为半形式化验证( s e m i f o r m a lv e r i f i c a t i o n ) 。基于模拟的验证方法按照运 行平台的不同，又可以分为软件模拟( s i m u l a t i o n ) 和硬件仿真( h a r d w a r e e m u l a t i o n ) 。 2 1 1 软件模拟 模拟是出现的最早也是最常用的功能验证方法，它的工作原理如图2 - 1 所示【2 3 l 。将待测试的设计( d e v i c eu n d e r t e s t ，d u t ) 置于测试平台( t e s t b e n c h ) 中，通过测试平台在设计的输入端口加上激励信号，在设计的输出端口观察 响应并与预测结果进行比较。 直观的模拟方式( 或叫专门测试，a d h o cv e d f i c m i o n ) 不但需要设计者 指定输入激励信号，还需要设计者指定输出响应，在电路规模较大时，这种 方式就会很繁杂，效率不高。为此可以引入用高级语言如s y s t e m c 或c c + + 描述的参考模型( 也叫黄金模型g o l d e nm o d e l ) 1 ，在待验证设计和参考模型 9 浙江大学博士学位论文：集成电路的逻辑等价性验证研究 的输入同时加上激励信号，通过它们输出的比较可以判断设计的功能是否正 确。 - - - - - - - - d - - - - - - _ 输出响应 输入激励d u t 比较 - - - - - j 图2 - 1 测试平台 软件模拟可以分为事件驱动的模拟( e v e n t d r i v e ns i m u l a t i o n ) 和基于周期 的模拟( c y c l e b a s e ds i m u l a t i o n ) 4 。事件驱动的模拟将电路中任何结点逻辑 值的变化视为一个事件，这个事件触发了电路中其他一系列结点逻辑值的变 化，它同时覆盖了设计的功能和时序模型，结果精确，能探测到设计中的毛 刺电路，尤其适用于异步电路的模拟，目前常用的模拟器v c s 和m o d e l s i m 都属于这种类型。基于周期的模拟只关心电路在时钟边界上的逻辑值，而忽 略电路在时钟周期内的变化，它比事件驱动的模拟更快捷，但不能提供完整 的时序信息。 模拟验证的质量可以通过测试的覆盖率来衡量，常用的覆盖率准则有代 码覆盖率和功能覆盖率。代码覆盖率是指测试过的代码在所有代码中的比例， 它可以是执行过的语句的百分比或是经历的分支语句的百分比，功能覆盖率 是指测试过的功能在所有功能中的比例。通过覆盖率分析可以使设计者的后 续测试更有针对性，为未被测试的部分编写特定的输入激励，同时去除对己 验证部分的重复测试。 模拟的特点是简单、容易实施，而且非常直观( 很多模拟软件都提供波 形文件) ，但也有非常致命的弱点：耗费时间长，例如对于一个3 2 位的比较 器电路，如果模拟器l m s 能完成一次模拟，那模拟完全部2 ”2 ”= 2 “种可 能的输入向量需要的时间为： 1 0 集成电路设计验证综述 缫3600x243 6 5 硼4 ，9 4 2 年 这么长的模拟时间对于任何设计都是不能忍受的，也是不现实的。除了 耗费时间长，模拟还有另一致命弱点：验证覆盖率严重依赖于输入向量，除 非将所有可能的输入向量都模拟一遍，否则不能保证完全的验证覆盖率。 2 1 2 硬件仿真 硬件仿真将电路设计下载到诸如f p g a 的硬件中，通过f p g a 的运行来 仿真实际i c 的运行。它的运行过程与软件模拟类似，也需要输入测试向量， 然后在芯片的输出引脚观察波形，通过特有的软件可以观察f p g a 内部信号 的取值变化，如x i l i n x 公司的c h i p s c o p e 软件和s y n p l i f y 公司的i d e n t i f y 软 件。 硬件仿真相比模拟最大的优点就是速度得到了提高，一般来说会提高了 好几个数量级，但与模拟相比，它只能观察芯片引脚信号或仿真软件设定的 信号，如果要观察其他信号的取值变化，必须在仿真软件里重新设定然后再 次仿真。硬件仿真还有其他一些缺点：比如硬件仿真器价格昂贵、可以仿真 的设计规模受到f p g a 门数的限制。 硬件仿真提供了一个比模拟更加真实的实验环境，而且由于仿真的速度 基本与实际芯片差不多，因而可以在f p g a 平台上运行软件，演示产品的工 作过程，现在很多产品的开发都要经过f p g a 验证这一关。与模拟一样，硬 件仿真难以保证测试的完全性，因为它只能证明设计错误的存在，而不能保 证设计错误的不存在。 2 1 3 形式验证 随着集成电路规模的不断增大，模拟需要的时间已经超过设计人员容忍 的极限，而仿真与模拟一样不能保证完全的验证覆盖率，作为一种新型的验 证方法，形式验证【4 】- 【1 3 】越来越受到人们的重视。形式验证是指用数学的方 浙江大学博士学位论文：集成电路的逻辑等价性验证研究 法隐式遍历所有可能的情况，它不需要测试向量，能达到模拟和仿真无法企 及的完全的验证覆盖率，在过去十多年中得到了广泛研究与应用。 模拟是先产生输入向量，再根据输入向量得到参考输出；而形式验证正 好相反，首先对设计进行分析，得到期望的输出行为，再用形式化的验证工 具去证明或反证明这些行为。因此可以说模拟是输入驱动的，而形式验证是 输出驱动的。 模拟可以看作是在验证输入空间上的点，除非将每一个点都模拟一遍， 否则就有错误存在的可能；而形式验证工具工作在性质的层面上，对于一条 待验证的性质，形式验证工具会隐式地穷尽所有可能的输入和状态。因此从 输出的角度去观察，模拟一次只检验一个输出点，如图2 - 2 ( a ) 所示，而形式 验证一次检验一组输出点，如图2 - 2 ( b ) 所示，图中每个方框都代表一条性质。 因此如果想要完全地验证一个设计，必须对所有的性质都验证一遍，这比遍 历所有可能的输入更实际，也更容易完成【4 】。关于形式验证，在第2 2 节将 有详细的介绍。 o o o o o o o o o o o o ( a ) 模拟 o o o o 三图 o o o o ( b ) 形式验证 图2 2 模拟与形式验证在输出空间上的区别 2 1 4 半形式化验证 形式验证具有完全的验证覆盖率，所需要的验证时间短，但也有缺点： 由于发展时间短，不成熟，能成功验证的设计规模不是很大。半形式化验证 【1 4 - 【1 6 】结合了传统的模拟验证和形式验证的思想，试图充分发挥这两种验 集成电路设计验证综述 证方法的优点。 半形式化验证将形式化方法( 特别是模型检验) 的分析、搜索技术同模 拟方法结合起来，模拟的结果被作为形式验证的起点，形式验证的反例被用 于重新引导模拟，两者互相结合、交替进行。对于形式化方法来说，它只分 析了全部状态空间的一部分，因而不如纯粹的模型检验那样容易受到内存爆 炸的困扰，在规模更大的电路验证中也能运用；对于模拟来说，它从形式验 证的结果得到了指引，更有针对性，能覆盖更多的边界情况。 基于断言的验证( a s s e r t i o nb a s e dv e r i f i c a t i o n ，a b v ) 就是一种典型的半形 式化验证方法j 断言可以描述设计的输入、输出等功能行为，可以被嵌入在 设计代码( 如v e r i l o g ) 中，也可以被放在一个单独的外部文件里，在模拟或 形式验证的过程中对断言进行检查，通过检查结果设计者就能知道设计是否 满足所描述的功能行为。 2 2 形式化验证方法分类 经过十几年的研究，形式验证有了一定的发展，出现了很多种验证方法， 常见形式验证的分类【2 】，【4 】- 【1 3 】，【2 4 】如图2 - 3 所示： 图2 - 3 形式验证的分类 等价性验证一般用于确保设计实现( i m p l e m e n t a t i o n ) 与设计原型 浙江大学博士学位论文：集成电路的逻辑等价性验证研究 ( s p e c i f i c a t i o n ) 的一致性，它多用于低层设计之间的验证，如r t l 级、门级和 版图级之间的验证等。但如何确保设计原型的正确性呢? 此时就需要用到性 质检验，性质检验是指对一个实现方案，用形式化的方法检验它是否满足某 些规则或性质，它多用于高层，如行为级验证。在性质检验过程中，首先需 要对系统模型和待验证的性质进行形式化的描述：如将系统用有限状态机的 形式表示，将待验证的性质用形式逻辑表示，再用验证工具检查性质是否得 到满足 2 4 1 ，如图2 - 4 所示。 图2 - 4 性质检验的过程 表现在具体的设计过程中，设计者根据产品要求写出系统的行为级描述 后，需要用定理证明或模型检验技术验证其正确性，通过这一关之后，设计 者需要将行为级描述逐步转化为r t l 级、门级和版图级描述，每一步转化之 后的描述都需要用等价性验证来确保功能的一致性。 国内对形式验证的研究起步比较晚，但近年来很多大学和科研院所开展 了这方面的研究工作，如中科院在可满足性问题、等价性验证和模型检验作 了很深入的研究【2 5 】_ 【2 9 】，复旦大学在可满足性问题及其在等价性验证中的 应用上作了很多研究【3 0 】一 3 3 1 ，清华大学在r t l 的可满足性问题上也作了研 究【3 4 】一 3 6 1 ，西安邮电学院在模型检验及s o c 的等价性验证方法作了很多工 作【2 】，【1 4 】，【3 7 】，浙江大学在可满足性问题及等价性验证方面也展开了研究工 作【3 8 】_ 【4 2 】。 2 2 1 等价性验证 在图1 2 所示的层次化电路设计中，电路设计从行为级被综合成r t l 级，再综合成逻辑门级，最后得到版图级，这期间综合工具的优化操作可能 1 4 集成电路设计验证综述 会引入错误，致使综合前后的电路功能不一致；为了满足时序、面积等方面 的要求，常需要对r t l 代码和电路版图做人工修改，这也可能引入错误。为 了确保综合前后、人工修改前后电路功能的一致性，就需要等价性验证。 由于逻辑门级电路的描述准确、简洁，对于非同一层次的等价性验证， 一般都是将它们转化为门级再进行验证，例如对r t l 级电路进行综合( 当然 没有一般综合时的优化操作) 、对版图级电路进行提取以得到门级电路然后再 验证。如果没有特别说明，本文中的等价性验证一般都是指两个门级电路之 间的验证。 对于两个组合电路，它们的等价性验证就是判断对于任何可能的输入， 它们的输出是否具有相同的取值。因为时序电路的输出不但与输入有关，还 与当时所处的状态有关，因此对于两个时序电路，等价性验证工具需要判断 对于所有可能的输入序列，它们是否具有相同的输出。 等价性验证方法一般分为功能性的和结构性的。功能性方法是指直接比 较两个电路的输出功能，如对组合电路，直接构建它们输出的功能函数，再 对两个电路对应输出的功能函数进行比较，这样就可以对这两个电路的等价 性做出判断，最常见的方法就是基于输入构建输出的精简的有序二叉判定图 ( 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