（计算机软件与理论专业论文）数字电路并发行为的ste验证方法.pdf

兰州大学硕士研究生毕业论文 摘要 设计验证在数字电路设计中扮演着重要的作用，功能正确性检验是设计验证 最基本的内容，用于判别设计规范和设计实现之间是否一致。在过去的二十几年 中，人们对于数字电路顺序行为的验证进行了深入的研究并提出了许多行之有效 的验证方法，例如，模拟的方法和形式化的方法等。然而数字电路是典型的并发 系统，对其并发行为的验证却由于复杂度的限制而至今没有提出任何直接的和有 效的验证方法，如何实现并发行为的有效验证就成为保证数字电路功能正确性的 关键因素。 本文在并发行为验证方面进行了探讨。首先介绍了s t e 验证方法的基本理 论和技术，对其优点和不足进行了详细的分析；其次对s t e 验证规范作了图形 化的扩展，提出了断言图的概念并给出了基于断言图的验证算法；进而引入进程 代数语言对并发系统进行刻画，建立了相应的并发模型，给出了语言到模型的转 化以及验证并发行为的流程；最后，探讨了动作细化在规范语言层次化描述中的 作用。 关键词；s t e ，断言图，进程代数，事件结构，动作细化。 兰州大学硕士研究生毕业论文 a b s t r a c t d e s i g nv e r i f i c a t i o np l a y sn l li m p o r t a n tp a r ti nt h ed e s i g np r o c e s so fd i g i t a l c i r c u i t s f u n c t i o n a lc o r r e c t n e s sv e r i f i c a t i o ni se s s e n t i a lf o rd e s i g nv e r i f i c a t i o nw h i c h i su s e dt oc h e c ko nt h ec o n f o r m a n c eb e t w e e ns p e c i f i c a t i o na n di m p l e m e n t a t i o n i nt h e p a s tt w e n t yy e a r s ，p e o p l eh a v es t u d i e de x t e n s i v e l ya n dp r o p o s e ds e v e r a le f f e c t i v e v e r i f i c a t i o nm e t h o d sf o rs e q u e n t i a lb e h a v i o r so fd i g i t a lc i r c u i t s ，s u c ha ss i m u l a t i o n m e t h o da n df o r m a lm e t h o d h o w e v e r , d i g i t a lc 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 s , d u et ot h ec o m p l e x i t yr e s e a r c h e r sh a v en o tp r o p o s e da n yd i r e c ta n de f f e c t i v em e t h o d s f o rt h ev e r i f i c a t i o no fc o n c u r r e n tb e h a v i o r s h o wt op e r f o r mt h ev e r i f i c a t i o no f c o n c u r r e n tb 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 l c i r c u i t s t h i sp a p e rd i s c u s s e ss o m ei s s u e so fv e r i f i c a t i o nf o rc o n c u r r e n tb e h a v i o r s f i r s t , i n t r o d u c et h eb a s i ct h e o r i e sa n dt e c h n i q u e so fs t ev e r i f i c a t i o nm e t h o da n de v a l u a t e i t sa d v a n t a g e sa n dw e a k n e s s e s t h e ne x t e n ds t ev e r i f i c a t i o ns p e c i f i c a t i o nu s i n g g r a p h i c a lt h e o r y ，p r o p o s et h ec o n c e p to fa s s e r t i o ng r a p ha n di m p l e m e n ta 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 l g o r i t h m f u r t h e r , i n t r o d u c ep r o c e s sa l g e b r al a n g u a g ef o r d e s c r i b i n gt h ec o n c u r r e n ts y s t e m s ，b u i l du pa s s o c i a t e dc o n c u r r e n tm o d e la n dg i v et h e t r a n s f o r m a t i o nf r o ml a n g u a g et om o d e la n dv e r i f i c a t i o np r o c e s sf o rc o n c u r r e n t s y s t e m sb e h a v i o r s a tl a s t d i s c u s s e st h ei m p o r t a n tr o l eo fa c t i o nr e f i n e m e n ti n s p e c i f i c a t i o nl a n g u a g e sh i e r a r c h i c a ld e s c r i p t i o n s k e yw o r d s ：s t e , a s s e r t i o ng r a p h , p r o c e s sa l g e b r a , e v e n ts t r u c t u r e ，a c t i o n r e f i n e m e n t 原创性声明 本人郑重声明：本人所呈交的学位论文，是在导师的指导下独立 进行研究所取得的成果。学位论文中凡引用他人已经发表或未发 表的成果、数据、观点等，均已明确注明出处。除文中已经注明 引用的内容外，不包含任何其他个人或集体已经发表或撰写过的科研 成果。对本文的研究成果做出重要贡献的个人和集体，均已在文中以 明确方式标明。 本声明的法律责任由本人承担。 论文作者签名：塑多日期：塑! 圭，型 关于学位论文使用授权的声明 本人在导师指导下所完成的论文及相关的职务作品，知识产权归 属兰州大学。本人完全了解兰州大学有关保存、使用学位论文的规定， 同意学校保存或向国家有关部门或机构送交论文的纸质版和电子版， 允许论文被查阅和借阅；本人授权兰州大学可以将本学位论文的全部 或部分内容编入有关数据库进行检索，可以采用任何复制手段保存和 汇编本学位论文。本人离校后发表、使用学位论文或与该论文直接相 关的学术论文或成果时，第一署名单位仍然为兰州大学。 保密论文在解密后应遵守此规定。 论文作者签名：塑查墨导师签名：么壬邀 对s t e 验证规范作了图形化的展开，提出了断言图的概念，给出了基于 断言图的验证算法； 引入进程代数语言描述系统的并发行为，实际上给出了并发行为描述的 语法定义；基于事件结构模型定义了进程代数中各种操作符的运算； 给出了验证并发行为的s t e 方法的流程。 探讨了动作细化在进程代数层次化描述中的作用； 文章实际上提出了数字电路中并发行为的验证框架，对指导数字电路中并发 行为的验证具有重要意义。而且由于并发性是普遍的现象，在现实生活中占有重 要的地位，验证框架的提出也为现实中的其他并发行为验证提供了参考。 1 3 本文组织 本文共分七章，下面简要介绍一下各章的内容： 第一章阐述了课题的研究背景、主要工作和组织结构； 第二章介绍了s t e 验证方法的产生背景和基本理论，分析了s t e 验证方法 的优缺点； 。 第三章对s t e 验证规范作了图形化的展开，提出了断言图的概念，并实现 了基于断言图的验证算法，目的是为后续理论研究作铺垫； 第四章给出了并发行为描述的进程代数语法，并以事件结构模型为基础定义 了各种操作符的运算，分析了进程代数语法到事件结构模型的转化过程； 第五章阐述了并发行为的验证过程，重点分析了如何从事件结构模型中获得 断言图； 2 兰州大学硕士研究生毕业论文 第六章介绍了动作细化的基本概念、讨论了三种分类方法并分析了它在系统 设计中的作用； 第七章是对论文研究工作的总结，以及对未来工作的展望。 3 兰州大学硕士研究生毕业论文 2 1 提出背景 第二章s t e 验证方法 在过去的二十几年中，验证领域无论在理论还是在实践方面都得到了极大的 发展，特别是对硬件的验证取得了更多更卓著的成就。然而验证仍然是一项复杂 而艰巨的任务，这从多种多样的验证方法和大量富有成果的研究上就能体现出 来。 硬件的验证方法大体上可以分为两类，即早期的模拟验证和后来的形式化验 证。模拟验证方法首先从设计者提供的电路描述( 通常以v h d l 文件或者v e r i l o g 文件的形式给出) 中抽象出一个电路模型，然后在这个电路模型的输入端注入测 试信号，并在其输出端观察响应结果以及与预期值进行比较闭。模拟验证方法的 电路建模能力强、运行效率高，不仅能够检验电路的逻辑正确性，而且还可以观 察逻辑动作的中间结果、查看每个单位时间内所有元件的状态。因此在过去的很 多年中甚至直到现在仍然是一种主要的验证手段。但是模拟验证方法本身具有不 完备性，即为了找出更多的设计错误通常需要选择大量的测试信号，如果测试信 号不能完全覆盖，那么许多错误就很有可能还隐藏在电路中而没有被发现。在数 字电路系统日益复杂的今天，显然要做到对所有信号的完全覆盖是非常困难的， 甚至是不可能的。因此，单纯的模拟验证方法已经无法达到人们的可靠性要求。 形式化验证方法是验证数字电路设计正确性的一条新途径。它用数学方法表 达系统的规范或系统的性质，然后利用严格的数学推理证明所涉及的系统满足系 统的规范或具有所期望的性质。在不能证明所期望性质的正确性时，则发现设计 错误【5 1 。形式化验证方法不考虑输入信号对输出信号的影响，而只关注电路本身 的结构，即对电路本身的结构进行推理，因此可以说形式化验证方法的覆盖率是 1 0 0 的。此外，由于形式化验证方法采用数学推理的方式，因此它还具有自动 分析特性。然而形式化验证方法的验证过程采用穷尽的处理方式，对于大型系统 的验证则耗时过长，因此形式化验证方法通常用于可靠性要求比较高的关键系统 的验证。 虽然对于数字电路的验证运用了模拟验证方法和形式化验证方法，但二者之 4 兰州大学硕士研究生毕业论文 间基本上保持着分工合作的关系，被用于不同的系统或者不同的验证阶段。这种 状态到了九十年代初期发生了改变。1 9 9 1 年b r y a n t 和b e a t t y 等人探索将模拟的 方法和形式化的方法结合，以此发挥两种验证方法的优点并克服其中的不足。他 们进行了最初的实验并取得了一定的成功【1 2 1 。后来经过s e g e r 和b r y a n t 等人不断 的改进和完善，1 9 9 5 年新方法最终以完整的理论形式出现并正式定名为s t e 嘲。 今天，s t e 验证方法已经是数字电路验证的最有效和最快速的验证方法，它不仅 能够完成传统的模拟验证方法可以完成的验证任务，而且尤其适合验证流水线等 数字时序电路。 s t e 验证方法作为一种先进的数字电路验证技术，从它一出现便引起了学术 界和工业界的广泛关注，目前有关它的研究仍在继续【1 3 】【1 4 1 。 2 2s t e 验证方法 s t e 验证方法大体可以分为三部分：一部分称为电路模型，展示电路的所有 可能行为；一部分称为验证规范，指明系统应该满足或者具有的性质；最后一部 分是验证器，完成指定的验证任务。图2 1 是s t e 验证方法的框图。 2 2 1 电路模型 图2 1 s t e 验证方法框图 电路模型是电路的抽象描述，是展示电路行为的载体。在s t e 验证方法中， 电路模型是一个二元组m = 【 ，y 】，其中 是完备格，表明状态空间；y 兰州大学硕士研究生毕业论文 是次态函数，具有单调性。 s t e 验证方法首先将电路节点的值域从 d ，j 扩展到 o ，j ，田，其中z 表示 一种不确定的或者未知的信息。其次在值域 d ，j ，z ) 上定义了一个偏序关系，即： 如果输入的测试向量中含有未知值z 并且通过模拟得出了二进制值( d 或j ) 的 结果，那么将输入的测试向量中的x 值替换为任意具体的二进制值时也能得出相 同的结果。通过这样的处理，s t e 验证方法用一个含有未知值工的测试向量就 可以同时表示多种不同的测试向量组合，因此用于验证的测试向量可以被显著的 约简。 由于电路在某一时刻的状态是由若干节点的取值共同决定的，因此值域的概 念被扩展。设d = d j ，册表示单个节点的取值集合，那么d 4 = la i - - d ， j 量is 所表示所有长度为肌的三值向量的集合。相应地，偏序关系也被扩展到 d “上，即a 6 当且仅当a i b l a f 墨m ) 。不过， 并不是完备格，因为任 给d 4 中的两个元素它们的最小上界都不存在。因此s t e 验证方法还引入一个特 殊的符号t 来表示这个缺失的最小上界，即c = d “u 可。 设是定义在c 上的偏序关系：( d v s c - c 都有s t ；如果s ，t 6 d m ，那么 s 墨t 当且仅当s tt 。注意量和t 被定义成两种不同的偏序关系，s 用于状态 之间的排序，而用于节点值的排序。 是一个完备格，也是一个电路模 型的偏序状态空间。图2 2 是一个反向器电路( a ) 及其状态空间( b ) 。 外 护“ro分0躺01 1 0 1 1 。 n 彦 ( a ) c o ) 图2 2 反向器电路( a ) 及其状态空间( b ) 电路模型的次态函数表达的是对电路节点在下一个时间单位内取值的约束。 由于输入节点的值是由外部环境控制的，因此电路本身不会对输入节点的值产生 任何约束。而电路的功能节点( 非输入节点) 的次态函数将是一个单调的函数l ，： 6 兰州大学硕士研究生毕业论文 c c ，其具体取值将由电路的拓扑和功能决定。图2 3 是反向器电路的次态函 数。 n d 。j d o d j 丑j z z - - x o 一j j o l x 图2 3 反向器电路的次态函数( 加o u t ) s t e 验证方法用状态序列推理电路模型的行为，然而并不是所有的状态序列 都表示了正确的模型行为，模型可接受的序列称为轨迹。 设s = s o s l e s o 是电路模型m 的任意状态序列。s = s 1 称为轨迹当且 仅当r ( s 1 ) = s “1 对于所有的f = 0 成立。从上面的描述中可以看出，次态函数y 计算得到的是系统在下一个时间单位内允许的最小指定状态，如果其他状态含有 的“信息”多于这个最小指定状态，那么它必将被系统允许。 令电路模型m 的所有轨迹的集合为工( d 。有时需要对轨迹的第一个状态做 某些限制，使其大于或等于s 中的某个元素，因此引入下面的记号： 工( m 力= s i s 工o da z j o ) 。 注意，工( 上) = 工( 加并且轨迹具有后缀封闭性( 如果s = s o s l s 2 是轨迹，那么 j = $ 1 s 2 也是轨迹) 。 2 2 2 验证规范 s t e 验证规范是形如m q 的断言，其中a 和c 是轨迹公式并分别称为前 提和结论。前提爿描述给定条件或初始状态，而结论c 描述在条件成立时希望 系统推理得到的结果。 定义2 1 ( 轨迹公式) 设p 是定义在s 上的一组简单谓词且p p ，那么轨 迹公式的语法是一个递归定义： f = pl f la f 2 l e _ ，i n f 。 如果一个轨迹公式不包含时序操作符n ，那么称这样的轨迹公式是瞬时的， 它描述系统在某一个时间点的性质。另外，轨迹公式第三条定义的“域约束”条 7 兰州大学硕士研究生毕业论文 件似乎有些奇怪，但事实上，它表示了一种有用的条件操作，即：轨迹公式f 只在条件成立( 表达式e 的值为真) 时有效。 ， 轨迹公式定义的基础是简单谓词，而简单谓词的集合是任意的，例如针对图 2 2 ( a ) 的反向器电路共有5 种简单谓词，即t r u e ，咖= 0 ，i n = j ，o u t = 0 和o u t = j 。而图2 2 ( a ) 的反向器电路的性质可以用如下的两个断言来描述： 伽= d ) j n ( o u t = j ) 和 = d 寺n ( o u t = 。 对于简单谓词，定义值是一个重要的概念，它描述了一个满足谓词的最小状 态。形式化地，p 是p 的定义值当且仅当p 0 ) = t r u e 对于所有p 主a ，4 s 成立。 相应地，以简单谓词为基础的轨迹公式也可以给出它的定义轨迹，它描述了满足 轨迹公式的最小轨迹。轨迹是一个序列，因此首先给出定义序列的概念。 定义2 2 ( 定义序列) 设f 是轨迹公式，其定义序列劝： 如果p 6 t 且p 7 为其定义值，那么西= 儿l “ 矗n f 2 = l u b ( 西l ，点f 2 ) ； 站啼，= e ? 如 如= 上儿。 在上述定义的第3 条出现了一个符号( ? ) ，它是一个中缀形式的选择函数： 删= 盅菇。 定义2 3 ( 定义轨迹) 设f 是轨迹公式，其定义轨迹毋为： 棚* i l u l u b 。l ( w t s 。 z ) 帏，。) ) ) 篡 从上述两个定义中可以得到这样的结论： 定义序列的计算仅与轨迹公式本身的描述有关，与电路的模型无关； 定义轨迹的计算是定义序列和次态函数共同作用的结果。 2 2 3 验证过程 首先给出轨迹公式的几条重要性质，它们是s t e 验证算法的基础，同时也 是保证s t e 验证方法的正确性的理论依据。 引理1 如果5 1 和5 2 是轨迹且有j l ss 2 ，那么j lh f j 2h f 。 8 兰州大学硕士研究生毕业论文 引理的证明是按照轨迹公式的层次采用归纳法完成的。感兴趣的读者可以参 看文献【6 】。这条引理说明轨迹具有单调性。 引理2 任给轨迹公式f 和它的定义序列昂，对于每一条轨迹s 都有5f - f 西互s 。 引理的证明同样请读者参看文献【6 】。这条引理的意义是：任何满足公式f 的轨迹，都必然“大于或者等于”公式f 的定义序列。因此这条引理更一般的意 义是：只要我们计算出如并且如果要测试某条轨迹是否满足公式，只要判断 该轨迹是否“大于或者等于”昂即可。 引理3 如果初始状态z lt ：z 2 ，那么任给轨迹公式，都有功乜1 ) 印。 这条引理的意义同引理l 类似，说明了定义轨迹的单调性。 引理4 设印是公式f 的定义轨迹，那么： 印工( 鸩力； 印h f ； 任给s l ( 峨力，sh f 留s 。 引理4 的第一条说明印是一条轨迹；第二条说明印是一条满足轨迹公式 f 的轨迹；第三条说明给定任何轨迹，只要它“大于或者等于”印国，它都必然 会满足轨迹公式f 。这条引理从总体上说明：对于任何轨迹公式，都存在一个 定义轨迹，并且该定义轨迹满足轨迹公式f 且最小。 根据上述引理，得到s t e 的算法流程如下： 计算函进而计算嘞； 计算昆； 比较如和锄0 ) 的大小。如果诧s 锄国成立，那么期望验证的系统行为成立。 2 3 符号处理技术 如果仅使用符号常量来描述电路的行为，将是一件复杂而繁琐的事情。例如 仅对一个简单的反向器电路就要给出两条轨迹断言( 见2 2 2 节) 。如果能用符号 变量及布尔公式表示电路的操作条件或者电路的功能，那么问题的描述将得到简 化。 9 兰州大学硕士研究生毕业论文 2 3 1 二叉判定图 二叉判定图( b i n a r yd e c i s i o nd i a g r a m j 简称b d d ) 是存储布尔公式的数据 结构，最早由i 朋于1 9 5 9 年提出1 1 5 1 。1 9 8 6 年b r y a n t 改进了b d d 的操作算法， 使得布尔公式的运算在b d d 上尤为高效【1 6 1 。 定义2 4 ( b d d ) 设五是电路节点的集合。一个b d d 是五上的有向无圈 图g = ( ke ，i n d e x ，v a l u e ) ，其中y 是两种类型顶点的集合：内部顶点v 的标记 是一个变量i n d e x ( v ) 懿, 并且每一个内部顶点都具有两个孩子节点l o w ( v ) 和 h i g h ( v ) ，其中l o w ( v ) 称为d 后继而h i g h ( p ) 称为j - 后继，相应地，边o ，l o w ( v ) ) 和o ， h i g h ( v ) ) 贝l j 分别称为d 边和j 边；终止顶点v 的标记是一个值v a l u e ( v ) e 仉j ) 并且 终止顶点没有出边。 图2 4 给出了节点集合恐上的布尔公式z l + x 2 x 3 x 1 的二叉判定图。其中内部 顶点用圆圈表示并分别标记为工l ，x 2 和x 3 ，而终止顶点用方框表示并分别标记为 0 ( 布尔公式d ) 和1 ( 布尔公式i ) 。0 - 边用虚线表示而j 边用实线表示，所有 的边都是自顶向下的指向。b d d 中根节点具有不同寻常的意义，它恰好描述了 给定的布尔公式。 图2 4 布尔公式工1 + x 蓼3 x 1 的b d d 表示 变量的排序对于b d d 来说是至关重要的，因为以不同的节点为根得到的 b d d 是不同的，因此，在构造一个布尔公式的b d d 前应该首先将变量的排序确 定下来。 定义2 5 ( 变量序) 设p _ _ p e r ( ) 是集合n 上的任意排列。排列p 在丑上 导出一个线性序( ，使得唧国t 唧o j 当且仅当it ，。线性序c 称为变量序。 确定了变量序的b d d 称为有序的( o r d e r e d ) b d d 。 定义2 6 ( 压缩的o b d d ) 一个o b d d 是压缩的( r e d u c e d ) ，当且仅当不 兰州大学硕士研究生毕业论文 存在两个不同的顶点v 1 和v 2 ，它们的顶点标记相同并且d 边和j 边的标记也相 同。 图2 5 中给定的变量序是耽 z 1x 3 x 4 ，其中( a ) 是一0 b d d 而( b ) 是相应 的r o b d d ，它们都表示了布尔公式工岱笋4 + x 2 。从例子中可以看出r o b d d 表 示的顶点数目明显比o b d d 少得多。 (a)(b) 图2 5 变量序为x 2 善1 x 3 x 4 的o b d d ( a ) 及r o b d d ( b ) 用压缩的o b d d 表示布尔公式不仅节省存储空间，而且它还是布尔公式的 一种规范形式，即一旦变量序确定下来，那么按照这个变量序所构造的r o b d d 也将被唯一的确定下来。此外，用r o b d d 还可以实现多种逻辑操作的高效计算， 感兴趣的读者可以参看文献【1 6 】。 2 3 2 三值逻辑编码 标准的b d d 仅能表示二值逻辑，而s t e 验证方法却以三值逻辑为基础，因 此，如何实现三值逻辑的编码将是首要解决的问题。 s t e 验证方法采用共轭编码( d a u l - r a i lc o d i n g ) 方式支持三值逻辑的b d d ， 即令0 = ，d ，j = ( j ，口) ，工= ( d ，d ) 。设a = ( a l ，口2 ) 和b = p l ，6 2 ) 是任意的符号变 量或布尔公式，那么基于三值逻辑b d d 的运算定义如下： aa b = ( 4 l b x ，a 2 v6 2 ) ； av b = ( 4 l vb t ，a 2 6 2 ) ； 一4 = 0 2 ，a 0 ； 1 1 兰州大学硕士研究生毕业论文 g l b ( a ，6 ) = ( a l b l ，q 2 a 6 2 ) ； l u b ( a ，b ) = ( 口l v b l ，a 2 vb 2 ) 。 经过不同的计算，一个三值逻辑的布尔公式就可以通过一对b d d 表示了二 采用符号处理技术之后，反向器电路的性质可以用下面的一条断言来描述： ( i n = 口) = = n ( o u t = 一4 ) 2 4 优点与不足 s t e 验证方法将三值建模、符号技术和时序逻辑1 1 7 】【1 8 l 融合在一起，获得了 许多优点： 首先，将电路节点的值域从 口，j ) 扩展n o ，j ，z ) 可以使模型描述更多的电路 现象。例如可以处理在正常的电路操作中由于短路而产生的非正常的电压，或者 由于竞争冒险或电路震荡而产生的中间行为。在所有这些情况下，都可以通过给： 电路节点赋值x 来表达一种不确定的信息。 其次，基于三值逻辑的偏序状态空间能够使一个模拟序列覆盖更多的操作条 件，这样用于验证的模拟序列被显著的约简，同时验证的效率也被提高。在s 髓 验证方法中，实际上仅用一条最弱的序列( 定义轨迹) 就可以完成验证任务。 再次，符号技术的应用使得验证规范的书写和电路行为的描述变得更清晰 输入节点的值不再是具体的逻辑值而可以是任意的符号表达式，因此，模拟的结 果也不再是简单的逻辑值，而是反映电路功能的布尔公式。 最后，由简单的时序逻辑组成的验证规范使得电路的验证能够以自动的方式 完成。只要给出所要设计的模型描述以及所要验证系统性质，不需要验证者与工 具进行很多交互，就可以自动的给出验证结果。 然而s t e 验证方法也有不足，即验证规范的语法仅使用了简单的操作符， 使得规范的表达能力十分有限，因此仅能对数字电路中的顺序行为进行刻画，而 无法获得并发行为的描述，从而使其验证也无法向并发行为展开。 兰州大学硕士研究生毕业论文 第三章s t e 验证规范的图形化 s t e 的验证规范采用受限的时序逻辑来描述电路的性质，即在规范中仅允许 出现布尔表达式和时序逻辑操作符n ，因此s t e 的验证规范描述的是顺序的系 统行为。本文将这种顺序的系统行为用一个带有标记的线性图表示，并称其为断 言图。 3 。1 断言图 定义3 1 ( 断言图) 断言图是一个五元组g = ( k ，e ，a n t , c o i l s ) ，其中v 是顶点的集合，v o 是初始项点，e 是有向边的集合，a n t 和c o i l s 是标记函数，分 别为每条边添加前提标记和结论标记。 图3 1 是描述反向器电路性质的断言图。图中初始顶点用双圆圈表示，前提 标记标注在边的上面，结论标记标注在边的下面，而每条边则代表了一个时间单 位。注意，并不是每一条边都有前提标记或者结论标记的，当前提或结论为t r u e 时，可以省略这样的标记。 i n = 4 o _ i k ) 们 v 0v i o u t = 1 4v 2 图3 1 反向器电路性质的断言图 为了方便算法设计，在断言图中规定：从初始顶点出发的任何路径，其前提 标记与结论标记的收集都是一条有效的s t e 断言。因此，一个电路模型满足一 个断言图，当且仅当它满足图中的所有s t e 断言。例如，从图3 1 的断言图中可 以导出两条有效的s t e 断言：脚= n ) 号t r u e 和【( i n = 4 ) n t r u e t r u e n ( o u t z - n ) 】，后者正是反向器电路性质的s t e 断言。于是得出这样的结论；断言图描 述的电路性质包含轨迹断言描述的电路性质。 3 2 基于断言图的验证算法 断言图描述的电路性质包含轨迹断言描述的电路性质，因此，一个电路模型 如果满足了断言图，那么它也必将满足标准的轨迹断言。另外，断言图还为本文 兰州大学硕士研究生毕业论文 后续的理论研究作了铺垫：在后续的研究中，将为系统的并发行为建立事件结构 模型，这个模型将以图形的方式存在，因此，需要能够在图形的基础上实现验证 的算法。因此断言图实际上是连接并发行为描述与s t e 验证方法的桥梁。 为了实现基于断言图的验证方法，算法必须完成下面的两个目标： 1 能够在断言图中提取有效的断言。并不是所有的断言都是有效的，只有 从初始顶点出发的路径才可能产生有效的断言。 2 对电路模型是否符合断言进行判定。这是标准的s t e 验证方法的功能。 算法3 1 基于断言图的验证算法。 f u n c t i o n 册( 6 3 刃始化 1 f o re a c he d g eei nt h ea s s e r t i o ng r a p hg 2 i f ei sf r o mt h ei n i t i a lv e r t e x 3 s m = a n t ；s i mp ) 保存了一条路径上的所有前提标记 4put ei n t ot h ee v e n tq u e u e ； 5 e l s e 6 s m = 彩； 执行模拟 7 w h i l et h ee v e n tq u e u ei sn o te m p t y 8 g e t a l le d g eef r o mt h eq u e u e ； 9 f o re a c hs u c o e s s o re d g ee o re 1 0 s i m 0 ) = s o n 0 ) u p o s t ( s i m 0 ) ) n a n t p ，) ； 1 1 i ft h e r ei sac h a n g ei ns i m0 ) 说明边e i 尚未处理 12put e i n t ot h ee v e n tq u e u e ； ，检验结论标记 1 3 f o r e a c he d g e e i n t h e g r a p h g 1 4 i f s i r ep ) 雪c o h $ e ) 1 5 r e t u r n ( f a l s e ) ； 1 6 r e t u r n ( t r u e ) ； 在上述算法中，p o s to 函数用来实现次态函数的功能。 1 4 兰州大学硕士研究生毕业论文 第四章基于进程代数的并发系统刻画 数字电路是典型的并发系统，它由若干功能部件组成，并通过电路板上的布 线连接在一起。虽然s t e 验证方法具有高效率和自动化特性，然而由于自身语 法的限制，s t e 验证方法只能做到对数字电路中顺序行为的描述和验证，其优越 性无法向并发行为的验证展开。 考察s t e 的验证规范，发现其语法定义的基础是简单谓词，而简单谓词则 是诸如电路节点赋值以及节点取值等的描述，如果将节点赋值、节点取值等概念 抽象，可以把它们看成是电路执行的动作。另外，时序逻辑操作符n 也可以这 样理解，即它以显示的方式将动作在时间上作了排序。如果在上一章提出的断言 图上进行考察，将会发现：抽象掉时间的概念后，系统展示的只有动作以及动作 发生的先后次序，这些动作可以看作是顺序执行的。因此，s t e 验证规范刻画的 实际上是系统执行的动作以及动作问的顺序关系。 既然s t e 的验证规范描述的是基于动作的顺序系统，那么如何基于动作描述 并发系统将是解决数字电路中并发行为验证的关键。而进程代数( p r o c e s s a l g e b r a ) 就是良好的、基于动作的且支持并发系统描述的形式刻画语言【1 9 1 。进 程代数提供丰富的操作符，通过一种组合化的方式来支持并发系统的描述，即可 以将一个大的系统分解为许多小的系统以求简化设计过程，也可以根据需要将小 的系统组合成大的系统以便观察系统的整体行为。因此，进程代数具有很大的灵 活性，是目前人们解决复杂系统描述的主要手段。 以动作为基础的进程代数能够同时完成顺序系统和并发系统的刻画，因此， 放弃s t e 验证规范的语法，用进程代数的语法替代将为并发行为的验证提供一个 全新的解决思路。 4 1 进程代数 4 1 1 进程代数简介 进程代数的研究最早可以追溯到二十世纪七十年代的早期1 2 0 l 。进程代数一词 的正式出现是在1 9 8 2 年由b e r g s t r a 和o p 提出的【2 1 1 。自1 9 8 4 年起，进程代数就被 兰州大学硕士研究生毕业论文 作为一个独立的研究领域，指用b e r g s t r a 和l ( 1 0 p 的代数方法研究并发进程【1 9 1 。然 而，现在的进程代数已经有了不同的含义。首先，进程这个词指的是系统的行为。 系统是展示行为的系统，特别是一个软件系统的执行、一个机器的动作，甚至一 个人的动作更是如此。行为是一个系统执行的动作或事件的总和，这些动作或事 件的执行可能是定时的也可能是随机的。通常为了研究需要，只考虑真实行为的 一种抽象，而不考虑其它方面；同时，常常只注意行为被观察到的结果，动作则 成为观察的单位，因此动作被考虑为离散的，即一个动作在某一时刻出现，并且 不同的动作在时间上被分离。所以，一个进程有时也被称为一个离散事件系统。 其次，代数这个词指的是用代数的或公理的方法讨论行为。综上，进程代数实际 上是用代数的方法研究系统行为。 进程代数有很多种，其中最主要的有b e r g s t r a 和k l o p 的a c p ( a l g e b r ao f c o m m u n i c a t i n gp r o c e s s e s ) 2 1 】，h o a r e 的c s p ( c o m m u n i c a t i o ns e q u e n t i a lp r o c e s s e s ) 2 2 1 ，m i l n e r 的c c s ( c a l c u l u so f c o m m u n i c a t i n gs y s t e m s ) 吲以及i s o 标准化组织 的l o t o s ( l a n g u a g eo f t e m p o r a lo r d e r i n gs p e c i f i c a t i o n s ) 洲。它们为系统行为 的描述提供了丰富的操作符。这些操作符以动作为基础，以进程为计算单位，即 可以提供顺序行为的描述，又可以提供并发行为的描述。本文将选取这些进程代 数语言的公共子集，包括前缀操作符( ) 、顺序组合操作符( ；) 、选择组合操 作符( + ) 和平行组合操作符( i i ) 。 4 1 2 进程代数的语法 在进程代数的框架下，一个系统( 通常称为一个进程) 由它所能执行的动作 组成。因此，首先假设一个可以观察到的所有动作的集合为o b s ，其中的动作用 a ，b ，c ，等小写字母来表示。另外还有一个外部不可见的动作f ( 耀o b s ) ， 用于表示系统内部执行的动作；特殊动作6 ( 6q o b s ) 是系统保留的标记，用于 表示一个进程的成功终止。令a c t 是所有动作的全集，那么a c t = o b su f ，毋。 定义4 1 ( 进程代数的语法) 设口以甜，gc _ a c t 。基本的进程代数由以下语 法产生： p = 0 i 、，i a p l p l ；易i 尸l + p 2 ip 100 1 2 进程代数的语法将进程代数看成是由进程的集合以及定义在其上的一些操 1 6 兰州大学硕士研究生毕业论文 作符构成的一个代数系统。下面是这些操作符的直观含义： o 是空进程，表示这个进程不执行任何动作； ，是终止进程，表示行为成功终止并且执行动作6 ，此后进程的行为类似 于空进程； 4 p 是动作前缀操作，表示系统先执行动作4 ，然后再执行进程p ； p 1 ；p 2 是两个进程的顺序组合操作，表示系统先执行进程p 1 ，待其成功地 结束后系统接着执行进程p 2 ； p l + 尼是两个进程的选择组合操作，其含义是系统要么执行进程p l ，要 么执行进程p 2 ，两者之间的选择是非确定的，即选择p 1 或者p 2 都有可能，具体执 行要依赖系统当时的运行环境。进程选择的非确定性是并发系统的一个重要特 性，也是区别于传统顺序系统的重要特征。 p 10g 尼是两个进程的平行组合操作，是进程代数中最重要的一个操作， 它代表了两个进程p 1 和p 2 的并发执行，其中集合g 中的动作是两个进程需要同时 执行的动作，即需要同步的动作。如果g = g ，则p l 和恐不需要同步任何动作， 此时称_ p l 与p 2 是异步并发执行的，并将0o 简记为。另外，为了书写方便，对 于只有一个元素的集合g ，将省略表示集合的花括号而直接用该元素表示集合。 如果没有用括号显式地给出操作符的优先级，则默认操作符按照以下的顺序 结合( 优先级由高到低) ：。；，+ ，0 。 4 2 并发模型的建立 进程代数是一种形式刻画语言，可以实现顺序系统和并发系统的刻画，但是 进程代数的表达式还不能直接用于系统行为的验证，因为上一章提供的基于断言 图的验证算法只能接受图形化的行为描述，因此必须首先将进程代数表达式转化 成可以计算的并发模型。本节将根据进程代数的操作符以一种组合化的方式构造 系统的并发模型。 4 2 1 事件结构模型 事件结构( e v e n ts t r u c t u r e ) 是非交织模型的一个主要分支，它最早用于连 接p e t f i 网和s c o t t 域理论【猢，后来事件结构模型被广泛地延伸和扩展，发展出很多 1 7 兰州大学硕士研究生毕业论文 分支，例如流事件结构 2 6 1 、束事件结构i 明和朴素事件结构【驾】等。 事件结构模型的基本要素有：被标记的事件以及这些事件之间的因果关系、 矛盾关系和独立关系。构成事件结构的基本单元是事件，一个事件就是一个已经 发生了的动作。对于一个动作的发生，它所发生的时间、发生的原因以及所发生 的环境可能各不相同，因此，引起的事件可能也不尽相同 定义4 2 ( 事件结构) 设4 c f 是所有动作的集合。事件结构( 在集合，重“上) 是一个四元组耶= ( e 以，f ) ，其中： e 是事件的集合； c _ e e 是一个偏序的因果关系，并满足“有限原因”规则：vg e ： d e i d e 是有限的； 撑e e 是一个反自反的、对称的矛盾关系，并满足“矛盾继承”规则： 、a 。e 。f e e ：d t ead 祷| e 特瓢 he 一彳c f 是动作标记函数。 有限原因规则说明：如果一个事件e 发生，那么引起该事件e 的原因是有限 的；矛盾继承规则说明：如果一个事件d 与某个事件e 矛盾，那么事件d 一定与 事件e 的所有因果后继矛盾。 事件结构用如下方式描述系统：动作名是系统所执行的活动，一个被动作4 ( a 邑4 c t ) 标记的事件表示动作a 的一个特定的出现，d ( e 表示d 先于日出现， d 撑e 表示在一次运行中d 和e 不会同时出现。因此，从上述定义中能够得到独 立关系c o 的定义：d e 静，( d = ev d eve ( dv d 群e ) 。很明显，独立关系是 对称的。 4 2 2 事件结构的表示 事件结构可以用图形来描述，其中事件用实心圆圈表示，旁边标注引起该事 件的动作，事件结构的因果关系用带有箭头的实线表示，矛盾关系用虚线表示， 没有标注因果关系和矛盾关系的事件之间则存在并发关系。图4 1 是事件结构基 本要素的图形化表示。 兰州大学硕士研究生毕业论文 a b c ( a ) 事件 ab p 一 ( c ) 矛盾关系 ab o ) ) 因果关系 ab ( d ) 独立关系 图4 1 事件结构的基本要素 图4 2 是一个事件结构的例子，该图形中有四个事件e 。e b e c ，印( 分别被动作 a ，b ，c ，d 标记) 。其中事件e b 和事件e 。互相独立，且是事件锄的原因，事件e 。与事 件岛矛盾，根据矛盾继承规则，事件e 。与事件e b 也矛盾。 d abc 图4 2 事件结构的例子 4 2 3 基于事件结构的操作 定义函数d s 【 ：p e s 使得每个进程都对应一个事件结构。集合a c t 是所 有可见动作与不可见动作的集合。为了叙述方便，首先给出事件结构的初始事件 和终止事件的定义。 定义4 3 ( 初始事件) 设嬲是事件结构，其初始事件是这样的集合： i n i t ( 嘲= 如e e l l o e e e ：e e ) 。 初始事件实际上是没有因果前驱的事件的集合。 定义4 4 ( 终止事件) 设嬲是事件结构，其终止事件是这样的集合： e x tc e s ) = e