（计算机软件与理论专业论文）事件驱动的系统级仿真器的操作语义及代数法则研究.pdf

华东师范大学硕士学位论文 事件驱动的系统级仿真器的操作语义及代数法则研究 摘要 s o c ( s y s t e m s 一。n a c h i p ) 系统目前应用得越来越多。一个s o c 系统可以包含不同的功 能模块，例如数字电路、模拟电路、硬件专用电路、存储器、微处理器、数字信号处理器 d s p ( d i g i t a ls i g n a lp r o c e s s o r ) 以及软件部分。传统的嵌入式设计方法采用硬件先行的 方法，在对时间和费用要求苛刻的今天，是不可行的。应用软硬件协同设计技术可提高开发 效率。通常，软硬件协同设计的设计流程的第一步是采用一种系统级描述语言描述系统，并 进行模拟仿真和系统功能验证。s y s t e m c 是建立在c + 十基础上的一种系统级描述语言，被许 多设计者用米对s o c 体系结构进行建模以进行体系性能的分析及软硬件协同设计。i e e e 已 经批准了s y s t e m c 为电子设计语言标准( i e e e l 6 6 6 ) 。 作为一种系统级描述语言，s y s t e m c 具有一些新的和有趣的编程特性，例如延迟的事件 通告、事件通告取消、事件通告覆盖、通馗更新以及d ej t a c y c i e 。这些新的编程特性使得以 前使用其它编程语言的工程师学习s y s t e m c 时，会产生一些迷惑。同时，开发s y s c e m c 的 仿真器、综合器以及验证器，都需要对s y s t e m c 语言的语义有一个严格、精确和无歧义的 理解。用自然语言所书写的帮助文档往往含有微妙的歧义。本文采用结构化操作语义的方法 给出了s y s t c m c 的一个核心子集的操作语义。同时，在此操作语义的模型上，定义了程序 的互模拟关系，用来判断两个程序是否等价。在此操作语义的基础上，采用p m l o g 语言实 现了该仿真器的原型。仿真器原型可以用来验证操作语义的正确性。最后，论文提出了一系 列s y s t e m c 语言所满足的代数法则。这些代数法则可在操作语义模型中通过互模拟进行验 证。据作者目前所阅读到的文章和资料来看目前对s y s t e m c 中那些新的和有趣的编程特 性的代数法则的讨论研究很少。 形式化语义和代数法则在实践应用是很有用的。操作语义模型是综合实现和验证的基 础。代数法则可以直接应用于工程中的优化设计，同时保证优化的正确性。代数法则还可以 h j 于程序转换。 关键字：操作语义，代数法则，系统级规范语言，s y s t e m c ，软硬件协同没计 仿真器，原型实现，事件驱动 华东帅范大学预l 学位论文事件驱动的系统级仿真器的操作语义及代数法则研究 a b s t r a c t n o w a d a y s ，s o c ( s y s t e m s o n a - c h i p ) s y s t e m sh a v eb e e nu s e dm o r ea n dm o r ew i d e i y o n e s o cs y s t e mm a yc o n s i s to fd 仃b r e n tf u n c t i o nm o d u l e s ，i n c l u d i n gh a r d w a r ec o m p o n e n t sa n d s o f t w a r ec o m p o n e n t s t ba c h i e v ch i g ip e r f o m a n c ew j t h1 0 wc o s t ，h a r d w a r e s o m v a r ec o d e s i g n m e t h o d 0 1 0 9 i e sa r ea d o p t e d u s u a l ly ，t h en r s ts t e po f h a r d w a r e ，s o 觚a r ec o - d e s i g ni si od e s c “b e t h es y s t e mb e h a v i o r su s i n gas y s t e m i e v e id e s c r i p t i o nl a n g u a g e s y s t e m ci ss u c hal a n g u a g eb a s e d o nc 。h s y s t e m ch 船b e e nu s e do ns y s t e mm o d e l i n ga n dh a r d w a r e ，s o 竹w a r ec o d e s i g n ，w i d e l y r e c e n t l y s y s t e m c2 ih a sb e e na p p r o v e da sa ni e e es t a n d a r d ( 1 e e e l 6 6 6 ) f o rs y s t e ml e v e ic h i p d e s i g n a sas y s t e m - 1 e v e ld e s cr i p “o n1 a n g u a g e ，s y s t e m cp o s s e s s e ss o m en e wa n di n t e r e s t i n g p r o g r a r n m i n gf e a t u r e s ，j n c l u d i n gd e i a y e de v e n tn o l i n c a t i o n s ，e v e n tn o t m c a t i o nc a n c e l a t i o n ，e v e n t n o t i f i c a t i o no v e r r i d i n ga n dd e l t a c y c i et h e s ep r o g m m m i n gf e a t u r e su s u a i l ym a k ep r o g r a m m e r s c o n f u s e d i ti sa j s om a n d a t o r yt op r 0 v i d eas t r i c t ，p r e c i s ea n du n 扪b i g u o u su n d e r s t a n d l n go f s y s t e m cf o rd e v e l o p m e n to fs i m u l a t o r s ，s y n t h e s i z e r sa n dv e r i f i e r s u s e rm a n u a l sw n e nb y n 砒u r a l l a n g u a g e sa l w a y sc o n t a i ns u b t l ea m b i g u i t i e s ，t h i 5t h e s i sp r e s e n t sa no p e r a t i o n a ls e m a n n c s o fak e m e ls u b s e ti a n g u a g eo fs y s t e m c ，u s i n gs t r u c t u r a lo p e r a t i o n a ls e m 越n c s b a s e do nt h e o p e r a t i o n a ls e m a n t i c s ，b i s i m u l a t i o ni sd e 矗n e dt oc h e c k 也ee q u i v a l e n c eo ft w op r o 笋a r n s a p r o t o t y p eo ft h es i m u l a t o ri si mp l e n l e n t e du s i n gp r o l o g ，w h i c hh e l p sc h e c kt h ec o r r e c t n e s so ft h e p r e s e n t e do p e r a l j o n a ls e m a n f j c s f i n a l j xas e to fa l g e b r a i cl a w so fs y s t e m ca r ep r e s e n 把d ，w h i c h c a nb ev e “丘e dv i ab i s i m u l a t i o no no p e r a t i o n a is e m 加t i c sm o d e l t bt h eb e s tk n o w l e d g eo ft h e a u t h o lt h e r ea r ef e wp u b l i c a t i o n sa b o u t t h er e s e a r c ho nt h ea l g e b r a i cl a w so fs y s t e m c o p e r a t j o n a js e m a n i c sa n da l g e b f a i cl a w sa r ev e r yu s e f u li np r a c t i c e ，o p e r a t i o n a is e m a n t j c si s a l s ot h eb a s ef o rf h r t u r ew o r ko ns y n t h e s i sa n dv e r i f i c a t i o n a l g e b r a i ci a w sc a nb ea p p l i e dl n d e s i g no p c i m i z a t i o na n dp r o g f a mt r a n s f o r m a t i o n ，w n hc o r r e c t n e s sg u a r a n t e e d k e y w o r d s ：o p e r a t i o n a ls e m a n t i e s ，a 1 9 e b r a i cl a w s ，s y s t e m c ，s y s t e m 1 e v e l ， d e s c r i p t i o nl a “g u a g e ，h a r d w a r e ，s o f h v a r ec o - d e s i g n ，s i m u l a t o p r o t o t y p e ，e v e n t d r i v e n 学位论文独创性声明 本人所呈交的学位论文是我在导师的指导下进行的研究工作及取得的研究 成果。据我所知，除文中已经注明引用的内容外，本论文不包含其他个人已经 发表或撰写过的研究成果。对本文的研究做出重要贡献的个人和集体，均已在 文中作了明确说明并表示谢意。 作者签名；耋她日期： 学位论文使用授权声明 本人完全了解华东师范大学有关保留、使用学位论文的规定，学校有权保留 学位论文并向国家主管部门或其指定机构送交论文的电子版和纸质版。有权将 学伎论文用于非赢利目的的少量复制荠允许论文进入学校国书馆被查湄。有权 将学位论文的内容编入有关数据库进行检索。有权将学位论文的标题和摘要汇 编出版。保密的学位论文在解密后适用本规定。 学位论文作者签名：驾 日期：坦垒兰粤 小痿 导师签名：了多二彳 日期：2 3 。一 华东师范大学硕士学位论文 事件驱动的系统级仿真器的撵作语义及代数法则研究 1 1 软硬件协同设计 第1 章概述 随着i c 制造技术的飞速发展，半导体加工上艺进入深亚微米时代，芯片的特征尺寸越 来越小，单位芯片上晶体管的数目越来越多，同时芯片的规模也越来越大已经可以在单个 芯片上集成上千万甚至成亿个晶体管。集成电路规模的变大，使得系统芯片s o c ( s y s t e m s o n a c h i p ) 的发展与应用成为了可能。s o c 将电子系统几乎全部的功能集成到 一块芯片上，从而在单个芯片上能实现数据的采集、转换、存储、处理和i 0 等多种功能。 换一个角度来说，s o c 能集成数字电路、模拟电路、硬件专用电路、存储器、微处理器、数 字信号处理器d s p ( d i g i t a ls i g n a lp r o c e s s o r ) 等多种异构模块，实现多个复杂的应用功 能。除了硬件模块外，s o c 系统还包含软件模块。s o c 的出现顺应了现代通信、电脑、消费 电子产品向高陛能、低功耗和低成本方向发展的趋势。但机遇到来的同时也带来了挑战，问 题可以归结为两个方面：硅复杂性和系统复杂性。系统复杂性源于两个因素，一个因素是集 成度的增加使得单一芯片上晶体管数目成指数级增长，另一个因素是消费者对电子产晶更多 功能，更低价格的需求，以及更短上市时间的压力。 1 1 1 软硬件协同设计方法的引入 般而言，s o c 系统都具备强大韵数据处理和存储能力，能适应了一类典型应用的功能 和性能要求；同时，它还应当具有灵活的软硬件可编程能力。软件的可编程性体现在基于同 一种类型的体系架构下，充分发挥软件本身的适应性和可重用性，减小更改硬件所带来的开 销，提高设计速度。硬件的可编程性在于通过对应硐的特殊功能定铷满足性能要求的专用加 速器，充分利用硬件本身的便携性和可扩展性，减小研发软件而带来的额外费用，缩短设计 周期。因此，s o c 的设计应该是一个软硬件协同设计的过程这也是s o c 系统一个非常重要 的标志。然而传统的集成电路设计方法一般都是将系统分为两个阶段：系统级软件开发部 分和电路级硬件设计部分。特别指出的是，软件开发和硬件设计往往是相对独立进行的，如 图1 所示。 图l 在系统级，软件开发人爨使用诸如c c 等高级编程语言进行系统描述和算法仿真，并 分析系统在软件层面的各项指标，撰写系统设计书，然后移交给硬件设计工程师。在电路级， 硬件设计师首先要花大量的时间理解系统设计书，之后才能利用v h d l 或v e r 儿o g 硬件描述 语言进行电路设计。在此手工转换的过程之中，可能还会引入人为的错误因素。另外，为了 验证软件开发的正确性，必须等到硬件全部完成之后才能开始进行软件测试和系统集成，大 人延长了设计的进程。根据有关统计从系统级设计到电路级设计所花费的时间一般是系统缎 设计所花对闻的3 倍左右。因此在系统级设计与电路级设计之间架设一座桥梁己经成为集成 电路设计领域极为迫切的任务，如图2 所示。 图2 1 1 2 软硬件协同设计技术 随着应用的不断发展，芯片的设计也越来越复杂，性能要求也越来越高，而且激烈的市 场竞争使得电子产品上市时间的压力越来越大，设计者需考虑的问题也越米越多，采用传统 的电路级设计必将导致许多估计不到的难度。因此，需要人们重新审视已经熟知的设计方法， 必须提出一套符合新的设计思路、新的工艺环境、严格的时序要求、以及高的性能标准的设 计方法。在探索s o c 设计方法进程中，系统级设计方法s l d ( s y s t e ml e v e ld e s i g n ) 的研 究获得了来自学术界、t 业界以及多种不同行业的重视。它是未来芯片设计中的最重要砝码 当然也是最具挑战性的内容 1 。 图3 概括了面向s o c 系统级的主要研究内容，包括：软硬件协同设计技术【2 、设计重 用技术、与底层相结合设计技术。三者相辅辐成、相互促进。软硬件协同设计技术常与设计 重用技术交织在一起，成为目前s o c 系统级设计的主要部分。 图3 传统的i c 设计方法采用硬件先行的方法，即先设计硬件，再根据算法设计软件，而在 深弧微米设计中，硬件的费用是非常大的，当设计完成后，发现错误进行更改要花费犬量 的费用和时间。在对时间乖费用要求苛刻的今天，此种方法是不可行的。 在s o c 设计中，为了既可缩短开发周期义能取得更好的设计效果，要求使用软硬件协 同设计技术。软硬件协同的方法可以使软件设计者在硬件完成之前接触到硬件模块，从而更 - 6 好地设计硬件的驱动、应用程序、操作系统等软件，同时可以使硬件设计者尽早接触软件 为软件设计者提供高性能的硬件平台，减少了设计中的盲目性，如图4 所示。 t r a d i t i o n a ld e s i g nn o w c o n c u r r e m ( c o d e s i g n ) f l o w s t a ，t s w k s l g h e db yl h d 。p e h d 日h g r 口t t p sc j x p e r “ 趾a r t ：妇日g p o 妙船，封口g ，口l pc e x p e r t sw l | hc o o p e r 口虹。h 图4 在s o c 中，尤其是在面向特定应用领域的s o c 中，软硬件的结合是非常紧密的，软件和 硬件之间的功能划分，以及它们的实现并没有固定的模式，而是随应用的不同而变化。一般 来说，面向s o c 的软硬件协同设计理论是从一个给定的系统描述着手，通过有效地分析系统 任务和所需的资源，采用一系列变换方法并遵循特定的准则自动生成符合系统功能要求、符 合系统约束的硬件和软件架构。目前，在软硬件设计中最为活跃的研究工作包括系统描述、 软硬件划分、软硬件协同综合、以及软硬件协同模拟与验证。图5 给出了一个较为普遍的面 向s o c 软硬件协同设计流程。 图5 系统描述 系统描述的研究内容主要包括描述模型与描述方法。系统描述的目的是在最高抽象层次 上( 系统级) 利_ i = 某种高级语言( 如c 、c + + 、s y s t e m c 或u m l 等) 描述整个系统的行为，获 取用户功能需求和约束要求，以便在详细设计开始之前，验证需求分析的正确性。同时进行 必要的性能分析作为后续设计的基础。系统描述可以独立于后续的实现过程，可以仿真运 行，也可以采取逐层精化的方法，将系统级描述精化为r t l 级的描述，再进行综合。 软硬件划分 软硬件划分是根据系统在描述与建模层次的分析结果，将系统功能合理地划分为软件实 现部分和硬件实现部分，并使整个系统的性能、成本最优，它是软硬件协同设计中的一个重 要课题。由于划分问题本身具有难度，加上s o c 带来的巨人搜索空间，使之成为一个传统难 题。研究人员虽然已经尝试了各种优化算法，但自动划分程序仍然不能取代有经验的设计者， 从系统功能描述自动生成软硬件代码的自动软硬件划分工具在近期l = | 尚不可能实用。 软硬件协同综合 软硬件综合是一个把高层次描述转化为低层次实现的过程。其首要任务是如何利f l = | 系统 级设计中提供的各种资源( 系统功能描述、可使用的软硬件模块等) ，同时满足系统性能 与代价约束，找到一个晟好的平衡点( 合理的设计表示模型、优化的体系结构等) 来实现从 功能到结构再到实现的转换。这种转化的结果应在软硬件划分的基础上，在已有的设计规则 和既定的设计目标前提下，决定系统中软件部分的具体实现方案和硬件部分的详细设计实 现，同时给出应用中性能代价瓶颁。 软硬件协同模拟与验证 软硬件系统模拟的目的是在硬件生产出来以前，通过模拟( 仿真) 的手段验证软硬件集 成方面的问题。软件模拟和硬什仿真都存在不同的抽象层次，抽象层次越高，模拟的速度越 快，但反映的细节也越少。软硬件协同仿真可以分为高层次仿真、低层次仿真和混合层次仿 真三种情况。目前对低层次仿真的研究比较成熟，其一般模式是软料调试环境、微处理器模 型和硬件r t l 描述的协同仿真它可以在尚未生产f _ _ j 硬件之前对虚拟模型进行一些早明的 调试，并为软件调试提供虚拟平台。软硬件协同验证的目的和协同仿真的一样，都是希望在 设计的早期验证系统软硬 串的正确性，特别是功能的正确性，性能的满足性。然而，验证基 本是通过形式化的方法，如模型检查和定理证明，来推理其系统的正确性。 1 1 3 典型s o c 系统级设计方法 s o c 系统级设计方法学在国外的研究十分活跃，许多b d a 厂商、研究机构以及大学都开 发了适应于s o c 系统级的设计工具，并提出相应的设计流程和设计方法。目前。在学术界和 业界比较认可的s o c 系统级设计方法掌，从性质上基本可分为三大阵营：自顶向下、自底 向上、上下结合或中间相遇。从具体的表现形式和实现方式来说，这三大阵营分别由以f 三 个研究团体提出的相关方法和技术支撑，即：美国加州大学i r v i n e 分校嵌入式系统研究小 组的基于s p e c c 的逐层细化求精设计方法 3 、法国t i m a 实验室系统级综合小组的基于纽件 的多处理器核s o c 设计方法 4 、美国加州大学b e r k e l e y 分校c a d 研究小组的基于平台的设 计方法 5 。表1 列举了三种不同的系统级设计方法的主要优缺点及其典型代表。 1 2 系统描述语言 s o c 系统一般是由硬件与软件两部分构成。传统上，硬件与软件有不同的设计工具与开 发流程，这不剥于系统性能的综合分柢，髓羞形式化方法的发矮。现代芯片设计通常使用硬 件描述语言( h a r d w a r ed e s c n p t i o nl a n g u a g e ，h d l ) 来描述各开发阶段的设计规范，从此硬 件的殴计方法开始向软件的设计方法靠近。对于s o c 系统的开发，基于r t l 的芯片设计方法 就显得过于底层。v e r i l 。g 语言和v h 口乙语言更象是硬件的汇编语言，用这样的语言开发s o c 系统常常过于复杂，功能测试消耗了人量的时间与资源。为此，人们寻求有更高抽象层次， 更模块化的设计方法。该方法应便于人们交换技术与经验( i n t e l l e c t u a lp r o p e r t y ，i p ) ，使 设计师在设计之初就能对系统架构在性能与资源消耗上有精确的量化估计。这需要有一种能 描述系统功能和各方面约束特性的系统级描述语言，该类语言应具有如f 的特性 6 ： 1 支持与具体实现方式无关的机器行为描述，为后续设计过程中算法选择留下足够空间： 2 具有完备的需求信息描述能力，支持包括通讯，多媒体，控制等不同领域的规范整合和 各种约束的整合： 3 在系统功能描述方面模块化，在系统结构描述方面架构化，能支持由不同计算模型生成 的系统与组件的整合； 4 有形式化方法做理论支撑，以减轻工程师在系统功能分析与验证方面的压力： 5 拥有可预见的量化分析手段； 6 有与系统级描述语言匹配的开发一【具和软硬件统一的开发流程，使软硬件在实现上的著 异将仅仅是编译选项上的不同。 建设系统级描述语言不是一蹴而就的，它是人们不断努力的结果，可行的策略是在现有 的语言基础上进行扩充。当前豹系统级描述语言的设计大致可以分为三类。第一类是提升已 有的硬件描述语言的抽象层次：第二类是扩展软件描述语言，i 止它们能够描述硬件的行为： 第三类是综合各语言的优势，创建新的语言。 1 2 1 源于硬件描述语言的系统描述语言 1 2 _ 1 1 s y s t e m v e “l o g s y s t e m v e r 儿o g 7 是源自硬件描述语言的系统级描述语言的代表。它对i e e e j 3 6 4 2 0 0 l 的v e r 儿o g 8 标准进行了较大规模的改动，在融合了v e r “o g ，c c h ，甚至 s u p e r l o g 等多种语言的特性后，为嵌入式系统设计工程师提供了前所未有的描述能力。其 关键特性包括： s y s t e m v e r i l o g 用类似于c + + 中模版的接口，在较高的抽象层次上连接各硬件模块。而 用以往的v e r 订o g 编写程序只能用基本数据类型来定义模块间的接口； s y s t e m v e r i l o g 引入了c 语言的部分语句构造和数据类型，如两态的”c h a r ”和”i n t ”等， 使s y s t e m v e r i l o g 可以调用普通的c 程序； s y s t e m v e r i l o g 提供四态的逻辑数据结构以表现硬件系统的特性： 0 s y s t e m v e r i l o g 引进了断言构造，咀便于程序属i 生的检验与程序正确性验证； s y s t e m v e r i l o g 倡导者的口号是“正确的方法是扩展当前有效的”( t h er i g h ts 0 1 u t i o ni s t oe x t e n dw h a tw o r k s ) s y s t e m v e r i l o g 的设计是试图- 止硬件语言来描述软件系统。因此， 用s y s t e m v e r i l o g 描述系统。工程师仍必须对硬件有相当的了解，不能站在超越实现方式的 高度来给出系统的规范。这是s y s t e 讥v e r i l o g 被诟病的所在。根植于硬件描述语言的 s y s t e m v e r il o g 由于抽象层次仍不够高，其仿真速度也无法与其它语言匹敌。 1 2 1 2v h d l 一2 0 0 x 为与以往的语言相区别，新的系统级描述语言通常会有一个s r s f 的前缀。令人好奇的 是，v h d l 9 界没有为跏f 呦做厂+ 告，似乎v h d l 的发展已停滞。其实，v h d l 的支持者 认为v h d l 根本不需要印f f 这个前缀，v h d l 是领先丁时代的语言，它可被广泛用于比r t l 抽象层次更高的各种设计环境。把v h d l 的修订版称作s y s t e m v h d l 将暗示，v h d l 具有与其 它h d l 相同的明显缺点。i e e e 的1 0 7 6j 作组称v h d l 在新世纪的第一个重要修订版为 v h d l 一2 0 0 x 。其新增特点是： 为了提高设计工作效率，v h d l 提供了一个可靠的类型系统，具有用户自定义类型、如 枚举型、有符号型、无符号型、比特型、比特欠量型、整数和受约束搭数型、实数型、 访问型( 指针) 和记录型。 增加面向对象的功能，以促进建模过程中的更高级别的设计重用以及更高级别的抽象。 i e e e 的1 0 7 6 工作组正在努力确定如何才能增加继承和增强的模板，以便允许子程序的 类型参数化。可以预期，面向对象的增强还将促进多个抽象级的接口建模。 计划采用a c c e l l e r a 的p s l 1 0 作为v h d l 的属性规范语言以提高设计质量和验证 自动化的效率。 1 2 2 源于软件语言的系统描述语言 支持从软件语言出发构建系统描述语言的支持者主要是些乐观的软件专家。他们认为， 随着计算机和设计自动化技术性能的提升，总有一天， ：程师只需键入”c c s i l i c o n ”命令， 编译器就可自动转换c c 十+ 或j a v a 程序到芯片网表 1 1 1 2 。但就目前而言，已开发i _ = 具的 自动化稃度仍然不够高，开发过程中需要人j 对系统规范进行精化。程序文本中不但要体现 算法，还要具有体现底层硬件特性的表达式描述能力。 正在开展中的将软件语言扩展到系统描述语言的研究及开发系统大致分为两类。第一类 以s y s t e m c 为代表，他们充分利用c + + 的可扩展性，直接引入硬什元素。第一类以s d e c c 为 代表，它们在基本的c 语言中加入新的关键词在较高的抽象层次上支持硬件特性。 a c c e l l e r a 组织的s y s t e m c 1 3 语言。a c c e 儿e r a 是一个由e d a 公司和集成电路设计公 司共同参与的产业联盟，它为各参与方共同关心的研发计划制定产业标准，让有兴趣的 机构可以根据标准开发自己的产品。s y s t e m c 就是其中的一个标准。s y s t e m c 的没计初 衷是为了填补s o c 设计与硬件描述语言在抽象层次上的巨人落差。因此，当时s y s t e m c 的目标仍然是r t l 设计。而没有涵盖软件编译的内容。它的工具链是沿袭硬件描述语言 的，倚赖仿真来保证设计的正确性。随着s y s t e m c 2 o 标准的公布，s y s t e m c 在软件方 面的缺陷已得到了弥补。i e e e 近日表示已经批准了s y s t e m c 为电子设计语言标准 1 4 。 据i e 旺称s y s t e m c2 1 将硬件和软件建模功能拓宽至更高抽象级。它令1 二程师从头 建造整个系统，从而加快设计，允许共享并复用知识产权。i e e e 标准化有助于将s v s t e m c 引入到更广泛的应用领域，并推动来自商用e d a1 二具更进一步的支持。 加州人学i r v i n e 分校的s p e c c 3 语言。该语言直接定义在 n s i c 基础上，提供系统 行为层级( b e h a v i o rh l e r a r c h y ) ，结构层级( s t r u c t u r a lh i e r a r c h y ) 并发，通讯 同步，状态机，异常处理，定时等多项体现嵌入式系统本质特性的程序语句。并且s d e c c 的开发流程，从算法，模块，时钟的处理，一直到r t l 级规范，执著地贯彻了体系结壮j 建模，功能正确性验证，设计性能评估，规范精化的理念。因此s p e c c 的支持者认为只 有s p e c c 才是严格意义下的系统级描述语言。 牛津大学的h a n d e l c 1 5 语言( 现为c e l o x i c a 公司拥有) 。h a n d e l c 起源，以c s p 1 6 为 理论依据的o c c a m 1 7 语言。其坚实的理论基础赋予了o c c a i i 菲常精细又非常好用的线 程结构，这使它在开发并发系统，反应式( r e a c t i v e ) 系统中拥有很强的优势。但是反对 h a n 吐e l c 的也大有人在。因为h a n d e l e 在改造o c c a j 矗的过程中加入了过多的硬件物理约 束，如引脚定义信号的边沿特性等。即在系统设计的早期就将实现方式给限定死了， 这是有违系统级描述语言设计精神的。值得一提的是在c e l o x i c a 最近公布的产品中有 一款面向s y s t e m c 的敏捷编译器( a g i l i t yc o m p i l e r ) 。这充分显示了s y s t e m c 的强人冲 击力。 1 2 3 基于j a v a 的系统描述语言 现实的s o c 系统是由一些交互工作的实在个体和对象构成。面向对象的语言更易于系统 建模，也就更容易被工程师接受。因此，最近出现的一些开发系统多是面向对象的。自然地 就有研究者提议用j a v a 语言作为系统描述语言。 j a v a l o g i c ( 现己被x i l i n x 合并) 的j h d l 1 8 是第一个将j a v a 程序转换成可综合r t i 。描 述的编译器。j a v a 的支持者认为，j a v a 生来就是为提高嵌入式系统开发生产力的，j a v a 程序比硬件描述语言的程序短很多，又支持通过申请线程的方式实现标准c c + + 所没有 的并发。反对者的意见是，j a v a 中没有c + + 中的操作符号重载，其后果是大量的函数调 用与系统行为的不确定性，从而很难在高层对系统进行精确的性能估计。一般认为，j i d l 是c + + 之后的选择。 j e d a 1 9 是另一个有影响的用类j a v a 语言作为系统级描述语言的尝试。它为j a v a 语言 提供了时间点与时间区间的描述构造，并从v e r a 2 0 借用了，0 蜘j 卫月舢e ， ，0 r 如j 卫鲫，以描述多进程。特别是它采用了a o p ( a s p e c t o r i e n t e dp r o g r a m m i n g ) 的理念，让设计工程师和验证工程师都先专注于各自的工作，然后把功能描述规范与功 能验证规范编织在一起形成测试单元( d e v i c eu n d e rt e s t ) 。因为j e d a 在设计之初是希 望为系统架构验证提供方便的手段，因此它没有综合工具，放j e d a 没能形成完整的工 具链，这在一定程度上限制了它的推广。 1 2 4 新定义的系统描述语言 s u p e r l o g 2 1 是v e r i l o g 的一个超集，又借用了c 语言中的部分语句。因此，现有的 v e “1 0 9 设计无需大规模改动依然可在s u p e r l o g 环境中被综合。它还卢称其兼备了 v e r i l o g 的简明与c 的抽象它不是简单地将v e r 订o g 与c 合并，而是对两者优势的增 值。可惜的是，s u p e r l o g 尚未被工业界中的大多数公司排上研发日程。a c c e l l e r a 也重 新回到s y s t e m v e r i l o g 的项目上了。 在构建系统描述语言方面，欧盟的e s t e r e l 2 2 计划其实早_ 】= 美国。e s t e r e l 的设计目 标是提供一个能描述系统功能与结构的语言。它支持图形化的组件建模，交互式仿真， 形式化特性验证，测试和文档生成。一些欧洲公司已用该语言成功开发了产品，但在欧 洲之外，其影响力甚弱。美国公司还没有对其支持。 上面我们简短地同顾了一些主要的系统级描述语言研究的历史与现状。可以看到在软硬 件领域对系统级描述语言存在争论的激烈。软件专家认为完全从硬件描述语言出发是不正确 的而另一方则坚持通过升级v e r “o g ，v h d l 的途径来昂终实现系统语言。从短期的角度看， 第一类源下硬件描述语言的方法最可行。因为它是硬件描述语言的精化，向f 兼容。遗存系 统( 1 e g a c ys y s t e m ) 在新环境r 无需二次开发仍然可用。这一演化方式将持续到硬件描述语 言有足够的抽象层次，其特性可被软件语言的自然扩充而涵盖。因此，第二类源于软件描述 语言的开发方式是中期的目标。从k 期的角度看，电子设计自动化产业( e d a ) 必将获得不同 于现有软硬件开发语言的系统级描述语言。这是第三类方式的追求。三类演化方式在达成目 标的时间上有先后，但在发展的时间上却是几乎同时的，并且互相影响，互有借鉴。 1 3 形式化语义 1 3 1 语义概要 随着计算机技术的发展，编程语言的发展非常迅速，各种各样风格类似或不同的编程语 言层出不穷。为了开发编程语言的开发工具和写出高效正确的程序，需要对编程语言有十分 精确的理解。一个编程语言主要由两部分构成：语法和语义。编程语言的语法显示r 程序代 码的样子以及语句的结构，而语义则赋予了程序具体的意义。语义可以应用于对编程语言进 行进一步的理论研究r 作和实践应用。形式化语义是关下严格描述程序或者崾件的意义或者 行为。严格性的需求是由于： 1 一些看起来似乎定义的很清楚的文档( 例如编程语言的帮助手册) 中还是含有很多歧义 和微妙的复杂性。形式化语义有助于将它们暴露出来。 2 形式化语义为实现、分析和验证提供了基础 在讨论编程语言的语义时，主要有二种类型的语义：操作语义( o p e r a t i o n a is e m a n t i c s ) 、 指称语义( d e n o t a t i o n a is e m a n t i c s ) 以及代数语义( a l g e b r a i cs e m a n t i c s ) 。这三种语义并不是 相互竞争的关系，而是适合于不同目的的不同技术。在某种程度上讲，它们分别适台丁不同 类型的编程语言。 1 3 2 操作语义 个编程语言的操作语义显示了一个程序如何运行【2 5 。操作语义不是定义个程序执 行后所观察到的整体效果，而是给出了一个在程序执行过程中所有单独步骤所构成的完备集 合。一个操作语义中的每一个单独步骤通常是以s o s ( 结胸 艺操作语义，s t u r a lo p e 烈l o n a i s e m a n t i c s ) 2 6 】的形式书写。s o s 已经成功的应用于定义多个编程语言的操作语义 2 7 。在 s o s 中，每一个独立的步骤都被描述为一个迁移。一个语言的操作语义一般就是有一个迁 移集合构成。 一个迁移规则具有如f 形式： c c 其中，c 是程序在执行一个典型步骧之前的状态的状况( n n g u r 雏；o n ) ，而c 描述了执行了 步骤后的状况。对于某些语言，迁移规则有好儿种类型。因此，迁移规则c 专c 可以扩展 成如f 的形式： c j - c ， 其中，b 可以被认为是迁移类型。 对于某些语言，它们的操作语义需要模拟某些可以发生a 动作的行为。这种情况下的 迁移可以写戒如f 的形式： c a c 其中，a 是可以立即被程序执行的动作。 1 3 3 指称语义 操作语义的形式化是基丁一个程序的意义的底层描述。这个描述并没有用到什么高深 的数学。而指称语义刚提供了程序的数学意义。指称语义的方法是基于纯粹的数学基础。因 此，指称语义是更抽象的。与操作语义相比，指称语义显示了程序作什么了。指称语义的重 要优势是： i 每一个程序的行为可以不需要在计算机上实际执行的情况下预期其行为。类似的，一个 编程语言的指称语义可以理解为是对程序如何在一台计算机上执行的抽象。 2 田为指称语义是基于数学理论的，所以我们可以对程序进行推理，例如，证明两个稃序 是等价的。 有许多种方法可以用米描述指称语义。失败发散( f a l i u r e s d i v e 唱e n c e s ) 模型成功地用于 了描述c s p ( c o m m u n i c a l l 丌gs e q u e n l i a lp r o c e s s ) 的语义【2 8 ，2 9 。每一个进程的观察 ( o b s e r v a t i o n ) 被形式化为两个集合：发散集合和必败集合。发散集合是一个痕迹( t r a c e ) ( 例 如，一系列鲍动作) 的集台鞠戍的。在进程执行完了这个痕迹厉，进程就变成发散c l 勺了。在 另一方面住失败集合中的每一个元素都是一个二元组。二元组中的第一个元素是一个动作 序列，表示进程能够执行的动作。而第二个元素是由动作构成的集合。在进程执行了第一个 元素中的序列中的动作后，进程不会执 j ：第二个元素集台孛的任何动作。 1 3 。4 代数语义 指称语义可以 3 来推导有趣的程痔性质。这些性质也可以在操作语义模型中，采 j 9 ：模 拟理论进行研究 3 0 。这些陛质大多数情况下都表示为代数法则( 一般都是等式) 【3 1 。代 数可以被f 程师商接用于符号计算以及优化设计。人多数代数法则能够表示成p ：o ，这表 示在任何上f 文中p 能够被q 替换，或者相反。住这种清况下，程序能够被转换成另外的 等价形式，或者优化形式。 由代数法则构成的集合也能表示一个编程语言的语义尽管程序的意义不是显式的给 出。编程语言更多的性质可以由这些代数法! 1 1 1 ) 推导出来。因此，代数法则军 由这些代数法则 推导出的性质可以看成是构成了一个完整的代数语义。第一个完备的代数法则集台是关丁 d u k s t r a 的1 | 确定性顺序编耩语言 3 i 。人们已经对编群语言o c c a m 的的代数法则也进行 了大量的研究f 3 2 】。 在代数法则的应用方面，h o a r e 、何和s a m p a i o 已经研究了如何使用代数的方法来保证 编译的正确性 3 3 】。何、p a g e 和b o w e n 研究了编程语言o c c a m 正确性可证的硬件综合 3 4 】。 1 3 5 编程统一理论 编程统一理论( u n j 母i n gt h e o r i e so fp r o g r a m m i n g ，简称u t p ) 是由h o a r e 和何在1 9 9 8 年提出的 3 5 】。u t p 涵盖了编程理论方面的l 午多重要领域，它可以看作是编程语言原理的一 个一致性的基础。它给出了d q k s t r a 的非确定性顺序编程语言的指称语义。为了处理关系理 论和实践之间的不一致性，设计( d e s i g n ) 怍为_ 关系的一个子集被引入，它包括了一个假定 ( a s s u m p l i 。n ) 和承诺( c d m m i t m e n t ) 对，u t p 同时也给出了顺序编程语言的个完备代数 演算，它可以将程序转换成一种语法受限的范式形式。许多高级编程特性也被引入，例如并 发结构雨交互式进程。它也包括了一些如何将操作语义平代数语义以及指称语义连接起米方 面的理论。l j ，r p 已经成功地川丁研究编稃语言的语义和代数法则。 1 4 操作语义 对编程语言的语法和语义进行区分是很自然的。语法是与一个程序的文法结构相关的。 因此，程序( z ：= x ；x ：= y ；y ：= z ) 的语法分析可以是：它是由符号；隔开的三条语句构成的。每 一条语句都是变量后面跟一个符号：= 和一个表达式( 这里只是一个变量) 。 语义是与语法正确的程序相关的。因此，上述程序的语义是：交换变量x 和y 的值。如 果需要更具体的解释它们，则需要看一f 程序的语法结构，并使用如下的解释： 顺序的语句之间是由：分隔的 语句由一个变最以及后跟的符号：= 和表达式构成 一个语句的意义的操作性解释就是说如何执行这个语句： 为了执行一个以；分隔开的