（计算机软件与理论专业论文）verilog形式化语义研究.pdf

一 ， f 9 训 摘要 ， ( v e r i l o g 是当前应用最为广泛的硬件设计语言之一，它可以用于硬件系统各种级别的设计，综合，仿 真为了保证设计的正确性，v e r i l o g 语言应该具有一个形式化语义标准；而且形式化语义同时也是一种 语言形式化开发方法的基础虽然现有的形式语义学工作已经被广泛地应用于程序设计语言的研究，但 是对v e r i l o g 的语义形式化工作做得显然很不够这就使得v e r i l o g 语言的使用者和设计者之间对语言产 生了不同的理解，给语言的实施与使用带来了困难厂7 本文的主要想法是想将形式化语义方法引入工业界应用极为广泛的v e r f l o gh d l 中，为v e r i l o g 的形 式化验证以及自动求精提供严格的语义基础，其主要内容包括三方面： 1 本文首先给出了一个比较完善的结构化操作语义模型来描述v e r i l o g 核心子集的语言特征眦子集包 含了事件驱动，基于共享变量的并发特性，时间延迟等v e r i l o g 的核心语言成分；而且在此操作语义 模型中，所有的v e r i l o g 程序将被统一地认为是开放式系统，这里所谓开放式系统指的是能够与外界 环境发生交互的系统；所以我们能够进一步提出v e r i l o g 的观察模型，并进而提出v e r i l o g 进程互模 拟概念以用来表示进程之间的观察等价性；并且我们证明了所定义的互模拟关系对于所有的v e r n o g 复合子来说是一个同余关系，从而为发展相应的进程代数理论提供了一个可靠性基础我们所提出 的互模拟思想不仅在理论上为v e r i l o g 程序的等价性概念提供了一个比较完善的框架，而且也在实 践上为证明程序等价提供了一种有效的技术r 2 然后本文给出了v e r i l o g 的代数语义，这是一个等式公理体系，它将v e r i l o g 语义特征通过代数规则 简洁准确地表达出来f 这些代数规则，诸如并行扩展规则，事件触发等，或者与通常并行语言相应 的规则很不相同，或者在其他语言中就根本不存在它们正好反映了v e r i l o g 独有的语义特征我们 的代数语义相对于前面所作的操作语义模型来讲是可靠的，即所有的这些代数规则左右两边的进程 在操作语义的观察模型下都是互模拟的户r 一 3 最后本文研究了代数语义的相对完备性。怛p 参照前面的操作语义模型，相对于扩展v e r i l o g 语言的一 个子集而言，我们的代数语义是完备的即所有符合这样语法的程序，如果它们是互模拟等价的， 那么它们同样可以在我们的代数系统中被推导相等在完备性证明过程中，我们采用了范式方法， 即构造一种语法上特殊的程序，任何属于上述子集中的一个程序通过我们的代数规则能够被转化为 范式程序，而且范式程序在操作语义模型下是互模拟的当且仅当它们是语法相同的该子集包括了 除循环程序外的所有v e n l o g 应用程序完备性工作的进展标志着我们对v e r i l o g 语言特征的认识的 进一步完善，因为我们不仅能通过操作语义模型来具体描述v e r i l o g 语言的执行细节，而且对于这个 模型中各进程的等价性能通过代数规则的形式很好地刻划出来 上述结果具有重要的理论意义，因为现有的进程代数理论主要是针对管道通讯并行语言而展开的， 而对于象v e r i l o g 这种以共享变量通讯为基础的复杂并行语言研究甚少，本文对此类复杂的基于共享变 量的并行语言的进程代数理论研究提出了一种通用有效的方法r 1 7 关键词：v e r i l o g ，操作语义，互模拟关系，代数语义。可靠性，完备性。范式 a b s t r a c t v e r i l o gi st h em o s tp o p u l a rh a r d w a r ed e s c r i p t i o nl a n g u a g ei ni n d u s t r y i tc a nb eu s e dt ot h ed e s i g n ， s y n t h e s i s ，a n ds i m u l a t i o nf o rh a r d w a r es y s t e ma ta l ll e v e l s f o re n s u r i n gt h ec o r r e c t n e s so ft h ed e v e l o p m e n t ， t h e r es h o u l db eak i n do ff o r m a ls e m a n t i c so fv e r i l o g ；a n daf o r m a ls e m a n t i c sw i l lb et h eb a s i so ff u r t h e r f o r m a l s u p p o r tf o r t h el a n g u a g e t h ef o r m a ls e m a n t i c sh a sb e e ns t u d i e dq u i t ee x t e n s i v e l y ，b u tt h a to f v e r i l o g l e s ss o a sar e s u l ti tw i l lb r i n ga b o u tt h e m i s u n d e r s t a n d i n gb e t w e e nt h el a n g u a g eu s e r sa n dd e s i g n e r s ，a n d w i l lm a k ei td i f f i c u l tt oi m p l e m e n ta n du s et h el a n g u a g e t h i sd i s s e r t a t i o nt r i e st oa p p l yt h ef o r m a lm e t h o d st ot h ei n d u s t r i a ls t a n d a r d v e r f l o gh d l ，a n dp r o v i d e as o u n db a s ef o rt h ef o r m a lv e r i f i c a t i o na n ds y n t h e s i so fv e r l l o gh d l p r o g r a m s i tm a i n l yi sc o m p o s e do f t h r e ep a r t s ： 1 f i r s t l yw ep r e s e n tap l o t k i n - s t y l es t r u c t u r a lo p e r a t i o n a ls e m a n t i c sf o rac o r es u b s e to fv e r i l o g ，a n dt h e s u b s e th a st h em a i nf e a t u r e so fv e r i l o gs u c ha se v e n t - d r i v e nc o m p u t a t i o n ，s h a r e d - v a r i a b l ec o n c u r r e n c y , t i m e - d e l a y , a n ds oo n a n di no u ro p e r a t i o n a ls e m a n t i cm o d e l ，v e r l l o gp r o c e s s e sa r er e g a r d e da so p e n s y s t e m s ，w h i c hc a l li n t e r a c tw i t ht h e i re n v i r o n m e n t s ；s ow ec a np r e s e n tam o d e lo fo b s e r v a t i o nf o r o p e nv e r l l o gp r o c e s s e s ，a n du s eo b s e r v a t i o ne q u i v a l e n c eb a s e do nb i s i m u l a t i o nt oi d e n t i f yp r o g r a m so f t h es a m eb e h a v i o r t h e nt h eo b s e r v a t i o ne q u i v a l e n c ec a nb ep r o v e dt ob ea c o n g r u e n c ef o ra l lv e r i l o g c o n s t r u c t o r s ，s oi tp r o v i d e sas o u n db a s ef o rd e r i v i n gt h ea l g e b r a i cl a w sf o rv e r f l o gp r o c e s s b i s u m u l a t i o n n o to n l yp r o v i d e sat h e o r e t i c a lf r a m e w o r kf o rd e f i n i n gt h ee q u i v a l e n c eb e t w e e nv e r i l o gp r o g r a m s ，b u t a l s og i v e sa ne f f e c t i v em e t h o dt op r o v et h ee q u i v a l e n c eb e t w e e n v e r i l o gp r o g r a m s 2 s e c o n d l y , w ew i l le x p l o r e t h ea l g e b r a i cs e m a n t i c so f v e r i l o g ，w h i c hi sac o l l e c t i o no fl a w sa s s o c i a t e dw i t h v e r i l o gc o n s t r u c t s t h e s el a w sp r o v i d eap r e c i s ef r a m e w o r kf o rd e s c r i b i n ga n dd e f i n i n gt h es e m a n t i c s o fv e r i l o g i np a r t i c u l a , ，m a n ya l g e b r a i cl a w s ，s u c ha se x p a n s i o nl a w s ，e v e n t t r i g g e r ，a n ds oo n ，e i t h e r d i f f e rf r o mt h e i rc o u n t e r p a r t so rd o e sn o ta p p e a ri no t h e rp a r a l l e ll a n g u a g e s t h e yj n s ts h o wu st h e s p e c i a lf e a t u r e so ft h es e m a n t i c so fv e d l o g a l lt h el a w sp r e s e n t e da b o v ea r es o u n dw i t hr e s p e c tt ot h e o p e r a t i o n a ls e m a n t i c s ，i e ，i ft h et w op r o c e s s e sa r et h et w os i d e so fal a w ，t h e nt h e ya r eb i s i m i l a r 3 a tl a s t ，w ew i l le x p l o r et h ec o m p l e t e n e s so ft h ea l g e b r a i cl a w sw i t hr e s p e c tt oas u b s e to fv e r i l o ga n d t h eo p e r a t i o n a ls e m a n t i c s ，i e ，i fs u c hp r o g r a m sa r eb i s i m i l a r ，t h e nt h e ya r ea l g e b r a i c a l l ye q u i v a l e n t f o rt h e p r o o f o fc o m p l e t e n e s s ，o u rm e t h o dw i l lb et h ed i s c o v e r yo fan o r m a lf o r mp r o g r a mf o ra n ys u c h p r o g r a m s e a c hs u c hp r o g r a mw i l lh a v ea ne q u i v a l e n tn o r m a lf o r mp r o g r a m ( t h r o u g ht r a n s f o r m a t i o n b yt h ea l g e b r a i cl a w s ) ，b u tt w on o r m a lf o r mp r o g r a m sw i l lb eb i s i m i l a ri nt h eo p e r a t i o n a ls e m a n t i c si f a n do n l yi ft h e ya r es y n t a c t i c a l l ye q u i v a l e n ti na s i m p l ew a y a n dt h es u b s e th a sc o n t a i n e da l m o s ta l lt h e w h i l e - f r e ev e r i l o ga p p l i c a t i o n s t h es t u d yo ft h ec o m p l e t e n e s st a k e sa s t e pf o r w a r do u ru n d e r s t a n d i n g o nt h es e m a n t i cf e a t u r e so fv e r i l o g ：w en o to n l yc a nu s eo p e r a t i o n a ls e m a n t i c st od e s c r i b et h ed e t a i lo f t h es i m u l a t i o no fv e r i l o gp r o g r a m s ，b u ta l s oc a np r o p o s el a w st oc o m p l e t e l yd e s c r i b et h ee q u i v a l e n c eo f v e r i l o gp r o c e s s e s t h e s er e s u l t sa r eo ft h e o r e t i c a ls i g n i f i c a n c e ，f o rt h et h e o r i e so fp r o c e s sa l g e b r aa r ec o n c e n t r a t e do nt h e c h a n n e l c o m m u n i c a t i o nc o n c u r r e n tl a n g u a g e s b u tt h e r ei sl i t t l ew o r ko nt h es h a r e d v a r i a b l ec o n c u r r e n tl a n - g u a g e s ，a n dw ep r o p o s eag e n e r a la n de f f e c t i v et r e a t m e n tt ot h er e s e a r c ho fs u c hk i n do fc o m p l e xc o n c u r r e n t l a n g u a g e si nt h i sd i s s e r t a t i o n k e y w o r d s ：v e r i l o g ，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 n ，a l g e b r a i cs e m a n t i c s ，s o u n d n e s s ，c o m p l e t e - n e s s ，n o r m a lf o r m 第一章前言 1 1 背景 本节主要介绍一下v e r i l o g 硬件描述语言以及形式语义学 1 1 1v e r i l o g 硬件描述语言 随着电子设计技术的飞速发展，专用集成电路( a s i c ) 与现场可编程门阵列( f p g a ) 的复杂程度越 来越高；设计这样复杂的电路及系统已不再是简单的个人劳动，而需要综合许多专家的经验与知识才能 完成在数字逻辑设计领域，迫切需要一种共同的工业标准来统一对数字逻辑电路及系统的描述，把专 家们设计的各种常用数字电路和系统部件建成宏单元( m e g c e l l ) 或者软核( s o f t c o r e ) 库供设计者使用，以 减少重复劳动，提高工作效率 硬件设计语言( h d l - - - h a r d w a r ed e s c r i p t i o nl a n g u a g e ) 正是顺应了以上历史潮流而应运而生的它 们是利用形式化方法来描述数字电路和设计数字逻辑系统的语言数字逻辑电路设计者可以利用这种语 言来描述自己的设计思想，然后利用电子设计自动化( e d a ) 工具进行仿真，再自动综合到门级电路，最 后用a s i c 或者f p g a 实现其功能 硬件设计语言发展已经有二十多年的历史，并成功地应用于设计的各个阶段：仿真、验证、综合 到9 0 年代，已出现了上百种硬件描述语言，它们对设计自动化起到了极大的作用但是这些语言各自 面向特定的设计领域与层次，而且如此众多的语言使得用户无所适从，因此迫切需要一种面向设计各领 域、各层次的并得到普遍认同的标准硬件设计语言这就是h d l 的标准化问题最终v h d l 和v e n l o g h d l 适应了这种趋势的要求，先后成为i e e e 标准 v e r i l o gh d l 是目前应用最为广泛的一种硬件描述语言，它是由g d a ( g a t e w a yd e s i g na u t o m a t i o n l 公司的p h i l i pm o o r b y 首刨的p h i l i pm o o r b y 所设计的v e r f l o z 快速仿真器极大推动了v e r i l o g 语言的 发展在c a d e n c e 公司收购g d a 后，c a d e n c e 公司决定公开发表v e r i l o g 语言，于是成立丁o v i ( o p e n v e r i l o gi n t e r n a t i o n a l ) 组织来负责v e r i l o g 语言的发展基于v e r i l o g 的优越性，i e e e 于1 9 9 5 年制订了 v e r i l o g 的i e e e 标准，即v e r i l o gh d l1 3 6 4 - 1 9 9 5 1 1 1 2 【3 】 v h d l 4 5 i 6 是另外一种使用非常广泛的h d l ，由于它是由美国军方组织开发，所以它很早地就成 为i e e e 标准这两种h d l 的共同特点就是：能形式化地抽象表示电路的结构和行为；支持逻辑设计中 的层次描述；可借用高级语言的精巧结构来简化电路的描述；具有电路仿真与验证机制以保证设计的正 确性；支持电路描述由高层到低层的综合转换等等不过v h d l 的风格是基于a d a 语言的，而v e r i l o g 却是基于c 的；正是由于这种语言编程风格的差别。使得v e r i l o g 更容易掌握，从而也就赢得了更为广 泛的设计群体与资源在美国，在电路设计领域v e r i l o g 与v h d l 的应用比率是6 0 与4 0 【7 1 考虑到v e r i l o g 是工业界应用最为广泛的h d l 外，还考虑到由于它来自民间的普通公司，所以相应 地v e m o g 的形式化语义工作开展得比较少，所以我们选取v e r i l o g 作为本文的研究对象，实质上本文的 研究方法对于研究其他硬件设计语言( 如v h d l ) 的形式化语义也是适用的 1 1 2 形式语义学及分支 程序设计语言是人类用来和计算机系统通信，并控制其工作的人工语言为了正确、有效地使用程 序设计语言，人们必须了解语言中各个成分的含义。并且要求计算机系统执行这些成分的所产生的效果 和其含义完全一致为了保证语言的准确实施和有效使用，就要使得语言的设计者，实施者以及使用者 对语言的语义有相同而且精确的理解 正是人们对语义精确理解的要求产生了形式语义学，形式语义学的研究开始于六十年代初在1 9 6 2 年的国际信息加工联合会上，美国斯坦福大学麦克阿瑟( j m cc a t h y ) 作了著名的报告”通往计算的数 学科学”，系统地阐述了程序设计语言语义形式化的重要性，并提出在形式语义学的研究中使用抽象语 法和状态向量等基本方法几十年来，形式语义学的研究取得了巨大进展它对程序设计语言的设计、 使用和实施都产生了深远的影响。语言的形式语义与形式语法一样都成为程序设计语言的必要组成部分 8 】【9 】 本文所涉及的形式语义学分支主要包括三方面：即操作语义学，指称语义学，和代数语义学( 1 0 1 操作语义 1 l 】 1 2 】 1 3 】的基本思想是用抽象的方法描述语言中每一个成分的执行效果。通常的做法 就是设计个抽象机( 或者称为转移系统) ，定义一组抽象状态，把语言的语法表示成抽象的形式，然后指 明抽象机每加工一个语言成分时将会产生什么样的状态转移 指称语义【1 4 i 5 i 6 1 的基本思想就是使语言的每一个成分对应于一个数学对象，该对象正是该语言 成分所谓的指称，它不像操作语义那样涉及语言成分的执行过程，而只需考虑各成分执行的最终效果， 并认为此最终效果应不依赖其执行过程 代数语义 1 7 1 8 1 9 2 0 2 1 】的基本思想是以抽象语法作为多基类代数的型构定义，将程序作为代数 表达式，将程序复合构造子作为函数符号，利用程序表达式问一系列等式或不等式规则给出程序语言的 语义这种代数描述方式同样能为定义与描述语言语义提供一个精确的理论框架，并且有助于语义形式 定义文本的规范化与模块化，降低描述的复杂度代数语义的两个很重要的问题就是研究代数规则的可 靠性以及完备性 这三种语义描述方法中：操作语义非常直观，容易理解，而且与实现或者模拟联系的比较紧密；而 指称语义方法贝惧有良好的数学基础，它在完整的一个数学框架下对语言的成分进行解释以及进行相应 的推理工作；而代数语义方法不仅通过等式规则直接反映了程序语言的代数性质，更为重要的是这些代 数规则可以被直接用来进行实际系统的求精或者验证工作；h o a r e ，h e 等在文献【2 2 】中建议：在研究具 体的程序语言时，最好同时运用这三种语义描述方法，即同时做语言的三种语义以适应不同的用途；其 中在研究代数语义的可靠性以及完备性时，我们参照的就是指鹭或者操作语义模型 目前形式语义学研究的一个特点就是理论与应用的分离从工程角度来看，程序语言的设计开发人 员往往并不采用形式化的严格方法，象c ，c + + 这样使用最为广泛的程序设计语言按照程序设计方法学 的观点来看。它们在设计上都有很严重的缺点而从理论的角度来看，研究者往往有过于追求抽象的倾 向，对常用的程序设计语言缺乏兴趣他们的研究工作侧重于研究数学性质良好的实验性程序设计语言， 而忽略了使用广泛的编程语言 v e r i l o g 尽管是应用最为广泛的h d l 外，但是它的形式化语义工作开展得显然很少，甚至连v e r i l o g 的语言i e e e 标准使用的只是非形式化的仿真算法，这样就带来了很多的麻烦，由于v e r i l o g 本身是涉及 硬件的所以不可避免地与并行性牵涉在一起，而由于我们在仿真时只能以先后顺序执行各进程，这样 就带来了非确定性，由于对这种非确定选择处理的不同，各种公司在制作它们的仿真器时对非确定性选 择采用了不同的处理方式这就造成了各种仿真器对于同一程序会有不同的仿真结果 2 3 2 4 1 所以只有 具有了形式化语义。才能确保语言的设计者以及使用者对语畜有相同而且准确的理解，人们才能在此基 础上开发自动综合以及验证工具，所以形式化语义同时也是一种语言形式化开发方法的基础 我们同时也希望借助形式化语义学的理论，能够帮助我们描述象v e r i l o g 这样的复杂的实用工业界 标准语言的执行过程，并且能够刻划它的性质，并将所得到的结果尽可能地用于硬件仿真，系统求精， 系统验证等形式化开发方法中 2 1 2 本文的工作 1 2 1 研究对象 这里我们主要从形式语义学的角度来考察一下所要研究的对象的语言特征 - 为了在各种层次上( 系统级，行为级，寄存器传输级，门级等) 来描述硬件系统，v e m l o g 语言具有 非常丰富的语言特征它主要包括： 事件驱动的计算过程事件既可以是导线或寄存器值的变化，也可以是抽象事件v e r u o g 程序的语 义是基于事件的调度与传播的一个进程模块的输入敏感信号发生变化，产生事件，驱动该模块被 调度执行，从而导致该模块的输出信号发生变化，从而产生新的事件，并将新的事件传播下去 基于共享变量的并发特性v e r i l o g 并发进程之间的相互影响可以被认为是通过共享变量来进行 的一个进程通过改变共享变量的值产生事件，从而触发所有等待此事件的进程已有的并发理论 如c c s ，c s p 1 2 2 5 等都以通道通讯为主，对硬件设计来说，通道并不是直接的物理概念共享 变量即共享导线或寄存器才直接与硬件设计对应以后我们可以看到，以共享变量为基础的并发系 统与基于通道通讯的并发系统之间存在着很大的差异 同时具有离救状态变化以及连续时间变化的混合特征v e r i l o g 的行为级功能描述成分如赋值，顺 序，分支，循环等，它们主要考虑系统在运行前后的状态型亿，而忽略运行所需要的时间从仿真 的角度来看，这些成分的执行是不需要任何时间的而v e n l o g 的另外一些成分如卫式，延时等实时 特征成分，大多是基于连续时间的它们描述的是系统在一段宏观时间区段内的变化情况 所以要能够给出v e r f l o g 的形式语义并不是很容易的为了使语言具有一个更加严格准确的标准， l人们开始了v e r i l o g 的形式化语义工作以下是对已有工作的简要总结，我们同时也分析了以下各种方法 的问题所在 1 2 2 研究现状及问题 1 2 2 1 操作语义方法 最早开始v e r i l o g 形式化语义工作的是m i k eg o r d o n 2 6 ，他最早提出了一个标准算法来描述v e r i l o g 程序仿真的操作过程，并且在该文中他对v e r i l o g 形式化语义的进一步工作提出了很好的建议h e ，x u ， g e r a r d o 等以上述算法为基础，给出了v e r i l o g 的一个子集的操作语义【2 7 【2 8 】但在他们的操作语义模型 中，他们把程序分为两个层次：顺序部件以及并发程序个并发程序作为一个封闭系统，它由若干顺序 部件组成他们仅仅考虑一个封闭并发系统内各种顺序部件的相互交互影响过程。却忽略了并发系统间 的相互影响正是因为他们把并发程序作为封闭系统，一个封闭系统是不会与外界环境交互的。那么怎 么能够比较封闭系统之间的行为呢? 所以他们无法以此操作语义为模型进一步提出互模拟( b i s i m u l a t i o n ) 技术以及相应的程序等价概念，更谈不上发展相应的进程代数理论等 i 2 2 2 指称语义方法 指称语义的方法主要集中在利用d u r a i o nc a c u l u s 【2 9 】来描述v e r i l o g 程序语义，其中心思想是把 v e r i l o g 程序放在d c 的语义模型中考虑，将d c 语义模型的一个区间作为程序一次运行过程的指称，并 利用d c 公式来描述这个运行区间的各种时序特征但是，作为一种硬件设计语言，v e r n o g 具有混合特 征，即它同时包括连续时间区间的变化，又有在同一时刻的零延迟状态迁移过程( 如在同一时刻有若干 赋值语句先后执行，但在宏观看来，所有这些计算是不占任何时间的) 为了描述这种混合特征，人们必 须在原有d c 的基础进行扩展以增强该逻辑系统的描述能力 g o r d a np a c e 利用关系d c ( r e l a t i o n a ld c ) 描述了v e n l o g 的一个子集【3 0 】，但它忽略了v e r i o g 的 3 共享变量特征为了描述该特征，p d y a 与d a n g 等建议使用# w d c 3 1 3 2 ，x u 使用了# w d c 来描 述了v e r i l o g 的一个子集 3 3 】，它包含了共享变量，递归计算等高级特征，但是这些工作还是把v e r i l o g 并发i 墼j 芋作为封闭式系统我们使用了扩展的i t l 来描述了一个更大的子集叫，这是我们在v e r i l o g 指 称语义上的尝试，而z h u ，h e 等也以扩展d c 3 5 】给出了v e r i l o g 的指称语义【3 6 】，这两项工作都希望把 v e r i l o g 程序作为开放式系统来考察与描述，并希望在程序等价理论上取得进展；但是为了刻翅 零延迟状 一 态迁移，所有以上工作使用的逻辑系统都要在原有d c 基础上进行扩展，扩展部分很多涉及高阶成分( 如 对状态变量允许使用存在量词) ，这样使得该逻辑系统变得极为复杂，而且我们在证明程序的等价性。以 及提出相应的进程代数理论时，我们必须从最底层的逻辑公式出发，利用该逻辑系统的证明规则进行推 导现在看来，这种证明方法遇到了极大的困难，因为在没有对这些逻辑系统的有关性质分析清楚的前 提下，进一步的工作很难进行下去；而且即使能够得到证明一些代数定理。证明过程也是极为复杂和冗 长的 1 3 本文所采用的研究方法及内容 我们在利用指称语义方法给出v e r i l o g 的语义后，在以其为基础去研究程序等价性以及有关进程代数 时也遇到了很大的困难这些困难促使我们重新转向了操作语义方法我们首先希望所提出的操作语义 模型能够很好地描述以上v e r i l o g 的语言特征，并且要把v e r i l o g 的所有程序( 包括顺序以及并发程序) 作 为开放系统，用统一的观点来看待所有程序与环境交互作用的万式，进程内部各部件之间的交互方式； 然后我们希望在此操作语义模型的基础上提出相应的v e r i l o g 程序的实时观察模型，即确定一个v e r i l o g 程序的哪些行为是外部的或者说是可观察的，然后在观察模型的基础上提出相应的互模拟概念，从而导 出相应的观察等价关系观察等价性( 互模拟关系) 描述了程序间的等价关系，证明两个程序等价即是 要构造这样一个等价关系，使得这个程序对在这个关系中如果我们再能进一步证明此等价关系的同余 性，那么我们的操作语义模型就能够为研究代数语义提供一个具体的参照模型 然后我们研究v e r i l o g 的代数语义即找出反映v e r i l o g 程序性质的所有基本代数规则，这些基本 的规则同样能为定义与描述语言语义提供一个精确的理论框架，并且它具有很好的规范化与模块化的优 点；然后以我们的操作语义模型作为具体的参照模型，进而为研究代数语义的可靠性与完备性其中可 靠性( s o u n d n e s s ) 是指代数语义中的等式规则左右两边的进程在操作语义模型下都是互模拟的，完备性 ( c o m p l e t e n e s s ) 是指所有在操作语义模型中是互模拟等价的进程都可以在代数语义系统中推导相等当 然由于为了代数推理的可能，我们适当扩展了v e m d g 语言，而完备性是相对于扩展v e r i l o g 语言的一个 子集而言的 1 4 本文的主要结果 本文最重要的一些结果如下所示： 1 我们为v e r i l o g 建立了一个比较完善的操作语义模型，该操傺语义模型不仅能够刻划v e r i l o g 的事件 驱动。基于共享变量通讯的并发特性，时间延迟等核心语言特征，而且以上这些语言特征是一般语言 都没有的，为了要刻划它们，我们在操作语义模型的状态转移系统中必须引入相应的描述机制；另。 外，我们所作的语义是面向开放式系统的操作语义，我们不再把并行程序作为一个封闭系统来处理 ，而是以统一的方式来看待进程内部各部件的组成与交互，以及进程与环境之间的组成与交互正 是面向开放式系统的语义才能保证我们以后提出互模拟的概念 2 在操作语义模型的基础上我们为v e r i l o g 进程建立了一个观察模型，这里观寨的含义指的是作为一 4 个外界环境在与该进程的交互过程中能够发现的现象在观察模型的基础上，我们进而成功地引入 互模拟的思想互模拟关系不仅在理论上为v e r i l o g 程序的等价性概念提供了一个比较完善的框架。 而且也在实践上为证明程序等价提供了一种有效的技术；然后我们证明互模拟关系是同余关系，这 个结果保证了互模拟关系在代数的替换规则下能够得到保持，从而使我们的操作语义模型能够为以 后的代数语义提供一个具体的模型( 把代数语义的等式关系映射到操作语义观察模型中的互模拟关 系) 注意一般的互模拟思想都是在基于管道通讯的并行语言( 如c c s ) 中被提出并运用，将它实际 运用于象v e r i l o g 这样基于共享变量通讯的复杂的并行语言时是需要很多改造以及技术处理的 3 我们给出了v e r i l o g 的代数语义，这是一个等式公理体系。它将v e r i l o g 语义特征通过代数规则简洁 准确地表达出来这些代数规则，如并行扩展规则，事件触发，状态等价规则或者与通常并行语言 相应的规则很不相同，或者在其他语言中就根本不存在它们正好反映了v e r i l o g 独有的语义特征 我们的代数语义相对于前面的操作语义模型来讲是可靠的，即所有的这些代数规则左右两边的进程 在操作语义的观察模型下都是互模拟的所以从这个角度来讲，我们的操作语义模型以及互模拟概 念是非常成功的，它为我们的推导v e r i l o g 这种复杂语言的进程代数提供了一种强有力的方法因为 从已有的工作来看 3 1 】 3 6 】【3 7 】，对于v e r i l o g 或者其他复杂的基于共享变量进行通讯的语言来讲，如 果以指称语义为基础。我们很难导出语言相应的进程代数 4 我们所提的代数语义是一套非常完整的等式规则，之所以完整，因为若参照前面所做的操作语义模 型，它相对于扩展v e r i l o g 语言的一个子集而言是完备的即所有符合这样语法的程序，如果它们是 互模拟等价的，那么它们同样可以在我们的代数系统中被推导相等在完备性证明过程中，我们采 用了范式方法即构造一种语法上特殊的程序，任何属于上述子集中的一个程序通过我们的代数规 则能够被转化为范式程序，而且语法不同的范式程序在操作语义模型下就是不互模拟的完备性工 作的进展标志着我们对v e r i l o g 语言特征的认识已经进一步完善了，因为我们不仅能通过操作语义 模型来具体描述v e r i l o g 语言的执行细节，而且对于这个模型中各进程的等价性能通过代数规则的 形式很好地刻划出来 1 5 本文结构 本文共分为六章，除本章外，其余各章组织如下： 第2 章给出了v e r i l o g 的操作语义模型，观察模型，以及互模拟等概念 第3 章给出了代数语义的所有代数规则，并对代数规则的推理运用作了详细讨论，同时对若干典型 代数规则进行了可靠性验证 第4 章研究了代数语义相对于扩展v e r i l o g 语言的一个比较小的子集的完备性从这个相对简化的 问题的讨论中我们可以得到很多有益的结论与提示，从而帮助我们第五章的讨论 第5 研究了代数语义相对于扩展v e r i l o g 语言的一个大的子集的完备性这个子集已经包含了除循 环程序外的所有v e r i l o g 应用程序 + 第6 章简要总结了本文工作后的心得体会，并阐述了对后续工作的一些设想 5 第二章v e r i l o g 的操作语义模型 2 1 引言 本章的主要任务就是研究v e r i l o g 的操作语义正如引言中所述的那样，我们希望所提出的操作语义 模型能够很好地描述以上v e r i l o g 的语言特征，并且要把v e r i l o g 的所有程序( 包括顺序以及并发程序) 作 为开放系统，用统一的观点来看待所有程序与环境交互作用的方式，进程内部各部件之间的交互方式； 然后我们希望在此操作语义模型的基础上提出相应的v e r i l o g 程序的实时观察模型，即确定一个v e r i l o g 程序的哪些行为是外部的或者说是可观察的，然后在观察模型的基础上提出相应的互模拟概念，从而导 出相应的观察等价关系观察等价性( 互模拟关系) 描述了程序间的等价关系，证明两个程序等价即是要 构造这样一个等价关系，使得这个程序对在这个关系中如果我们进一步能证明此等价关系的同余性， 则在此基础上就可以发展v e r i l o g 相应的进程代数，进而研究v e r i l o g 的代数性质 本章的其余部分组织如下，在第二节我们给出所要研究的v e r i l o g 子集部分在第3 节，我们以g o r d a n 所提出的仿真语义为基础，提出操作语义模型中的状态与相应的状态转移行为，并且提出相应的观察模 型第4 节则真正给出操作语义模型的转移系统的形式化描述第5 节则先将观察模型的各种可观察行 为进行形式化定义，然后以此为基础，定义相应的互模拟概念，以及程序的观察等价关系第6 节则对 本章的工作做了一个总结，分析了建立我们操作语义模型的核心思想为了清楚起见，我们把观察等价 关系同余性的详细证明放在了本章的最后，同时通过这个证明我们展示了利用互模拟技术证明进程等价 的技巧 2 2v e r i l o gh d l 的语法 v e r i l o g 的语法如下： p ：= = e 1 9 1 s k i p i c h a o s l s t o p p ：p l i fbp e l s ep l w h i l ebp l a l w a y sp l b e g i np e n d i p i f p 其中g 为用于事件调度的卫式控制语句，主要有，延时卫式# l x ( 为大于0 的整数) ，事件卫式 ( q ) 夕：= ( 叮) j 书 目：= v l p o s e 西ev l n e g e 由ev i a ( n 1v 7 2 vr n ) 为了代数推理的需要，我们对v e r i l o g 语言进行了相应的扩展扩展成分主要包括： 1 终止程序e 2 并行赋值语句= e ，其中2 ，e 为变量表与表达式表，并且z 与e 的长度相等 3 布尔赋值卫式语句 ( 6 = e ) 4 非事件卫式 ( ，”) 5 布尔事件卫式语句 ( 址q ) 6 与复合事件卫式语句 ( q 1a t 7 2 a ) 7 卫式选择语句g x d g 2 1 1 d g 。，其中g i = 9 或者g i = 9 - + p 8 i f 程序i f ( e lp l ，c 2p 2 ，c ，lj k ) 我们采用了非展平( u n f l a t ) 式的语法形式，并发程序可以出现在任何的嵌套，而不像展平结构那样并 发程序只能出现在语法的最外层这主要是为了定义开放式系统语义而设计的另外，除原子语句外， 复合程序可分为两大类，并发复合与顺序复合程序 6 t 我们定义p t e x t 为所有符合推理语言语法的v e r i l o g 程序集合 2 3 操作语义模型以及观察模型 2 3 1 事件调度语义与操作语义模型 我们的操作语义以文献【3 8 1 所提的仿真算法为基础，该算法是基于事件调度及传播的在某一仿真 时刻，如果系统中有若干进程处于激活状态( 即该进程的的头一条语句是能够立即执行的赋值，分支等 顺序成分，这些成分的执行是零延迟，或者是瞬时的，所以我们以后称之为瞬时动作) ，那么仿真调度程 序非确定地选择一个进程执行，并且将当前的数据状态记录下来，作为一个新的事件的起始状态，该进 程执行这些瞬时成分直至遇到卫式语句为止这时，该进程所执行的语句可能导致新的数据状态，这个 由起始数