（计算机软件与理论专业论文）面向ip的psl规范重用方法研究.pdf

学位论文独创性声明 本人所呈交的学位论文是我在导师的指导下进行的研究工作及 取得的研究成果。据我所知，除文中已经注明引用的内容外，本论文 不包含其他个人已经发表或撰写过的研究成果。对本文的研究做出重 要贡献的个人和集体，均已在文中作了明确说明并表示谢意。 作者签名：篮蜢垒日期：垒丑生：兰l 学位论文授权使用声明 本人完全了解华东师范大学有关保留、使用学位论文的规定，学 校有权保留学位论文并向国家主管部门或其指定机构送交论文的电 子版和纸质版。有权将学位论文用于非赢利目的的少量复制并允许论 文进入学校图书馆被查阅。有权将学位论文的内容编入有关数据库进 行检索。有权将学位论文的标题和摘要汇编出版。保密的学位论文在 解密后适用本规定。 学位论文作者签名；个恐耦砸 日期：垒! ! z ! ! ：型 导师签名。f 易 稚p 日期：趔1 ? 中文摘要 中文摘要 近十年来，i p 设计重用来已成为片上系统( s o c ) 开发领域所关注的重点，性 质或断言将被广泛采用在验证过程之中。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 设计规范变得非常有价值。 性质规范语言( p s l ) 是一种描述电路和嵌入式系统的工业标准语言，p s l 的 许多特性潜在地支持在硬件设计过程中使用基于i p 重用的方法。需要注意的是 重用不能被滥用，因为如果没有很好的组织，设计规范的层次结构会变得非常混 乱。 本文将讨论基于i p 的p s l 规范组合的方法，从三个层次来保证p s l 规范的 正确性。在最低一层，提出了一套检查性质是否正确地被a s s e r t 和a s s u m e 引导 的规则，这些规则能够检查p s l 性质是否被正确断言或是假设；在中间一层，给 出了基于i p 规范组合的语义；在最上层，本文使用i p 规范的组合语义来组织验 证单元的继承。 在上述工作的基础上，开发了基于i p 的p s l 规范重用工具i p s l ，该工具能 够让开发者将基于i p 设计的方法应用于p s l 规范设计之中，在对已有i p 进行重 用的过程中使用户缩短开发的时间。 关键词：性质规范语言，基于口的设计，语义，重用 英文摘要 a b s t r a c t r e u s eo fi pd e s i g n sh a sb e e naf e a t u r eo fs y s t g l n - o l l c h i pd e v e l o p m e n to v o rt h e l a s td e c a d e p r o p e r t i e so ra s s e r t i o n sa g eb e i n gi n c r e a s i n g l yu s e di nv e r i f i c a t i o n ，a n d t h ee s t a b l i s h m e n to fp s la sas t a n d a r dl a n g u a g ef o rp r o p e r t ys p e c i f i c a t i o ni n c r e a s e s t h ev a l u eo f w r i t i n gp r o p e r t i e sd e s i g n e df o rr o 1 s e t h ep 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 eo s l li sa l li n d u s t r ys t a n d a r dl a n g u a g ef o r c i r c u i ta n d 锄b e d d e ds y s t e md e s i g n p s lh a sm a n yf e a t u r e sp o t e n t i a lf o rd i r e c t i n g h a r d w a r ed e s i g ni nt h e p - b a s e dr e u s e b u tg a t es h o u l db et a k e nn o tt oa b u s e 咖s e w i t h o u tg o o do r g a n i z a t i o n , t h es p e c i f i c a t i o nh i e r a r c h yc a ne a s i l yg e te x t r e m e l y m e s s y i nt h i sp a p e r , w ep r o p o s e dm e t h o d sf o rc o m p o s i n gp s ls p e c i f i c a t i o nu n d e rt h e i p - b a s e da p p r o a c h - t h em e t h o d sc d s u r et h ec o r r e c t n e s so fp s ls p e c i f i c a t i o n si nt h r e e l a y e r s ，a tt h el o w e s tl a y e r , w ed e f i n e da s e to fr u l e sf o rp r i n c i p l e dc o n s t r u c t i o no f p r o p e r t i e s t h o s er u l e sc a l lc h c c kw h e t h e rp r o p e r t i e sa r ed i r e c t e dc o r r e c t l yb ya s s e r t a n da s s u l n e a tt h em i d d l el a y e r , w es t u d i e dt h es e m a n t i c so fc o m p o s i n gw - b a s e d p s ls p e c i f i c a t i o n s a tt h eh i g h e s tl a y e r , w ea p p l i e dt h es e m a n t i c sf o rs p e c i f i c a t i o n c o m p o s i t i o n t oo r g a n i z ev e r i f i c a t i o nv u n i ti n h e r i t a n c e i nt h i sp a p e r , w ed e v e l o pa ni p - b a s e dp s lr e u t o o li p s lt h ea i mo fi p s li st o h e l pu s c l sa p p l y1 1 一b a s e dd e s i g nm e t h o d o l o g yt op s ls p e c i f i c a f o m ，w h i c he n a b l e s d e v e l o p e r st or e d u c et h et i m eb yr e u s i n gp r e - e x i s t i n gi pc o 嘲 k e y w o r d ：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 ) , i p - b a s e dd e s i g n , s e m 柚f i e s ，r e u s e 2 面向口的p s l 规范重用方法研究 第一章引言 1 1 背景及意义 自从1 9 6 5 年m o o r e 提出著名的“摩尔定律”以来，世界半导体产业的发展 一直遵循着这条规律，日前一块芯片通常可容纳百万以上的晶体管门电路。从而 使得具备完整系统结构与功能的片上系统( s o c ) 有了实现的可能。s o c 技术 可将执行控制庭算或信号处理功能的处理器、存储器、周边电路及特制逻辑电 路( i n t e l l e c t u a lp r o p e r t yc o r e s ，i p 核) 整合到一块芯片中。 s o c 设计面临诸多挑战。其中m 核的复用最为关键。据d a t a q u e s t 统计， 口核已经成为一项产业，2 0 0 5 年全球s o c 设计的8 0 都是采用以口核为主而 进行设计的，坤核成为集成电路产业中增长最快的一部分。虽然口核销售额前 5 名的是a r m 、r a m b u s 、t t p c o m 、s y n o p s y s 、m i p s 等几家公司，但我们同 时注意到国内也出现了以碑核为主打产品的公司，如四川登巅微电子、芯原微 电子、苏州国芯、智芯科技以及龙芯的c p u 等，因此口重用已成为业界关注 的焦点。 口重用作为降低开发成本，缩短开发周期的一项技术，被广泛应用在电子电 路设计中，通过将已有的口集成迸系统，能够侠速开发新的功能。随着m 重用 被广大集成电路设计公司所重视，如何保证需要集成进入系统的m 能够达到设 计要求或者与已有系统兼容，在职重用时，通常要对的行为进行验证和确认， 从而保证m 本身的正确性，并且能够在系统中正确运行。因此，有必要探讨开 源口核集成的方法学，找到建立可验证口的有效手段和验证工具。 在高可信系统设计过程中。形式化规范仅仅作为功能规范的表示是不够的。 本论文中。我们拟对i p 形式化规范的演算体系及相关工具进行深入研究，它是 其他众多技术与方法得以正确并高效应用的基石。正确的m 规范重用是搭建良 好系统规范的保证。面向口的规范技术通常都支持规范的继承与集成，口规范 中既有专门描述环境行为的规范子句，又有专门描述口自身行为的规范子句。 在规范继承与集成时，规范子句的角色会随着口接口属性的变化而改变。当一 些口的接口在系统集成时变为内部变量或操作时，原先的环境行为规范子句可 能成为集成后系统的行为规范子句。 p s l 语言作为碑规范描述语言，很好地支持了口规范的重用，同时f a r k a s h s j 在p r o s y d i ”】的研究报告中指出滥用p s l 语言验证单元的继承，或未经严格组 织的规范重用会使系统规范的架构变锝极其混乱，这反而降低了规范的可信性和 可重用性。因此，我们需要对基于口的p s l 规范重用进行研究。给出p s l 规范 重用的明确语义。 4 面向口的p s l 规范重用方法研究 综上所述。展开高可信的面向i p 的演算体系研究具有现实的理论意义和应 用价值，本文将在设计规范层面上探讨基于m 的p s l 规范重用的设计方法。 1 2 国内外研究现状 i ) p 核标准 上世纪9 0 年代初，由于集成电路制造技术和e d a 工具的快速发展，芯片设 计规模和设计复杂度急剧提高，出现了一批像a r m 这样的专门为第三方公司提 供可复用的集成电路模块的口供应商。 m 供应商的出现和s o c 设计方法学的普及，极大的促进了集成电路设计业的 发展，伴随着p 的推广和使用，也出现了一系列急需解决的问题： 1 )口供应商需要提供怎样的文件，才能使m 用户能够方便、准确的进行 口选择； 2 )口的使用者并不熟悉i p 结构，如何才能快速的对其进行修改以适应设计 者的需要： 3 )由于s o c 各模块间的通讯并没有一个统一的标准，造成口集成的困难， 如何才能解决口的接口标准的问题： 4 ) 口种类很多，设计同一类型的口公司亦很多，如何建立一个相对客观的 口评价体系，实现对i p 质量的评估； 5 ) 如何进行口的验证； 6 )口使用的最大障碍之一是p 的知识产权保护，如何有效地建立起口的 保护体系 这一系列问题的出现，最终导致了m 核标准的产生及相关国际组织的出现。 口标准组织的建立，是国际大公司为协调s o c 设计和使用过程中遇到的一 系列问题，并以这些大公司的现有技术和未来的市场为服务对象，自发组成的联 盟。 v s i a “7 1 是最早的i p 核标准组织，成立于1 9 9 6 年，迄今已经有l o 余年的历 史，是全方位制定口标准的开放性的国际联盟，成员包括系统设计公司、半导 体供应商、e d a 公司、口提供商。其后在世界各地陆续出现了区域性或国际性 的联盟和组织。以促进本地区和国家s o c i p 产业的形成和发展，如日本的i p t c 、 韩国的s i p a c 、台湾的s o c 推动联盟，口网上交易网站有法国的d & r 和英国的 v c x 等。随着s o c i p 产业的发展出现了专业性更强的组织如o c p 一口和 s p i r i t 。鉴于v s i a 在口标准开发和制定上的全面性和权威性，o c p - - i p 接口 标准在业界的广泛采用及s p i r i t 日益受到关注，下面对这三个组织的的情况作 面向口的p s l 规范重用方法研究 一简要介绍。 v s i a 现在大约有7 0 家成员，其目的是为系统芯片工业建立统一的技术规范 和标准，这些规范和标准可以作到使不同来源的m ( 在v s i a 中称为v c 即v t r t u a l c o m p o n e n t ，虚拟元件) 进行集成并相匹配。2 0 0 4 年以前v s i a 是以工作组的形 式开展工作，陆续成立了模拟混合信号、功能验证、依靠硬件的软件 ( h a r d w a r e - d e p e n d e n ts o f t w a r e ) 、实现验证、口保护、与制造相关的测试、片 上总线、系统级设计、虚拟元件质量、基于平台的设计和虚拟元件转让，共1 1 个开发工作组。 2 0 0 3 年v s i a 根据工作任务对工作组进行了调整，其中模拟，混合信号和实 现验证工作组合并为一个实现工作组，撤消了系统级设计工作组，剩余9 个工 作组。这些工作组为s o c i p 工业界制定的标准，规范文件从类型上可以分为四 类：疋交付使用文档规范标柑文件，m 复用设计标准、m 质量评估标准、口 知识产权保护，一共有二十几个，这些标准规范得到了工业界的广泛认可。 2 0 0 4 年v s i a 根据s o c f l p 产业的发展进行了重组，开始以四个支柱( p i l l a r ) 为核心开展工作，这四个p i l l a r 就是现在的v s i a 工作组。四个p i l l a r 分别是口 质量p i l l a r 、i p 保护p i l l a r 、p 基础设施p i l l a r 及由原来的工作组形成的r & d p i l l a r 。 每个p i l l a r 负责与p 集成和复用相关的技术和商业上的解决方案，v s i a 为每个 p i l l a r 提供市场和管理方面的支持。v s i a 把其使命重新定义为通过提供前沿的商 业和技术上的解决方案以及洞察m 开发、集成和重用技术，极大地提高s o c 设 计团体的生产力。 o c p - - i p 是另个值得关注的p 组织。o c p i p 成立于2 0 0 1 年1 2 月，是一 个非盈利性的联盟，最初的成员有s o n i c s 公司、n o k i a ，t e x a si n s t r u m e n t s ，m p s t e c h n o l o g i 髑，u n i t e dm i c r o c l c c t r o n i c sc o r p o r a t i o n 。联盟以s o n i c s 公司的o c p ( o p e nc o r ep r o t o c 0 1 ) 接口规范为基础，目的是为即插即用的s o c 设计提供一 套完整的通用标准m 插座接口，把o c p 发展成接口标准。 s p i r i t 是专门从事口数据打包与集成自动化的组织，成立于2 0 0 3 年6 月， 发起成员有a r m ，b e a c hs o l u t i o n s ，c a d e n c ed e s i g ns y s t e m si n c ，m e n t o rg r a p h i c s ， r o y a lp h i l i p se l e c t r o n i c s s t m i c r o e l e c t r o n i c sa n ds y n o p s y si n c 。s p i r i t 致力于在 两个领域建立标准：口元数据描述标准，及与相应e d a 工具的a p i ，从而实现 口文档和数据自动输入到应用环境中。s p i r i t 的成员将在实际的项目中测试这 套标准，以提供坚实的检验基础。s p i r i t 已发布s p i r i t i 0 ，在2 0 0 4 年的d a c 上几家e d a 公司( c a d e n c c 、m e n t o r 、s y n o p s y $ ) 和i p 公司( a r m , p h i l i p sa n d s t ) 演示了支持s p i r i t 的工具和口。 我国集成电路产业起步较晚，对口标准的研究和应用也是近几年才开始的 6 面向口的p s l 规范重用方法研究 事。然而随着s o c 设计技术的广泛使用，无论是疋的设计公司还是i p 的用户， 越来越清楚的认识到一个统一的坤标准对口的设计、集成和交易的重要性。2 0 0 2 年信息产业部作出决定，成立了集成电路口核标准工作组。四年来在信息产业 部科技司、产品司和中国半导体行业协会的领导与支持下，工作组为中国口核 标准的制定及其在业界的推广等方面作了大量的工作，建立起集成电路口核标 准体系，发布了l l 项i p 核相关标准，取得阶段性的成果。口核标准工作组有 成员单位近4 0 家，分别来自l c 设计企业、l c 生产企业、整机企业、高校和研 究所。工作组的标准制定战略是产学研相结合，自主创新与国际接轨相结合，建 立科学完善的口核技术标准体系，制定我国m 核技术标准。目标是加快口核 的复用，提高企业自主创新能力，形成我国自主知识产权m 核产品，促进口核 产业的形成与发展，提高我国集成电路产业的国际竞争力。 2 ) 形式化规范的正确性验证 rb l o o m 等人开发并实施的形式化需求分析工具r a t ( r c q u i r c m c n ta n a l y s i s t 0 0 1 ) 脚使得用户能够理解并且设计p s l 撰写的规范。r a t 建立在性质保证 ( p r o p e r t y 舡s i l 叫赋【1 5 】) 方法学和性质仿真( p r o p e n ys i m u l a t i o n l 2 2 ) 方法的基础之 上，这些理论旨在验证p s l 设计规范本身是否正确捕获到了用户实际的需求， 需求分析并非为了得到一个与已有性质相符的实现，而仅仅关注于规范层面，这 也是它与模型检查【1 2 2 3 1 检验规范与实现是否相符的不同之处。r a t 工作在p s l 对序层之上，目前还尚未支持验证层上的验证，r a t 工具于2 0 0 5 开始编写，并 于2 0 0 6 年加入了p r o s y d 项目。 3 ) 组件理论 a s s u m e - g u a r a n t e e 推理是组件理论中一个重要成果，它被广泛地应用于程序 模块化组合验证，并取得了良好的效果，其基本思想是，在验证多个程序模块或 多个并发进程时，可以对这些模块或进程的上下文或输入、输出参数进行假设， 基于这些假设条件分别对各个单独的模块或进程进行验证，然后验证这些假设条 件得到满足即可，这种分而治之的方法往往能大幅度地降低验证开销。 何积丰院士提出的r c o s 洲理论基于他和l t o a r e 建立的统一程序理论【1 0 】之上， 其主要思想就是将面向对象的软件开发方法与形式化方法结合起来，定义了一些 重要的基于组件软件开发的概念。包括：接口、契约、交互协议、组件集成、组 件发布及精化。r c o s 给出了使用统一的多视角的方法对组件化系统进行建模、设 计及分析。 7 面向m 的p s l 规范重用方法研究 2 0 0 1 年由l u c ad ea l f a r o 和t h o m a s 丸h e n z i n g e r i v 式提出了一种新的用于描 述接1 ：3 的理论接口自动机i s 6 1 。与已有的各种方法不同，在该理论中有两个突 出的特点：乐观方法和博弈思想。前者用于定义开放式系统中的接口兼容问题， 后者用于描述这一问题的语义。 接口自动机描述了组件接口的时序特性，即接口交互活动间的先后顺序关 系。接口自动机虽然基于传统的自动机，但它将接口的输出保证和输入假设整合 在一起，纳入到该形式化系统中加以处理。输出保证反映了本接口请求的各种外 部服务间的先后顺序关系相当于对环境所作的假设；输入假设反映了本接口 对外部提供的各服务间的先后顺序关系相当于自身行为的一种描述。此外接 口自动机还引入博弈思想来处理接口与环境间的关系，即判别接口兼容性的新方 法一乐观方法。它与传统的所谓“悲观方法”不同，认为只要存在一个可以保 证组合后的接口能在其中正确运行的环境，那么原接口就是可兼容的。同时，由 于采用了“乐观方法”来处理接口组合问题，使得组合后的接口状态大幅度减少， 因而接口自动机又是一种轻量级的形式化系统，这也是接口自动机由于那些基于 。悲观方法”的形式化工具的所在【2 引。 接口自动机理论中，将接口与环境是中看作是一个博弈中的对立双方。环境 一方的目标就是要尽一切可能找到一个策略来满足接口的所有输入假设。判断两 个接口是否兼容就是求解博弈中环境一方的获胜策略。若环境有获胜策略则两个 接口是兼容的，否则两个接口是不兼容的。 4 ) p s l 复用技术 验证硬件模块往往需要为测试环境和模块性质编写大量代码，有时候需验证 的模块有多个工作模式，这些模式都需要被覆盖，因此会有大量的性质需要编写。 通常情况下，要开发一个拥有大量代码的模块时，模块化设计将会是很好的选择， 这样不仅能够增加代码的可读性。同时也支持构件的重用。 p s l 包含了许多不同语言的结构特征，一些结构类似于早期的语言，比如 v h d l 和v e r i l o g 2 1 。p s l 也包含了丰富的时序结构以及特殊的组合结构验证 单元。f a r k a s h 等人在研究报告中阐明了如何使用p s l 编写规范从而达到口重用 的目的，但同时也特别指出，在对验证单元的重用上，必须遵守一定规则，如果 滥用验证单元的继承将导致规范的层次结构非常混乱。 p s l 复用包含多个层次，f a r k a s h 在他的文章中提出了以下9 种不同类型重 用方法例： 1 ) 不同工具件的重用 2 ) 形式化验证与仿真间的重用 3 ) 不同设计层次间的重用 面向口的p s l 规范重用方法研究 4 ) 不同设计版本之间的重用 5 ) 验证单元问的重用 6 ) 组合框架内的重用 7 ) 设计之间的重用 8 ) 内建复杂性质的重用 9 ) 相似问题的解决方法的重用 在硬件设计领域，形式化方法之所以未被广泛应用的原因就是对于给定的系 统来说我们很难对其形式化验证的复杂度进行评估，也就是说，对一个大型系统 来说，验证工作会非常复杂和艰难，为了使形式化方法有效果，人们通常对将整 个系统分成若干个子模块( 口) ，并对这些子模块分别验证。这种验证方法需要 解决的问题就是在子模块验证都正确的情况下，如何保证整个系统也是正确的。 f a r k a s h 【8 l 在5 ) 6 ) 7 ) 三种重用方法中涉及到口复用，强调了a s s u m e - g u a r a n t e e 卅 模式。我们使用接口性质来描述每个子模块，根据接口类型( 输入或输出) 的不 同，这些性质可以分为环境假设和行为保证。环境假设描述的是该模块所在环境 所需要满足的情况，只有在环境满足了假设的情况下，模块才能保证其行为的正 确性。图1 1 给出了a s s u m e - g u a r a n t e e 的情况。 i p i p 行为 ( g u a r a n t e e ) 环境假设 ( a s s u l e ) 图1 1i p 行为，环境假设示意图 1 3 研究目标 本文的目标是构建一套理论正确、实践可行、面向构件的形式化规范正确性 验证方法体系。该体系支持从口单元设计到系统集成各关键步骤中p s l 设计和 操作的正确性验证。我们将从如下方面讨论p s l 规范的正确性： 1 ) 单p s l 规范子句的可实现性； 9 面向口的p s l 规范重用方法研究 2 ) 构件规范的一致性验证方法，该方法确保构件规范中由环境假设子句与行 为承诺子句描述的系统是可实现的； 3 ) 构件规范精化验证方法，该方法确保构件是可比较的，从而为构件替换的 可行性提供分析手段； 4 】p s l 规范的兼容性验证方法，该方法为p s l 规范集成的可行性分析提供支 持； 5 1p s l 规范操作的正确性验证方法，该方法有助于梳理系统设计中的规范架 构，使设计师通过规范继承与集成操作自底向上地演化出系统规范，并且这样的 系统规范仍然满足构件规范的各要素。 i a 研究内容 为了实现基于口的p s l 规范重用，本文将着重从以下几个方面展开论述： 1 ) 研究高可信可验证i p 核表示 为了建立对i p 核质量的信任，保证i p 核集成后系统的可靠性，在将i p 集 成进系统前必须对i p 进行验证。无论i p 核是否开源，i p 核通常由接口定义， 规格说明文档和某种形式( 寄存器传输级描述或电子元件连接网表) 的文本三部 份构成。 高可信可验证i p 核应有满足如下特征的说明文档，1 ) 行为描述子句必须是 人与计算机都可阅读的。人可读是成为文档的必要条件，机器可读是实现自动验 证的充分条件。2 ) 行为描述子句必须是可推理，可演算的。只有对i p 行为有精 确的数学定义，才有机器自动验证的可能。 i e e e 一1 8 5 0 一p s l 标准使得用统一的语言描述信号的时序关系成为可能，并有 精确的形式语义作支撑。因此p s l 是很好的高可信i p 行为规范语言。本文研究 如何使用p s l 语言进行i p 核行为规范描述。这是验证工作的基石，是后续时序 特性规范抽象的目标，也是时序特性规范集成和一致性检验的基础。 2 ) 研究规范子句角色检验方法 面向i p 的规范演算系统解决的是规范子句在i p 规范的继承与集成中角色的 判定，从而实现自底向上的i p 规范演化。 一个规范子句只能有一种角色，环境假设或行为承诺。p s l 语言中，环境假 设子句由a s s l l l d e 关键词引导，行为承诺由a s s e r t 关键词引导。i p 理论告诉我 们，若一个i p 是另一i p 的精化，则该i p 的环境假设必定较弱，而行为承诺必 定较强。较弱的环境假设使该i p 有更好的环境适应能力，而较强的承诺表示其 行为更易控制，有更多的确定性。因此，环境假设子句与行为承诺子句必须被正 1 0 面向m 的p s l 规范重用方法研究 确的引导词引导，否则会造成i p 规范精化验证的错误。要建设面向i p 的规范演 算系统，首先必须保证所有的规范子句都被正确地引导。本文拟对p s l 规范的操 作数类型进行约束。然后根据语言构造中相应操作数的输入输出类型确定规范 子句的类型，如环境的行为规范，i p 的行为承诺，或错误的规范类型。这一规 范自动分类机制可检查用户因将假设的环境行为标注为承诺的i p 行为，或将i p 行为标注为环境行为而产生的错误。 3 ) 建立面向构件的规范演算系统 p s l 在验证层支持v u n i t 用i n h e r i t 关键词继承其他v u n i t 的规范子句，p s l 的验证单元有模块、实例和无绑定三种上下文配置方式。但p s l 标准中没有对被 继承的v u n i t 的绑定类型给以限制，这是造成当前p s l 规范集成中i p 规范体系 混乱的根本原因。从i p 的角度看，i n h e r i t 与模块绑定的v u n i t 的规范子旬类 似与软件中类的扩展，或“继承”：而i n h e r i t 与实例绑定的v u n i t 的规范子句 恰似i p 的聚合，或“集成”。因此，i n h e r i t 既可理解为i p 继承，也可理解为 i p 集成。i p 规范继承与集成对原i p 中子句在新i p 中角色变化的影响是不同的。 “继承”是一种扩展，它不影响原i p 接口在新i p 中角色的变化。i p “集成”将 使原i p 的部分接口成为集成后i p 的内部变量，从而使部分原i p 的规范子句变 成新i p 的内部行为规范子句。这意味着，“集成”操作对i p 规范不是封闭的， 集成后的规范将既含有描述接口的规范子句，又含有描述内部行为的规范子句。 因此，i n h e r i t 关键词在i p “集成”与“继承”时应有不同的语义。继承语义研 究将以v u n i t 绑定类型的不同，确定i n h e r i t 所代表的实际含义，再以i p 接口 属性的变化为依据，判定原i p 规范子句在新i p 中的角色，从而获得i p “集成” 与“继承”后新i p 的规范。 1 5 本文贡献 1 ) 提出了一套检查p s l 性质是否正确地被a s s e r t 和a s s u m e 引导的规则。 一个规范子句只能有一种角色，环境假设或行为保证。p s l 语言中，环境假 设子句由a s s u m e 关键词引导，行为保证由a s s e t 关键词引导。环境假设子句与 行为保证子句必须被正确的引导词引导，否则会造成口规范精化验证的错误。 要建立面向m 的规范演算系统，首先必须保证所有的规范子句都被正确地引导。 本文对p s l 规范的操作数类型进行约束，然后根据语言构造中相应操作数的输 入输出类型确定规范子句的类型，如环境的行为规范，m 的行为保证，或错误 的规范类型。这一规范自动分类机制可检查用户因将假设的环境行为标注为承诺 的口行为，或将口行为标注为环境行为而产生的错误。 面向i p 的p s l 规范重用方法研究 2 ) 给出了基于口规范组合的语义。 对口核进行组合后，在新的集成系统中，一些原本是接口的变量会转化为 内部变量，这些变量对外部不再可见，由于变量类型的改交，一些与之相关的 p s l 性质的意图也会发生改变，本文定义了i p 组合后内部性质的判定规则，将 集成后的p 规范进一步抽象，以便对集成后的讲规范进行验证。 3 ) 定义口继承组合语义。 由于p s l 规范未能对继承的语义给予明确说明，而随意的对口进行继承会 导致继承的失败，我们定义了口规范的继承语义。根据继承对象的不同，规继 承操作一共有7 种情况，这些情况都被归结到三种继承类型中：扩展、聚合以及 实例化 4 ) 设计并实现了基于口的p s l 重用设计的工具。 在基于摩的p s l 规范重用方法的基础之上，设计并开发相关工具软件i p s l ， 该工具为广大集成电路设计者提供了重用和检验口的有效手段。 1 6 本文结构 本文第二章介绍了性质规范语言o s l ) 的概况，p s l 语言是本文研究的基础， 也是形式化描述系统规范的有效工具。 第三章介绍了面向口的p s l 规范设计方法，包括如何使用接口规范来描述 一个口，如何进行性质保证以及性质意图检查等概念。 第四章提出了基于口的系统集成的方法，研究了p s l 中继承的概念，对口 之间组合和继承操作的具体语义给予说明。 本文的第五章介绍了基于口重用理论所设计的基于的p s l 设计工具i p s l v 1 0 。这是一个可视化的p s l 规范设计平台。用户可以方便的进行口的验证及 重用。 1 2 面向口的p s l 规范重用方法研究 第二章p s l 语言规范 2 1p s l 的由来 传统的对系统功能规范说明都是采用自然语言，这种说明形式一般都是比较 含糊的，并且由于缺乏标准的机器可执行代码而无法进行验证。本文介绍的性质 说明语言( 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 的前身s u g 一2 l 】语言是由i b m 的h a i f a 实验室经过8 年研究开发的，是一 种说明性的形式化性质规范语言。其语义是严格的，但是易于理解和使用。可以 用类似定理的形式描述要验证的属性，这些描述可以作为模型检验和定理证明 的输入，也可以做模拟程序中检查程序的输入。 p s l 是在e d a 领域的标准化组织a c c e l e t a 的功能验证技术委员会发布的。它 的语言参考手册p s l l r m 1 0 1 版本于2 0 0 3 年4 月己发布。p s l i 1 版本于2 0 0 4 年2 月发布。2 0 0 5 年国际标准化组织将p s l 作为标准i e e e 1 8 5 0 发布。 2 2 p s l 的目标 p s l 是为完成如下硬件功能规格需求所特别开发的 3 0 1 ： 便于掌握、书写及阅读 明确的语法 严格定义的形式化语义 很强的表达能力，规范能够描述现实中的设计性质 在仿真和验证中拥有高效的算法 2 j p s l 用途 p s l 是一种能够用形式化规范描述硬件的语言，它被用于描述验证时在设计 中需要保持的性质。p s l 提供了一个既便于编写又非常精确的方法来撰写规范， 它一方面可以用来编写功能规范，另一方面能够作为功能验证工具的输入。 1 ) 功能规范 p s l 可以用来捕获设计中内部行为的需求，同时也被用于描述设计所需要的 环境假设，这两者能够确保更有效的功能验证和设计的重用。 p s l 的一个重要的作用是可以作为功能规范文档来代替用自然语言写的规 范说明一个p s l 规范既可以描述一个常量，也可以描述一个多时钟的行为。p s l 面向i p 的p s l 规范重用方法研究 规范说明是由跟在一系列假设后面的断言组成，p s l 性质是建立在布尔层表达 式、顺序表达式和时序表达式的基础上建立起来的。v e t i l o g 的布尔表达式： e l 均0e n b 这个表达式描述在设计中的某个时刻，信号e n a 和e n b 至少有一个被断言。p s l 顺序表达式： r e q ；a c k ；l c a n c e l 描述一个时钟序列，期间r e q 首先被断言，随后a c k ，最后是c a n c e l 未断言。以上 两个表达式能够使用时序操作符a l w a y s 和n e x t 来连接： a l w a y s r e q ；a c k ；! c a n c e l ( n e x t 2 ( c n ai i 即b ) ) 说明跟在( r c q ；a c k ；! c a n c e l 序列的两个时钟后信号c n a 或c n b 在被断言。 a s s e r ta l w a y s r e q ；a c k ；! c a n c e l ( n e x t 2 ( e n a0 e n b ) ) 完整的规范说明，加t a s s c r t 指示词，说明在设计中这个属性期望出现并在验 证的过程中加以验证。 2 ) 功能验证 p s l 可以作为验证工具的输入，不仅适用于动态验证的仿真，也可以用于形式 化的验证模型检验和定理证明。 仿真：p s l 规范描述可以自动地对仿真进行检查。直接将验证集成在仿真工 具：用自动的测试激励工具解释p s l 语义驱动仿真器；生成h d l 监视器；仿真结束 时分析路径。 形式化验证：p s l 是标准时态逻辑即线性时态逻辑和分支时态逻辑的扩充。 采用p s l 基础语言的规范说明可以解释成线性时态逻辑，对应的p s l 可选的分支 扩展可以解释成分支时态逻辑同时加上辅助的硬件描述语言的代码。 2 4 p s l 结构 按照功能进行区分，p s l 语言可以分为布尔层，时序层，验证层和建模层四层； 2 4 1 布尔层 布尔层主要记录设计的状态和定义可能被其他层次使用的属性。布尔层用来 假设某个时钟应具有的属性，所定义的条件都参照其相应硬件设计语言中的信 号、变量和值。在布尔层中，所有这些h d l 表达式都被解释成对应的布尔值。 例如c n a c n b 表示信号c n a 和e n b 在某一时刻有一个被断言，布尔表达式描 述的只是信号的状态，但是并未定义时序关系，在布尔层，验证工具无法知晓什 么时候需要c n a0e n b 这个条件成立。 面向口的p s l 规范重用方法研究 2 4 2 时序层 时序层是p s l 的核心，除了定义简单的属性，还用来描述涉及到信号问时序 关系的属性。 在布尔层e n a e n b 上加上时态操作符a l w a y s ， i p a l w a y se l l a0e n b ，这样就 说明了在任何时刻信号e n a 和e n b 至少有一个要被断言。 2 4 3 验证层 验证层为验证工具提供指示词，用来告诉工具对这个属性如何进行处理。例 如验证层的指示词可以告诉工具去验证属性是否保持或检查测试实例中是否覆 盖了某个特定的序列。验证引导词主要有：a s s u m e 、a s s e r t 、c o v e r 等，例如： a s s e r ta l w a y se n a 0e n b 完整的规范说明，加丁 a s s e r t 指示词，说明在设计中这个属性期望出现并在验证 的过程中加以验证。 2 4 4 建模层 建模层构建辅助的状态变量、状态机，为验证构造辅助的代码，但不属于设 计的部分。 2 5p s l 验证层对重用的支持 验证单元( v e r i f i c a t i o nu n i 0 是验证层中的一个重要成果，它被用于将多个验 证指令或其他p s l 语句打包。验证单元有三种类型v u n i t 、v m o d e 和v p r o p ，验证单 元类型v m o d e 用来描述环境假设，它只包含a s s u m e 指令，相反，v p r o p 能包含拥 有a s s e r t 弓l 导的指令。 验证单元通过绑定相应对象模块或者实例，从而将验证单元中的信号与被验 证设计中的信号联系起来，绑定对象可以是模块、实例或者是空，如果一个验证 单元绑定了一个模块，那么验证单元中的信号和对应模块的所有实例中的相应信 号连接，例如： v u n i tm a ( m o d u l ea ) ( ) 如果验证单元绑定了一个模块的实例，那么验证单元中的信号只与该实例中 的信号相连。例如： v u n i ti i ( m o d u l e _ a i l ) ) 验证单元i l 中的变量与m o d u l ea 的实例订相对应。 另外一种情况就是没有显式绑定，那么这个验证单元不会与特定的对象关 联，它常被用于将通用的p s l 声明组织起来，从而被其他的p s l 验证单元继承使 面向口的p s l 规范重用方法研究 用。例如： v u n i t n _ a 0 ) 验证单元的继承是验证单元中的一个重要的性质，一个验证单元可以继承一 个或者多个验证单元，而被继承的验证单元又能继续继承其他验证单元。 继承有两个作用： 验证单元中的p s l 声明能引用被继承的验证单元中的上下文。 当一个验证单元作为验证工具的输入时，当前的验证单元与其所继承的所有 验证单元的上下文都被放在一起来定义验证环境和确定验证指令。 例：假设有两个模块块b l o c ka 和b ，其中a 的输, h , ( a o u t l ，a o u t 2 ) 分别是b 的 输入( b i n l ，b i n 2 ) ，从而形成了一个由a 和b 组成的模块c 。 b l o c k c a i n l a o u t i b i n l b l o c k ab l o c k b a o n t 2b i n 2 图2 1 验证单元继承示意图 下面的验证单元描述了这两个单元的交互情况： v m o d em c o m m o n p r o p e r t ym u t c x ( b o o l e a nb l ，b 2 ) = n e v rb l & b 2 ； v p r o pp ( 珀栅 p r o p e r t yo n e _ h o t o o l e a nb l , b 2 ) = a l w a y s ( ( b 1 & & f b 2 ) 0 , 2 & f b l ) ) ； ) 验证单元m c 衄蛐o n 和p c b m m 没有被显式地绑定，它包含了通用的性质定 义且被定义为了v m o d e ，所以能被其他v u n i t 单元继承。 v u n i t a m o d e ( b l o c k a ) i n h e r i tm c o m m o n ； a s s u m em u t c x ( a i n l ，a i n 2 ) ； ) 1 6 面向p 的p s l 规范重用方法研究 v u n i tb m o d e ( b l o c k b ) i n h e r i tp c o m m o n ； i n h e r i tm c o m m o n ； a s s u m em u t e x ( b i n l b i n 2 ) ； a s s e r to n e _ _ h o t ( b o u t l ，b o u t 2 ) ； ) v u n i