（微电子学与固体电子学专业论文）集成电路设计中基于断言的验证方法研究.pdf

摘要 ! 皇! 曼! 曼曼a , i | i h ! ! 曼 摘要 半导体技术的发展使芯片集成度不断提高，芯片功能也越来越复杂。然而验 证能力的增长速度远远落后于制造能力和设计能力的增长速度，功能验证已经成 为现在集成电路设计中的主要挑战之一，是限制芯片设计效率进一步提高的瓶 颈。 a b v ( a s s e r t i o n b a s e dv e r i f i c a t i o n ) 是近年来出现的一项集成电路功能 验证的新技术，可以应用于基于仿真的验证和形式验证之中。本文的主要研究内 容是a b v 在基于仿真的验证中的应用。本文通过比较不同的断言实现形式，选择 在验证中使用s v a ( s y s t e m v e r i l o ga s s e r t i o n ) 对设计进行断言检验，并进行覆盖 率统计。文章详细介绍了s v a 的结构、基本语法以及与设计的绑定方法。 本文将基于断言的验证方法应用到了两个开源代码模块的功能验证之中，它 们分别是u a r t 模块以及8 位精简指令集处理器r i s cs p m 。根据设计的特点 采取了不同的验证策略：对u a r t 的验证采用直接方式生成激励，在设计源代 码中插入s v a 语句对有限状态机和端口信号进行检查和断言覆盖率统计；而对 r i s cs p m 应用约束随机验证，并结合了覆盖率驱动的验证技术。同时应用覆盖 率组定义功能覆盖率模型，利用s v a 对设计的关键功能进行检查并强化覆盖率 模型。 验证结果表明，基于断言的验证方法增加了验证过程的可观测性，便于在仿 真中对设计缺陷进行定位。将a b v 与约束随机验证技术以及覆盖率驱动验证技 术相结合，可以提高验证过程的可控性，加速覆盖率目标的实现。 关键词：基于断言的验证方法；s y s t e m v e r i l o g 断言；约束随机验证；功能覆盖 a b s t r a c t a b s t r a c t w i t ht h ed e v e l o p m e n to fs e m i c o n d u c t o rt e c h n o l o g y ，b o t ho ft h ei n t e g r a t i o nd e g r e e a n df u n c t i o n a lc o m p l e x i t yo fi n t e g r a t e dc i r c u i t ( i c ) h a v ear e v o l u t i o n a r yi n c r e a s e h o w e v e r ，t h ei n c r e a s eo ff u n c t i o n a lv e r i f i c a t i o na b i l i t yd o e sn o tc a t c hu pt h a to ft h e f a b r i c a t i o na b i l i t ya n dd e s i g na b i l i t y ，w h i c hm a k e sf u n c t i o n a lv e r i f i c a t i o no n eo ft h e m a i nc h a l l e n g e si ni cd e s i g nc y c l e f u n c t i o n a lv e r i f i c a t i o ni s b e c o m i n gt h e b o t t l e n e c kw h i c hr e s t r a i n si cd e s i g nf r o mf - r r t h e rd e v e l o p m e n t t h em a i nc o n t e n to ft h i sp a p e ri st h ea b v ( a s s e r t i o n - b a s e dv e r i f i c a t i o n ) ，w h i c hi sa n e wv e r i f i c a t i o nt e c h n o l o g ya p p l i c a b l ei nb o t hs i m u l a t i o n - b a s e dv e r i f i c a t i o na n d f o r m a lv e r i f i c a t i o n b a s e do nt h ef a c tt h a ts i m u l a t i o n b a s e dv e r i f i c a t i o ni ss t i l l 血e m a i nm e t h o d o l o g yu s e di ni cd e s i g np r o c e s s ，t h i sp a p e rs t u d i e sa b va p p l i c a t i o ni n s i m u l a t i o n - b a s e dv e r i f i c a t i o n b yc o m p a r i n gt h ep e r f o r m a n c eo fd i f f e r e n ta s s e r t i o n f o r m a t s ，s y s t e m v e r i l o ga s s e r t i o n ( s v a ) i sa d o p t e dt o d e s c r i b ea s s e r t i o n s t h e s t r u c t u r ea n ds y n t a xo fs v a ，a n dm e t h o d st ob i n ds v at od e s i g n sa r ei n t r o d u c e d a sa p p l i c a t i o ne x a m p l e s ，c a s es t u d i e so ff u n c t i o n a lv e r i f i c a t i o nf o rt w oo p e ns o u r c e d e s i g n s ，u s i n gs v a a r ep r o v i d e d o n ed e s i g ni su a r tm o d e l ，t h eo t h e ri s8 一b i tr i s c c p um o d e l a c c o r d i n gt ot h e i rf u n c t i o n a lc h a r a c t e r i s t i c s ，d i f f e r e n tv e r i f i c a t i o n s t r a t e g i e sa r ea d o p t e d i nt h eu a r tc a s e ，d i r e c tt e s tm e t h o di su s e d t h em a i nw o r ki s t oi n s e r ta s s e r t i o n si n t of i n i t es t a t em a c h i n e ( f s m ) a n dp o r ts i g n a l st os e r v ea s m o n i t o r sa n dc o l l e c tc o v e r a g ei n f o r m a t i o n i nt h el a t t e re a s e ，c o n s t r a i n e d r a n d o m v e r i f i c a t i o n ( c r v ) c o m b i n e d 晰t l lc o v e r a g e - d r i v e nv e r i f i c a t i o n ( c d v ) i sa d o p t e d a f u n c t i o n a lc o v e r a g em o d e lu s i n gs y s t e m v e r i l o gc o v e r g r o u pi sb u i l tt oc o l l e c t c o v e r a g ei n f o r m a t i o na u t o m a t i c a l l yi ns i m u l a t i o n s v ai sa l s ou s e dt os t r e n g t h e nt h e c o v e r a g em o d e la n dm o n i t o rt h ek e y f u n c t i o n p o i n t s t h es t u d i e dr e s u l ts h o w st h a ta b vi sf e a s i b l ea n dc a nb ea p p l i e di nt h ed e s i g na n d v e r i f i c a t i o np r o c e s st oi m p r o v et h eo b s e r v a b i l i t yo fv e r i f i c a t i o np r o c e s sa n dm a k e si t e a s i e rt ol o c a t ed e s i g nb u g s a b vc o m b i n e dw i t hc r va n dc d vc a ni m p r o v et h e c o n t r o l l a b i l i t y o fv e r i f i c a t i o na n da c c e l e r a t e st h e p r o c e s st o m e e t c o v e r a g e r e q u i r e m e n t k e y w o r d s ：a b v ；s v a ；c o n s t r a i n e d r a n d o mv 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 独创性声明 本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研 究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他 人已经发表或撰写过的研究成果，也不包含为获得北京工业大学或其它教育机构 的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均 已在论文中作了明确的说明并表示了谢意。 躲麟吼型：互尘 关于论文使用授权的说明 本人完全了解北京工业大学有关保留、使用学位论文的规定，即：学校有权 保留送交论文的复印件，允许论文被查阅和借阅；学校可以公布论文的全部或部 分内容，可以采用影印、缩印或其他复制手段保存论文。 ( 保密的论文在解密后应遵守此规定) 签名：虚莲蓬导师签名：名，丛丝日期! ：坐， 第1 章绪论 曼曼! ! ! 曼! ! 曼曼! ! 曼! 曼! o _ i i i i!m i ! 曼! 曼! 曼曼皇曼鼍曼 第1 章绪论 1 1 课题背景及课题意义 近年来半导体制造工艺正按照摩尔定律所预示的那样不断发展，晶体管尺寸 越来越小。工艺的快速发展使得一些高整合度的概念，例如s o c ( s y s t e m o n c h i p ) 得以变为现实。在电子市场对于嵌入式系统的成本、功能以及功耗提出更高要求 的驱动下，s o c 设计技术已经成为一种发展趋势。 随着集成电路设计工具的不断改进、更新，以及先进设计方法学的提出和应 用，集成电路的设计能力也不断提高，数字集成电路设计规模正在按照指数规律 增长。片上系统所包含的晶体管数量变得惊人的多，这就导致其中包含的门也越 来越多。目前，一块s o c 上就已经可以包含上千万个门，这就增大了电路出错的 几率，也使验证工作变得更加复杂。如果用设计中的状态数来衡量功能复杂度的 话，则设计的功能复杂度随着设计规模又呈指数增长。功能复杂度的增长主要是 指单芯片上包含的组件种类增多，不同种类组件的数量也变多。随着这些组件的 种类和数量增加，对芯片的整体功能和性能而言，各组件之间的接口就变得越发 重要。此外，片上软件和模拟器件也越来越频繁地出现在芯片中，这又进一步提 升了系统的复杂度，同时对传统的验证方法提出了挑战。 另外，如上文所言，随着消费者对i c 产品功能要求的不断提高，片上系统 技术已经成为发展趋势。而系统的规模的增加以及其包含功能的多样，使设计更 多的倾向于利用已经设计好的i p ( i n t e l l e c t u a lp r o p e r t y ) 模块。i p 重用技术 也使得设计的负担逐渐转移到验证工作。 图1 - 1 所示很直观的反映了集成电路设计、验证及制造三个阶段的现状。 可以看出，集成电路制造能力、设计能力及验证能力分别递减，设计鸿沟( d e s i g n g a p ) 、以及验证鸿沟( v e r i f i c a t i o ng a p ) 正逐年增加。换句话说，设计能力的 进步赶不上制造工艺的快速发展，同时验证技术水平又远远落后于设计能力的增 长。另外从图中可以看出，尽管集成电路验证能力从1 9 9 6 年起显著增长，然而 与设计和制造能力相比，增长趋势明显比较缓慢。总体而言验证技术已经落后于 设计和制造能力，模拟和验证工作成为整个集成电路产业发展的瓶颈，对进一步 提高设计生产率造成了障碍。 国际半导体技术发展报告指出，验证已经成为目前集成电路设计流程中开销 最大的工作。在人力资源方面，在目前的工程项目中，验证工程师的数量已经超 过设计工程师数量，尤其对于功能复杂的实际，这一比例已经达到了2 ：1 甚至 3 ：1 ；在时间开销方面，普遍接受的看法是，验证过程占整个项目开发周期的 7 0 左右。 北京i 大学i 学硬学位论文 v e r i f i c a t i o nd e s i g n g a pg a p 1 b 3 口j1 9 b 】0 0 0】咖 图l - i 验证能力与设计、制造能力的差距 f i g u r e l - it h e g a p s b e d c e n v c r i f c a t i o na b i l 咄d e s i g na b i l i t ya n d f a b r i c a t i o na b i l i t 5 , 对于中等复杂度的芯片而言即便在验证上投入了大量资源，但在芯片投产 之前仍然需要经过多次流片。更有甚者，当一块有缺陷的芯片流入市场，不得不 返工时，不仅会增加其设计费用，还会拖延上市时间，而这对更新换代极快的电 子产品来说几乎是致命的。上市时间推迟会冲击产品受益，缩小市场份额，使公 司陷入穷于应付的困境“1 。例如，1 9 9 4 年奔腾处理器浮点处理部分出现瑕疵而被 迫召回，i n t e l 为此付出了47 5 亿美元的高昂代价。近年来，i c 相关产品因为 设计缺陷被召回的新闻也曾出不穷。 由于上述的原因，如何对芯片设计进行完整、有效的验证，尤其是功能验证 已经成为硬件设计中极其重要的部分。基于i c 开发流程中验证工作的重要性， 本课题结合一些设计实例对目前验证的新方法进行研究，并尝试应用相关理论对 结果进行分析。这些研究对于i c 开发流程系统化、规范化有着重要的意义。 12 功能验证中的热点问题及国内外研究进展 121 功能验证基本原理 设计的过程是把设计规范转换为实现方案的过程，而验证则与设计过程相 反，它是通过各种方法核对设计规范和输出结果一致性的过程。图卜2 表明了 一种设计变换的验证是通过另一条有公共起点的恢复路径完成的，验证是检查设 计变换的结果和设计变换的起点是否一致的过程。这里所提到的设计变换可以包 i，ji；ej：a；，8 第1 章绪论 括设计规范的r t l ( r e g i s t e rt r a n s f e rl e v e l ) 编码、插入扫描链、把r t l 代码综合 成门级网表，以及门级网表的版图设计等任何具有输入和输出的过程嗍。 起点 设计变换 终点 验证 图i - 2 验证中的恢复路径模型【2 】 f i g u r e 1 2r e c o n v e r g e n c em o d e li nv e r i f i c a t i o np r o c e s s l 2 1 设计中的错误主要有两种，第一种是在设计实现或者说设计变换中引入的， 这种错误是实现错误而非规范错误。由于设计过程中不可避免的加入了人为因 素，而任何人为因素都会产生不确定性和不可重复性。例如在r t l 编码的过程中， 必须由人对设计规范进行解释，按照自己的理解完成编码。而验证工程师则需要 验证这些代码是否功能正确。这一过程的恢复路径如图i - 3 所示。 r t l 编码 设计规范 验证 图1 3 不确定状态的恢复路径模型【2 】 f i g u r e1 3r e c o n v e r g e n c em o d e li nu n s t a b l es t a t u s 2 1 在上述情况下，验证过程只检查了最终设计是否满足设计工程师对设计规范 的理解，而无法检查出这种对设计规范的解读是否存在错误。为了防止此类错误 的发生，一种方法是利用软件直接从设计规范中综合出一个实现方案。这种方法 可以消除大多数人为错误，但是软件自身的缺陷或是对其使用方法的不当仍然可 能导致错误的产生。也可以采取防差错技术( p o k a - y o k e ) 降低此类错误发生的 机率。这种技术是指把设计流程中人的介入过程规范化为一系列特定的序列和步 骤，它离全自动的过程仅一步之遥1 2 。另外一种方法是冗余。在可靠性要求很高 的情况下，例如a s i c 设计中经常使用冗余性的方法。用不同方法多次实现同样 的规范，并加以比较。从理论上说，规范实现的次数越多，验证可产生的可信度 就越高。另外每个人( 或小组) 完成的设计变换都由另一个人( 或小组) 独立的 进行验证，见图1 - 4 ，在集成电路开发流程中，为了防止对设计规范的错误理解 而产生的设计缺陷，验证人员应该独立于与设计人员，以保证验证过程的准确性。 这也是目前i c 开发流程的一个重要特点。 北京工业大学工学硕士学位论文 设计规范 验证 图卜4 冗余在不确定状态下的应用嘲 f i g u r e1 4a p p l y i n gr e d u n d a n c yi nu n s t a b l es t a t u s 2 】 设计中的第二种错误存在于设计规范之中。它可以是在规范中未能说明的功 能描述，或是不现实的功能，相互矛盾的需求等等。这种错误可以也可以通过冗 余性来检测。此外，在设计实现的后期，相互冲突的需求也会逐步显现出来。 功能验证的目的是确定一个设计是否实现了预期的功能，即验证了设计意 图，它检验了设计与其规范的一致性。由于设计规范通常由设计人员用自然语言 编写，而不是用精确的形式描述语言来编写，因而不可能证明一个设计与设计规 范相符。功能验证只能证明设计缺陷存在，而无法证明设计缺陷不存在【2 j 。图1 5 所示为功能验证路径模型。 r t l 编码 设计规范 功能验证 r t l 代码 图卜5 功能验证路径模型2 1 f i g u r e1 - 5f u n c t i o n a lv e r i f i c a t i o nr e c o n v e r g e n c em o d e l h 1 2 2 功能验证方法学 完整的验证方法应从验证计划做起。验证计划中应当包括需要详细验证的指 定功能，即设计特征、操作、边界点( c o m e rc a s e s ) 、事务等等。除了验证计划 外，还需要在验证过程中决定验证方法学所使用的语言或语言集【l 】。此外，如上 所述，根据验证的原理，验证是在有限的时间内找出尽可能多的设计缺陷，而不 能证明设计百分百正确。由此引出两个问题：怎样判断验证过程是否完成? 怎样 评价验证质量? 这就需要一种度量验证质量的尺度，即覆盖率。通常用不同的覆 盖率综合考量验证结果，例如代码覆盖率、功能覆盖率等等。 为了更好的研究验证方法学，可以根据不同标准将功能验证进行分类。例如 第1 章绪论 根据实现方法的不同，功能验证可以分为黑盒验证、白盒验证以及灰盒验证。 使用黑盒方法进行验证不需要考虑设计是如何实现的，所有的验证都可以通 过接口完成，无需直接访问设计的内部状态，也无需了解设计的内部结构和实现 方法。这种方法的优点是它不依赖于设计的任何特定的实现方式，它是真正的一 致性验证。黑盒法的缺点是在大规模设计中并不适用。因为大规模设计中有太多 的内部信号和状态，而这些深嵌在设计内部的关键功能很难控制和观测。换句话 说，黑盒法很难给设计设置一种状态或隔离特定的功能。 白盒法要求对设计的内部结构具有完全的观测和控制能力。这种方法可以迅 速设置需要的状态和输入，或特定的功能。其缺点一是需要了解设计实现的细节； 二是白盒方法与特定的设计实现紧密相连，一旦设计被改动，测试平台也需要随 之改动，可移植性差。白盒方法可以作为黑盒方法的补充，用于系统级验证当中。 例如s o c 通常由若干独立设计和验证的模块组成。系统级验证时可以把系统看 作是由很多黑盒组成的一个集合，而整个系统是一个白盒，具有完全的可控性和 可观测性。 灰盒法是根据设计实现的相关性在黑盒法与白盒法之间进行折中。它通过设 计的顶层接口对设计进行控制和观测，同时针对设计实现的特殊功能进行专门的 验证。灰盒法通常会通过对设计进行一些非功能性的修改以提高设计的可控性和 可观测性。本课题所研究的通过在设计r t l 代码中插入断言检验器的方法即可 归类为灰盒法。 此外，也可以将功能验证分为基于仿真的验证、基于形式方法的验证以及半 形式化验证。 ( 1 ) 基于仿真的验证( 动态验证) 动态功能验证主要是指功能仿真。仿真是将r t l 设计代码内嵌于软件编写 的模拟其工作环境的测试平( t e s t b e n c h ) 中，通过对待验证设计d u v f o e s i g n u n d e rv e r i f i c a t i o n ) 施加验证矢量，然后检查其行为是否按照设计规范运作【3 】。仿 真是目前功能验证的主要手段。这种方法的优点是简单、适用范围比较广且不受 设计规模的影响，基于仿真的验证是目前主流的验证方法。但是它局限于软件的 速度，一般适用在设计的前中期，尤其是模块级的验证上。当仿真出现错误时， 定位b u g 需要增加验证时间。 ( 2 ) 基于形式方法的验证( 静态验证) 形式验证方法属于静态验证，与基于仿真的方法相比，其优势在于不需要写 任何测试向量，易于定位设计缺陷【4 】。但是，需要占用大量内存空间，因此由于 形式化验证方法在容量、应用范围和对硬件环境要求的局限性，目前只适用于一 些中等规模的电路。有两种基本的形式化验证：等价性检验( e q u i v a l e n c ec h e c k i n g ) 及性质检验( p r o p e r t yc h e c k i n g ) 。 北京工业大学工学硕士学位论文 等价性检验是确定两个实现方案在功能上是否等价。它被广泛的应用在以下 情形：一是比较插入扫描链前后的电路，来确定增加扫描链不会改变电路的核心 功能；二是在设计的后期，检查r t l 代码在综合前和综合后的一致性；另外等 价性检验也用于比较从设计版图提取的晶体管网表与其r t l 版本的晶体管网表 的一致性。等价性检验通常应用两种基本的方法：一个是可满足性方法，即通过 对输入空间进行系统搜索，以找出一个输入向量或者是能够区分两个电路的向 量；另一种方法是把两个电路转换为正规的表达形式并加以比较【5 j 。 性质检查也称为模型检查( m o d e lc h e c k i n g ) ，它根据设计规范建立具有一 般性特征的模型，通过形式上的检查来证明模型特征的正确与否。它通常应用在 设计的高级阶段，用来检查具有普遍性的问题，同时验证设计人员的设计行为是 否违规【6 】。性质检查的核心思想是在整个状态空间中搜索不符合性质的点。如果 发现这样的点，说明性质不满足，此点会成为一个反例。然后生成从反例中导出 的波形，用户借此排除设计缺陷：反之，性质满足。 ( 3 ) 半形式化方法 这是一种混合验证方式，它是一种把基于仿真的验证和基于形式方法的验证 相结合的方法，采用输入向量并在形式上围绕向量的相邻部分进行验证。 1 2 3 功能验证中的热点问题 由于形式方法本身的缺陷，目前基于仿真的方法依然是验证中广泛应用的主 流方法，形式方法只作为辅助方式。根据功能验证原理，。我们可以把基于仿真验 证的一般过程归纳为以下流程，见图1 - 6 所示。 l 设计描述 预期响应 图1 - 6 基于仿真的功能验证流程 f i g u r e1 - 6s i m u l a t i o n b a s e df u n c t i o n a lv e r i f i c a t i o nf l o w 第1 苹绪论 这里的设计描述一般是指用硬件设计语言描述的待验证设d u v ( d e s i g n u n d e rv e r i f i c a t i o n ) ，通过测试平台( t e s t b e n c h ) 给设计施加激励，并观察设计 的输出响应。将输出响应与预期响应比较，如果两者不同说明设计存在错误。采 用这种传统的验证流程，存在以下几个问题： ( 1 ) 验证过程的可控制性及可观测性( 可视性) 传统的基于仿真的功能验证，需要通过t e s t b e n c h 给d u v 施加激励，并观 察响应。我们假设设计中存在设计缺陷( b u g ) ，如图1 7 所示。要诊断设计错误， 就要求t e s t b e n c h 通过输入激励能够驱动设计内部的问题，这是可控性的要求。 另外，由设计问题所产生的与期望不符的响应，一定要能够传输到设计的输出， 并且这个与期望不符的错误响应与预期响应的差别一定要能够被检测到，这是对 可观测性提出的要求。但是在目前的大多数t e s t b e n c h 之中，接受验证的设计输 出数目很少，因此很多设计问题不可能被观测到。即便设计内部的错误对激励发 生了错误响应，要把这个错误传送到输出端1 ：3 往往需要很长时间的延时，这就使 错误信息不能够及时被观测到；另外，即使内部的错误响应及时传送到输出端， 但由于目前设计的规模，需要用大量的激励向量，同样仿真的输出信息量也非常 庞大，一些错误的响应信息会淹没在验证输出信息之中，因此很难在验证中做到 不遗漏任何一个错误响应。 ( 2 ) 错误定位问题 当发现错误响应信息后，需要对错误进行定位，找到引起特定错误响应的设 计问题在设计源文件中的具体位置，并改正，这是错误定位和纠错的过程。由于 目前i c 的庞大规模和功能复杂度，错误定位以及纠错的时间甚至要远远超过发 现设计问题的时间【8 】。首要原因是发现与预期不符的响应之后，造成某个错误响 应会有许多可能的原因，或者这个错误响应是多个不同的设计问题引起的综合的 结果。另外一个重要因素是，设计本身的规模使设计内部问题发生的错误响应传 送到输出端口往往需要很长时间的延时，这个延时时间也造成了错误定位困难。 ( 3 ) 激励生成方式 根据验证计划，由测试台给设计加入激励，即一系列输入向量。传统的基于 仿真的功能验证中，往往是根据设计的特定功能和特征要求生成输入向量，这种 方式称为直接测试( d i r e c tt e s t ) 。直接方式生成的输入向量偏重于验证设计者特 别关注的区域，而实际的设计错误往往会在不被注意的其它区域( c o m e rc a s e s ) 。 因此，为了能够对这些边角区域进行验证，就要在直接验证的基础上，利用随机 方式围绕那些直接方式所覆盖的输入空间上的点进行扩展 9 1 。 ( 4 ) 验证覆盖问题 由于前面所提到的设计的规模和功能的复杂性，使得用穷举的方法对设计所 有可能的输入和状态进行验证变得不可能。因此需要解决一个根本问题：怎样知 北京工业大学工学硕士学位论文 道验证是否已经足够了。验证覆盖是对验证程度的一种度量，可以表示为已经验 证的条目占所有可能条目的百分比【l j 。这里所说的“条目”可以是设计实现的一行 代码，或是设计规范中的一项功能等等。而怎样定一个功能，甚至是设计中的所 有功能，也是一项很大的挑战。另外，目前有很多覆盖的度量方法，每一种都有 缺陷，需要各种度量覆盖的方法综合考量。 1 2 4 功能验证技术进展 为了赶上设计能力的发展，解决传统的功能验证的不足，近年来集成电路功 能验证能力不断的增长，主要原因是一些新技术的出现，如图1 7 所示。 图1 7 功能验证技术的发展 f i g u r e1 - 7e v o l u t i o no ff u n c t i o n a lv e r i f i c a t i o nt e c h n i q u e s 激励的生成方式，由最初的直接验证发展到随机验证，以及近年来出现的约 束随机验证等等，这些方法都有效的提高了验证激励的生成效率【1 0 1 。另外，形式 方法的出现有效地补充了动态验证的不足。功能覆盖技术、覆盖率导向的验证方 法考虑到了验证覆盖的问题；特性描述语言( p s l ) 等硬件验证语言( h v l ) 的 出现更有效的提高了验证的效率【l 。 如图1 7 所示，断言的概念在1 9 9 5 年左右被引入到硬件设计验证当中。在 设计和验证过程中合理有效的加入断言并与目前的验证方法相结合，就构成了基 于断言的验证方法【l2 j ( a s s e r t i o n b a s e dv e r i f i c a t i o n ) 。断言的应用极大的提高验 证过程的可视性，并且加速了设计问题的定位，因此目前断言已经被广泛的应用 到实际项目当中果【i 引。c i s c os y s t e m s ，i b m ，i n t e ll s il o g i c ，m o t o r o l a 等已经 把断言作为验证过程中必不可少的一部分。而且a b v 的在实际项目中的应用也 有着非常好的效果：在d e ca l p h a2 1 1 6 4 项目中，3 4 的b u g 通过断言找出，c y r i x m 3 ( p 1 ) 项目中1 7 的b u g 直接通过断言找出【1 4 1 ，而在唧的某项目中，这一数 字达到了8 5 上述的几种验证新技术具有各自的优点和局限性，在实际项目中往往是几种 第1 章绪论 技术相互结合使用，互为补充 1 5 】。本课题的研究内容即为断言在基于仿真的功能 验证中的应用。 1 3 论文结构 本文的内容分为五章，论文结构如下： 第一章是绪论部分，简单介绍课题的学术背景、理论与实际意义，相关领域 的研究进展和存在的不足，以及课题的主要研究内容。 第二章为理论基础部分，介绍了断言的概念、发展以及s y s t e m v e r i l o g a s s e r t i o n 的应用方法等。 第三章及第四章分别是基于断言的验证方法的两个应用实例以及结果分析。 最后是结论部分，在总结本论文完成情况的基础上，指出对本课题进一步研 究工作的展望与设想。 第2 章s v a 的应用方法 2 1 断言概念的发展 断言在软件开发过程中已经得到了广泛的应用。在1 9 9 5 年左右，断言的概 念就被引入到硬件开发过程中。断言的原型是最初写在设计中的叫做“看门狗” 的逻辑( w a t c h d o g l p 画c ) ，作用是监视电路中的一些关键功能，一旦出错就会采 取相应措施，这种看门狗”逻辑占用硬件资源。 硬件设计验证中断言的概念是对设计对象的属性特性或行为特性的描述，这 些特性保证了硬件能够正常工作。断言在验证过程中的作用，类似于“看门狗” 逻辑，但是断言一般只用于仿真阶段，不会被综合，因此不占用硬件资源。如果 一个在验证过程中被检查的属性与期望不符，则断言失败：如果一个在设计中被 禁止出现的属性，在验证过程中出现了，则这个断言失败。 验证过程中可以用仿真器、模拟器或是形式分析工具来分析断言。断言作为 监视器( m o n i t o r ) 来确保设计的特定性质“p r o p e r t y 会出现、总是保持或是绝不 出现。断言检验在基于仿真的功能验证中的工作原理如图2 1 所示。在设计和 验证阶段，我们在设计中所关心的功能及结构点附近加入断言，在功能仿真时， 这些断言或失败或成功，失败的断言可以通过日志或波形即时显示出来，所以没 有必要把内部错误的影响传到输出端口，这就增加了设计的可视性。由于一般把 断言插入到所关注的功能点，所以可以很快的在失败的断言附近找到错误点，纠 错时间也可以大大缩短。换句话说，使用了断言之后，能够在“时间”和“空间” 上都更接近设计内部的错误。 圈 圈 e 图2 - 1 断言在基于仿真的验证过程中的应用”1 f k u m 2 - ! a p p l y i n ga s s e r t i o n i ns l m u l a t i o n - b a s e d v e f i f i c m i o n c 7 i 北京工业大学工学硕士学位论文 2 2 几种不同断言的比较 断言用于描述设计必须满足的属性或者一定不能出现的属性。这样的属性经 常出现在设计规范或通信协议中，需要在验证阶段进行检验。在上一节中提到过， 断言又被称为监视器或检验器，已经被用作一种调试技术的方式，在设计验证流 程中使用了很长时哥1 6 】。目前已经发展出多种方式实现断言。传统上使用v e d l o g 或v h d l 很难描述它们，特别是与时序相关的属性。而目前出现了很多属性描 述语言例如p s l ，s v a 1 。7 1 ，以及断言库，例如o v l ，q v la n d0 i nc h e c k e r s 1 8 j 。通 过它们使得描述设计属性变得简单和有效。下面详细介绍实现断言检查的几种方 丸0 ( 1 ) v e r i l o g 厂、r h d l 用v e r i l o g 可以实现一些断言检查，如下面的例子是利 用v e m o g 描述一个监视器，它用来监测d m a 缓冲器的溢出情况。这种监视器 仅用于仿真过程，当需要时通过v e r i l o g 条件编译命令“、i f d e f 来实现。v e r i l o g 语 言本身的过程性以及冗长性的特点，使其不能很好的控制时序，更不适用于需要 大量断言的情况。另外，v e r i l o g 本身没有提供内嵌机制收集功能覆盖数据，所 以需要编写大量额外的代码来实现这一功能。虽然v h d l 本身带有关键字 “a s s e r t ”可以用于断言检查，但是与v e r i l o g 相似，用v h i ) l 描述断言检查过于 冗长和复杂。 p r o c e s s ( d m a c l k ) b e g i n i f d m ae l k e v e n ta n dd m ae l k = 1 t h e n a s s e r tn o t ( f i f of u l la n df i f ow r i t e ) r e p o r t “d m ab u f f e ro v e r f l o w s e v e r i t yf a i l u i 己e ： e n di f ； e n dp r o c e s s ；v h d l 断言检查 ( 2 ) p s l ( p r o p e r t ys p e c i f i c a t i o nl a n g u a g e ) p s l h 口性质描述语言，由标准 化组织a c c e u e r a 的功能验证技术委员会发布。它是一种用来定义和验证设计属 性的语言。可以直接在r t l 代码中使用p s l 结构，这种方式通过p r a g m a 机制实现。 在不支持p s l 的i 汀l 设计工具中，这种机制可以让用户方便的使用p s l 语言u 9 1 。 第2 章s v a 的应用方法 p s l 是形式化结构语言，分为4 个独立的层：布尔层，时态层，验证层和建 模层。布尔层由包含变量和语言的操作符组成的布尔表达式构成。布尔表达式在 离散的时间点上计算其值。时态层是p s l 语言的主要部分。时态层的表达式既 包含来自布尔层的表达式，也包含时态层操作符和扩展的时序正则表达式 ( s e r e ) 。时态层表达式通常用来在时间序列上建模。验证层通过语法的验证指示 词，将p s l 语句插入到h d l 模块中。 p s l 断言由用p s l 写的特性结合人们熟悉的硬件描述语言( v h d l 或v e r i l o g ) 写的布尔表达式并加入时态操作符和p s l 定义的序列构成。布尔表达式加上时态 操作符和序列就可描述状态随时间的变化关系。所以用带有p s l 的硬件描述语 言能更加简洁清楚地描述时态关系。在寄存器传送级设计中同时加上断言，并且 使得这些断言风格贴近r t l 代码，将使数字硬件的设计和验证过程结合起来，给 设计验证带来方便。另外，p s l 也提供了在验证过程中的一种衡量方法，通过在 形式规范的特性上建立的功能覆盖模型来衡量设计质量。而且对于硬件设计师和 验证工程师来讲，p s l 也提供了一种标准方法，可以为他们提供详细的机器可读 的设计规范文档。用p s l 写的特性可以作为注释嵌入到h d l 代码中，另外也可以 作为独立的文件。下面是一个p s l 断言的例子： p r o p e r t yd m a b u f f e r o v e r f l o w = n e v e r ( f i f o _ f u l la n df i f o _ w r i t e ) ( p o s e d g ed m a _ c l k ) ； a s s e r td m a _ b u f f e r _ o v e r f l o w ； p s l 断言检查 ( 3 ) o v l ( o p e n v e r i f i c a t i o nl i b r a r y ) o v l 是由a c c e l l e r a 组织推出的采用了断 言思想的验证库【2 0 j 。o v l 实际上是使用v h d l 、v e r i l o g 等语言定义和实现了一些 常用的属性声明。用户可以在设计里面直接使用这些属性声明来检测设计是否遵 从了相应的设计属性。o v l 支持采用s y s t e m v e r i l o g 、v h d l 、v e f i l o g 和p s l 的基 于断言的验证。o v l 这个库中包含一系列预定义模块，把这些模块例化在硬件设 计代码中，就可以得到预期的断言效果。前面的d m a 缓冲器断言检查用o v l 表 示如下： ( 4 ) s v a ( s y s t e m v e r i l o ga s s e r t i o n ) s v a 是s y s t e m v e r i l o g l 拘- - 个子集，专 门用来描述设计的属性。s y s t e m v e r i l o ga c c e l l e r a 织制订。a c c e l l e r a - i r 的 北京工业大学工学硕士学位论文 s y s t e m v e r i l o g 委员会成员来自模拟器、合成器、验证方法学等厂商，以及i e e e 1 3 6 4v e r i l o g 标准小组、资深设计与验证工程师。s y s t e m v e r i l o g 是一种硬件描述和 验证语言( h d v l ) ，硬件设计和验证工作都可以用s y s t e mv e r i l o g 语言完成，这个 特性可以让验证工程师和设计工程师使用同一种语言完成各自的工作。与使用不 同的设计和验证语言相比，设计和验证阶段使用统一的语言可以更容易地让两个 独立的小组理解彼此编写的模块功能。目前的版本s y s t e m v e r i l o g3 1 的侧重点在 验证部分，结合t s y n o p s y s 与i b m 在验证技术上的成果，包括了断言和功能覆盖 率的特性。下面的例子是一个s v a 检验器： 根据实现形式的不同，断言大致可以分成两类：基于语言的断言和基于库的 断言。基于语言的断言通过具有简洁语法和明确定义的形式语义的性质描述语言 来描写，p s l 和s v a 就是两种重要的基于语言的断言，特点是灵活、可以精确描 述设计的性质。但是p s l 和s v a 都是新的语言，要熟练应用它们需要花费一定的 时间。o v l 和0 i n c h e c k e r s 是基于库的断言，它们把常用的一些断言以库的形式 表示，这样就克服了学习新语言的麻烦。但是基于库的断言只包括一些最常用的 断言，库的实现机制受到结构和语义的限制，因此不能直接对库中的断言监视器 进行扩展。当需要描述的断言特性不能通过直接例化库中的断言检验器实现时， 只能通过增加新端口和参数来实现新的断言特性。此外，熟悉断言库中断言检验 器的端口及参数的意义和用法也需要花费一定的时间。 图2 2 是d v c o n 0 5t r i pr e p o r t 中对i c 设计验证人员中应用断言的情况所作的 统计，可以看出s v a 近年来得到了越来越多的应用。这一趋势得益于 s y s t e m v e r i l o g 标准化的过程。作为硬件设计和验证语言，s y s t e m v e r i l o g l 拘应用前 景非常当广泛。基于这一趋势以及s v a 本身的优点，本文选用s v a 应用于a b v 的 研究。 叠 i