（电路与系统专业论文）形式验证中的vhdl信息处理实现方法与技术分析.pdf

北京交通大学硕士学位论文 摘要 y 5 8 5 9 9 4 数字电路系统的设计验证方法是当前数字电路系统设计领域的一个前 沿性课题【7 j 。对设计结果的验证，特别是对a s i c 设计的验证是整个设计周 期中的一个重要环节。在设计最终成片前需要完成对整个设计的完整充分的 仿真，因为设计实现定型后，就很难以从硅片上再对系统做修正和改进和进 行随后的费时费力的整个系统的布局布线等一系列环节。随着当前的数字电 路系统规模越来越大，系统结构的复杂度越来越高，致使整个设计验证的工 作量和费用都在迅速的增长。所以采用什么样的验证的方法和技术已经成为 e d a 技术中的一个重要研究课题。 数字电路系统的设计中，一般把验证分为三个层次 7 】：第一个层次是 系统级验证，目的是保证系统设计要求与约束条件能正确体现在系统功能和 结构的设计结果中；第二层次是逻辑级检验，逻辑级验证是在系统级验证的 基础上，对已完成的逻辑综合结果进行模型检验，以确保系统状态正确，以 及所设计的逻辑结构能正确合理地实现所需要的状态：第三个层次是电路级 验证，它的目的是检查逻辑设计的电路综合结果，保证所使用的电路满足设 计要求，并且检查能否实现系统的设计要求和约束条件。 本文针对m e a l y 机结构模型研究了v h d l 设计中的模型提取技术，同 时对v h d l 语言的描述特征进行较为详细的分析。在本文最后的章节，通 过应用实例对提出的方法进行了应用说明和印证，为将来要进行的分层验证 实现提供了的基础，对功能验证和r t l 级验证起着承上启下的作用。 关键词数字电路系统、v t i d t , 、模块提取、信息提取、e d a 未经作者、导师同意 勿全文公布 北京交通太幸硕士学位论文 a b s t r a c t t h ev e r i f i c a t i o nm e t h o d o l o g yo fd i g i t a lc i r c u i td e s i g ni sc u r r e n t l ya n a d v a n c e di s s u ei nt h ed o m a i no f d i g i t a lc i r c u i ta n ds y s t e m v e r i f i c a t i o ni sa n i m p o r t a n tp a r t o f d e s i g n ，e s p e c i a l l y i n a n y a s i c d e s i g nc y c l e s i t l s i m p o r t a n tt h a tc o m p l e xd e s i g n sa r e s i m u l a t e df u l l yb e f o r ep r o t o t y p e sa r e b u i l t ，a si t r s d i f f i c u l tt of i n db u g si ns i l i c o na n dg o i n gt h r o u g ha d d i t i o n a l l a y o u tc y c l e si sc o s t l ya n d t i m ec o n s u m i n g w i t ht h em o r eb i g a n d - b i gs c a l e o fd i g i t a lc i r c u i ts y s t e ma n dt h em o r ec o m p l e xo ft h es y s t e ms t r u c t u r e ，b o t h w o r k l o a da n de x p e n d i t u r eo ft h ev e d f i c a t i o no ft h ed e s i g nr e s u l ti n c r e a s e r a p i d l y s ot h et e c h n i q u eo f v e r i f i c a t i o na r eb e c o m eac r i t i c a lr e s e a r c ht a s k i nt h ee d a t e c h n o l o g yd o m a i n c o m m o n l y ，t h ev e r i f i c a t i o n o f d i g i t a l c i r c u i t s y s t e md e s i g n w a s d i v i d e di n t ot h r e ec o r r e l a t i v el e v e l s t h ef i r s tl e v e li ss y s t e mv e r i f i c a t i o n ， w h i c hf o c u so ne n s u r i n gt h er e q u i r e m e n ta n dt h ec o n s t r a i n tc o u l dr e p r e s e n t c o r r e c t l yi nt h ef u n c t i o na n ds t r u c t u r eo fd e s i g nr e s u l to f t h ed i g i t a ls y s t e m ； t h es e c o n dl e v e lo fv e r i f i c a t i o nn a m e d l o g i cv e r i f i c a t i o n ，w h i c hp r o c e s s e s m o d e lc h e c k i n go nr e s u l to fl o g i c a ls y n t h e s i sb a s e do nt h ec o m p l e t i o no f s y s t e mv e r i f i c a t i o n ；t h e t h i r dl e v e ld o e sc h e c k i n gc i r c u i tt od e t e r m i n e w h e t h e rt h ec i r c u i ts t r u c t u r ec a ns a t i s f yt h er e q u i r e m e n ta n dc o n s t r a i n to r n o t ，w h i c hi sc a l l e dv e r i f i c a t i o no f c i r c u i tl e v e l i nt h i st h e s i s ，t h et e c h n o l o g yo fm o d e le x t r a c t i o nf r o mv h d l p r o g r a m i ss t u d i e da n dt h e d e s c r i p t i o n c h a r a c t e r i s t i c so fv h d lp r o g r a ma l e a n a l y z e di nd e t a i lb yh e a d i n ga g a i n s tm e a l y c o n s t r u c t i o nm o d e l i nt h el a s t p a r to ft h et h e s i s ，t h ee x t r a c t i o nt e c h n o l o g yw a se x p l a i n e d a n dv e r i f i e db y s o m ei n s t a n c e s ，w h i c hw i l lp r o v i d et h eb a s i so fs t u d y i n go nt h em u l t i - l e v e l a n d m u l t i l a y e rm o d e lc h e c k i n g i nv e r i f i c a t i o na u t o m a t i o nd o m a i n k e y w o r d d i g i t a lc i r c u i t $ s t e m , v h d l ，m o d e le x t r a c t i o n , i n f o r m a t i o n e x t r a c t i o n ，e d a i i 北京交通大学硕：l ：学位论文 序论 检查设计实现中所包含各种信息是否满足设计要求的过程叫做验证j 。 对于电子系统而言，验证就是要提取电路系统设计中所包含的信号、连线等 信息，并建立反映系统功能、状态、时序等特性的模型，最后通过对模型数 据的分析处理，得出设计是否正确的结论。验证存在于硬件设计的各个环节， 如果以某种方式穷尽地模拟系统每一种可能的执行情况，则可以证明( 穷尽 分析) 系统的正确性。因此，验证的目的是检查设计正确性，如果不正确， 找出设计中存在的问题或缺陷。 随着集成电路( i c ) 制造技术和计算机技术的飞速发展，主流的工艺 向着深亚微米发展，电路系统规模越来越大，集成度和控制逻辑复杂度越来 越高，片上系统设计和超大规模系统设计已成为目前和将来的发展趋势，采 用传统的基于仿真和模拟的方法对含有百万门的数字电路系统设计进行验 证已经无法满足设计的要求【1 】。s o c 实现的功能越来丰富，设计也日趋复 杂化，设计验证的工作也越来越繁重。据统计，在大多数复杂的集成电路设 计中，验证所耗费了整个设计周期的三分之二，设计过程中所需验证工程师 的人数一般是r t l 设计工程师人数的二倍【2 | 。整个设计完成时，测试向量 编码构成全部设计编码的8 0 ，验证这个瓶颈在硬件系统设计中越显突出。 因此，如何对复杂的数字系统设计有效地实现验证是目前面临的重大问题。 而对复杂数字电路系统进行验证的方法和技术也已成为了e d a 技术中一个 重要的课题。 目前，数字硬件集成电路系统验证的基本思想是提取系统设计中所包含 的功能、状态、信号及结构互连信息，建立相应的设计模型，根据设计要求 检查设计模型的正确性和规范性，所采用的绝大部分是形式化模型验证技 术。近几十年来，i c 模型的形式化验证理论、方法与技术获得了巨大的发 展，并已经成为e d a 工具的重要组成部分。 形式化验证方法为设计人员提供了与仿真验i 正j f n 的一种有效手段，来 保证设计的正确性。模型验证技术就是一种形式化验证技术，是验证有限状 态并发系统的一种自动化技术，与传统的基于仿真、模拟、测试和演绎推理 的验证方法相比有诸多优势。目前，模型检验的验证方法已经被成功的应用 于对复杂时序电路和通信协议结果的验证。 北京交通人学坝l 学位论文 在当前的s o c 和v l s i 系统设计中，大量的使用了4 i 知设计细节的第 三方i p 核，给形式化验证的进行提出了难题。针对这一实际情况提出的分 级验证技术，其基本思想是，在系统级进行功能验证和信号互联结构验证， 在模块级利用基于m e a i y 机模型检查技术进行状态验证。而根据这一基本 思想提出的系统级m f m c ( m i s s i o nf l o wm o d e lc h e c k i n g ) 【z 】验证技术， 即在系统级建立系统功能设计模型，并以任务和任务流形式描述对系统功能 设计规范，这种建立设计模型和规范的技术，初步解决了在使用第三方i p 核情况下所面临的不知设计细节的问题，并可以进行多个i p 核的系统综合 验证。 本文应用对系统设计中所包含的信号互连关系进行形式化验证的技术， 分析研究了有关的互联结构模型和具体的模型结构，同时给出了v h d l 设 计中模块、信号及互连信息的提取方法，并通过实例进行说明。 2 北京交通人学硕1 。学位论史 第1 章形式验证的基本概念与技术 测试( t e s t i n g ) 是保证设计正确性的一个手段，由于硬件系统的测试 是在加工后进行的，所以测试只能证明错误的存在而不能错误的不存在，对 于复杂的系统，进行穷举的测试也是不可能的，甚至设计一个有效的测试方 案和评价其故障的覆盖都是相当困难的 1 1 。 形式验证属于计算机科学中形式化方法的应用，它从数学上证明设计结 果是否与设计规范一致。也就是说，当你写出一个给定系统的描述后，形式 化验证可以验证的是满足这种描述的系统每一种可能的行为，精确地证明设 计的有关特性。不需要任何输入矢量就可以回答证明某种抽象模型与设计实 现的对应关系，而且由于它基于严格的数学定理，形式验证技术毫无疑问的 可以回答设计“正确”或者“不正确”，解决了基于仿真验证方法所关心的 质量问题。 1 - l 形式化方法 研究形式化方法首先要弄清它的主要研究对象，研究目的、研究方法和 研究特点。对于当今广泛应用于众多场合中的硬件系统和软件系统都有出错 的情形有严格的要求。由于硬件或软件系统出现错误而导致的系统瘫痪和崩 溃的事件时有发生。 最早的形式化方法可以说是逻辑与逻辑推理，它的目标是使推理机械 化。从广义上讲，这一目标受到许多挫折，比如说逻辑系统的不完备性 ( i n c o m p l e t e n e s s ) 、逻辑系统的不可判定性( u n d e c i d a b i l i t y ) 、自动推理 的难处理性( i n t r a c t a b i l i t y ) 。但是在一些实际应用上，逻辑方法和自动推 理起着非常大的作用。 就目前而言，形式化方法的主要研究对象是计算机系统的设计和验证。 这里的计算机系统可以是硬件系统、软件系统、嵌入式( e m b e d d e d s y s t e m ) 系统、分布式( d i s t r i b u t e ds y s t e m ) 系统、实时系统( r e a l - t i m e s y s t e m ) 、反应式系统( r e a c t i v es y s t e m ) 、混合系统( h y b r i ds y s t e m ) 等。形式化方法的最主要目的是帮助工程师构造正确、可靠和稳定的计算机 系统，形式化方法的晟基本的特点是利用数学的概念、方法和工具来解决设 计的正确性问题。形式化方法就是一些使用数学技术来进行归档、设计、分 析或验证计算机软硬件的方法。形式化方法中，数学扮演着重要的角色，它 3 北京交通大学硕i 学位论文 提供了对设计的精确描述和概念性结构，通过基于设计的计算可以预测设训 实现的行为【。 一般来说，形式化方法是具有形式语义的记号和工具来明确地表述所要 设计的计算机系统的设计要求，即给出系统规范( s p e c i f i c a 七| o n ) ，并根据 系统规范利用上述记号和工具对系统具有的性质和最终实现的正确性进行 严格的证明。 形式化方法中，使用的数学成为数学逻辑，用逻辑方式生成形式表示和 解构，其计算是基于推导的计算。这种基于数学的表示就称为形式规范语言， 概念上的逻辑结构提供了对规范的精确解释。例如，解释规范在内部是一致 的、一个规范满足另一个规范或者一个规范实现另一个规范是什么含义。对 形式规范的计算就是检查规范之间相互关系的计算，即证明个规范实现或 满足另一个规范。这种对形式规范假定定理的证明过程就称为形式验证【l 】。 1 _ 2 形式化规范和形式化验证 规范( s p e c i f i c a 七| o n ) 是明确地表达所要设计的系统及其性质的过程。 形式规范表达了系统的功能行为、定时特性或内部结构。形式规范描述利用 离散数学的概念明确地描述系统需求并作为文档，这个过程增加了对系统的 理解，消除了不一致性、模糊性和不完整性，并为之后的综合、逐步求精及 其正确性的证明建立基础并提供辅助。但是由于难以保证需求分析的完全正 确性，如何保证规范的完全正确性是对形式化方法的一个严重挑战。目前可 借助于快速原型法、运行规范( a n i m a t i o n ) 等部分地加以解决。 形式化验证比形式化规范向前迈进了一步，它对设计的系统进行分析， 以便证明系统所具有需要的性质，是一种用正式的描述技术建立设计规范 ( 要求) ，利用计算机技术自动完成验证工作的验证技术，具有传统的仿真 技术无法实现的高度自动化。随着系统设计规模的不断扩大，形式验证将逐 步成为新的主流验证技术。一般来说，形式化验证方法可以分为等价性检验 ( e q u i v a l e n c ec h e c k i n g ) 、模型检验( m o d e lc h e c k i n g ) 和定理检验 ( t h e o r e mp r o v i n g ) 方法。 等价性检验的主要目的是在一个设计经过变换之后，穷尽地检验变换前 后的功能的致性。即证明设计的变换没有产生功能的变化。这里说的变换 可以是综合、布局布线、测试、时钟树的插入、扫描链的重排序、f p g a 到 a s i c 的转换等。等价性检验的基本原理是建立被比较的两个模型之间的关 4 北京交通大学硕t 学位论史 系。检验的依据是数学的定理和公理，以及设计实现所利用的标准单元库的 精确的描述。等价性检验程序自动确定被比较的两个设计的关系，而不需要 用户的输入。它的优点是使用简单，容易集成到设计流程中。 比如，要对一个现有的门级或物理级网表写出其r t l 级模型，以使原 来的设计能够重用，这时也可以利用等价性检验。另外，如果设计者要将原 来的设计的功能进行必要的修改，等价性验证产生的信息可以用来帮助设计 者确认所做的修改是否达到了目的。如果把等价性检验同模拟集成在一起， 就可以把等价性检验得到的反例送给模拟程序进行纠错。在整个设计流程 中，最初的规范应当对于用户的要求来说是正确的，这个规范在后来一步一 步地实现和细化。每一步的实现行为都应当同前面的设计相一致。于是就可 以用等价性检验来验证这种一致性。 e m c l a r k e 等人提出的基于一种计算树逻辑( c t l ) 和有限状态机 ( f s m ) 的模型检验已经走过了十多年的艰苦历程，其基本性质是用c t l 公 式表达程序或电路的时序性质，用f s h 表示程序或电路的状态转移的抽象 的结构。通过遍历f s m 来检验时态逻辑公式的正确性。随着程序或电路规 模的增大，状态数目将呈指数增加而引起组合爆炸。它是模型验证的关键问 题。在1 9 8 7 年，利用模型识别中的次要因素及其层次结构的对称性， r k u r s h a n 提出了同态化简( h o m o m o r p h i cr e d u c t i o n ) 的方法，从而减 少了计算的复杂度。8 0 年代末，又发展出了符号模型检验和二叉判定图 b d d ( b i n a r y d e c i s i o nd i a g r a m s ) 技术。符号模型检验的含义是用一个布 尔公式表示使它满足的所用状态，而这个布尔公式则以压缩方式存储在 b d d 中，而在遍历过程中已经标识的状态也用布尔函数的b d d 表示。通 过适当排列变量的顺序可以大大简化图的结构，这使得模型检验可以处理大 规模的数据结构和控制序列，从而缓和了组合爆炸的问题。 经过上述的改进，模型检验方法目前已经达到实用化，并为工业界所接 受。模型检验的优点是完全自动化，如果设计不满足给定的性质，检验结果 可以给出反例，从而帮助设计人员找出设计错误，这一点可能是他最大的吸 引人之处。 系统及其性质可以用基于某种逻辑的形式化系统的公式表示。以形式化 系统的公理和推理规则为基础，可以逐步推导出表达系统性质的公式，从而 证明设计的系统具有该性质。当然，推导过程中往往需要反映模型的假设条 件的定义和引理。如果利用一个计算机程序来辅助手工推导过程，这个计算 5 北京交通夫学硕l 学位论文 机程序可以称为机械定理证明器。它与自动定理证明器之问构成自动化程度 不同的定理证明器。由于使用定理证明器需要较高得数学能力并要经过相当 长时i s j 的训练，因而这种验证方法的代价较高。对一般的软件开发，使用它 难以与开发进程同步。但是它能够处理具有无限状态的系统，因而具有各种 特点的定理证明系统已经成为学术、教育和工业上有力的验证工具。硬件设 计工程师也可以用它解决其他工具不能解决的问题，从而对自己的设计的正 确性有更高的把握。 1 3 形式化方法的意义和局限性 形式化方法用数学方法表达系统的规范或系统的性质，并且根据数学理 论来证明所设计的系统满足系统的规范或具有所期望的性质。在不能证明所 期望的性质时，则可能发现设计错误。实践证明，形式化方法确实通过形式 化规范和证明而增强了对系统的理解而发现了设计错误，通过形式化的自动 验证发现了用在其他方法不能发现的设计错误。因此有充分的理由说明形式 化方法是计算机系统设计验证的一条有效途径。 1 3 1 形式化方法的意义 从历史上看，形式化方法确实是来源于理论界的利用数学概念和工具来 解决程序正确性的问题所做的努力。尽管这些研究成果未能在软件生产实践 中全面推广，但是对软件工程毕竟产生了方法学方面的重大影响。后来这些 成果又在硬件设计中应用并发展，目前己取得了突破性的进展。可以认为， 形式化方法的研究路线不是传统的科学发现的模式，即“实验归纳 理论验证实验”的模式。而是“理论演绎验证实验一 佯谬论创造性思维理论”的模式。所以，从科学方法论的角度来 说，形式化方法不是学术界闭门造车的产物，而是以演绎法为主的科学研究 方法的运用。 尽管形式化方法的研究经过几十年的努力取得了很大的成绩，但是仍不 能令人满意，从而引起人们的怀疑和责难，这也是正常的现象。通过这个过 程，人们对形式化方法的局限性会有迸一步的认识。 1 3 。2 形式化方法的局限性 形式化方法不隧代替传统的方法。形式化方法所倡导的是利用严格的数 学工具形式化地表示研究的对象。这里的形式化主要是指用具有严格语义的 6 北京交通人学坝i ：学他论文 科学符号和数学系统进行描述和推驯。可见，形式化方法是种数学证明方 法，不是实验方法。因此，形式化方法在多数领域是对传统方法的补充，而 不是代替原有的方法。用模拟方法进行数字硬件的设计仍然是当前的主流， 形式化验证可以同模拟结合起来，至少作为一个有益的补充。但是我们可以 对它寄予更大的希望。 规范的正确性问题。形式化方法一个基本的概念是形式化规范，要对这 个规范进行推导和证明，也就是验证。而验证其实就是两个模型之间的比较， 我们将其中个模型作为g o l d e n 模型，另一个模型作为被检验模型。对于 功能验证而言，g o l d e n 模型就是反映用户要求的系统规范，是后续设计的 依据，被检验的模型就是以h d l 语言或者电路图输入方式所设计的逻辑模 型。但是，系统规范本身是否正确? 这可以说是一个带有致命性的问题。只 要我们不能完全保证软件和硬件的用户需求是完全一致性，验证的出发点就 可能是不正确的，这样的话，即使验证的结论为逻辑设计正确，实际结果也 会存在b u g 。所以，应当说设计和验证是一个迭代过程，有时可以在验证 的过程中发现规范的不一致和不完全的问题，这时，我们可以反过来补充和 完善规范。有时我们可以产生可执行的或“动画式”的规范，事先对规范进 行检查和考验，尽量保证规范的完全性和正确性。目前，对系统规范的描述 还没有统一的国际标准，并且不同的验证技术具有不同的描述方法。因此， 如何正确地描述系统规范是目前急需解决的一大问题。 证明的正确性问题。形式化方法主要的手段是利用定理证明程序来辅助 人们证明硬件或软件的实现达到了设计的目的。但是谁来保证这些证明程序 本身的正确性? 即使这些程序是正确的，谁来保证运行这些程序的硬件的正 确性? 因此，形式化方法并不能完全保证设计的正确性，只不过通过利用形 式化方法加强了对正确性的信心，进一步发现设错误，利用严格的手段堵塞 了可能的漏洞。它并不是解决所有问题的灵丹妙药。随着形式化方法的发展， 人们期望，在经过检验的硬件上运行经过验证的软件，逐步形成可靠性极高 的经过证明包含软件和硬件的证明系统。 模型的精确性问题。形式化规范和证明，不管它们处理的对象是硬件还 是软件，实际上是利用对象的各种模型。这些模型是否正确，是否足够准确， 这对于形式化方法的解决问题的质量和效率仍然是至关重要的。在这方面， 形式化方法和传统的方法是一样的。研究对象的建模问题是对形式化方法的 限制因素，形式化方法也必须采用和研究合适的模型。 7 北京交通_ 人学硕士学位论文 第2 章v h d l 语言分析 v h d l 语言产生于8 0 年代，它的全称是“超高速集成电路硬件描述语 言( v h s i ch a r d w a r ed e s c r i p t i o nl a n g u a g e ) ”一儿，v h d l 的结构 和方法受到e d a 语言的影响，并吸收了其它硬件描述语言的某些优点， 1 9 8 6 年3 月，i e e e 开始致力于v h d l 的标准化工作，为此，成立了审查 和完善v h d l 的标准化小组。1 9 8 7 年1 2 月，i e e e 推出了i e e es t d 1 0 7 6 1 9 8 7 。v h d l 语言成为i e e e 标准以后，很快在世界各地得到广泛 应用。1 9 9 5 年，中国国家技术监督局组织编撰并出版了c a d 通用技术 规范，推荐v h d l 作为我国电子设计自动化( e d a ) 硬件描述语言的国家 标准。 为了增强v h d l 语言的描述能力，方便设计应用，i e e e 在广泛征集各 方面意见的基础上，对i e e es t d1 0 7 6 1 9 8 7 进行了改进和扩充。修订版 与1 9 9 3 年4 月成为美国国家标准局( a n s i ) 标准。并于同年9 月被i e e e 认可为标准，即i e e es t d1 0 7 6 - 1 9 9 3 。 v h d l 已经作为最重要的一种描述和验证硬件的标准被广泛接受，并逐 步取代了原有的非标准硬件描述语言。多数电子设计自动化厂商都提供了支 持标准v h d l 综合和验证环境。现在，v h d l 和v e r i l o g 作为i e e e 工业标 准硬件描述语言，得到了众多e d a 公司的支持，已经成为了事实上的通用 硬件描述语言。 2 1v h d l 的基本技术特征 v h d l 是一种独立于实现技术的语言，它不受某一种特定工艺的束缚， 允许使用者在其范围内选择工艺和方法，为了适应未来的数字硬件技术， v h d l 还提供将新技术引入现有设计的潜力。v h d l 是一个在程序设计语言 的意义上全类型化的语言，即所有硬件部件和元件的描述必须给出明确的类 型。语言的语法分析程序可以检查描述的类型的一致性。支持硬件设计的层 次设计方法，支持从抽象的系统规范到详细的门级描述，支持以模拟为主的 验证过程。它具有丰富的数据类型、并发和顺序的语言构件，它不受某一特 定工艺的束缚，允许设计者在其使用范围内选择工艺和方法。 v h d l 语言的最大特点是描述能力极强，覆盖了逻辑设计的诸多领域和 层次，并支持众多的硬件模型。具体而言，v h d l 较其他的硬件描述语言有 8 北京交通大学硕十学位论文 如下优越之处一j ： 1 描述方式上，支持从系统级到门级电路的描述，同时也支持多层次 的混合描述：描述形式可以是结构描述，也可以是行为描述，或者 二者兼而有之； 2 设计方法上，既支持自底向上( b o t t o m - u p ) 的设计，也支持自顶向 下( t o p d o w n ) 的设计；既支持模块化设计，也支持层次化设计； 支持大规模设计的分解和设计重用； 3 既支持同步电路，也支持异步电路；既支持同步方式，也支持异步 方式； 4 既支持传输延迟，也支持惯性延迟，可以更准确地建立复杂的电路 硬件模型； 5 数据类型丰富，既支持预定义的数据类型，又支持自定义的数据类 型；v h d l 是强类型语言，设计电路的安全性好； 6 支持过程与函数的概念，有助于设计者组织描述，对行为功能进一 步分类： 7 提供了将独立的工艺集中于一个设计包的方法，便于作为标准的设 计文档保存，也便于设计资源的重用。 8 v h d l 的类属提供了向设计实体传送环境信息的能力； 9 v h d l 的断言语句可用来描述设计实体本身的约束信息，支持设计 直接在描述中书写错误和约束条件，不仅便于模拟调试，而且为综 合化简提供了重要信息。 2 2v h d l 语言的信息分类 v h d l 语言包含的语法信息是指，在编程设计中，一些经常会被使用的 v h d l 关键字、专有名词等。v h d l 语言的信息可分为如下几个方面：【1 3 】 1 设计实体和配置( d e s i g ne n t i t i e sa n dc o n f i g u r a t i o n s ) 2 子程序和包( s u b p r o g r a m sa n dp a c k a g e s ) 3 类型( t y p e s ) 4 声明( d e c l a r a t i o n s ) 5 名称命名( n a m e s ) 6 公式( e x p r e s s i o n s ) 7 顺序语句( s e q u e n t i a ls t a t e m e n t s ) q 北京交通人学坝l 。学位论文 8 并行语句( c o n c u r r e n ts t a t e m e n t s ) 9 范围可见性( s c o p ea n dv i s i b i l i t y ) 1 0 设计单元以及对之分析( d e s i g nu n i t sa n d t h e i ra n a l y s i s ) 为了能说明的清楚，在此做个约定 1 小写的单词表示一种句法范畴的词，比如 f o r m a l _ p o r t _ l i s t ， 2 黑体的单词表示v h d l 语言中的关键字，比如 e n t i t y 3 用竖线可以把等号右边的两个可选项分开。如果竖线出现在左 大括号之后，那么这条竖线不代表任何意义，将仅仅代表它本 身： e t t e ro r _ d i g i t ：= l e t t e ri d i g i t c h o i c e s ：= c h o i c e 1c h o i c e ) 4 用方括号括起来的项，表示是可选的，比如： r e t u r n _ s t a t e m e n t ：= r e t u r n 【s t a t e m e n t 】 5 用大括号括起来的项，表示会重复多次出现也可能不会出现的 项： t e r m ：= f a c t o r ( m u l t i p l y i n g _ o p e r a t o rf a c t o r ) 2 2 1 设计实体( d e s i g ne n t i t i e s ) ( 1 )实体声明( e n t i t yd e c l a r a t i o n s ) e n t i t yd e c l a r a t i o n ：= e n t i t y i d e n t i f i e ri se n t i t y _ h e a d e r b e g i n 】 1 0 北京变通犬学蹦 学位论义 e n d 【e n t i t y 】 e n t i t y _ s i m p l en a m e 】； 其【| 1 ， e n t i t y _ h e a d e r ：= f o r m a l _ p o r t _ c l au s e 】 p o r t _ c l a u s e ：= p o r t ( p o t l i s t ) ； p o r t _ l i s t ：= p o r ti n t e r f a c e _ l i s t ( 2 )结构体( a r c h i t e c t u r eb o d i e s ) a r c h i t e c t u r e b o d y ：= a r c h i t e c t u r ei d e n t i f i e ro f e n t i t y _ n a m e i s a r c h i t e c t u r e _ d e c l a r a t i v e _ p a r t b e g i n a r c h i t e c t u r es t a t e m e n l p a r t e n d 【a r c h i t e c t u r e 】 a r c h i t e c t u r e _ s i m p l e _ n a m e 】； 其中， a r c h i t e c t u r e _ d e c l a r a t i v e _ p a r t ：= ( b l o c k _ d e c l a r a t i v e _ i t e m ) a r c h i t e c t u r e _ s t a t e m e n t _ p a r t ：= p a c k a g e _ d e c l a r a t i v e _ i t e m ：= t y p e d e c l a r a t i o nl s u b t y p e _ d e c l a r a t i o ni c o n s t a n t _ d e c l a r a t i o nlu s e _ c l a u s e ( 2 ) 程序包的结构体( p a c k a g eb o d i e s ) p a c k a g e b o d y ：= 1 1 北京交通人学硕h 学位论文 p a c k a g eb o d yp a c k a g e s i m p l e n a m ei s p a c k a g e b o d y d e c l a r a t i v e p a r te n d p a c k a g eb o d y 】 p a c k a g e s i m p l e n a m e ； 其中， p a c k a g e b o d yd e c l a r a t i v e p a r t ：= p a c k a g e _ b o d y _ d e c l a r a t i v e i t e m p a c k a g e _ b o d y _ d e c l a r a t i v e i t e m ：= t y p e d e c l a r a t i o nis u b t y p e _ d e c l a r a t i o nl c o n s t a n td e c l a r a t i o ni u s ec l a u s e 2 2 3 类型( t y p e s ) ( 1 ) 标量类型( s c a l a rt y p e s ) s c a l a r _ t y p e _ d e f i n i t i o n ：= e n u m e r a t i o nt y p ed e f i n i t i o nii n t e g e r _ t y p e _ d e f i n i t i o n ( 2 ) 枚举类型( e n u m e r a t i o nt y p e s ) e n u m e r a t i o n _ t y p e _ d e f i n i t i o n ：= ( e n u m e r a t i o n l i t e r a l ( ，e n u m e r a t i o n l i t e r a l ) _ ) e n u m e r a t i o n l i t e r a l ：= i d e n t i f i e ri c h a r a c t e rl i t e r a l ( 3 ) 整数类型( i n t e g e rt y p e s ) i n t e g e r _ t y p e _ d e f i n i t i o n ：= r a n g e _ c o n s t r a i n t r a n g ec o n s t r a i n t ：= r a n g er a n g e r a n g e ：= s i m p l e _ e x p r e s s i o nd i r e c t i o ns i m p l ee x p r e s s i o n d i r e c t i o n ：= t oid o w n t o 2 2 4 声明( d e c l a r a t i o n s ) d e c l a r a t i o n ：= t y p e _ d e c l a r a t i o nl s u b t y p e _ d e c l a r a t i o n o b j e c td e c l a r a t i o ni i n t e n a c e _ d e c l a r a t i o ni e n t i t y _ d e c l a r a t i o nlp a c k a g e _ d e c l a r a t i o n ( 1 ) 类型声明( t y p ed e c l a r a t i o n s ) t y p ed e c l a r a t i o n ：= f u l l _ t y p e _ d e c l a r a t i o n f u l l _ t y p e _ d e c l a r a t i o n ：= t y p ei d e n t i f i e ri st y p e d e f i n i t i o n ； 1 2 北京交通大学硕l 学位论文 t y p e d e f i n i t i o n ：= s c a l a r _ t y p e d e f i n i t i o n ( 2 ) 子类型声明( s u b t y p ed e c l a r a t i o n s ) s u b t y p e _ d e c l a r a t i o n ：= s u b t y p ei d e n t i f i e ri s s u b t y p e i n d i c a 七i o n ； s u b t y p e _ i n d i c a t i o n ：= t y p e _ m a r k c o n s t r a i n t t y p e _ m a r k ：= t y p e _ n a m eis u b t y p e _ n a m e c o n s t r a i n t ：= r a n g e _ c o n s t r a i n t ( 3 ) 对象声明( o b j e c td e c l a r a t i o n s ) o b j e c td e c l a r a t i o n ：= c o n s t a n t _ d e c l a r a t i o nis i g n a l d e c l a r a t i o ni v a r i a b l ed e c l a r a t i o n 其中， c o n s t a n t _ d e c l a r a t i o n ：= c o n s t a n ti d e n t i f i e r _ l i s t ：s u b w p e _ i n d i c a t i o n ：= e x p r e s s i o n ； s i g n a l _ d e c l a r a t i o n ：= s i g n a li d e n t i f i e rl i s t ：s u b t y p e _ i n d i c a t i o n ：= e x p r e s s i o n 】； v a r i a b l e _ d e c l a r a t i o n ：= v a r i a b l ei d e n t i f i e r _ l i s t ：s u b w p e _ i n d i c a t i o n ：= e x p r e s s i o nj ； i n t e r f a c ed e c l a r a t i o n ：= i n t e r f a c e _ s i g n a l _ d e c l a r a t i o n i n t e r f a c e ：= s i g n a l d e c l a r a t i o n s i g n a l i d e n t i f i e r _ l i s t ： m o d e 】 s u b t y p e _ i n d i c a t i o n ：= s t a t i c _ e x p r e s s i o n m o d e ：= i nlo u t i n t e r f a c e _ l i s t ：= i n t e r f a c e _ e l e m e n t ( ；i n t e r f a c e _ e l e m e n t i n t e r f a c e _ e l e m e n t ：1 1i n t e r f a c e _ d e c l a r a t i o n 北