（计算机应用技术专业论文）并发的广义符号轨迹赋值的研究.pdf

孔! 【sl ， 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工 作及取得的研究成果。据我所知，除了文中特别加以标注和致谢的地 方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含 为获得电子科技大学或其它教育机构的学位或证书而使用过的材料。 与我一同工作的同志对本研究所做的任何贡献均己在论文中作了明 确的说明并表示谢意。 签名：纽! 盛：雄日期：矶f o 年歹月叫日 论文使用授权 本学位论文作者完全了解电子科技大学有关保留、使用学位论文 的规定，有权保留并向国家有关部门或机构送交论文的复印件和磁 盘，允许论文被查阅和借阅。本人授权电子科技大学可以将学位论文 的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或 扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后应遵守此规定) 签名：纽熊! 丛导师签名：丝i 强 日期：7 , 0 1 q 年，月珥日 工 ，lr ， f ， “一、 ， 摘要 摘要 随着数字逻辑设计的规模越来越大，复杂度越来越高，功能验证已成为设计 过程中的首要瓶颈。在过去几十年中，人们对于数字电路顺序行为的验证进行了 深入而广泛的研究并提出了许多行之有效的验证方法，主要分为基于模拟的和基 于形式方法的验证技术【1 1 。然而，数字集成电路是典型的并发系统，如何实现对并 发行为的有效验证就成为保证数字电路功能正确性的关键因素。 本文在了解国内外形式验证技术研究成果的基础上，对当前主流形式化验证 方法中的广义符号轨迹赋值( g e n e r a l i z e ds y m b o l i ct r a j e c t o r ye v a l u a t i o n ，g s t e ) t z - 3 】验 证方法进行了深入的研究和拓展，修改断言图及其验证算法使之能更简洁的描述 和验证数字电路的并发性质。 本文在研究方法上，首先深入学习和研究了广义符号轨迹赋值相关的理论包 括电路模型、电路模拟方法，符号轨迹赋值【4 5 】和广义符号轨迹赋值的核心算法。 并通过实例展示了断言图描述电路并发性质时的不足。 其次，学习和研究了进程代数【6 。8 】的表示方法后，本文提出了一个基于广义符 号轨迹赋值的组合方法来克服断言图不能简洁描述电路并发性质的限制。( 1 ) 提 出了一个规范语言，它能用组合的方式简洁的描述系统的并发行为。这种组合是 逻辑的，不依赖于对系统实现细节的深入理解。这个语言是对广义符号轨迹赋值 规范语言的拓展，它引入了一个新的m e e t 运算符，用类似于进程代数的方式表达。 ( 2 ) 针对新的断言图规范，本文对经典的广义符号轨迹赋值的算法进行了修改， 该算法能直接深入规范的语法结构并建立从规范的语言元素到电路状态集合的模 拟关系。本文设计了一个高效而实用的方法来直接验证并发规范。 第三，在平台f o r e 平台环境【9 】下利用f l 语言对改进后的并发验证算法进行 编码实现和测试。实验结果表明修改后的断言图和算法是有效的，在验证并发性 质时确实能够减小断言图的复杂度。 最后，对全文进行系统、全面的总结，指出了下一步研究和改善的方向。并 展望了形式化验证算法在电路设计领域的良好应用前景。 关键词：形式化验证，g s t e ，进程代数，并发系统 ， a bs t r a c t a sd i g i t a ll o g i cd e s i g n sg r o wl a r g e ra n dm o r ec o m p l e x ，f u n c t i o n a lv e r i f i c a t i o nh a s b e c o m et h en u m b e ro n eb o t t l e n e c ki nt h ed e s i g np r o c e s s i nt h ep a s tf e wd e c a d e s ， p e o p l eh a v es t u d i e di n d e p t ha n de x t e n s i v e l yo nv e r i f i c a t i o no fs e q u e n t i a lb e h a v i o r so f d i g i t a lc i r c u i t sa n dp r o p o s e ds e v e r a l e f f e c t i v ev e r i f i c a t i o nm e t h o d s ，m a i n l yi n c l u d e s i m u l a t i o nb a s e da n df o r m a lm e t h o db a s e dv e r i f i c a t i o nt e c h n o l o g y h o w e v e r , d i g i t a l c i r c u i t sa r et y p i c a lc o n c u r r e n ts y s t e m h o wt op e r f o r mt h ev e r i f i c a t i o no fc o n c u r r e n t b e h a v i o r si sac r i t i c a lf a c t o rt oi n s u r et h ef u n c t i o n a lc o r r e c t n e s so fd i g i t a lc i r c u i t s b a s e do nu n d e r s t a n d i n go fl o t so fp r e v i o u sw o r ko nf o r m a lv e r i f i c a t i o n ，w es t u d y d e e p l yt h eg s t em e t h o dw h i c hi s o n eo ft h e c u r r e n t l ym o s ti m p o r t a n tf o r m a l v e r i f i c a t i o nm e t h o d s ，a n de x t e n di tt om a k ei tc a ns u c c i n c t l yd e s c r i b et h ec o n c u r r e n t p r o p e r t i e so fd i g i t a lc i r c u i t si nv e r i f i c a t i o n o ns t u d ym e t h o d s ，f i r s t l y , w es t u d i e dt h et h e o r ya b o u tg s t e ，i n c l u d i n gc i r c u i t m o d e l ，c i r c u i ts i m u l a t i o nm e t h o d s ，s y m b o l i ct r a j e c t o r ye v a l u a t i o na n dt h ek e r n e l a l g o r i t h m so fg s t e b e s i d e st h a t ，w es h o wt h es h o r t a g eo fg s t ew h e ni td e s c r i b et h e c o n c u r r e n tb e h a v i o rb y e x a m p l ei nt h et h r e ec h a p t e r s e c o n d l y , a f t e rs t u d y i n gt h ep r o c e s sa l g e b r a , w ep r o p o s e dac o m p o s i t i o n a l a p p r o a c hb a s e do ng s t et oo v e r c o m et h el i m i t a t i o nt h a tt h eg s t ec a n ts u c c i n c t l y d e s c r i b et h ec o n c u r r e n tp r o p e r t i e so fs y s t e m ( 1 ) w ep r o p o s e das p e c i f i c a t i o nl a n g u a g e t h a ta l l o w st h ec o n c u r r e n tb e h a v i o ro fas y s t e mt ob e s p e c i f i e ds u c c i n c t l yi na c o m p o s i t i o n a lm a n n e r s u c hac o m p o s i t i o ni sl o g i c a la n dd o e sn o tr e l yo nad e e p u n d e r s t a n d i n go f t h ei m p l e m e n t a t i o nd e t a i l so ft h es y s t e m t h el a n g u a g ei sa ne x t e n s i o n o ft h eg s t es p e c i f i c a t i o nl a n g u a g ew i t han e wo p e r a t o r m e e t a n di se x p r e s s e di nt h e f o r mo fp r o c e s sa l g e b r a ( 2 ) a g a i n s tt h en e w c o m p o s i t i o n a l a s s e r t i o n g r a p h s p e c i f i c a t i o n ，w em o d i f i e dt h ea l g o r i t h mo fg s t e t h em o d i f i e da l g o r i t h mh a st h e a b i l i t yt ow a l kt h r o u g ht h es y n t a c t i c a ls t r u c t u r eo ft h es p e c i f i c a t i o na n de s t a b l i s ha s i m u l a t i o nr e l a t i o nf r o mt h el a n g u a g ee l e m e n t so ft h es p e c i f i c a t i o nt ot h es e t so fs t a t e s i nt h ec i r c u i t i i a b s t r a c t t h i r d l y , w es t u d i e dh o wt oi m p l e m e n tt h em o d i f i e da l g o r i t h mu s i n gf li nf o r e p l a t f o r ma n dd o n et h ee x p e r i m e n tt ot e s ti t 1 1 1 ee x p e r i m e n tr e s u l t ss h o wt h a tt h en e w a p p r o a c hi se f f e c t i v ea n di tc a nr e d u c et h ec o m p l e x i t yo f t h ea s s e r t i o ng r a p h f i n a l l y , ac o m p r e h e n s i v es u m m a r yi sg i v e na b o u tt h i st h e s i s ，a n dp o i n to u tt h e d i r e c t i o no ff u r t h e rr e s e a r c ha n di m p r o v e m e n t ，a n dt h ep r o m i s i n ga p p l i c a t i o np r o s p e c t o ff o r m a lv e r i f i c a t i o n k e y w o r d s ：f o r m a lv e r i f i c a t i o n ，g s t e ，p r o c e s sa l g e b r a , c o n c u r r e n ts y s t e m 目录 目录 第一章绪论。1 1 1 概述。1 1 2 验证的基本概念和原理1 1 2 1 验证的基本概念1 1 2 2 验证的基本原理。3 1 3 验证方法学4 1 3 1 基于模拟的验证4 1 3 2 基于形式方法的验证6 1 4 研究现状与研究内容8 1 4 1 研究现状8 1 4 2 主要工作8 1 5 论文组织9 第二章广义符号轨迹赋值。1 0 2 1 电路模型。1 0 2 1 1 网表1o 2 1 2k rip k e 结构1 1 2 2 电路模拟方法1 2 2 2 1 二值模拟1 2 2 2 2 三值模拟1 3 2 2 3 符号模拟15 2 3 符号轨迹赋值1 6 2 3 1 性质规范：16 2 3 2 验证算法17 2 4 广义符号轨迹赋值1 9 2 4 1 断言图。1 9 2 4 2 验证过程2 1 2 5 本章小结2 8 i v 目录 第三章并发性质的刻画的研究3 0 3 1 问题来源3 0 3 2 进程代数3 2 3 2 1 进程代数简介3 2 3 2 2 通信系统演算c o s 3 2 3 3 断言语言的研究3 4 3 3 1 基本概念3 4 3 3 2m e e t 运算符一3 7 3 3 3 并发规范3 8 3 4 并发规范模型检验算法设计3 9 3 5 本章小结4 2 第四章并发验证算法的实现的研究4 3 4 1f o r t e 验证环境4 3 4 1 1f o r t e 简介4 3 4 1 2e x1 f 格式4 4 4 1 3 函数语言f l 4 5 4 2 并发验证算法的实现4 8 4 2 1 软件框架4 9 4 2 2 算法流程5 0 4 2 3b d d 处理技术5 1 4 2 4 参数化表示技术5 6 4 2 5 数据结构及关键源码5 7 4 3 验证实验6 3 4 3 1 三输入端电路6 3 4 3 2 投票机系统实例6 5 4 4 本章小结6 6 第五章结论与展望6 7 5 1 研究总结6 7 5 2 研究展望6 8 致谢6 9 参考文献7 0 个人简历及硕士期间研究成果7 4 v 目录 个人简历7 4 获奖情况7 4 参与的科研项目7 4 v i 第一章绪论 1 1 概述 第一章绪论 近年来，随着微电子技术的高速发展以及人们对信息技术的需求的不断增加， 集成电路的规模越来越大，设计大规模复杂集成电路的关键问题之一是如何检查 设计的正确性，即设计验证。传统的验证方法有模拟、测试和仿真技术，但是对 于大型的系统，模拟和测试都不可能是完全的，只能针对某些典型的情况或者随 机的进行模拟或测试，不能保证完全的错误覆盖，这就难以完全排除所有的设计 错误。由于集成电路的复杂性，它的试制费用相当昂贵，又由于电子产品市场的 剧烈竞争，产品的上市时间极为重要，设计中遗留的一点微小的错误将可能造成 巨大的经济损失或者引起人员伤亡等灾难性的后果。据统计，目前设计验证的时 间占整个设计周期的5 0 , - 8 0 t 1 4 】。因此设计的正确性验证已经成为设计的瓶颈， 被称为“验证危机 。 如何解决设计正确性已迫在眉睫。形式化验证是指从运用数学的方法对电路 功能进行完备的证明或者验证电路的实现方案是否实现了电路设计规范的功能的 验证方法。它能保证对所用情况进行验证，在集成电路设计验证中得到越来越广 泛的验证。形式化验证技术在集成电路设计的各个层次都得到了运用，主要的方 法有定理证明、模型检验【l o 1 3 】和等价性检验。 1 2 验证的基本概念和原理 1 2 1 验证的基本概念 设计过程是将一组设计规范转换为规范实现的过程。在规范层次上，规范指 明了设计所执行的功能但并不涉及如何去执行。规范的实现方案给出如何提供其 功能的细节。规范与其实现方案均为功能描述的一种形式，但它们的具体性和抽 象性是出于不同层次的。描述的抽象层次越高，给出的细节就越少；因而规范的 电子科技大学硕士学位论文 抽象层次比实现方案要高。 较高层次 抽象层次 1lr 较低层次 设计流程 功能性规范 算法描述 r t l r - 级网表 晶体管级网表 物理布局 较少 上 细节 上 较多 图1 1 设计的抽象层次图 如图1 1 所示，表示设计过程抽象性的图谱的抽象性从上到下不断的降低：功 能规范，算法描述，寄存器传输级( r t l ) ，门级网表，晶体管级网表，物理布图。 沿着图谱的任意层次，都可以给出一个更低层次的多种形式的描述。例如，在门 级，就有着无限种类的电路可以实现相同的r t l 描述。在设计过程中，在图1 - 1 第一章绪论 验证是一个与设计相反的过程，它从一个实现方案开始，并且确认该实现方 案是否满足其设计规范。于是，在设计的每一步都有验证步骤与之对应。例如， 把功能规范转换为算法实现的设计步骤要求有验证的步骤，以确保算法能执行规 范中的功能。与此类似，物理设计层从门级网表层生成的布图也需要相应的验证。 总之，设计验证包括许多方面，比如，功能验证、时序验证、布图验证及电学验 证等。本论文只研究功能验证，图1 2 展示了设计过程与验证过程之间的关系。 1 2 2 验证的基本原理 设计的过程可以看作是一组规范转换为一个实现方案的路径。验证的基本原 理包括两个步骤。在第一个步骤中，把一个规范转换为一个实现方案，这一步叫 做验证转换。在第二个步骤中，把验证所产生的结果和设计所产生的结果进行对 比从而检验出错误。如图1 3 所示。通常，验证转换的结果发生在验证工程师的头 脑中，其形式是从规范中推导中得到的性质。例如，验证工程师可以根据规范和 计算获得模拟输入向量的预期结果，这个结果就是一种实现方案。 图1 3 利用冗余性验证的基本方法 模型检验的原理是上述原理的一个变体，它的第一个步骤是从设计规范中抽 取必要的性质，用一种规范来表示，第二步检验设计是否满足规范表示。如图1 4 所示。 ；j “规范 性质检验 ：零种规范表示，卜 其他设计 图1 _ 4 一个来自模型检验基本方法的变体 典型的基于模拟验证的模型也是符合验证原理的。基于模拟验证的模型包含 吗 ：。 足 酣rp0 电子科技大学硕士学位论文 四个组成部分：电路、测试模式、参考输出和比较机制。电路在测试模式下被模 拟，并把测试结果与参考输出加以对比。由设计路径产生的实现方案就是电路， 有验证路径产生的实现方案则是测试模式和参考输出。之所以考虑把测试模式与 参考输出作为验证路径的实现结果，是因为在确定从测试模式产生的参考输出的 过程中，验证工程师把基于规范的测试模式转换为参考输出，而这一过程正式一 个实现的过程。最后，比较机构对模拟结果进行抽样以确定它们是否与参考输出 相同。基于模拟的验证的原理如图1 5 所示。 规范 其他设计 1 3 验证方法学 图1 5 模拟方法对基于冗余的验证的影响 出 模拟 在目前流行的验证方法中，验证方法主要有两大类型：基于模拟的验证和基 于形式方法的验证。这两种类型之间的主要区别在于是否存在测试向量。基于模 拟的验证方法依赖于测试向量，而基于形式方法的验证则不然。另外还有一种方 法可区分这两种类型，即模拟方法是面向输入的( 设计者给定输入测试) ，而形式 方法则是面向输出的( 设计者需要提供需要测试的输出特征) 。有一种混合方式的 类型，称为半形式化验证，这种方法用输入向量并在形式上围绕向量的相邻部分 进行验证。由于半形式化是上面两种类型的结合，故这里不单独讨论。 1 3 1 基于模拟的验证 基于模拟的验证是一种最为常用的验证方法。在基于模拟的验证中，设计被 置于一个测试基准之下，把输入激励施加于测试基准，然后从设计获得输出并将 它与参考输出进行比较。测试基准由支持设计的操作代码组成，有时也生成输入 激励，同时把输出与参考输出进行比较。输入激励可以在模拟之前产生，并在模 拟时从数据库读到系统设计，或者可以在模拟运行时生成。类似的，参考输出也 4 第一章绪论 可以提前生成或者即时生成。对于后一种情况，将参考模型与系统设计以锁步方 式进行模拟，并对两个模型的结果进行比较。 在对设计进行模拟之前，通过运行一个l i n t e r 程序能够检查静态错误或者潜在 错误或者编码风格错误。它不需要输入向量，因此能够检测与输入激励无关的错 误。接下来，在测试计划中生成项目的输入向量。针对特定功能和特征要求的输 入向量称为定向测试。由于定向测试在输入空间中偏向于设计者特别注意的区域， 而错误经常也出现在那些设计者不注意的区域，因此，为了把注意力从特别关注 的区域转移到其他区域，可以在采用定向测试的同时进行伪随机测试。建立这些 测试之后，选择模拟器执行模拟过程。衡量一个设计的模拟的测试的质量是该测 试所提供的覆盖率。覆盖率度量了该设计的模拟及验证的程度。当模拟时观察到 非预期输出时，必须找出其根本原因。此外，当发现一个错误后，必须与设计者 沟通并修复错误。通常，可以把错误记录到错误跟踪系统，该系统会向该设计的 所有者发送一个通知，然后由所有者对错误进行锁定修复。 基于模拟验证的典型的流程总结如图1 6 所示，图中虚线部分表示基于模拟验 证的特有的部分。与形式验证方法比较，这些部分被形式验证的相应部分所取代。 图1 - 6 基于模拟的验证的流程图 电子科技大学硕士学位论文 1 3 2 基于形式方法的验证 与基于模拟的方法不同的是，基于形式方法的验证不需要生成测试向量。目 前的形式验证技术主要有等价性验证、模型检验以及定理证明。其中，模型检验 和定理证明属于性质验证类型。典型的形式验证如图1 7 所示。虽然形式验证并不 需要测试向量，但是需要测试基准，这些测试基准使得电路处于正确的操作模式。 设 计 错 误 图1 - 7 形式验证的典型流程图 ( 1 ) 等价性验证 等价性验证【1 5 】是确定两个实现方案在功能上是否等价。等价性检验有两种基 本的方法。一种方法对输入空间进行系统搜索，以找出一个输入向量能够区分两 个电路的向量，这种方法称为s a t ( 可满足) 方法【l6 1 。s a t 方法与自动测试模式 生成算法类似。另一种方法是把两个电路转换成正规的表达形式，并比较它们。 正规方法的特点在于，两个逻辑函数等价当且仅当它们的相应的表达方式是同构 的。换言之，两个表达方式出了名称之外是相同的。简化的有序的二叉判定图【1 7 j ( r o b d d ) 就是一种正规表达形式。两个等价函数的简化的有序的二叉判定图在 图形上是同构的。如果等价性检验失败，检验程序将生成输入向量序列，当该向 量序列被模拟时可以显示出两个电路之间的差别。 ( 2 ) 模型检验 模型检验是形式验证的主要技术，它能处理比等价性检验更为一般的问题， 其目标是证明或者反驳某个电路具有规范某一部分性质。模型检验方法的基本思 想是把要验证的时序电路抽象为一种有限状态机和k r i p k e 结构模型，并用一种时 6 第一章绪论 序分支逻辑( c t l ) 语言来描述要验证的电路所应该满足的性质；然后状态机分析 或者称之为状态空间搜索的技术来判别该时序逻辑所描述的命题正确与否。在模 型检验方面有一种代表性的方法是符号模型检验方法，它用b d d 来表示整个电路， 并将状态转换函数和输出函数在一起加以表示，称为转换关系。 由于符号计算在克服计算复杂度方面取得了很大进展，符号模型检验已经有 不少工业规模的电路得到验证，其中包括p c 局部总线【1 8 - 1 9 1 、一个飞行控制器【2 0 】 等。虽然符号模型检验取得了很大成功，但在由于工业级规模验证问题和规范的 复杂性，模型检测仍然存在“状态爆炸 问题【2 l 】，目前的解决办法有自动抽象、 组合的模型检测、以及将模型检测和定理证明相结合等。 此外，模型检验程序还会在能力和效率上表现出对被验证的性质的高度的敏 感性。某些性质很容易判定，而另一些则不能结束运行，或者不能为工具所接受。 例如，某些模型验证程序不接受无界时间的性质。有界时间性质是指在某一个固 定的时间区间的性质。 本文研究的广义符号轨迹赋值g s t e 是一种依赖于符号模拟的基于四值格的 模型检验技术。它已经在门级和晶体管级验证大规模硬件设计中显示出巨大的潜 力，并能够高度的自动化。 ( 3 ) 定理证明 与模型检验利用的是状态空间搜索的办法不同，定理证明利用了演绎推理的 方法。在定理证明的过程中，把性质表述为数学命题，把设计表述为数学实体， 并把数学实体作为若干个公理。其目标是，确定命题是否可以从公理中演绎得到。 如果可以，其性质就得到证明；否则，其性质就不存在。定理证明程序的自动化 程度低于模型检验程序，所以，更需要用户的手动帮助。用户利用工具把与命题 有关的信息集中在一起并建立中间目标( 即引理) ，而工具则根据输入的数据试图 实现中间目标。 如要有效的使用定理证明，需要对工具内部操作有深刻的了解，还要熟悉数 学证明的过程。虽然不够自动化，但是对定理证明的有效使用可以处理比模型检 验规模更大的设计，而且只占更少的内存。此外，定理证明程序能接受更为复杂 的性质。例如，定理证明程序能够处理用高阶逻辑( h o l ) 书写的性质，而模型 检验程序几乎只能处理一阶逻辑及计算树逻辑或其变化形式。h o l 具有比一阶逻 辑更强的表达能力，能够精确地表示复杂的性质。 7 电子科技大学硕士学位论文 1 4 研究现状与研究内容 1 4 1 研究现状 数字集成电路是典型的并发系统。目前，如何对并发系统进行规范和验证已 经有了广泛的研究，主要分为两个方面：层次状态机【2 2 彩】和进程代数。其中大部 分的方法主要集中在对规范公式、规范的正确性、以及模块优化策略上面。 模型检验是重要的形式化验证方法，如何利用模型检验方法去对一个实现去 验证其并发的性质规范是越来越受到人们重视。例如，近年来，为了解决符号模 型检测状态的爆炸问题，基于“假设一保证 的组合方法【2 6 2 8 】越来越受到欢迎。在 这种方法中，被验证的电路被描述为一些并行的有限状态组件的组合，电路的正 确性被表述为局部性质的集合。这些局部性质是用来刻画每个组件相应的正确性， 但前提是假设这些组件之间的接口是正确的。这种方法比较有效是因为它首先分 别用模型检验验证每个组件的正确性，然后通过假设保证推理来得到整个电路的 正确性。这种方法的主要缺点是它写的规范非常依赖于实现，要求用户非常了解 各个组件之间是如何交互的。因此，它更是一种靠手工、繁重的、对实现修改十 分敏感的方法。 广义符号轨迹赋值是符号轨迹赋值的拓展，它很好的解决了符号轨迹赋值上 面存在的缺陷，并允许用户根据需要在表达能力和时间效率、完备性和空间效率 之间取得一个良好的平衡。最重要的是它具有了传统模型检验一样的表达能力。 在i n t e l ，它已被广泛的应用于含有数以万计状态的超大规模复杂电路的设计验证 中。但是由于其性质描述语言断言图的顺序性质，使得它不能够很简洁的描述电 路的并发行为。因此，如何修改传统断言图，使其更加容易简洁的描述并发性质 并对其验证就显得非常具有实际意义。 1 4 2 主要工作 依托以上研究背景，本文主要对广义符号轨迹赋值的断言图和及其验证算法 进行研究，使得广义符号轨迹赋值能更好的验证电路的并发性质。研究的主要内 容以下三个方面： 首先，研究如何刻画并发系统及其性质，修改拓展顺序断言图使其更加容易描 述系统的并发性质。 第一章绪论 其次，研究广义符号轨迹赋值如何验证电路的并发性质，即如何对拓展后的断 言图进行验证，设计验证算法。 最后，研究如何在f o r e 平台下拓展实现设计的并发验证算法，使其集成到f o r e 当中。 1 5 论文组织 第一章，绪论。 该章节首先从宏观的角度介绍了验证的基本概念和原理以及验证方法学。然后 介绍了本文的研究意义、研究内容和组织结构。 第二章，广义符号轨迹赋值。 这一章主要介绍了广义符号轨迹赋值，包括它的发展历史，理论基础以及它的 用法。首先介绍了电路的两种模型结构；其次，介绍了随着集成电路规模的不断 扩大以及对性质表达力的不断提高，传统的模拟是如何发展为符号轨迹赋值进而 发展为广义符号轨迹赋值的。 第三章，并发性质的刻画的研究。 这一章描述了如何利用进程代数的思想拓展传统的广义符号轨迹赋值的断言 图使其能够更加简洁的描述刻画系统的并发性质并进行验证。首先，介绍了问题 的来源和进程代数的语法。其次，对传统断言图进行拓展，使其描述并发性质更 加规范。最后，提出针对拓展后并发规范的模型检验算法，并对其复杂度进行了 简要分析。 第四章，并发验证算法的实现的研究。 该章节内容主要是研究在f o r t e 平台下如何实现并发的广义符号轨迹赋值算 法。首先，介绍了f o r e 平台及e 】d i f 格式和f l 语言；其次，分析了f o r e 的框架 设计、并发验证算法的流程、关键技术以及重要数据结构和源码；最后，给出了 两个实例对实现进行验证，并分析其优缺点。 第五章，结论与展望。 这一章对本文的主要研究工作进行了系统的总结，同时描述了并发的广义符号 轨迹赋值的不足和进一步研究的方向。 9 电子科技大学硕士学位论文 2 1 电路模型 第二章广义符号轨迹赋值 本节将介绍两种形式的电路模型。第一种电路模型是电路网表，它是对电路的 门级描述，一般直接被模拟工具使用。第二种电路模型是k r i p k e 结构，它是一个 更加抽象的模型，对推理验证非常有用。在这里，电路模型是同步的，它在某一 时间的输出是当前状态节点的状态与当前电路输入节点输入的函数，它们称为反 应式的系统。模型中的每一个状态表示实际物理电路的一个特定的稳定的电压配 置状态。布尔值表示电路的在某一个节点的电压值，高电平表示为l ，低电平表示 为0 。 2 1 1 网表 电路网表模型是各种逻辑门和状态门以及它们之间的连线的集合，主要用于基 于门级模拟的验证，例如，广义符号轨迹赋值。每一个门用一个相应的布尔函数 来表示，这个函数的输出将根据其输入变化而变化，这些门被允许共享的数量有 限的连线连接。这些连线属于电路节点的集合。 b = a d 口 c = b d = 1 口 电路网表电路图 图2 - 1 电路网表及电路图 如图2 - 1 所示，一个电路网表以及相应的电路图。该电路的节点被标为口，b ， c 和d 。每个节点的激励函数被表示为布尔表达式，其中b 表示b 节点的前一个状 态的值，时延单元( 锁存器) 在电路图中被表示为一个长方形，它的输入b 始终与 其输出的前一个状态值c 相对应。节点口为电路的输入节点，它没有激励函数。 与形式验证中典型的模型如状态转换图和自动机相比，由于电路网表按照物 1 0 第二章广义符号轨迹赋值 理电路拓扑逻辑布局及其功能编码，所以电路网表具有更好的结构性。按照如图 2 1 所示的这种方式，电路网表表示的电路模型是系统的乘积，每个系统表示一个 门的模型，用一个赋值表达式来表示。使用这种方法表示的好处有两个，一是电 路的不同部分能够被独立的分析和模拟；二是能够使模型的表示保持简洁。 2 1 2k rip k e 结构 虽然电路网表的这种电路模型被基于模拟的技术直接使用，但是由于在电路 抽象推理中，电路的性质主要依赖于电路的功能而不是它的拓扑逻辑布局，所以 电路网表并不适合用于与电路模拟相关技术的推理，而另一种更加抽象的模型用 来推理这种技术则非常有用，这种电路模型就是k r i p k e 结构【l0 1 。k r i p k e 结构一种 非确定的有限状态机，它由s a u lk r i p k e 在1 9 6 3 年提出，主要用于模型检验中系统 的建模。k r i p k e 结构是一个有向图，它的节点表示系统的可达状态，有向边表示 状态的转移关系。k r i p k e 结构的形式定义如下： 定义2 - 1k r i p k e 结构是一个二元组k = ( s ，d ，其中： ( 1 ) s 为电路模型的有限状态集合； ( 2 ) t s s 是转换关系。 电路状态的集合s 由布尔向量s b 。组成，其中s 为电路的状态。我们用j o ) 表示节点以的值在状态s 中。转换关系丁表示电路状态间的转换关系的集合。k r i p k e 结构不像自动机，没有在状态转移上标记输入符号，其转移函数只取决于目前的 状态。在验证过程中，一个电路的k r i p k e 结构保持不变。 图2 - 2 k r i p k e 结构 如图2 2 所示为图2 1 所示网表的k r i p k e 结构，电路的状态用四位布尔向量表 示，其变量顺序为a b c d 。电路模型的有限状态集合s 为满足条件b = 口人d 和d = 1 c 电子科技大学硕士学位论文 的集合。若s ( b ) = j ( c ) ，则状态s 到s 有一条有向边，这些有向边的集合即为转换 关系r 。状态和转换关系分别为s = 0 0 0 1 ，0 0 1 0 ，1 0 1 0 ，11 0 1 ) 和 t = ( 0 0 0 1 ，0 0 0 1 ) ，( 0 0 0 1 ，11 0 1 ) ，( 0 0 1 0 ，0 0 0 1 ) ，( 0 0 1 0 ，11 0 1 ) ，( 1 0 1 0 ，0 0 0 1 ) ，( 1 0 1 0 ，11 0 1 ) ，( 11 0 1 ， 0 0 1 0 ) ，( 11 0 1 ，1 0 1 0 ) ) 。 k r i p k e 结构没有初始状态的概念，这和硬件系统的实际情况相一致，在硬件 系统中，如果不对系统的初始状态进行设置，电路开始处于何种状态我们并不知 道。这一点不同于软件系统，软件系统总是开始于一个初始配置的状态。有些硬 件组件具有“复位 功能，在这种情况下，复位后的状态可以被看作初始状态。 但是，并不是所有系统都是这样，所以“复位并不是基于符号轨迹赋值验证的 电路模型的一部分。 定义2 2 给定k r i p k e 结构k = ( s , t ) ，其后像( p o s t - i m a g e ) 函数 p o s t 置：2 s 专2 s 满足p o s t k ( 尺) = s v es3 s r ( s ，j ) 丁) 。 定义2 - 3 给定k r i p k e 结构k = ( s , t ) ，其前像( p r e i m a g e ) 函数p r e 置：2 s 2 s 满足p r e 置( r ) = s ss s r ( j ，s ) 丁 。 k r i p k e 后像函数将包含于s 的状态集合映射到它的后继状态的集合。而前向 函数则刚好相反。 在图2 2 的k r i p k e 结构表示的电路中，在满足节点b 为0 的状态的集合的后 像函数转换的结果为满足节点c = o 的所有状态的集合，即： p o s t ( 0 0 0 1 ，0 0 1 0 ，1 0 1 0 ) ) = 11 0 1 ，0 0 0 1 这个结果是和电路所表示的一致，因为一个锁存器分割了b 和c 两个节点。 定义2 - 4k r i p k e 结构的迹是一个非空有穷状态序列盯s + ，对所有的吒满足 ( 仃，盯) t ，其中0 0 0 图2 - 9 断言图 2 3 2 验证算法 为了比较清晰简单的介绍s t e 验证算法，下面用断言图来取代s t e 的断言语 言。断言图是广义符号轨迹赋值的性质描述语言，它是由s t e 的断言发展而来的。 一个s t e 断言如果用断言图来描述，则该断言图的每个顶点没有分支和循环。此 时，断言图演变为一条简单的直线段，其由若干小线段组成，每个小线段代表一 个时间段。每一个小线段上标签了该时间段的前序条件和后序结论，形式如图2 1 0 所示。 。 ( a o c o ) ( a l c 1 ) ( a t - 1 c k ) a - - - - ，嘞- - - - - i _ o - - - 嘲 q o q lq 2q k 1 图2 1 0s t e 断言图 符号轨迹赋值的基于断言图的验证算法【3 4 1 分为三个部分：一、提取断言图中 的断言，并初始化模拟过程；二、基于该结构的内部模拟。三、判定结论断言是 1 7 电子科技大学硕士学位论文 否满足。如图2 - 11 所示。算法中的p o s t 为电路模型k r i p k e 结构的后像函数。s i m 为模拟关系，是边到状态集合的映射，利用它可以计算每一步模拟的结果。 图2 1 l 基于断言图的s t e 验证算法 利用上述算法考虑验证如下的s t e 断言： 彳1 & n ( a 2 ) & & 膏( 彳i ) - - - - c l n ( c 2 ) & & 2 ( c 七) 首先，将该断言转换成断言图的形式，如图2 1 0 所示。其次，上述算法的验 证过程分为两个阶段：模拟阶段和验证阶段。模拟阶段是指由从初始边到边 ( g ，g 。) 的初始路径的前序词序列驱动的向前模拟的过程，路径上每一条边的模 拟的结果产生于其相应的边的模拟的每一步。例如：在初始边( v ，1 ，。) 上，s ，= a ， 是模拟的第一步产生的状态集合；而( 1 ，1 ，。) 的下一条边( 1 ，。，v ：) 上的 s 2 = p o s t ( s 1 ) n 彳2 则产生于模拟的第二步。状态集合序列 s 1 ，