（计算机应用技术专业论文）针对gste的电路模型抽取.pdf

i-。一 “o ! 、 j 的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或 扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后应遵守此规定) 签名：么堑盔导师签名：j 垒! 习赴 日期：妒f 、年f 月 斗日 设计与芯片制造的严重脱节。阻碍芯片设计发展的一个重要因素便是如何验证芯 片设计的正确性。传统的模拟验证已经难以满足芯片设计的要求。而形式化验证 方法因其是基于严格的数学方法来确保芯片设计的正确性，因此已经在芯片设计 领域受到越来越多的重视。实现形式化验证的理论并形成相关验证工具软件的一 个关键点就是电路模型的抽取和仿真。 本论文首先研究和学习了形式化验证的相关理论知识，包括该理论的主要分 支，发展情况。并对目前形式化验证领域的主流算法g s t e 进行了深入学习和研 究，并对比了该算法与传统算法的不同。 其次对当前学术界以及工业界的一些常用工具s m v , v i s ，f o r t e 等进行研究 和源码剖析。并对当前电路设计语言v e r i l o g 进行学习研究后，在基于以上工具 所提供的电路描述语言的基础上简化v e r i l o g 。设计了一套针对g s t e 算法的验 证工具的电路描述语言的语法和语义。然后让软件能够方便的对电路进行描述并 对电路模型进行抽取。最后设计了系统的框架以及技术路线。 然后，研究了电路设计前端语言描述与数字电路形式化验证算法的结合点。 分析了电路模型在计算机内存中表示的相关数据结构。研究了如何将一个用语言 描述的电路抽取为适合采用g s t e 算法来进行验证的电路模型，使得g s t e 算法 能够应用在实际的电路设计领域。使用编译工具l e x ，y a c c 实现了本软件的电路 输入前端，在对语法树进行语义推理后产生了电路模型的二叉判定图数据结构后， 交由后端g s t e 验证算法进行电路模型的形式化验证。本论文在对数字电路仿真 进行了相关研究后，基于抽取的电路模型，实现对该电路模型的仿真，能够得到 相应的波形图，从来能方便的对g s t e 算法进行演示。 最后对全文进行了系统全面的概括总结，并指出了本文所设计工具的不足以 及下一步的改进方向，并展望了形式化验证算法在电路设计领域的良好应用前景。 关键词：形式化验证，g s t e ，电路模型抽取，电路模型仿真，v e r i l o g t h ed e v e l o p m e n to fa l li m p o r t a n tf a c t o ri ni cc h i pd e s i g na n dc h i pm a n u f a c t u r i n gi sa s e r i o u sd i s c o n n e c t h i n d e rt h ed e v e l o p m e n to fc h i pd e s i g ni sa l li m p o r t a n tf a c t o ri nh o w t ov e r i f yt h ec o r r e c t n e s so fc h i pd e s i g n t r a d i t i o n a la n a l o gc h i pd e s i g nv e r i f i c a t i o nh a s b e e nd i f f i c u l tt om e e tt h er e q u i r e m e n t so ft h ef o r m a lv e r i f i c a t i o nm e t h o di sb a s e do ni t s r i g o r o u sm a t h e m a t i c a lm e t h o d st oe n s u r et h ec o r r e c t n e s so fc h i pd e s i g n ，s ot h ef i e l do f c h i pd e s i g nh a sb e e nm o r ea n dm o r ea t t e n t i o n t oa c h i e v et h ef o r m a t i o no ff o r m a l v e r i f i c a t i o no ft h et h e o r ya n dt o o l sr e l a t e dt ov a l i d a t i o ni sak e yp o i n ti st h ec i r c u i t m o d e le x t r a c t i o na n ds i m u l a t i o n i nt h i sp a p e r , f i r s to fa l lr e s e a r c ha n ds t u d yo ft h ef o r m a lv e r i f i c a t i o no ft h er e l e v a n t t h e o r e t i c a lk n o w l e d g e ，i n c l u d i n gt h et h e o r yo ft h em a i nb r a n c ho fd e v e l o p m e n t a n di s c u r r e n t l yt h em a i n s t r e a mo f t h ef i e l do ff o r m a lv e r i f i c a t i o na l g o r i t h m sg s t ec o n d u c t e d i n - d e p t hs t u d ya n dr e s e a r c h ，a n dc o m p a r e dt h ea l g o r i t h mw i t ht h et r a d i t i o n a la l g o r i t h m s d i f f e r e n t s e c o n d ，p a i r so fd i g i t a lc i r c u i t sa n dd i g i t a lc i r c u i td e s i g nm e t h o dr e l a t e dt o a s u m m a r ys t u d yo fd i g i t a lc i r c u i td e s i g nf r o n t - e n dc i r c u i td e s c r i p t i o na n dd i g i t a lc i r c u i t s f o r m a lv e r i f i c a t i o na l g o r i t h mp o i n t a n a l y s i so fh o wt h ec i r c u i tm o d e le x p r e s s e di nt h e c o m p u t e rm e m o r y , d a t as t r u c t u r e ，a n ds t u d i e dh o wt ou s el a n g u a g et od e s c r i b ea c i r c u i t e x t r a c t i o na l g o r i t h ms u i t a b l ef o ru s eg s t et ov e r i f yt h ec i r c u i tm o d e l ，a l l o w i n gg s t e a l g o r i t h mc a l lb ea p p l i e dt op r a c t i c a lc i r c u i td e s i g nz o n e t h i r d l y , i nt h ec u r r e n ta c a d e m i ca n di n d u s t r i a lc i r c l e ss o m ec o m m o nt o o l ss m v , v i s ， f o r t ea n do t h e rr e s e a r c ha n ds o u r c ea n a l y s i s ，a n dt h ec u r r e n tc i r c u i td e s i g nl a n g u a g e v b ri i ，o gl e a r n i n gs t u d i e s ，i nv i e w o ft h ea b o v et o o l so f f e r e db yt h ec i r c u i td e s c r i p t i o n i i l a n g u a g es u m m a r i z e do l lt h eb a s i so fg r a m m a t i c a ls i m p l i f i c a t i o nv e r i l o gp r o d u c e da s e to fa l g o r i t h m sf o rv e r i f i c a t i o nt o o l sg s t ec i r c u i td e s c r i p t i o nl a n g u a g es y n t a xa n d s e m a n t i c s ，s ot h a ti tc o u l de a s i l yd e s c r i b et h ec i r c u i ta n dt h ec i r c u i tm o d e le x t r a c t i o n u s i n gt h ec o m p i l a t i o nt o o l sl e x ，y a c ci m p l e m e n t st h ec i r c u i to ft h i ss o f t w a r ee n t e r t h ef r o n te n d ，i nt h es y n t a xt r e eg e n e r a t e df r o ms e m a n t i cr e a s o n i n g ，t h ec i r c u i tm o d e lo f t h ed a t as h l l c t l l r eb i n a r yd e c i s i o nd i a g r a mb yt h eb a c k - e n da u t h e n t i c a t i o na l g o r i t h m g s t ef o r m a lv 舐f i c a t i o no ft h ec i r c u i tm o d e l i no r d e rt ov i s u a lo b s e r v a t i o n so ft h e c i r c u i td e s c r i p t i o nl a n g u a g ed e s c r i b e st h ec i r c u i tb e h a v i o r , t h i sp a p e ri nt h ed i g i t a l c i r c u i ts i m u l a t i o nc a r r i e do u tr e l e v a n ts t u d i e s ，b a s e do nt h ee x t r a c t i o no ft h ec i r c u i t m o d e l ，r e a l i z a t i o no ft h ec i r c u i tm o d e lo ft h es i m u l a t i o n ，t h ec o r r e s p o n d i n gw a v e f o r m s c a nb e ，n e v e rb ea b l et oc o n v e n i e n tp r e s e n t a t i o no ft h eg s t e a l g o r i t h m f i n a l l y , t h ep a p e rc o n d u c t e das y s t e m a t i ca n dc o m p r e h e n s i v es u m m a r yo fc o n c l u s i o n a n dp o i n t e do u tt h el a c ko fd e s i g nt o o l si nt h i s a r t i c l e ，a sw e l la st h en e x ts t e pt o i m p r o v et h ed i r e c t i o na n dl o o k sf o r w a r dt ot h ef o r m a lv e r i f i c a t i o na l g o r i t h mi nt h ef i e l d o fc i r c u i td e s i g nag o o da p p l i c a t i o np r o s p e c t s 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 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 ，m o d e l a b s t r a c t ，s i m u l a t i o n 1 1 i 目录 j 第一章绪论1 1 1 引言1 1 2 研究背景与意义2 1 1 1 研究背景2 1 1 2 研究意义3 1 3 主要研究内容4 1 4 章节安排5 第二章验证概念与方法介绍7 2 1 模型检测介绍7 2 1 1 模型检测系统模型8 2 1 2 模型检测验证规范8 2 1 2 模型检测算法介绍1 1 2 1 4 模型检测总结1 2 2 2 符号轨迹赋值算法( s t e ) 介绍1 2 2 2 1s t e 系统模型13 2 2 2s t e 系统性质描述1 3 2 2 2s t e 算法流程简介15 2 2 4s t e 算法总结15 2 3 广义符号轨迹赋值算法( g s t e ) 介绍1 6 2 3 1g s t e 系统模型16 2 3 1g s t e 性质描述1 7 2 3 3g s t e 算法介绍1 9 2 3 4g s t e 算法总结2 2 2 4 本章小结2 3 i v 目录 第三章软件总体框架以及描述语言设计2 4 3 1 现有验证工具比较一2 4 3 1 1 验证工具s m v 2 4 3 1 2 验证工具v i s 2 6 3 1 3 验证工具c o s p a n 2 9 3 1 4 验证工具f o r t e 31 3 2 电路描述语言以及性质描述语言设计3 2 3 2 1 电路描述语言v e r i l o g 介绍。3 2 3 2 2 电路建模语言设计3 5 3 2 3 电路性质描述语言设计3 7 3 3 验证工具框架设计3 9 3 4 技术路线和方案4 0 3 5 本章小结4 1 第四章电路模型抽取与仿真的实现4 2 4 1 电路模型介绍4 2 4 1 1 方程表示法4 2 4 1 2 自动机表示法。4 3 4 1 3 网表表示法4 4 4 2 二叉判定图介绍及电路模型的表示。4 6 4 2 1b d d 介绍4 6 4 2 2 电路模型的b d d 表示4 9 4 3l e x 和y a c c 介绍及电路模型抽取前端实现5 2 4 3 1l e x 呢y a c c 介绍5 2 4 3 2 电路模型抽取前端实现5 6 4 4 电路模型抽取算法及实现5 7 4 5 仿真算法及实现6 3 4 6 实现结果一6 6 4 7 本章小结6 8 v 目录 第五章总结与展望6 9 5 1 本文总结6 9 5 1 1 主要研究成果和创新点6 9 5 1 2 存在的不足7 0 5 乒下一步工作的展望和设想7 0 致谢7 2 参考文献7 3 个人简历及硕士期间取得的学术成果7 7 v i i 第一章绪论 1 1 引言 第一章绪论 集成电路在人类的现代文明中发挥了巨大的推动作用，带领人类进入了电气 文明时代。历史上的第一块集成电路芯片是t i 公司的j a c kk i l b y 于1 9 5 8 年设计成 产，该芯片在4 平方毫米的面积上集成了大概二十多个元器件。在其后的发展中， 集成电路芯片面积越来越小，而在单位面积上集成的元器件数量却越来越多。在 1 9 6 5 年，i n t e l 公司的摩尔曾预言集成电路芯片上的元器件数量将每年增加一倍， 在1 9 7 5 年他更正为集成电路上的芯片数量每两年将增加一倍，这就是著名的摩尔 定理【1 1 。摩尔定理较为准确的预言了集成电路的发展。目前的超大规模集成电路芯 片上已经集成了大概1 0 ，0 0 0 0 个等效门，现今最先进的工艺水平所生产的芯片上集 成的元器件数量已经达到8 0 多亿个。如今，基于集成电路的产品已经广泛的应用 在人们的社会生产生活中，家电、汽车、工业机器人、手机、物联网、l e d 等各 种设备都离不开集成电路芯片。集成电路芯片已经渗入到社会经济生活的方方面 面，并带来了巨大的经济效益。据统计，在2 0 0 5 年全世界集成电路产业所带来的 经济效益达到了2 3 5 0 多亿美元。据经济学家预计，到2 0 1 0 年全球集成电路产业 规模将达到大概4 3 0 0 亿美元。我国的集成电路起源于六十年代，最近几年发展十 分迅猛，在世界集成电路市场中占据举足轻重的地位。2 0 1 0 年中国半导体产业所 产生的经济效益将超过8 0 0 亿美元，年增长率将达到1 8 左右。如今我国已经有 集成电路相关企业6 0 0 多家，其中设计企业已经达到4 0 0 多家。 随着集成电路集成度的大幅提高，如何保障芯片设计的正确性已经成了限制 集成电路芯片设计的一个主要因素。因此，一般芯片设计企业都极为重视芯片的 测试与验证工作。在一般的芯片设计项目中，参与项目的验证人员的数量要多于 芯片设计人员。对于复杂的芯片设计项目，验证人员与设计人员的比例更是达到 2 ：1 甚至3 ：1 的比率。芯片验证所花费的的时间占整个项目周期的5 0 一8 0 。传 统的芯片验证方法，是采用测试向量进行输入，然后通过对比测试所得的结果与 预期结果来查看原有设计是否正确【l 捌。由于可能的输入太多，比如一个3 2 位的电 路就有2 3 2 次方种输入可能，因此测试用例无法覆盖整个测试空间。模拟测试的最 电子科技大学硕士学位论文 大缺陷在于必须精心挑选测试用例以便达到设计代码的所有分支。但实际上是很 难达到的，而一旦出现测试用例没有覆盖到的地方造成芯片流片后错误被发现， 将造成巨大的经济损失。1 9 9 4 年i e t e l 公司推出的第一款奔腾芯片出现了浮点数 除法错误，导致该公司大量召回该款芯片，造成了数亿美元的损失。由于模拟向 量测试法的不完全可靠性，使人们逐渐重视依靠数学推理来严格保证设计正确性 的形式化方法。 1 2 研究背景与意义 1 1 1 研究背景 形式化验证是对当前的i c 设计领域的研究中的一个热门也是前沿的研究方 向。2 0 0 7 年的图灵奖即授予了为形式化验证理论和实践做出了巨大贡献的e d m u n d m c l a r k 、e a l i e ne m e r s o n 和j o s e p hs i f a k i s 。 形式化验证的研究是伴随自动机，形式语言等理论的研究一起发展起来的。 在二十世纪六十年代，计算机科学家为了对软件进行规范描述以及如何确保正确 产生了兴趣，并进行了研究。在二十世纪七十年代，围绕着对科学计算中对翻译 程序的需要，产生了定理证明技术。二十世纪八十年代，随着p n u e l i 将时态逻辑 应用到交互式程序的验证，形式化验证有了很大的进展。1 9 8 1 年，c m u 的e d m u n d m c l a r k 提出了模型检测技术并由m c m i l l a n 实现了基于该理论的形式化验证自动 工具s m v ，很大的推动了形式化验证技术的发展【5 】。但初期的模型检测只适用于 小规模的电路验证，当电路规模变大后存储空间会爆炸性增长。八十年代后期， 随着符号模型检测的提出以及二叉判定图等数据结构的应用，极大的提高验证系 统的规模，模型检测在硬件设计中产生了巨大的成功。但是当面对大型复杂的系 统设计时，传统的模型检测仍然有很大的局限性。在九十年代，i n t e l 公司的工 程师b r y a n t 等人试图将传统的模拟检测方法与模型检测理论相结合，并成功的提 出了符号轨迹赋值( s t e ) 算法。该算法成功的解决了i n t e l 公司设计的芯片设计中 的浮点数溢出错误，并被i n t e l 、m m 、m o t o r o l a 等公司采用。虽然符号轨迹 赋值算法功能强大，但由于其性质描述语言的局限性限制了它的应用范围。九十 年代中期，i n t e l 工程师j i ny a n g 等人对s t e 算法进行了扩展提出了广义的符号 根轨迹赋值( g s t e ) 算法，该算法引入了新的断言图语义，大范围的扩充了算法所 能描述的电路性质，成为了未来形式化验证的新的方向。如今扩展符号轨迹赋值 算法已经受到了学术界和广泛注意【3 】。本项目得到了国家自然基金面上项目 2 第一章绪论 ( 6 0 9 7 3 0 1 6 ) 的支持。 1 1 2 研究意义 本论文的研究意义大致从广义的符号根轨迹赋值( g s t e ) 算法的学术价值、产 业价值和g s t e 算法的实际应用价值三个方面阐述。 ( 1 ) g s t e 算法的学术价值。 自二十世纪九十年代b r y a n t 等人提出符号根轨迹赋值算法( s t e ) 以来，该算 法已经成功用于大型芯片的设计验证领域。i n t e l 公司用该算法成功的找出了芯 片设计中的浮点数溢出错误并应用在有1 0 0 0 0 0 0 万个门的大规模的数据流的路径 上。m o t o r a l a 公司也曾使用该算法来验证数百万门级的存储芯片设计。但是 s t e 的缺点是其仅能验证有限时间段内的性质，而且提供的抽象手段也不够，因 此在实际应用中有一定的局限。广义符号根轨迹赋值算法( g s t e ) 对s t e 算法进 行了扩展，引入了新的电路性质描述语言，使得对电路性质的描述可以扩充到无 限时间域。并且从传统性质的可满足性扩展到了一致性满足。g s t e 提供了高度抽 象的手段，使得实际应用中可以节约大量内存，进一步减轻了内存爆炸问题从而 可以应用在规模更大的电路验证中【4 ，5 1 。g s t e 算法发展历史还比较短，对该算法 的研究还有很多工作需要做，比如高度抽象带来的错误路径的伪报错问题等。因 此对g s t e 算法的研究和工程化具有极高的学术价值。 ( 2 ) g s t e 算法的产业价值。 i c 产业在今天的全球经济中已经占据了十分重要的地位。在2 0 0 5 年全世界 集成电路产业所带来的经济效益达到了2 3 0 0 多亿美元。据经济学家预计，到2 0 1 0 年全球集成电路产业规模将达到大概4 0 0 0 多亿美元。我国的集成电路产业的发展 也是十分的迅猛。在世界i c 市场中占据了举足轻重的地位。2 0 1 0 年中国半导体产 业所产生的经济效益将超过8 0 0 亿美元，年增长率将达到18 左右。如今我国已 经有i c 相关企业五百多家，其中设计企业已经达到三百多家。在集成电路的设计 中，验证人员的数量在整个开发中所占的数量最多，耗费的资源也较大，大概要 占整个项目额度的三分之一左右。对于验证的软件工具各个集成电路设计企业都 有很大的需求。但是目前c a d e n c e ，s y n o p s y s 等公司的自动验证工具都是数十 万美元一套，其使用成本过于庞大。在我国，形式化验证也是出于刚刚起步的阶 段，在学术研究以及产业化方面都远远落后。在国产的验证e d a 工具中，暂时还 没有能进入商业领域的产品。因此，如果能将对g s t e 算法的研究成果实现为e d a 工具，将带来很大的产业价值，并为我国在形式化验证工具领域的发展带来契机。 3 电子科技大学硕士学位论文 ( 3 ) g s t e 技术的实际应用价值 在s t e 算法提出后，i n t e l 公司实现了相应的工具f o r t e ，该工具实现了 基本的s t e 算法，但对g s t e 算法没有提供很好的支持。本课题要研究从电路设 计语言的输入，但电路模型的抽取，再到将电路模型交由后端核心g s t e 算法处 理的整个工具实现，以便将g s t e 技术应用到e d a 工具中。并在该工具中提供仿 真功能，使得用户可以方便的对电路设计进行模拟仿真和形式化验证。在对核心 算法的基本实现的基础上，本课题开发的软件提供了图形界面，使得本软件有较 好的用户交互性，更加利于用户操作。 1 - 3 主要研究内容 目前，形式化验证技术主要由以下几部分组成：1 刻画电路模型的方式。2 验 证算法。3 描述性质的方式。验证软件的一般操作流程为输入电路模型，输入电路 性质，电路模型的抽取和数据结构的建立，电路性质的抽取以及数据结构的建立， 核心算法的运行以及查找错误路径并反馈，仿真波形的演示等几部分。 本课题主要研究：针对g s t e 算法，参考v e r i l o g 以及其他验证工具的等模 型描述方式设计本软件所使用的电路描述语言和性质描述语言。对电路进行模型 抽取，以便后端g s t e 核心算法对电路模型进行运算，并进行仿真。主要包括以 下三个方面的内容： 首先，针对g s t e 验证平台设计整个软件的实现框架， 主要包括：模型描述输入部分，性质描述输入部分，模型的抽取，性质的提 取，g s t e 算法运行，查找错误路径并显示以及仿真的展示。该框架各个部分的关 系如下图所示： 图1 - ig s t e 验证系统 4 第一章绪论 其次：对如何在计算机中表示电路模型进行了研究，并对该模型的表示方法 进行了实现。 第三，参考v e r i l o g 以及其他验证工具的描述语言，针对本软件的特点设计 电路描述语言的语法，并设计断言图的输入形式。定义了电路描述语言以及断言 图语言的语法树结构以及语义。 第四，针对设计的电路描述语言设计编译器，利用l e x ，y a c c 实现该编译程 序。在编译后所得的语法树上进行遍历以及推导，以提取电路模型的数据结构以 及断言图的数据结构。将这些数据结构提交后台的g s t e 算法进行相应的验证操 作。 第五，对提取的电路模型进行仿真。利用抽取模型所得到的描述方程，以及 提供的输入部分，保存寄存器的相关状态，不断代入输入的值来更新方程的值。 得到当前的电路状态并给出相应的仿真波形。 1 4 章节安排 全文共分五章。前两章主要介绍了本课题的理论发展、选题依据及形式化验 证技术的研究和学习，第三章和第四章是本论文的重点，主要介绍了课题实现框 架和具体细节。具体的章节安排如下： 第一章，绪论。 主要介绍了形式化验证的发展历史，发展现状，产业状况，研究意义以及本 论文的研究内容和章节安排。 第二章，验证概念与方法介绍。 主要介绍了验证的基本概念以及基本的验证方法。介绍了形式化验证中的经 典的三个方法。首先，详细的介绍了模型检测的基本概念、算法流程、以及其优 缺点。其次，介绍了根轨迹符号赋值算法的基本概念和流程，以及该算法的优点 和不足。最后，介绍了广义符号根轨迹赋值算法的概念以及算法细节，比较了三 者之间的差异，以及各个算法优点和缺点。 第三章，软件总体框架以及描述语言设计。 对当前学术界所实现的几款验证软件如s m v , v i s ，f o r t e ，c o s p a n 进行了介 绍和对比。参考v r i l o g 以及上述几款验证工具的描述语言设计了针对g s t e 算 法的电路描述语言的语法形式以及语义。并参考这些软件对g s t e 验证平台进行 了总体框架设计，分析了本软件的技术路线和方案，为软件的具体实现打下了很 5 电子科技大学硕士学位论文 好的基础。 第四章，电路模型抽取与仿真的实现。 详细介绍了电路模型的相关概念，以及该模型在内存中实现的数据结构二叉 判定图。介绍了为实现对电路模型的抽取所需要的编译器实现工具l e x ，y a c c 。 详细介绍了如何在编译所得的语法树的基础上，对语法树节点进行语义判推理得 到电路模型的数据结构。最后描述了如何对抽取得到的电路模型进行仿真并到相 应的波形数据。第三章和第四章是本论文的研究重点。 第五章，结论与展望 对本论文进行了全面的总结，指出了当前实现的不足以及接下来的改进方向， 并展望了形式化验证在各个领域的广泛应用。 6 第二章验证概念与方法介绍 第二章验证概念与方法介绍 形式化验证技术起源于二十世纪六十年代并成熟于二十世纪八十年代。该技 术利用了严格的数学推理和证明方法来判断实现是是否满足规范，具有完备性。 形式化技术被用在各个领域。在电路设计领域，形式化验证得到了成熟的应用。 目前，在实际工程领域应用较广的验证技术包括模型检测技术、符号根轨迹赋值 技术以及广义符号根轨迹赋值技术。本章将分别对以上三种验证技术进行详细的 介绍。 2 1 模型检测介绍 二十世纪八十年代初，美国的c l a r k e 和e m e r s o n 提出了模型检测( m o d e l c h e c k ) 技术。b r y a n t 在二十世纪八十年代中期改进b d d ( b i n a r y d e c i s i o nd i a g r a m ) 。 将b d d 进行了化简、统一，成为了表达布尔公式的有效方法。1 9 8 7 年，m c m i l l a n 将模型检测理论引入工程实践，成功的实现了第一款模型检测自动验证软件s m v ， 使得模型检测技术逐渐的进入了实践。模型检测技术主要由以下三个部分组成【5 j ： 对于系统模型的描述，一般而言，对于系统的描述都是通过某种描述语言 实现的。 对于系统要被验证的性质的描述。 验证方法，用于证明系统模型是否符合性质规范。 系统模型可由m 表示，规范用公式q 表示，验证方法用于计算m 是否满足q ， 即ml = q ，模型检测的框架有由下图表示： 图2 - 1 模型检测框架 7， 电子科技大学硕士学位论文 2 1 1 模型检测系统模型 在模型检测里面，系统模型m 是一种被称为迁移系统的模型【6 1 ，该模型可用 一个三元组表示 1 4 , 1 5 】：m = ( s ，哼，l ) 其中： 1 s 是有限状态集 2 专蹀上的迁移关系 3 l ：s 寸2 肚是一组标记函数，即该状态满足的性质 在模型检测里面，是需要初始状态集合s o 的。集合r 描述了系统状态之间的 转移关系。l 表示每个状态所满足的条件。以下图为例： 图2 - 2 系统模型例子 考虑图2 2 的系统模型，可知其定义如下： d e f s = ( s o ，s 1 ，s 2 d e f - - 9 = ( s 0 ，s 1 ) ，( s 1 ，s 2 ) ，( s 2 ，s o ) ，( s 2 ，s 2 ) ) d f _ f l ( s o ) = x o ) d e f l ( s 1 ) = 仁1 ) d e f 三( j 2 ) = x o ，x l 其中，x l ，x 2 是原子公式。由以上关系我们可以得知该系统具有三个状态： s 0 ，s 1 ，s 2 。在s o 状态下，原子公式x 0 为真，x 1 为假。在s 1 状态下，原子公式 x 1 为真，x 0 为假。在s 2 状态下，原子公式x 0 ，x 1 都为假。该系统具有迁移关系： s o 专s 1 ，s l 哼s 2 ，s 2 专s 0 ，s 2 专s 2 2 1 2 模型检测验证规范 验证规范是用于描述期望系统所具有的性质。在模型检测中，验证规范是用 8 第二章验证概念与方法介绍 时态逻辑来描述的。在传统的命题逻辑和谓词逻辑中，公式的真假是静态的，要 么在所有状态所有路径下为真要么在所有情况下为假【8 一。与传统的逻辑公式不同 的是，时态逻辑是动态的，即一个公式有可能在某些状态下为真也有可能在某些 状态非真。公式的真假可以随着状态的不同而改变其值。时代逻辑主要由线性时 代逻辑l t l 和分支时代逻辑组成。以下将分别对两种逻辑进行介绍。 ( 1 ) 线性时态逻辑l t l ( l i n e a r - t i m et e m p o r a ll o g i c ) 线性时序逻辑表达的是一个时间路径，可以无限延伸到未来的时间点。l t l 的表达语法如下1 6 , 1 7 ： 定义2 1 ：l t l 语法 ：tl 刈pi ( 1 矽) l ( 人矽) i ( v 矽) i ( 矽争) l ( j 矽) i ( ，矽) i ( g ) i ( 己矽) i ( 乃矽) i ( 庐r ) 其中t ，上，p 是公式中的原子，x ，f ，g ，u ，w ，r 是时态连接词。x 指的是 下一个状态。f 值得是未来的某个状态。g 指的是未来的所有状态。u 指的是指导 某个状态为止。r ，w 分别指“释放”和“弱直到”。以下是两个l t l 公式的例子： ( ( ( 印) a ( g g ) ) _ ( p 腑) ) 伊( pj ( g ，) ) v ( ( 1 9 ) 己) ) 用l t l 可以方便的描述系统迁移模型的性质： 定义2 2 ：设m = ( s ，寸，三) 是一个系统的迁移模型，艽= s l 寸是m 中的一条 路径，矽是一个l t l 公式，该路径是否满足一个l t l 公式由l _ 表示，其中i _ 的定义 如下： 1 尢i - t ，即一条路径用于满足l 2 尢l “，即一条路径永不满足上 3 艽i _ p ，当且仅勘三( j ) ，即在该状态下p 为真 4 艽l = 1 ，当且仅当艽| 5 茏| - 1a 矽2 ，当且仅当氕f = l 且茺| _ 矽2 6 茏i = 矽1 v 矽2 ，当且仅当茏l - 矽1 或艽l _ 矽2 7 艽l _ i 6 1 专2 ，当且仅当只要艽i _ 1 就有尢! = 矽2 8 茏| _ 删当且仅当尢2i - 矽，其中艽2 指的是当前状态下一个状态开始的路径。 9 艽i - g 矽当且仅当对所有f 1 ，艽i l o 茺l _ 尉当且仅当存某个在i 1 ；使得艽l - 矽 i i 艽 矽唧当且仅当存在某个i 1 ，使得尢i - 讲且对所有吻= 1 ，i - i 有茏l = 1 2 尢i 脚当且仅当存在某个f 1 ；使得尢t = - 俎对所有的f = l ，尢7i = 矽 9 电子科技大学硕士学位论文 或者对所有k 1 ，有艽。| _ 1 3 艽i - 织缈当且仅当或者存在某个f 1 ；使得艽l = 殂对所有的扛1 ， 有艽i _ p ；或者对所有的k 1 ，有茏。 伊 l t l 可以描述的性质范围比较广。比如描述不管如何总会到达某种状态，这 条性质可用l t l 公式g f s t a t e 来表示。又比如描述操作系统的磁盘调度算法，当 读写第一条磁道时，一个向外移动的磁头在第二条磁道上会向同方向移动【7 】。可以 用公式g ( d i s k 2 d i r e c t i o n o u tag o t o d i s k l 专d i r e c t i o n o u t u d i s k 2 ) 来描述。但是由于 l t l 中，时间路径是线性增长不存在分叉，因此l t l 公式不能用于描述某些路径 存在性的性质。比如性质：磁头停在了第一条磁道并永远不会移动。这条性质实 质上是说从每一个路径上的状态开始，都存在一条沿着该路径可能使得磁头停留 在第一条磁道的路径。因此在时态逻辑里面又引入了计算树逻辑c t l 。 ( 2 ) 计算树逻辑c t l ( c o m p u t a t i o n t r e el o g i c ) l t l 公式默认是包括所有的分支的。因此l t l 公式很难描述类似存在性满足 的概念。c t l 公式除了具有l t l 中的时态算子u ，f ，q x 外还引入了量词a 以及e 。 其中a 表示该验证包含所有的分支，e 表示验证中是否有某条分支满足。 定义2 3 ：设m = ( s ，- - ，l ) 是一个系统的迁移模型，s s ，矽是一个c t l 公式， 该状态是否满足一个c t l 公式由l - 表示，其中i - 的定义如下： 1 m ，s i - t 且m ，s l “ 2 m ，jl = p 当且仅当p l ( s ) 3 m ，si - 1 p 当且仅当m ，si p 4 m ，jl = 1a 2 当且仅当m ，ji = 矽1 且m ，si = 矽2 5 m ，ji - 矽1 v 2 当且仅当m ，ji - l 或者m ，s | - 矽2 6 m ，si _ 矽1 专矽2 当且仅当m ，sl 1 或者m ，jl _ 2 7 m ，si _ 勋当且仅当对所有使得的s 专s l ，有m ，s li - 。于是，4 跆义为 在所有的下一个状态满足。 8 m ，jf _ e x 当r 仅当对某个使得的s - - s l ，有m ，s ll - 矽。于是彳跆义为 在某个下一个状态满足，御鸟脚寸对偶的。 9 m ，j a 0 2 当且仅当对所有满足的s l = j 的路径s l - - s 2 专，以及沿该路 径的所有s ，有m ，si - 矽。a g 意味着所有以s 开头的路径，殓局成立。 1 0 m ，si _ 弱矽当且仅当存在一条满庙l = s 的路径s l - - ) s 2 专，以及沿该 路径的所有s ，有m ，sl - 矽。e g 意味着存在一条以s 开头的路径，雄局成立。 1 1 m ，jl - a f 当r 仅当对所有满足，1 = j 的路径s l s 2 专，存在某仆f 1 0 第二章验证概念与方法介绍 使得m ，s ii m ，a 臆味着所有s 开头的路径，存在未来某个状态满足痧 1 2 m ，si _ e f # 当r 仅当存在一条满足n = s 的路径s l 专s 2 一，存在某个s i 使得m , s il _ m ，噫昧着存在一条s 开头的路径，