（微电子学与固体电子学专业论文）时序电路的功能验证方法和技术研究.pdf

j e 瘟銮道太堂鲤堂僮垃塞生塞摘蓬 中文摘要 摘要：为了解决验证成为集成电路与系统设计行业瓶颈的现状，避免设计后期发 现错误的昂贵修补代价，尽早发现设计的错误，本论文主要研究了设计前端的功 能验证方法和技术。将现阶段数字电路中使用较多的时序电路作为研究对象，采 用仿真验证的评估方法进行分析，通过分析大量仿真实验数据作为依据，利用代 码和功能覆盖率结合的评估方法进行综合分析，比较两种基于不同建模方法( 基 于状态转换表和基于状态转换图) 的功能验证方法，总结出适合时序电路的验证 方法。 本文首次比较基于状态转换表和基于状态转换图的功能验证方法，并总结出 两种方法各自的特点和适合时序电路功能验证的方法，为验证工程师挑选验证方 案提供了有利的数据支持。实验证明：由于基于状态转换图的验证方法具有实现 简单，算法搜索效率高，产生的测试序列短，仿真运行时间短及很高的有效性， 容易实现自动化等优点，所以适合于大中规模时序电路的验证。而基于状态转换 表的方法虽然原理简单。但测试序列很长而且有效代码率不离，有效性差，且随 着设计规模的扩大，尤其是对时序电路这样复杂的电路形式来说，测试向量会随 着输入变量和状态数的增加成指数增加，最终使仿真时问过长，成为不可能完成 的任务。所以对于时序电路而言，基于状态转换图的方法是更加适合的验证方法。 本文也尝试了功能覆盖率和代码覆盖率结合的评估方案，及断言与仿真验证结合 的功能覆盖率检查方法，使仿真结果透明化，具有更高的可观测性。结果表明： 功能覆盖率和代码覆盖率结合在一起为设计和验证提供了一个完整的质量验证标 尺。 关键词：功能验证；仿真验证；功能覆盖率；代码覆盖率；状态转换图；状态转 换表；时序电路；u s b i p 核 分类号： j e 塞窑逼太堂亟堂焦监窒 垦墨! 基! a b s t ra ( 了r a b s ，r r a l 了r i no r d e rt os o l v et h ep r o b l e mt h a tv e r i f i c a t i o nh a sb c c a m et h eb o t t l e n e c ko fi c ，- _ 一 d e s i g na n ds y s t e md e s i g ni n d u s t r y , t oa v o i dt h eh i g hr e p a i rc o s to ff i n d i n gf a u l t si nt h e d e s i g na n a p h a s e , a n dt of i n df a u l t s a ss o o na sp o s s i b l e , t h ef u n c t i o n a lv e r i f i c a t i o n m e t h o d sa n dt e c h n o l o g i e si nt h ei cf r o n t e n dd e s i g ni nt h i sd i s s e r t a t i o na i er e s e a r c h e d 功ed i s s e r t a t i o nt a k e st h es e q u e n t i a lc i r c u i t 鹊s t u d y i n go b j e c ta n du s e sm a n yk i n d so f s i m u l a t i o nv e r i f i c a t i o nc o v e r a g et oa n a l y z et h eg r e a td e a lo fe x p e r i m e n td a t a , i n c l u d i n g c o d ec o v e r a g e a n df u n c t i o n a lc o v e r a g e t h e nt w od i f f e r e n tv e r i f i c a t i o nm e n l o d 譬一 b a s e ds t a t et a b l ea n db a s e ds t a t ec h a r ta r ec o m p a r e d ，a n df i t t i n gs e q u e n t i a lc i r c u i t m e t h o di ss u m m a r i z e d v e r i f i c a t i o nm e t h o db a s e ds t a t et a b l ea n dm e t h o db a s e ds t a t ec h a r ta r ec o m p a r e d f o rt h ef i r s tt i m e , a n dc h a r a c t e r i s t i c so ft w om e t h o d sa n df i t t i n gs e q u e n t i a lc i r c u i t m e t h o d sa r es u m m a r i z e d e x p e r i m e n ta p p r o v e st h a tv e r i f i c a t i o nm e t h o db a s e ds t a t e c h a ne x c e e d st h em e t h o db a s e ds t a t et a b l ei ns i m p l i c i t y , s e a r c ha r i t h m e t i ce f f i c i e n c y , t e s t i n gs e q u e n c el e n g t h ，t e s t i n gs p e e da n dv a l i d i t y b e c a u s ei ti se a s yf o ra u t o m a t i o n ，i t m o r es u i t sf o rl a r g eo rm i d d l es c a l ec i r c u i t s o nt h eo t h e rh a n d , t h em e t h o db a s e ds t a t e t a b l ep r o d u c e sf u l l s c a nl e s tv e c t o r s a l t h o u g hi th a ss i m p l ep r i n c i p l e ，b u ti tw i l lh a s m o r ea n dm o r et e s tv e c t o r , t i l lb e c o m e st h ei m p o s s i b i l i t yw i t hi n c r e a s e do fc i r c u i ts c a l e ， e s p e c i a l l yw h e nc o p ew i t hs e q u e n t i a lc i r c u i t s ot ot h es e q u e n t i a lc i r c u i t ，t h em e t h o d b a s e ds t a t ec h a r ti sm o r es u i t a b l e i nt h i sd i s s e r t a t i o n , t h ee v a l u a t i n gs c h e m et h a t f u n c t i o n a l c o v e r a g ec o m b i n e dc o d ec o v e r a g ei sa d o p t e d 1 1 i ef u n c t i o n a lc o v e r a g e c h e c k i n gm e t h o dw h i c h a s s e r t i o nc o m b i n e ds i m u l a t i o ni sa d d r e s s e di nt h i sd i s s e r t a t i o n i tc l a r i f i e ss i m u l a t i o nr e s u l t sa n dm a k e st h es i m u l a t i o nm o r eo b s e l n a b l e 1 1 l ec o n c l u s i o n s h o w st h a tf u n c t i o n a lc o v e r a g ec o m b i n e dc o d ec o v e r a g ep r o v i d ea ni n t e g r a t e dq u a l i t y v e r i f i c a t i o ng a u g e k e y w o r d s ：f u n c t i o n a lv 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 ；f u n c t i o n a lc o v e r a g e ； c o d ec o v e r a g e ；s t a t ec h a r t ；s t a t et a b l e ；s e q u e n t i a lc i r c u i t ；u s bi pc o r e c l a s s n 0 ： 致谢 本论文的完成离不开老师和同学们对我在研究技术和研究思想上的帮助、指 导和支持，在此，向他们一一表示感谢。 首先感谢我的导师骆丽教授在毕业设计期间对我的悉心指导，是她凭借自己 在科研领域敏锐的洞察力和先进的研究理念帮我加深了毕业设计的理论深度，挖 掘出其中的学术价值。在骆丽教授的引导下，我通过比较现有验证方法，总结出 毕业论文中提出的时序逻辑电路适合的验证方法。在两年半的研究生学习过程中， 谢谢老师对我的谆谆教导。 此外，还要感谢李哲英教授，他在我们导师出国和生病期间给我提供了很多 的指导和帮助。李哲英教授一丝不苟的工作态度和严谨求实的治学风范给我留下 了深刻的印象，在引领我学习和科研的同时，他也教会我很多为人治学之道。我 的毕业设计正是在李哲英教授的指导下才得以顺利完成。在此，向李哲英教授表 示诚挚的谢意。 还要感谢我的同学们，有问题请教他们都会给我耐心的解答，在论文写作过 程中，也给了我莫大的帮助，尤其是要感谢我的室友邢强，还在生活上给了我很 多的帮助。 最后，感谢我的父母，他们对我的关爱和支持是我不断进步的动力。 韭裹銮适太堂亟堂僮论塞 j 直 1 1 验证的意义 1 引言 整个集成电路行业逐步形成集成电路( i n t e g r a t e dc i r c u i t ，简称i c ) 设计、芯 片制造、芯片封装三大行业l l l 2 1 1 3 l 。其中，芯片制造和封装行业发展速度大大超过 了i c 设计行业的发展，使设计生产率拖累了工艺进步可能带来的设计规模的提高， 出现了设计生产鸿沟，如图1 。而i c 设计行业中的设计和验证领域也发展不平衡， 验证的发展水平落后于设计的发展水平，出现了验证鸿沟，如图2 所示。 随着设计规模和复杂性的不断增加，尤其是知识产权( i n t e l l e c t u a lp r o p e r t y ， 简称口) 重用等当前复杂片上系统( s y s t e m o nc h i p ，简称s o c ) 设计的出现，要 求对设计的功能进行更加充分的验证。2 0 0 3 年度的国际半导体技术发展报告指出， 验证已经成为集成电路设计流程中开销最大的工作。在目前的工程项目中，验证 工程师的数目超过了设计工程师，对于复杂设计更是达到2 ：1 或是3 ：1 的比率。 造成这种局面的原因有：一方面是设计规模正如摩尔定律所指出的呈指数增长。 如果用设计中的状态数目来衡量功能复杂度，则设计的功能复杂度随着设计规模 又呈指数增长。如此惊人的发展速度，对验证技术的处理能力提出了极大的挑战； 另一方面，历史上对设计流程中的其他环节( 如逻辑综合、布局布线) 的问题关 注颇多，而对验证重视不够，造成验证成为目前行业发展的瓶颈。如果没有重大 突破，验证将成为未来集成电路设计流程中的重大障碍。因此，对验证方法和技 术进行研究对于现阶段集成电路发展有着重要的意义。 图1 设计生产鸿沟( t h eg a pb e t w e e nd e s i g na n dm a n u f a c t u r e ) 北塞銮适太堂鲤堂僮监塞王l 畜 设计复杂性 图2 验证鸿沟( t h ev e r i f i c a t i o ng a p ) 1 2 验证的基本概念 验证是证明一个设计能正确实现其功能的过程1 4 j 。验证不是一个测试平台，也 不是一系列测试平台( t e s t b e n c h ) ，使用汇聚模型可以从概念上清晰地描述验证 过程，如图3 所示。其中变换( t r a n s f o r m a t i o n ) 可以是任何包含有输入输出的过 程，例如根据规范( s p e c i f i c a t i o n ) 写出寄存器传输级( r e g i s t e r t r a n s f o r m a t i o nl e v e l ， 简称r t l ) 代码、扫描链的插入、把r t l 级代码综合为门级网表、根据门级网表 布局布线等。验证过程是一个相反的过程，它从变换的结果出发回到起点。 变换( t r a n s f o r m a t i o n ) 验证( m e r i f i c a t i o n ) 图3 验证过程( t h ep r o c e s so fv e r i f i c a t i o n ) 验证是一个永远也不会完成的过程，因为验证只能证明存在错误，不能证明 不存在错误。即验证的错误类型可分为i 型和型两种，如图4 。i 型错误( 也叫 否定错误f a l s e n e g a t i v e ) 是比较容易验证的类型，就是在不存在错误的地方发现 了错误。一旦错误的解释被证实，验证结果的答案将从否定到肯定，那么错误就 不再存在了。i i 型错误( 也叫肯定错误f a l s e p o s i t i v e ) 是最严重的一种，就是把有 错的设计认为是没有错误，带有潜在的危险。所以，验证过程一定要避免l l 型错 误的发生。 2 j e 塞窑道太堂亟堂焦i 金塞i l 言 差的 设计 好的 设计 有错误没错误 类犁h 肯定错误 类型i 否定错误 图4 错误类型( t y p e so fe n o r ) 1 2 1 验证在设计流中的地位 集成电路的设计经历了从小规模( s s l ) 、中规模( m s i ) 到大规模( l s i ) 、超 大规模( v l s i ) 的发展，集成电路内晶体管的数量按照摩尔定律高速发展，现在 已经进入了s o c 的开发阶段。 随着设计规模的扩大，设计方法和各种e d a ( e l e c t r o n i cd e s i g n a u t o m a t i o n ) 工具也不断的改进。现在一般的数字集成电路的设计流程【5 】如图5 所示。 一 一 ，i ， ) ，；，& & 等等。 3 、验证层( v e r i f i c a t i o nl e v e l ) 验证层描述一些引导性内容，用于指示验证 工具对时序层所描述的设计属性采用何种方式进行处理。如针对该属性的内容来 1 7 韭瘟銮通太堂亟堂僮纶塞 笾墓验适殴迁毡 进行模型检验，还是以该属性为约束规范设计的外部输入信号，或是确定该属性 描述的内容是否被验证过程触发等，此外验证层还包括为了便于引导性内容的描 述建立的一些结构。验证层包括的命令有a s s e r t ，& q c u m e ，c o v e r 等和验证的单元 v m o d e ，v p r o p ，v u n i t 等等。 4 、建模层( m o d e l i n gl e v e l ) 建模层用于描述验证环境。针对形式化验证和 仿真验证，建模层提供不同的环境建模方法。 要结合断言描述语言的四个层次进行功能属性描述，比如在仲裁器中要检查 “应答信号( g n t a ) 在没有请求信号( r e q a ) 的条件下绝对不会发生”，这样一 个功能属性( a 1 ) ，用p s l 语言描述如下： p s la l ；a s s e r tn e v e rc m t a & & ! r e q a 三、基于断言的验证方法 基于断言的验证方法，实质上只是一种工具。它可以和动态仿真相结合，得 到更好的可观测性和覆盖率；也可以和静态形式验证相结合，获得更好的可控性。 本文是利用断言与仿真相结合，研究其功能覆盖率。整个断言验证的过程1 9 j 如图 1 0 所示。 3 2 6 小结 图1 0 断言验证方法( a s s e r d o nv e r i f i c a t i o n ) 各种覆盖指标都有各自的优缺点和适用的范围，总结如表2 。 表2 各种覆盖指标的比较( t h ec o m p a r i s o no f c o v e r a g e ) 覆盖类型优点缺点应用 代码覆盖简单易行 不够准确最基本的覆盖 完整正确的f s m 提取适合基于状态机模型的 状态机覆盖容易查错，概念清晰 困难设计 错误模型覆盖有针对性代价昂贵验证后期 辅助代码的添加会影 标记覆益针对性强关键处的查错误 响仿真结果 功能覆盖容易理解，有效很难完全重要的设计 韭裹至垣态堂亟堂焦：i 金塞值裹坠延的置信 3 3 评估方案 基于3 2 节各种覆盖的比较，其中代码覆盖率是最基本的，也是不可缺少一种 覆盖率，但简单的1 0 0 代码覆盖率无法保证设计被1 0 0 验证；而对于功能验证 来说，功能覆盖也是很重要的，功能验证可以有效的表明哪些功能已经经过测试， 根据这些信息调整测试激励的产生，但是功能覆盖率并不能完全的代替代码覆盖 率，代码覆盖率在保证代码书写质量上仍有着重要的地位，只有当代码覆盖和功 能覆盖都达到1 0 0 时，才可以认为设计得n t 比较好的验证，功能覆盖率和代码 覆盖率结合在一起为设计和验证提供了一个完整的质量验证标尺。所以本文采用 代码覆盖率和功能覆盖率相结合的评估方案。 代码覆盖率的产生由仿真工具m o d c l s i m 直接产生结果，而m o d e l s i m 6 0 中没 有功能覆盖的功能，所以通过观察仿真波形的传统分析方法来检查基本功能是否 覆盖。为了更方便的发现功能错误，本文使用断言语句与仿真相结合的方法来实 现。这样使仿真结果透明化，具有更高的可观测性。 对仿真结果进行评估前，要首先搭建验证的模型，下面介绍常用的建模方法。 3 4 常用建模方法 不同的设计会搭建不同的验证模型，不同的验证模型也相应有不同的验证、 覆盖方案。数字逻辑系统的状态变化都是由输入逻辑变量和控制逻辑信号所引起 的，对时序逻辑系统逻辑关系的描述就是对系统状态的描述方法。下面介绍时序 电路的常用的状态描述模型。 3 4 1 状态方程 数字逻辑系统中描述状态与各输入逻辑变量之间、状态与状态之间逻辑关系 的逻辑表达式叫做状态方程。 设q 表示一个时序逻辑系统的状态变量，x 表示该时序逻辑系统的输入交量， c 表示该时序逻辑系统的控制变量，则有关q 的状态方程为q “+ 1 x c 矿。 例如+ 1 = x c q ”表示在控制信号有效时( c = 1 ) ，如果输入逻辑变量的逻辑值 为0 ，则系统的次态为0 ，而如果输入逻辑值为1 ，则系统的次态为q ”，保持原态。 状态方程的方法描述时序逻辑功能比较抽象，适合使用形式验证的方法利用 公式推导来验证。 1 9 3 4 2 状态图 以图形方式描述时序逻辑系统状态的方法叫做状态图法。如图1 1 所示。 1 d 图1 1 状态图( s t a t ec h a r t ) 有限状态图是最常用的一种时序电路的数学模型。最基本的有限状态图由一 个内含起始状态的状态集，一个输入字母表，和一个状态转换函数构成，状态转 换函数将输入符号和有限状态图的当前状态映射到下一个状态，有限状态图的计 算始于一个起始状态和一个输入信号，根据状态转换函数转换到新的状态。从有 限状态图又可衍生出各种类型，其中最基本的类型有两种：m e a l y ( 米莱) 型 输出是当前状态和所有输入信号的函数；m o o r e ( 摩尔) 型输出仅是当前状态 的函数。 基于状态图的验证方法可以采用基于算法的测试产生验证方法。这些算法主 要思想就是用最少的时间或产生最短的测试序列来覆盖每个状态和每条弧线。 3 4 3 状态表 以表格方式描述时序逻辑系统的状态与输入逻辑变量、状态与状态、状态与 输出之间的逻辑关系的表格叫做状态表。表3 是米莱型，表4 是摩尔型。 表3 米莱型状态表( m e a l y s t a t e t a b l e ) 表4 摩尔型状态表( m o o r e s t a t e t a b l e ) 入 o1 o 1 10 0 0 o 硒1 1 + 1 z ) 火 01 o0 1 o1 0 ，o 11 1 o 0 0 1 ( + 1 z ) 状态表或状态转换表，是描述一个有限状态机实现的操作的基本方式，这类 描述方式称为有限状态机的低层描述，低层描述的应用相当普遍。但是，对于一 个简单的有限状态机来说，它的低层描述也可能相当复杂，以一个简单的交通灯 控制器，l s c a s 8 9b e n c h m a r k 电路中的一个模块s 2 9 8 为例，它的状态转换图中 有2 1 8 个状态，以及1 0 9 6 个状态转换分支，庞大的状态数和复杂的转换序列，给 基于低层描述的处理带来了难以克服的困难。另一方面，随着超大规模集成电路 复杂性的不断升级，电路的高层描述在电路分析中受到越来越多的重视，电路设 计的过程可以看作从高层描述到低层描述的映射，然而这种映射不是一对一的。 基于有限状态机的状态转换表来书写其行为描述代码，以及给定一个行为描述程 序，要求对它实现的有限状态机的操作进行分析以得到状态转换表，工作量很大。 基于状态表的模型适合穷举的方法进行仿真。但在使用穷举法进行验证时， 必须保证所有的输入信号都具有逻辑独立性，就是要保证测试矢量的每一组信号 都是完备信号，测试矢量是一个完备信号集，只有这样，才能保证测试的正确性。 3 4 4 激励表 在设计时序逻辑系统时，系统状态和输出变量是设计要求，因此系统状态、 状态变化是已知的，这时需要确定已知状态、状态变化和对应输出的条件下，应 给时序逻辑系统施加什么样的输入变量。当把状态作为自变量，输入变量作为因 变量时，可以列出反映系统状态和输入变量之间的逻辑真值表，叫做激励表。 3 4 5 触发器 触发器是描述时序逻辑系统的一种基本图形模型，通过触发器这种记忆元件 也可以反映系统状态与输入信号和控制信号之间的关系。 3 5 总结 整个仿真验证的评估过程：首先使用一种建模方法对设计对象进行建模，再 基于搭建好的模型的基础上分析可能会出现的错误有哪些、会在何处何时发生， 然后根据自己的方法编写测试向量，最后用覆盖指标来检验测试向量的有效性和 整个验证完成的情况，决定是否需要继续验证工作。- 整个评估过程在时序电路的验证中仍然适用，但要根据时序电路的特点进行 各种方法有效的选择。下面章节介绍时序电路的特点及验证方法。 2 1 4 时序电路的功能验证 4 1 时序电路的验证 电路按照逻辑功能可以划分成组合逻辑电路和时序逻辑电路如图1 2 所示。时 序逻辑电路又可分为同步时序电路和异步时序电路。组合逻辑电路是具有一组输 入一组输出的非记忆性逻辑电路。电路功能的基本特点是任何时刻的输出信号仅 取决于该时刻输入信号的组合，而与电路在输入信号前的状态无关。组合电路由 门电路组成，但不包括存储信号的记忆单元，输入输出无反馈通路，信号单向传 输，且存在传输延迟时间。而时序电路的基本特点是任意时刻的输出信号不仅和 输入信号有关，而且和电路原来状态有关。同时电路结构中一定会包含存储记忆 的单元电路。 图1 2 组合电路和时序电路的基本结构 ( c o m b i n a t i o nc i r c u i ta n ds e q u e n t i a lc i r c u i tc o n f i g u r a t i o n ) 由于组合电路和时序电路功能的区别，所以两者功能的描述方法和验证方法 也存在很大区别。组合电路的功能描述方法有真值表、逻辑表达式、逻辑图、卡 诺图和波形图等。时序电路的功能描述方法有三个方程( 输出方程、驱动方程和 状态方程) 、状态转换表、状态转换图和时序图等。由于组合电路相对比较简单、 验证方法和工具都已经很成熟，而时序电路相对复杂，而且现有方法比较少，所 以本文主要对时序电路的验证方法和技术进行研究。 现有的时序电路的验证技术，大致可分为两大类：仿真技术和形式技术。基 于形式技术的验证方法的研究比较多，如文献1 1 0 l 1 1 j 【1 2 j 【1 3 】中采用不同的方法对时序 电路进行等价性验证，等价性检查的方法大致可分为遍历f s m 和利用组合电路技 术的方法，核心都是比较两个f s m 是否等价。文献【1 4 1 1 5 l 【1 6 i 是一种模型检查方法， 核心就是将要验证的规范和电路实现的行为用某种形式进行建模，并证明电路实 现满足规范的过程。只是建模方法和证明过程的不同。还有定理证明的文献旧。 而基于仿真技术的验证方法研究的比较少，大部分是针对门级电路的仿真，面向 前端功能验证方法的研究更加少 时序电路的功能仿真验证方法实质上就是通过产生一系列的测试向量去验证 电路的功能正确性。而时序电路的测试产生一直被业界认为是很困难的【l s l 。考虑 前面第2 3 1 节提到的几种常用的测试产生方法，利用伪随机方法测试时序电路非 常困难的，根本无法满足要求；利用自动决定测试方法，增加测试点，是一种解 决途径，但是不够系统性，依赖于验证工程师的经验；最后，基于某种功能描述 模型结合相应的算法产生测试向量，使所有寄存器元件都具有可控性和可观测性， 这也是最流行的一种时序电路的测试方法。 时序电路的功能描述模型有( 即建模方法) 如第3 4 节所介绍的五种方法，但 实际中最常用的时序电路的描述方式是基于有限状态机的，可分为状态转换表和 状态转换图两种方法。因为不同的功能描述方法会有不同的验证方法。本文着重 研究基于状态转换表和状态转换图两种描述方法的不同验证方法的区别。下面分 别介绍两种验证方法的基本原理和各自的验证流程。 4 2 基于状态转换表的验证方法 状态转换表是描述一个有限状态机实现操作的基本方式【1 9 1 ，这类描述方式称 为有限状态机的低层描述，而且这种低层描述的应用相当普遍。状态转换表实质 上就是将输入和当前状态作为输入的真值表f 刎。 现在基于状态转换表的验证方法有很多，但基本的核心就是对所有可能的错 误都进行穷举式的验证方式，其中也会采用一些方法和技术来达到节省验证时间 和减少测试矢量的目的。例如文献【2 l 】利用唯一的输入输出序列来编写尽可能长的 序列，减少操作的次数，从而达到缩短验证时间的目的，该方法适合单元级的小 规模电路的验证。文献【2 2 l 中采用一种严格的算法使产生的测试向量有一定的优先 顺序，也可以缩短覆盖最多的s s t ( s i n g l es t a t et r a n s i t i o n ) 错误的时间，该方法 比较适合大的时序电路。基于状态表的验证方法不仅可以检查单状态变换错误， 还可以检查多状态变换错误的存在，文献瞄j 中的方法可以检测出多个相关次态的 错误或是多个输出的错误。 由于1 2 l j 中全浏览电路( f u l ls c a nc i r c u i t s ) 的验证方法简单易行，而且比较有 代表性，所以本文利用该方法来研究基于状态转换表的功能验证方法的特点。 4 2 1 全浏览电路验证方法介绍 全浏览电路( f u l ls c a nc i r c u i t s ) 的验证方法是基于状态转换表，面向单一状 态转换错误类型、具有1 0 0 错误覆盖率的一种功能验证方法。该方法的核心是利 用唯一输入输出序列( u n i q u ei n p u t - o u t p u ts e q u e n c e ) 编写尽可能长的测试矢量， 使覆盖所有状态转换所使用的操作次数最少，从而达到缩短验证时间的目的。 在4 2 6 节会利用一个例子具体介绍这种方法的原理，介绍基本原理前先介绍 一下用到的基本概念。 状态s 的唯输入输出序列就是可以区分电路中其他的状态的序列。更准确 的说，当电路开始于状态s ，输入序列a 产生的输出结果用b ( a ，s ) 表示。如果输 入序列d s 对于每个状态；- s ，都有b ( d s ，s ) - b ( d s ，釜) ，那么序列d s 是 状态s 唯一的输入输出序列。输出结果可以是下一状态的区别，也可以是输出信 号的区别。本论文采用输出状态不同作为区分。 4 2 2 验证的流程 i 状态转换表 l l 找出唯一输入输出序列 - - 4 产生测试激励l i 仿真运行 l - - 1 覆盖率分析 i 图1 3 验证方法流程图( v e r i f i c a t i o nf l o wc h a r t ) 验证从设计规范出发，根据控制的输入信号和反馈的信号，建立状态转换表。 再根据状态转换表，产生仿真激励。要求覆盖全部的情况，然后分析覆盖率，产 生反馈或是验证结束。实现步骤如下： 利用状态转换表的描述方式根据设计规范对设计进行建模 根据状态转换表，找出唯一的输入输出序列 利用输入输出序列的算法编写测试矢量 确认达到要求的覆盖状态时，停止测试；否则产生反馈，继续测试。 2 4 4 2 3 状态转换表模型 状态表模型，在时序电路里称为状态转换表模型，是所有相关输入信号和输 出信号的可能组合。具体建模步骤如下： 1 、根据设计规范，确定能影响控制行为的信号，可以是化简后的； 2 、根据设计规范，确定所需要的状态； 3 、将状态为纵列，控制信号的所有组和为横列，搭建状态表； 4 、再添入每种控制下的状态走向和输出结果，完成状态表。 例如对于一个有5 个控制信号和3 个状态的器件，那么就有25 3 种状态转 换，即有9 6 个需要测试点。如果对于小规模电路，还是可以实现的，但是到了系 统级或是大的模块，就不可能完全覆盖或者实现很耗费时间。 4 2 4 仿真激励产生 产生测试激励之前，要找出每个状态的唯一输入输出序列。方法就是找出输 入某序列的条件下次态是唯一的序列。不是所有的状态都有唯一输入输出序列的。 考虑状态表描述的电路功能和对电路的全部测试，所以测试每个状态转换是 可能的。考虑一个状态变换s f 二! = l l s f ，即从状态s i 开始在输入组合为a j 时， 下一状态是s 和输出组合为。可以通过浏览初始状态s f 输入主要的输入组合 af 来测试这个状态变换，最后观察主要的输出组合，观察下一个状态。如果输出 组合不同于，或是下一状态不同于s 玎，就说明发现一个错误。 测试矢量编写的过程：从初始状态s i o 开始，输入a j o 时下一个状态应该是 s i o j o 。如果s i o j o 没有唯一的输入输出序列，那么测试产生必须停止，此次操作 结束。但是，如果s i o j o 有唯一的输入输出序列d 咖i o ，而且还存在还没有被测试 的状态。就利用序列d 咖i o ，使测试达到下一状态剐1 ，继续输入未测试的输入组 合a j l ，到达下一个状态s i l j l 。然后继续利用唯一的输入输出序列，使一次操作 完成尽可能多的状态。因此，测试序列有下面的格式 s i o ! - ! ! 一s f o f o ：! ! ! f ! i _ s f l ! ! z ! 一s f l ，1 ：! i ! ! 一s f 2 ! z 2 一s f 2 ，2 。 如果不编写尽可能长的测试序列，每次就会从下一状态重新开始测试，这样 还需要把上一次测试的结束状态和开始的状态连接起来，使测试缺乏连贯性，延 长测试时问。 4 2 5 覆盖分析 无论哪种验证方法都要分析方法的有效性，即对该方法进行相应的覆盖评估。 基于状态转换表的方法基本上是全覆盖的全面测试，但要注意这种全覆盖也是有 前提的，是面向某一种或几种错误类型的，例如【2 1 l 【2 2 】中是面向单一状态变换错误 的，而【矧中是面向多个状态变换错误和输出错误的。 覆盖分析的方法采用3 3 节介绍的代码覆盖率和功能覆盖相结合的方案。 4 2 6 实例介绍 表5 是假设已知的状态转换表。有四个状态0 、1 、2 、3 和两位输入和一位输 出。输入输出值以二进制形式给出。表中“”前表示下一状态，后面表示输出。 表5 状态转换表( t h es t a t et a b l e ) 输入 拱荔 0 00 11 01 l 0o ，1 1 1帅0 0 1 1 1 1 1 3 ，10 0 22 ，12 ，13 1 3 1 1 3 1 1扰3 13 1 唯一的输入输出序列在表6 中列出。对于状态0 ，输入序列( 0 0 ) 时，只有状 态o 的输出状态为0 ，与其他状态区分开来。同样方法找到状态o 的另一个唯一输 入输出序列( 1 0 ) ，状态2 的唯一输入输出序列( 0 0 ) 。对于状态1 和状态3 ，唯一 的输入输出序列不存在。 表6 唯一输入输出序列( u n i q u ei os e q u e n c e ) 状态唯一序列末状态 01 00 l 20 02 3 测试产生过程：首先测试的是状态转换0 堡 叶o ，然后利用唯一的状态转换 序列是0 0 连接到状态0 。可以测试另一个从状态0 开始的状态转换。增加状态转 换o g l + 1 。状态1 没有唯一的输入输出序列，那么在这点上就停止构建测试。测 试序列为0 盟一o 塑一o 盟一1 ，此时完成了o 鲤一0 和0 虹一1 的测试。其余 部分以同样原理进行测试。 4 3 基于状态转换图的验证方法 基于状态转换图的建模方法是时序电路有限状态机的最常用的描述方式，由 于其非常的直观，用状态图来描述规范也最容易理解，所以现有的这类验证方法 也非常多 2 4 1 巧1 1 2 6 1 。核心思想就是基于已有的状态图，产生测试激励，使尽可能多 的覆盖每个状态和状态转移条件，并且同时使测试时间缩短。 本文选择文献i 卅中的优化路径选择方法，因为本方法比较容易理解，还能实 现自动化。所以用这种方法作为基于状态转换图验证方法的代表。 4 3 1 有限状态机优化验证方法介绍 有限状态机优化验证方法是基于状态转换图模型，利用图论和数学规划方法 分析并解决有限状态机验证路径的选择优化的问题。实际证明该方法可以使用更 短的时间有效的解决有限状态机验证的问题。不仅可以全面覆盖状态转移条件， 而且验证效率较高。 下面介绍该方法的一些基本概念。 1 、有向图d 中，以顶点t j 为起点的弧的数目叫做 的出度，记作d e 霉k 扣) ；以 顶点 为终点的弧的数目叫做”的入度，记作d e g 加( v ) 。 2 、在有向图d 中，存在一条路径可以从d 中的某一点出发，经过d 中每条 弧一次且仅一次，这样的路径称为e u l e r 路径；如果存在这样的封闭回路，它遍历 d 每一条弧一次且仅一次，这样的回路称为有向e u l e r 回路。 3 、一个有向图d 存在e u l e r 回路的充分必要条件是d 是连通的，并且是平衡 的，即d e g d t ( v 1 ) - d e g l h ( v i ) 。 4 、线性规划数学模型的一般形式为 r a i n s2 c ，x ， 石，zo ( ，：k ，以) 其中4 玎，b i ，。j ( i 一1 ，肌；j - 1 ，雕) 为已知常数。 5 、d i j k s l x a 算法：弓 入辅助向量己，其分l i 1 表示当前找到的从源点 到 每个终点l ，的最短路径的长度。用加权邻接矩阵d i s t i y 】表示有向图，d i s t i j 】表 示弧1 ，。，y ，) 上的权值，若如，1 ，i ) 不存在，则d i s t i j 】表示为某一最大值m 。向量 s 是已找到的从t j 出发最短路径的终点集合，其初始值为空集。 6 、邻接矩阵根据图的定义可知，图的逻辑结构分为两部分：v 和e 的集合， 其中v 是顶点集，e 是边集。因此，用一个一维数组存放图中所有顶点数据：用 一个二维数组存放顶点间关系( 边或弧) 的数据，称这个二维数组为邻接矩阵。 7 、距离矩阵用图论的术语来说，假设有一个图g - ，e ) ，其中v 是顶点集， e 是边集，设d 一犯口) 是由顶点i 和顶点，之闻的距离所组成的距离矩阵。 8 、有限状态机验证是功能验证的一个组成部分，但并不等同于功能验证。这 是因为状态机验证偏重于对状态转移情况的遍历，而功能验证往往代表着对一系 列状态转移不同组合情况的确认，图1 4 所示为功能验证包含的内容以及这些内容 彼此之间的区别和联系。 图1 4 功能验证和有限状态机验证的关系 ( t h er e l a t i o no ff u n c t i o n a lv e r i f i c a t i o na n df i n i t es t a t em a c h i n ev e r i f i c a t i o n ) 功能验证不仅包含了有限状态机验证问题，还包括对不同状态转移组合情况 的验证以及对角落事件的验证。所以，尽管有限状态机的所有状态和转移条件都 已经覆盖了，但并不代表功能全部实现了。为了验证功能，采用断言的方式来检 验功能覆盖。 4 3 2 验证流程 验证从规范文件出发，首先依据规范文件搭建验证模型，该模型用状态转换 图的方式来描述，依据建立的状态转换图模型和优化验证方法产生仿真激励，最 后分析覆盖率结果，提供一个反馈给t e s t b e n c h ，当覆盖达到要求的指标时，验证 可以结束。整个验证方法的流程如图1 5 所示。 既然激励产生和功能断言的编写都是基于状态转换图模型的，那么首先介绍 如何搭建仿真模型。 4 3 3 建模理论 图1 5 验证方法流程图( v e r i f i c a t i o nf l o wc h a a ) 采用状态转换图建模，可以避免现有功能验证中，提取功能验证点不完整的 问题；其次，采用状态转换图的方式，很直观更容易理解。 状态转换图模型的搭建过程如图1 6 【卅，首先要确定影响总线控制行为的信号， 然后确定满足总线规范的状态，再找出所有引起状态转换的事件，最后确定每个 状态的位置。 确定能影响控制行为的信号 l 根据规范确定所需的状态 j 找出影响状态变换的所有事件 l 确定每个状态的位置 l ( 状态转换图完成) 图1 6 状态图的搭建( b u i l d i n gs t a t ec h a r t ) 4 3 4 激励产生 激励产生过程是利用在状态转换图的基础上构造e u l e r 回路的方法( 硬件有限 状态机e u l e r 回路存在性可证明) 。具体构造方法：从入度节点出发，找一条到出 度节点最短的有向路径，添加这条有向路径上的所有重弧得到的图，重复此步骤， 直至所有非平衡点变成平衡点，此时可得到有向e u l e r 回路。实质就是重复路径的 选择问题。测试按照遍历e u l e r 回路的顺序产生即可得到。 在添加重弧之前要知道每条路径的权重值，即进入某一状态后停留的时问。 权重值可以是真实的值，也可以是估算的结果，主要是为路径选择提供参考。确 定使状态转换图变成欧拉回路所添加的一组弧线的权重和最小，才达到优化的目 的。实现验证的过程如下： 1 、由有限状态图产生邻接矩阵和距离矩阵，其中邻接矩阵说明了有限状态图 对应的有向图的状态转移及出度入度关系，距离矩阵是在计算最短路径时结合邻 接矩阵使用的。 2 、由邻接矩阵计算得到非平衡结点，然后结合距离矩阵通过算法计算出非平 衡结点之间的最短距离关系矩阵。 3 、使用数学规划的匈牙利算法从最短距离关系矩阵中计算得到优化路径。 该方法可以通过编程实现，设计实现流程如图1 7 。其中g r a p h 运算模块用来 实现第2 步中对于非平衡结点的计算，产生非平衡结点之问的对应矩阵，经过 d i j k s t r a 算法模块之后将产生关系矩阵，并由数学规划算法模块计算得到验证路 径。但本论文中并没有实现自动化。 邻接矩阵 距离矩阵 锢一囡 回一圜 图1 7 程序实现流程示意( p r o g r a mi m p l e m e n t a t i o nf l o wc h a r t ) 4 3 5 覆盖分析 覆盖分析同样利用3 3 节中提到的方法，采用代码覆盖率和功能覆盖率来综合 评估基于状态转换图的方法。具体数据见5 2 3 节。 拙廛銮道太堂亟堂焦论窑吐度虫蹬数功能验证 4 3 6 验证实例 例如图1 8 状态转换图，首先找到它的出度节点和入度节点，1 、3 、4 为出度 节点，出度值为1 ，而2 、6 、7 为入度节点，入度值为1 。那么从出度节点到入度 节点就有图1 9 中的六种排列组合方式，要确定哪种方式最优，即时间最短。在选 择之前还要知道每条路径的权重，即在一个节点停留的时间，这个数据可以是估 计的值，不需要准确的值。然后得到邻接矩阵图2 0 ，再通过d i j k s t r a 算法可计算 出第4 种方式时间最优。将2 - - - - 4 、6 1 和7 3 添加到图1 8 中，即可得到欧拉 回路。再遍历构建好的欧拉回路，得到测试路径的顺序。 图1 8 状态转换图( s t a t ec