（微电子学与固体电子学专业论文）形式验证在soc设计中的应用研究.pdf

摘要 摘要 本文的研究内容是作者在英飞凌硕士实习期间，参与完成的手机基带s o c ( s y s t e mo nc k p ：即片上系统) 项目验证内容的一部分。作者深入研究了形式验 证在s o c 设计中的具体应用。并结合由英飞凌所开发的形式验证工具o n e s p 烈， 研究了形式验证在s o c 设计中的流程和具体的实施方法。通过对形式验证流程的 深入研究，作者提出了一种简化流程的方法。该方法具有很高的直观性和高效性。 本文阐述了运用o n e s p 玳进行一致性检查和等价性检查的具体方法。研究 了一个具体的设计在形式验证各阶段在工具内部的表现形式。同时引入了 o n e s p 烈的一些常用命令。详细研究了形式验证中的模块验证，也叫做特征检查， 阐述了模块验证的具体流程，并结合一个小的设计实例研究了如何编写特征例 ( p r o p e n y ) ，如何查找错误。同时引入了基于o n e s p 矾的特征语言i t l ( i n t e m a l l a i l g u a g e ) 。以s o c 设计中至关重要的p c l ( p o r tc o 曲d 1 1 i 百c ：即端口控制逻辑) 模块为实例，研究如何针对该模块开展特征检查，并编写特征例。针对在s o c 的 验证中如何简化特征检查流程、提高验证效率的问题，给出了一种切实可行的简 化特征检查流程的方法，并详细介绍了运用这种简化流程的方法进行特征检查的 图形界面。 本论文研究的内容已经广泛的应用于s o c 的验证中，论文中所提出的简化特 征检查的策略也成功地运用到了实际工程项目中。工程实践表明，该方法能有效 简化特征检查流程、提高验证效率，具有高效可靠直观等优点。 关键字：片上系统形式验证模块验证特征检查端口控制逻辑 a b s 仃a c t 3 a b s t r a c t f o 皿a 1v 耐f i c a t i o ni ns o cd e s i 印a r es t l l d i e da 1 1 dd e s i 驴e di 1 1 “sd i s s e r t a t i o n ， w h i c hc o m e s 丘- o mt h ep r o j e c to fab a s e b a l l ds o cc m po fm o b i l ep h o n ei i lh l f i n e o n c o m p a i l ya sai n t e m s h i p t h ea u 协o rh a v ead e e p l yr e s e a r c ho nt 1 1 e 印p l i c a t i o no f f o m a lv 商f i c a t i o ni i las o cd e s i 弘a n df o 肌a lv 舐f i c a t i o nf 1 0 wa n dd e t a i l 卸l e m e n t a t i o nm e t h o dr e s e a r c hi i ls o cb a s e do nf o m a lv e r i f i c a t i o nt 0 0 1o n e s p n w h i c hi sd e v e l o p e db y1 1 1 丘n e o n t l l r o u 曲m i sr e s e a r c h ，m ea u t h o rp r o p o s e dag o o dw a y t op r e d i g e s tm ev 嘶f i c a t i o nn o w i ti sp r o v e dt h a tm es 仃a t e 百e sp r o p o s e di 1 1m i sp 印e r a r ee f 话c t i v e ，i n t u i t i o l l i s t i ca 1 1 dr e l i a b l e t h er e s e a r c hw o r ko ft h j sd i s s e n a t i o nm a i n l y i n c l u d e s ： n i s 廿1 e s i ss h o ws o m ec x a m p l e st od e s c r i b et h ei d i o 聊1 1 i cm e t h o d so nt 1 1 e c o n s i s t e n c yc h e c ka n de q u i v a l e n c ec h e c k a n de x p l a i n sh o wt h ed e s i g r i sa r er 印r e s e n t e d w j 伽nn l eo n e s p i z lt 0 0 1 s ，a 1 1 dh o wt h ec o 姗a 1 1 d si nt h es e t u pm o d ea r eu s e dt oc r e a t e t h i sr 印r e s e n t a t i o n t h et h e s i si n t r o d u c e st h em o d u l ev e r i f i c a t i o nw l l i c ha l s on 锄e d p r 叩e r t yc h e c l ( i n g i te x p a t i a t e s 吐1 ee x a c t l yp r o c e s so fm o d u l ev 嘶f i c a t i o n a n dt h e a u m o rc 0 瑚【b i i l e das m a l ld e s i 印m o d u l et os h o wh o wt 0w n t ey o u ro w np r o p e r t i e sa n d h o wt od e b u gn l ef a u l t na l s on a r r a t es o m ea b o u tp r o p 瞰yl 锄g u a g ei ，r l ( i 1 1 t e m a l l a n g u a g e ) a sp c l ( p o r tc o n t r o l1 i 百c ) f o ra ne x a i 【1 p l et od oaf i l r t h e rr e s e a r c ho nh o w t oc r e a t e p r o p e r t ya z l d h o wt o p r e d i g e s tt h ep r o p e r t yc h e c k i i l gn o w n 舀v e saa v a i l a b l e p r e d i g e s t i o nm e t h o do fp r o p e r t yc h e c kn o wa i m i n ga tm ep r o b l e mo fh o w t oi m p r 0 v e t h ee 伍c i e n c yo fv e r i f i c a t i o n a tl a s t ，i ts h o w sad e t a i lu s e m li n f o m a t i o no ft h eg i n t e r f 萏c e r h er e s u l t ss t u d i e di nm i sd i s s e r t a t i o na r es u c c e s s 血1 1 ya p p l i e df o r t h ev e r i f i c a t i o no f s o c a n dt h en o w p r e d i g e s t i o ns t r a t e 百e sp r o p o s e di n 雠sp 印e ri su s e df o rt l l er e a l p r o je c ts u c c e s s 龟l l yi ni n f i n e o n i ti si 1 1 d i c a t e dm a tm em e t h o dc a np r e d i g e s tm e p 叫) 鳅yc h e c k i n gn o we m c a c i o u s l y a n di te x a c t l ys a t i s f i e st h es p e c i f i c a t i o n 1 ( e y w o r d ：s o cf o m a l f i c a t i o nm o d e lc h e c l ( i n gp r o p e n yc h e c l 【i n gp c l 西安电子科技大学 学位论文独创性( 或创新性) 声明 秉承学校严谨的学分和优良的科学道德，本人声明所呈交的论文是我个人在 导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以标 注和致谢中所罗列的内容以外，论文中不包含其他人已经发表或撰写过的研究成 果；也不包含为获得西安电子科技大学或其它教育机构的学位或证书而使用过的 材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中做了明确的说 明并表示了谢意。 申请学位论文与资料若有不实之处，本人承担一切的法律责任。 本人签名：曷询寿、 日期 矽矿7 ，3 1 西安电子科技大学 关于论文使用授权的说明 本人完全了解西安电子科技大学有关保留和使用学位论文的规定，即：研究 生在校攻读学位期间论文工作的知识产权单位属西安电子科技大学。学校有权保 留送交论文的复印件，允许查阅和借阅论文；学校可以公布论文的全部或部分内 容，可以允许采用影印、缩印或其它复制手段保存论文。同时本人保证，毕业后 结合学位论文研究课题再撰写的文章一律署名单位为西安电子科技大学。 本人签名： 导师签名： 日期砂7 岁- 日期 伊芋 ，? 厶d、镬 古凡 夕 囟t 口旧、争 第一章绪论 第一章绪论 在s o c ( s y s t e mo nc k p ) 的设计过程中，验证是影响项目开发进度的关键因素。 主要原因在于随着s o c 芯片复杂度的提高，验证的模块也成指数的增加。工业实 践表明，在目前的设计流程中，验证所需时间已经占到整个设计周期的7 0 ，甚 至高达8 5 以上。目前芯片一次投片成功率( f i r s ts i l i c o n ) 只有3 5 左右，主要 原因就是验证不够充分【1 1 。s o c 设计的验证需要投入大量的资源，而随着设计规 模的增大，验证技术已经落后于设计和制造能力，使模拟和验证成为整个设计流 程的瓶颈，给提高设计生产率造成了障碍，因此如何更快更好地完成验证工作是 目前业界所关注的问题。 1 1s o c 验证存在的挑战 任何一种e d a 工具都不能完全解决s o c 验证问题。因为验证必须在各个角 度进行。例如从下面多个方面考虑【2 】： ( 1 ) 规范是否正确。在进行系统设计时，首先要对所设计的系统的要求有一个 规范。此规范若用自然语言描述，可能产生歧义。用形式化的方法来描述，或者 用一套符号体系来刻划就比较严格。 ( 2 ) 设计队伍正确理解规范的问题。这是设计的基础。若没有正确的理解，那 么下面的一切工作都建立在错误的条件下，也就无法实现设计要求。 ( 3 ) 每个模块设计的正确性。在自顶向下的设计中，每个模块是否正确地实现 了规范中的部分功能。 ( 4 ) 模块之间的接口是否正确的问题。当每个模块都是正确时，并不能保证设 计就是正确的，在模块正确的基础之上，还要考虑它们之间的接口是否正确。 ( 5 ) 是否真正完全实现了所需要的功能。在以上各个问题都解决的情况下，还 要考虑是否真正实现了所需要的功能。所以很难确定在什么情况下验证算是完成。 验证的困难体现在下面两个方面： ( 1 ) 验证的复杂性。对于一个基本触发器来说，状态数目是2 个，要测试模式 的数目是4 个：对于z 8 0 微处理器，有2 0 8 个寄存器和1 3 个基本输入，那么可 能的状态数目为2 2 0 8 + 1 3 = 2 2 ”，对于1 m p s 的计算机来说需要花费1 0 5 3 年才能仿 真完所有的转移，z 8 0 大约有5 k 门。对于2 0 m 门的芯片、片上系统又要多长时 间呢? ( 2 ) 验证的完整性。由于不能对设计的所有情况进行仿真和验证，那么验证又 在什么情况下是完整的呢? 是当我们耗尽时间和金钱时、是当我们需要制造产品 时、是当我们检查完h d l 代码的每一行的执行时，还是当我们测试了一周，而 2 形式验证在s o c 设计中的应用研究 没有发现一个新的错误时? 对于一个设计者来说，并没有理想的完整性。因为设计往往是非常复杂的， 无法确保全部功能的覆盖，并且可能的矢量数目远远超过所允许进行测试的时间。 在验证过程中，随着发现错误数目的减少，查找错误所需要花费的时间和金钱却 在增加。所以验证需要解决好两个问题：多大程度的验证就足够了? 和什么时间 验证开始进行? 上述问题就是s o c 设计中所遇到的不可避免的问题，这也给s o c 验证带来 了巨大的挑战。 1 2s o c 验证的策略 一般的验证的方法【3 1 自顶向下的验证方法：从整个系统到单个部件来验证。自底向上的验证方法： 从单个部件到整个系统来验证。基于平台的验证方法：在一个已经存在的平台中 来验证开发好的口。基于接口的系统验证方法；在接口层模拟每一个模块。对于 自底向上的方法来说，它进行的验证是局部的，对功能p 核能够比较容易和比较 快地捕捉错误。然后，s o c 的设计就是在这些高度可信赖的“无错误”的p 核上进 行。而最后的综合验证是适合应用基于接口的系统验证方法。 典型的验证方法 仿真t e s t b e n c h ：把一个设计置于验证环境下，来验证输入信号经过该设计 后是否得到希望的响应。测试环境通常是指t e s t b e l l c h 。个验证环境通常包括一 组部件：如总线功能模块、总线监视器、存储模块等，以及这些模块在所要验证 的设计的相互连接，验证还要有适当的模式和矢量。 随机测试：在没有工程师的参与下，创建测试脚本，来进行功能验证。 逆向测试：避免由一个错误来引起其它的错误，逆向测试是可以自动完成的， 它产生新的测试检验测试结果，并产生测试报告。以上的方法都是仿真，从电路 的描述抽象出模型，然后将外部激励信号或数据施加到此模式中，通过观察该模 型在外部激励信号作用下的反应来判断该电子系统是否达到了设计目标。仿真的 方法是目前进行设计时常用的方法，根据不同的仿真层次，有不同的仿真工具。 形式化验证：形式化验证是不同于仿真方法的对逻辑设计结果进行的另一种 验证方法。在自上而下的设计过程中，在设计的各个阶段和级别，每一级设计都 是以上一级的设计作为设计目标，得到本级的设计结果的结构描述，这是设计和 综合的过程。验证的任务就是证明所得到的结果正确的实现其设计要求。这里通 常包括两个方面： ( 1 ) 下一级所实现的功能与上一级的设计目标所要求的功能相一致，既功能验 第一章绪论 证。 ( 2 ) 下一级本身符合设计规则和条件制约，包括连接关系的限制、时间关系的 配合等，这就包括结构验证、时序验证和规则验证。 由于计算机工业的迅猛发展对设计自动化的需求，以及计算机结构与逻辑体 系的密切联系，形式化验证的研究也随之迅速发展。近年来，陆续有许多有效的 方法问世，并逐步向实用化方向发展。 1 3 形式验证在s o c 设计中的应用 形式验证是一种系统化方法，用穷举的算法技术证明设计实现满足设计规范 的特征。它覆盖了输入的所有可能序列，不需要开发测试向量，检查所有的边角 逻辑，提供了完整的覆盖率。 形式验证主要有两种方法：等价证明和特征检查【4 】。 1 等价证明 证明最终网表和原始的i 玎l 设计的等价一直是个问题。一种方法是放弃r t l 模型，只用门级模拟作功能验证。另一种是用相同测试集在r t l 和门级作模拟， 然后比较两者的输出结果。显然，用模拟来证明等价是不够的。而且两种方式都 会引入模拟瓶颈，延缓项目的上市时间。用形式等价证明取代门级模拟，可极大 减少验证时间，能提供穷举覆盖率的验证质量。 等价证明用数学方法证明两个设计的逻辑功能是否等价，确保最后的设计实 现的功能与寄存器级设计相同。证明时，一般选用规范作为比较标准。等价证明 可用来验证从寄存器级到g d s i i 版图整个芯片设计实现的功能，实际上，在低抽 象层次更加有用。 当前r t l 设计流程中，需要证明等价性的有r t l 和r t l 、i 汀l 和门级设计、 门级和门级以及版图和门级。为了改善性能、降低功耗、缩小面积或者提高可测 性，就要改进r t l 设计。综合工具和人工干预都有可能引入错误，就要检验综合 得到的门级设计实现与可综合i 玎l 设计的一致性。测试插入、扫描链排序、时钟 树综合以及模块的自动生成，也都有可能把错误引入门级设计，因此要检查修改 前后门级实现的一致性。物理设计工具中的缺陷和人工修改版图，都会引入错误。 物理设计实现的验证，首先从版图中提取出门级模型，然后与门级设计进行比较， 来证明两者的图形的等价性，即版图和电路一致性检查。 当前主流r t l 设计综合技术只优化组合逻辑，不改变时序逻辑。因此形式等 价证明工具假定设计的时序逻辑相同，只证明综合逻辑的等价性。形式等价证明 精彩之处在于用符号方式来推理证明或证伪等价性。符号逻辑，在整个输入范围 内分析代表逻辑网络的数学表达式，从定义上讲它就是穷举的。因此只要证明表 4 形式验证在s o c 设计中的应用研究 达式等价性，就证明了在任何输入输出上的等价。但等价证明算法非常复杂，无 法处理很大的设计。因此必须对设计进行划分以限定问题。一般把设计分割成逻 辑锥。逻辑锥是一个逻辑网络，所有的边界都由寄存器、端口或黑盒组成。锥的 概念源于这种逻辑网络有多个输入一个输出，呈锥子形状。 2 特征检查 特征检查用数学方法检查设计是否具有给定的特征，如总线控制器不多于一 个或者每个发出的信息包都得到了确认。特征比较小，易描述。特征集可以根据 设计的进展添加完善。特征检查多用在业务级和寄存器级，这样可以尽早发现错 误，以较小代价修正错误【5 j 。 特征是设计的行为属性，可以是高层属性如网络包的收发特点，或低层属性 如有限状态机的状态编码特点。特征一般用来描述设计中的边角逻辑、设计边界 或内部模块间的接口协议，有时用来描述复杂的础儿构造。 在形式验证里，不用创建测试基准，验证师用一组特征( 称为约束) 指定合 法的输入行为。这组约束是对设计周围环境的抽象，限制形式引擎在合法状态空 间中搜索。约束规定设计周围环境的静态行为，如在写周期里双端口存储器的读 地址不能等于写地址；和动态行为，如握手协议中模块收到请求信号后，必须在 规定的时间内发出恰当的应答信号。没有约束，形式引擎会报告虚假错误，而非 设计错误。事实证明，模拟接口断言约束对于特征检查很重要。若约束过严，形 式引擎就不能发现设计中的错误，也不会给出任何警告信息。对约束进行模拟就 可以发现问题，任何在模拟时发生冲突的约束，要么r t l 错误，要么约束过严。 在约束限制下，形式引擎穷举搜索设计的合法空间，证明设计特征永远存在， 或找到违反特征的激励序列( 反例) 。如果既没有发现证明特征成立的证据，也 没有特征不成立的反例，该特征就是未定特征。特征检查的首要目的是未定特征 的数目最小化，其次是告诉验证师检查每个未定特征的彻底程度。反例很有价值， 如果特征描述和约束都正确，那么每个反例都意味着设计中存在一个真正错误。 设计师可以根据反例修改设计中对应错误。相反，证据没那么有用，它不告诉你 哪儿有问题或者下一步该做什么。只有设计中所有特征都有证据证明其成立，证 据才能提高对设计质量的信任程度。但也许有些特征漏掉了。搜寻证据和反例需 要不同的技术，即静态形式验证和动态形式验证。 静态形式验证从设计的复位状态开始，在约束限制下，运用多种算法证明违 反某个特征是不可能的。主要的算法基础是模型检查、符号模拟和基于s a t 的推 导。为了处理大规模设计的复杂特征，需要划分设计，抽出与该特征有关部分进 行证明。这种对设计进行划分的形式技术叫做有界模型检查方法。对简单特征或 者很小的设计如两万门，静态分析验证不仅能提供证据也能找出反例。 第一章绪论 动态形式验证主要用来搜寻反例即设计错误，而非证据。为了效率最大化， 它从设计在模拟时的某个状态( 种子) 开始，因此是动态的。动态形式验证算法 分析每粒种子。给定种子后，依据约束，在种子开始的几个周期内，用极快的有 界模型检查方法为每个特征穷举搜寻反例。发现反例后立即报告，并移向下个特 征。所有特征证明结束后，移向下粒种子。如此反复。 1 4 形式验证的优缺点 从前面对形式验证的介绍中，相信读者对形式验证这种验证方法的优缺点已 有所了解，下面归纳一下形式验证的优缺点( 6 】。 1 形式验证的优点 a 更早发现设计缺陷，降低周期和成本 由于市场竞争激烈，i c 设计规模越来越大，而设计周期却越来越短。能否及 时发现错误对设计周期有很大的影响。另一方面，根据错误发现的时间和纠正错 误所损耗的资源的关系图，错误是否被更早的被发现同样对设计经费有很大的影 响。形式验证工具能够根据设计的结构自动地提取特性q r o p e n y ) ，表达成作为判 断标准的断言( a s s e n i o n ) 并且给与验证。由于形式验证的方法不需要验证者给与激 励，所以工程师能够在仿真之前较方便的发现一些错误，从而做到最早的纠正设 计中的不良。 b 断言取代测试例( t e s tc a s e ) ，减小验证难度【7 】 利用基于仿真的验证方法，工程师往往为了验证某一特性而编写一系列的测 试例，甚至要考虑到一些特殊的测试例。 着所验证的逻辑的复杂程度的不断加大， 这一切需要花费大量的时间、精力。随 验证所需的测试例成级数增长，以至于 某些特性已难以用测试例完全验证。对于形式验证，只要能将特性表达成为断言， 形式验证工具能够自动验证特性的正确性，极大的方便了测试者。最近，形式验 证工具所用的语言已标准化，测试者能够更方便、准确的表达所要验证的特性。 c 1 0 0 覆盖率，提高验证质量【s 】 形式验证不再依赖于测试者所给与的激励，而是通过数学的方法验证r t l 代 码与断言是否一致来确定设计的正确性，从而规避了测试例完整性问题，达到验 证的1 0 0 覆盖率。 d 结合断言验证方法，快速隔离错误【9 】 如今，断言验证的思想方法已广泛应用于s o c 验证中。这主要是由于断言验 证能够增强代码的可观测性，迅速找到错误根源。通常，形式验证工具应用断言 验证的方法，断言以注释形式出现在代码中，从而既不影响原有代码的工作，又 充分发挥了断言验证方法的作用，快速隔离错误。 6 形式验证在s o c 设计中的应用研究 e 不影响原有验证流程，易整合其它验证方法【l o 】 s o c 系统不断增大，以至于任何一种验证方法都难以单独完整地完成验证任 务。因此，各s o c 设计公司应用多种验证方法相结合，从而快速、高效完成验证 任务。 2 形式验证方法的不足 a 适合模块级或中小系统级的验证【l 由于形式验证存在状态空间爆炸性增长的可能，当系统变复杂时，验证将占 用较多的计算机资源，耗时增加。当系统复杂程度超出状态空间搜索的半径所能 覆盖的范围，形式方法已无法完成验证任务。 b 适合控制逻辑验证，验证的完整性取决于特性是否被全面准确的表达 形式验证一般具有两种断言：一种是工具自动提取的结构方面特性表达为断言， 一种是用户为验证功能方面的特性而应用形式语言定义的断言。一个系统是否被 完整的验证取决于两种断言是否准确表达了特性以及特性是否被完全表达【1 2 1 。 1 5 论文的研究意义与选题依据 众所周知，功能验证在芯片的整个设计周期中占用的时间最多。尽管目前有 许多技术可用于减少验证时间，但最终应当如何选择? 答案并不简单明了，而且 经常令人迷惑并要付出高昂的代价。 一个项目中需要使用的工具和技术必须在设计周期的初期就确定下来，以便 获得新验证方法费用预算的准确信息。经常有公司因为错误估计了运转这些新型 工具和技术所需的设计和技术的复杂性而浪费大量的资金和资源。产品的抽象级 越高，越容易设计；同样的，抽象级越高，越容易犯严重的错误。一个架构上的 缺陷可能会导致整个芯片的损害，而在门级网表中的连线错误可以通过重制解决。 例如，v e m o g 为设计者提供了一种相对容易的接口，以便他们在相当抽象的层次 上进行设计。当设计曾经作为制约性的瓶颈时，撕l o g 为设计生产率带来了指数 增长，并且大大推动了复杂芯片的发展【13 1 。但是如果设计者不了解在复杂的设计 周期中语言上的细微差别，就很容易犯错。在验证成为瓶颈的今天，同样的观点 也适用于许多验证技术和语言。 在上一节的介绍中，可见形式验证的方法，能够早期发现错误，1 0 0 的覆盖， 提高验证质量，同时又只适合模块级和控制逻辑的验证。所以现在形式验证与仿 真验证结合使用，实现优势互补，而不是一方替代另一方。在s o c 设计中，为了 缩短开发周期，提高验证可靠性，验证师经常将两种方法完美结合。由于利用了 形式验证主要依靠电脑完成，这样模块级的控制逻辑验证可以和其它工作同时完 成。由于在模块级数字逻辑验证之前，控制逻辑验证己基本完成，大部分错误已 第一章绪论 7 排除，数字逻辑验证大大加快。当进入系统级时，一般逻辑极复杂，形式工具难 以完成验证，主要通过依靠仿真验证来完成验证任务。如此，在不同的阶段，应 用不同的方法，从而充分发挥两者的优势。通过项目实践表明，合理应用形式验 证，项目时间能缩短至原来的三分之二或更多。 目前，有许多e d a 厂商开发了自己的形式验证( f o 锄a lv 嘶f i c a t i o n ) 工具。 如表1 1 所示，不但每家公司开发的工具必须依赖于自己的语法编写特性( p r o p e n y ) 测试例，而且每种工具都有自己的局限性【l4 1 。这就给验证师带来了一些困惑，究 竟该选用什么工具? 该工具能否满足验证计划要求? 又该怎么使用该工具? 该怎 么写特性测试例? 该工具流程是否简单易行? 等等。鉴于这些问题，该论文选用 h l 丘n e o n 公司开发的o n e s p i n 工具对上述问题做一一解答。h l f i n e o n 公司开发的 o n e s p i n 工具功能非常强大，既可以做等价性检查( e q u i v a l e n c ec h e c k i n 曲，又可以 做特性检查( p r o p e n yc h e c k i n go rm o d e lc h e c l 【i n 曲，包括动态和静态检查。这篇论 文主要以o n e s p i n 工具为平台，举例介绍了该工具在做一致性检查、等价行检查 和特征检查的流程和具体方法。重点研究了特征检查的方法，并通过举例，研究 了如何写特性( p r o p e r t y ) 测试例去做特性检查、如何调试( d e b u g 西n g ) 代码或者 特征例等问题。最后着重研究了简化基于o n e s p i i l 的特征检查流程的问题，并提 出了一种简单可行的方法，该方法具有很高的直观性和高效性。通过该论文，相 信读者会对基于o n e s p m 的形式验证方法在s o c 设计中的应用会有更深入的了 解。 表1 1 形式验证的工具 e q u i v a l e n c ed y n a m i c s t a t i c o 1 1 1 ( m e n t o r ) s 0 1 i d i f y ( a v e r a n t ) o n e s p i n ( 1 1 1 f i n e o n ) m a g e l l a l l ( s y i l o p s y s ) f o r m a l p r o ( m e n t o r ) j a s p e r g 0 1 d e n c o u n t e rc o n f o n n a l ( c a d e n c e ) i n c i s i v ef o n n a lv e r i6 e r ( c a d e n c e ) f o n n a l i t y ，e s p ( s y n o p s y s ) 形式验证在s o c 设计中的应用研究 1 6 论文工作概述与安排 这篇论文主要研究如何以o n e s p i n 为平台，根据设计特性编写特性测试例， 以及编写特性的一些技巧和如何查错，并给出了一种简化特征检查流程的方法。 论文的篇章结构安排如下： 第二章，介绍基于o n e s p i n 的形式验证方法。首先介绍o n e s p i n 的交互界面， 然后分别对一致性检查和等价性检查举例进行简单的介绍，在2 4 节中会详细说 明设计o n e s p i n 工具中表现形式，最后列举一些o n e s p i n 的常用命令。再转向如 何编写自己的特性测试例，以及如何运用别名( a l i a s ) 和宏名( m a c r o ) 。 第三章，对基于o n s p i n 的模块验证做重点介绍。在章节开始，首先介绍了一 下模块验证的一般流程，然后举例详细介绍了如何进行特征检查，最后介绍了 p r o p e r t y 语言i t l ( 3 3 节) 。 第四章，是论文的重点所在，主要以s o c 设计中不可缺少的模块p c l ( p o r t c o n t r 0 1l 0 百c ) 为例，研究如何针对该模块开展特征检查，并编写特征例。论文 最后，结合我在英飞凌的实习经验，针对在s o c 的设计中如何简化特征检查流程、 提高验证效率的问题，给出了种切实可行的简化特征检查流程的方法( 4 3 节) ， 并给出了运用这种简化流程的方法，进行特征检查的图形界面( 4 4 节) 。该方法 在实际项目的应用中，使得特征检查的流程取得了很大程度上的简化，提高了验 证效率。 第五章对本文作了全面的总结。 第二章基于0 s p i n 的形式验证方法 第二章基于o n e s p 烈的形式验证方法 2 10 n e s p i n 图形界面 0 i 麟砌读入了设计后，它的图形界面如图21 所示。图中三个数字标示的方 框是o l l 铒妇提供给用户的主要功能。用户可以方便的通过这些按钮去实现其功 能。其中方框1 中，主要是用于用户执行设计设置( d i 辨s 曲l p ) ： 读入设计( r 荫d i 鸩i i i 也ed 鹤i 舯：d l b 锄i o n f o r m l 丘1 v b i n t o n 自 v 耐l 皑6 l ) 详细阐述设计( b r 咖也e d 瞄i 舯：eb u t t o n ) 编译设计( 咖i l e t h e d i 弘：c b u c 【o n ) 指定时钟信号和复位时序( s p 姆d o d cp i 地盐dr 姻吐嘲u 曲) 蕾2 l o 嘴p 妯的图形界面 在第一步d e s i 鲫s 岬完全结束后，用户可以转抉到三种主要模式之一，c c 、 m v 或者e c 此后r 先前组成s 哪模式的按钮将会被隐藏并且显示当前模式的 按钮。详细的s c 呻模式如图2 2 所示。从左至右。这些按钮依砍执行读入、，l 龇 文件、读八v 耐k g 文件、设计详细阐述( d 蛔d n g 也ed e 甄驴) 、编译( c o m p l i l i 嵋) 设计和端口( p i n t h 。p o r t s ，o n l y e c m o d e ) 一rpt二一 l o 形式验证在s o c 设计中的应用研究 -1芦盆盆警盆誓蓝一=笛；茹i盆笛誓五翟誓；=茹；茹盔盘；二一 s 蝴! 舅鹫莲妪习匣爿竭囹国9 0 | d e nj ， 图2 2s e t u p 模式 图2 1 中的方框2 是s h e l l ：每个功能的输出信息都会显示在这里。方框3 包 括以下功能： h i d i n gt l l es h e n e i l t e n n gg u im o d e h i d en l eg u i e n t e r i n gs h e nm o d e 】m e r r u p t i n gt h ee x e c u t i o no f ar u l l l l i n gc o n u n a n d c a l l i n gt h eh e l pb r o w s e r o n e s p i n 提供了非常强大的帮助命令，这很方便用户很快的查找命令和掌握 该工具，很大的方便了验证师，节省了验证时间。那么如何获得帮助呢? 除了在 g 叽界面下直接点击h e l p - b r o w s e r 外，用户可直接在o n e s p i ns h e l l 区中输入命令 h e l p ”。h e l p 命令可以获得对一个命令的详细语法描述。例如，以下命令都可以 获得r e a dv e m o g 命令的语法描述： s e t l l p h e l pr e a d _ v 舐1 0 9 s e t u p h e l p 水v e m o 矿 除h e l p 命令以外，o n e s p i ns h e l l 也支持使用t a b 键自动匹配( t a b c o m p l e t i o n ) 命令。当用户输入了命令的前几个字母，再按下t a b 键，如果输入的前几个字母 在命令中是唯一的，s h e l l 就可以自动输入该命令；如果不唯一，s h e l l 就会列出所 有匹配的命令，用户可以通过上下键自由选择，例如： s e 呻 r e a d t a b c o i n p l e t i o n 的功能不光适合于命令匹配，在命令的选项( o p t i o n ) 和文件 名的匹配上同样适用。 用户要退出o n e s p i l l 时，可以在s h e l l 中输入：e x i t 如果用户没有保存数据库 ( 缸a b a s e ) ，o n e s p i l l 就会弹出对话框，提示是否保存数据库。 2 2 一致性检查举例 这部分主要举例说明如何用o n e s p i l l 执行一致性检查( c o n s i s t e n c yc h e c l ( i n g ) 。 1 r e a da d e s i 盟 在这个例子中，假设存在个v 谢1 0 9 文件包含了整个设计。在把o n e s p i n 调起来以后，用户可以通过在s h e l l 中输入以下命令读入v 嘶1 0 9 文件。 s e t l l p r e a d 一v e r i l o gs d r a m v 用户也可以在g u i 界面下，点击s e m p 目录下的r e a dv e r i l o g ( v ) 。 2 e l a b o r a t i o na n dc o m p i l a t i o n 第二章基于0 僻p i n 的形式验证方法 在读入全部的v h d l 和v 鲥l o g 文件后，必须对设计做d 曲谢眦i s o 妇口 d a b o r i 把 对于一些对验证无关紧要的单元( 1 l i l i t ) ，用户可以通过一些特别的说明( 在 25 节将会介绍) 使其不被编译，提高验证效率。 s m p p i l e 这个命令会产生一些单元的内部描述见图23 。 鹰麓曼霪蒸震雾墨= = = 圈23 完成编译后的。峭咖界面 3 s e t m o d e t o c c o n e o 有三种可选的模式。在c 竹( c o 雌i s t c n 。yc h 幽曲模式和 “m 、，伽砷山谛c 鲥。懒式都可实现一致性检查( l 酤鞋c yc h o 出岵) 。这 种重复是因为一致性检查是非常有用的而且便于用户集中注意力在等价性检查 ( e q u i v m c ec h e c k i n g ) ，而不需要3 6 0 m v 许可证( 1 k e n 辨) 所以值得推荐。 为了进入一致性检查，可在s i d l 中输入下面的命令： m l 矿s 吐n o d e c c 注意，该命令会将命令提示符从e i u 矿转变到饥”，如图2 4 所示。 4 c o n s l s l e n c y c h e c 幽g w 油m o d e l b u i l d i n g a s se r l i o n s 在c c 模式，许多的基本检查会被自动执行。这些检查都是基于设计中插入 的一些断言实现的。在工程应用中，该功能一般很少用到。所以这里不做详述。 执行完一致性检查后，便可以开始执行模块验证( | n o d u i e 州n c 越i o n ) 或者 特征检考( p r o p e n yc h e c k i n g ) 。关于模块验证将在第三章作详细介绍。 ；一引州_i兰 堡呙囊黑芸一 誊圜型 一一 一 形式验证在s o c 设计中的应用研究 图24o n e 印m 在c c 模式 2 3 等价性检查举例 这部分主要举例说明如何用0 n 髂p i n 执行等价性检查( c q u i v 蛆啪c h e c k i n g ) 。 等价性检查主要是检查两个门级网表( g 甑“e v dn 蚰i 趾) 之阃是否一致或者r t l 级与门级网表级是否一致以及两个r t l 描述是否一致。在此将以前一部分提及 例子的v 嘶l o g 设计和v 壬玎) l 设计作为对比举例。 1 r 朋d 也e t w o d 商g 在o n e s p i l i 中，被比较的两部分设计被冠以象征性的名字9 0 1 d ”和 铆i 刚”。通常，假设g o l d d 髂j 印是正确的，把i 州s c d d 画鲈与g 。l d 锄d i 印 进行比较。为了强制某一命令工作在p l d d c s i 印或者m 6 s e d 如啦n 上，必须指 定相应的选项窨o l d 或者f e v i s e d 如果投有指定这些选项，系统将教认当前的 设计是g o l d d e s i 乳命令也将会工作在当前的设计。 通过下面命令读入两个卸) l 文件。 s 曲叩芦r 朗d - 聊i l o gs d 胁v m 妒d - v h d l f e v i s e d s d r m v h d 读入上述两个文件后的0 i 懈咖界面如图2 5 所示。 第二章基于o n e s p i n 的形式验证方法 女8 s i o ns 山p e 剧ri 、* i 。j “。三。一w1 0 0s n d 洲s 出口 叵王至至：! ! j 雪重i j ig 。”e n 【，岳d ，# 由氇# 嚏。、孝” 6 0d e n * 5 9 n 驰 r e v 目“o e 5 目“ 1 s w l g o q e s o 岫 l a u 8 v e n o a ；口w 。mv e i 口目n o p 口sv h d 型竺! 上! 坐l _ 垦型! 划竺竺u 壁些上! 划 s h e t i l ”t 叩咖r i l o q vi l 。i 。f 妇t ：1 8 oo o n l d n d l i “日 l 。i _ 皿l l n i l i a l i 2 a t 川1 1 e 。，“36 怖o p 州洲d l p t 帅t 抽d 1k 】f 一一 l n v i - f u l l y i 1 l h 1 d e5 h s h “m o d et oh e j 0 图2 5 读入两个文件后的0 1 1 唧i n 界面 2 e l a b o r 蚵o 卸d o 埘l 撕 在读入设计文件后，设计必须做e l a b o r a t i o n 。之后，必须对设计进行c 唧i l e 。 s e 呻 d a b o r a 把b d i h s e m p c o m p i k o t b 编译成功后，o 印i n 会产生两个设计( 9 0 1 d 和椭。d ) 的内部描述( 曲如1 a l ”m n 删：l m i t m o d e l ) 3 & t m o d c t oc c 成功完成编译后，便可以开始等价性( e q u i v 面锄c ec h 。c 虹n g ) 。 s a t i l p s 吐_ j o d c e c 注意，该命令完成后命令提示符将从飞e 呻”转变到钮”指示模式的转变 如图2 6 所示。 4 m ”p i n sa n d s 僦 设计的对比以g o l d 曲d 耐印和r e v i s e dd e d 印的输入、输出和状态的映射 ( m a p p 吨) 为基础。它们的映射关系通过m a p 命令建立起来的。完成映射后的 m e 蛐界面如图2 7 所示。 0 p m 印 5 c 优n l a 把t h e t w o 蜥鲫 在映射的建立之后，两个设计便可以开始对比。 形式验证在s o c 设计中的应j 研究 一7“ ? - ：l 一二一h 二w “= 。1 _ 一 _ 一- 啊毋 、。0 囝 厢。 暖? 蜒用口_ 孵硎啊。一一黜群蠲謦龃战嗣田黯一一墨! 幽 一一 j一“0 d - i s l 自s 1