（电路与系统专业论文）数字系统形式设计的理论与方法研究.pdf

摘要 过去几十年来，微电子技术的高速发展和人们对信息技术的强大需求使得现代集 成电路系统的规模和复杂程度日趋提高。这必将导致对集成电路系统级的设计、制造 提出更高的要求。从目前集成电路的制造技术看，深亚微米制造技术的突破使得在单 一硅片上实现信号采集、转换、存储、处理和输入输出功能的片上系统( s y s t e m s o n c h i p ，s o c ) 成为可能。相形之下，系统级的设计就越来越成为重要的因素。提高数字 系统的设计层次、减少高层设计对象是当前集成电路设计的一个方向。但是，现有的集 成电路设计方法学和设计支撑工具并不支持抽象的高层次的设计。 另一方面，确保系统设计的正确性也是系统级设计的极大的挑战。在主要依靠设 计师自身积累的经验的情况下，现有的设计验证技术也无法有效保证系统设计的正确 性。1 9 9 4 年i n t e l 公司的p e n t i u m 芯片中的浮点除法运算错误是在其大量进入商用后才 被一位用户发现的，虽然这种错误发生的概率为几亿分之一，但这个设计错误还是为 i n t e l 公司造成4 。7 5 亿美圆的经济损失和无形的形象损失。 为了提高数字硬件的设计层次，保证数字系统设计的正确性，采用“形式化方法“ ( f o r m a lm e t h o d s ) 设计数字硬件或者集成电路系统是一种比较好的途径。所谓形式化方 法，就是利用严格的数学方法，从给出系统设计的规范( s p e c i f i c a t i o n s ) 开始并逐步地推 导或者验证系统的方法。 本文将试图研究数字系统形式设计所涉及的主要理论、方法和技术；探讨在系统级 的层次应用形式设计的可行性，并提出一种新的数字硬件形式化设计方法。 本论文的研究和创新工作主要包括以下内容： ( 1 ) 对形式设计方法所取得的成果作了详细的回顾，并讨论了形式设计过程中所用到 的理论和方法。详细论述了形式规范、程序的精化演算的作用、类型、适用范围。在此 基础上，分析了几个用形式方法设计的硬件系统。 ( 2 ) 提出了以a g e n t 组成的硬件设计的形式计算模型f c m h d ( f o r m a lc o m p u t a - t i o n a lm o d e lf o rh a r d w a r e d e s i g n ) 。这是一个基于两层的形式设计模型。该模型将简 化形式设计的过程并有效降低设计过程的复杂性。给出了f c m h d 的区间时态逻辑 ( i n t e r v a lt e m p o r a ll o g i c ，r r l ) 语义。作者以时段演算( d u r a t i o nc a l c u l u s ，d c ) 为工 具对v h d l 的子集进行了形式语义分析；通过分析v h d l 和v e r i l o g h d l 部分语句的 形式语义，为硬件描述语言的分析、设计、编译提供了一个严格的理论基础和新的途 径。同时也对本文后半部分提出新的硬件描述语言c h d l 作好准备。 i i中文摘要 ( 3 ) 提出了一个新的硬件描述语言一“基本硬件描述语言”c h d l ( c o r e h a r d w a r e d e s c d p t i o n l a n g u a g e ) 。该语言的抽象程度要稍高于目前常见的硬件描述语言，但又很 容易将其转换为常见的硬件描述语言。并给出了c h d l 的形式语义及常用的硬件的语 义：提出了把c h d l 转换为v h d l 或v e r i l o g h d l 的方法。 ( 4 ) 论述了f c m h d 的精化演算并给出了具体的精化规则；论述了i t l 的复合验 证。 ( 5 ) 运用前面讨论的理论和方法，研究了一个比较大的实例。从给出高层设计规范， 利用精化公式逐步导出设计问题的代码。 关键词：形式方法、形式设计、数字系统、集成电路设计、i n t e r v a lt e m p o r a l l o g i c a b s t r a c t i nt h el a s ts e v e r a ld e c a d e so rs o ，t h ef a s td e v e l o p i n go fm i c r o e l e c t r o n i ct e c h n o l o g y a n d g r o w i n gr e q u i r e m e n t f r o mt h ev a r i o u sk i n do fs o p h i s t i c a t e da p p l i c a t i o n sm a k et h e m o d e m i n t e g r a t e dc i r c u i t ( i c ) m o r ec o m p l i c a t e d i ns c a l ea n d f u n c t i o n a l i t y t h e s e w i l l i n e v i t a b l y l e a dt ot h e h i g h e r d e m a n d sf o r d e s i g n i n g a n d m a n u f a c t u r i n g o fi c s y s t e m s a sf a ra st h es t a t eo ft h ea r to fm a n u f a c t u r i n gi c s y s t e m s ，t h et e c h n i q u e s o fd e e p 。 s u b m i c r o nm a k ei tp o s s i b l et oi m p l e m e n tf u n c t i o n so f s i g n a ls a m p l i n g ，c o n v e r t i n g ，s t o r - i n g ，m a n i p u l a t i n g w i t h i nas i n g l ec h i pw h i c hi sc a l l e ds y s t e m s o n c h i p ( s o c ) h e n c e t h es o - c a n e d “d e s i g np r o d u c t i v i t yg a p ”w h i c ho u ra b i l i t yt od e s i g nc o m p l e xi n t e g r a t e d c i r c u i t sw a sf o u n dt ob e l a g g i n g t h et e c h n o l o g y s c a p a b i l i t ya p p e a m t h e m o s t o b v i o u ss o l u t i o nf o rc l o s i n gt h i sg a pi st or a i s et h el e v e lo fa b s t r a c t i o ni nd e s i g n d ot h ed e s i g nm e t h o d o l o g ya n dd e v e l o p m e n tt o o l sw eu s et o d a yw i l lm e e tt h e n e e do f d e s i g n a b s t r a c t i o na f t e rr a i s i n gt h ed e s i g nl e v e l ? t h ea n s w e ri sp r o b a b l yn o t o n t h e a n o t h e r h a n d s ，b e c a u s e o f t h e i n c r e a s e i n c o m p l e x i t y o f h a r d w a r e ，t h e s u b t l e e r r o r si sm u c h g r e a t e r h o w c a nw e g u a r a n t e e t h ec o r r e c t n e s so f d e s i g n ? o n e w a y o f a c h i e v i n g t h e s e g o a l s i s b y u s i n g f o r m a l m e t h o d s , w h i c h a r e m a t h e m a t i c a l l yb a s e dl a n g u a g e s ，t e c h n i q u e s ，a n d t o o l sf o r s p e c i f y i n g a n d v e r i f y i n g s u c h s y s t e m s t h e s em e t h o d s b e g i n w i t ht h ef o r m a ld e s i g n s p e c i f i c a t i o n sg i v e nb y t h ed e s i g n e ra n d t h e nd e r i v et h et o p d e s i g n c o d e s b yu s i n g r e f i n e m e n tc a l c u l u sl a w s t h i s d i s s e r t a t i o n e x p l o r e s t h e p o s s i b i l i t y o f f o r m a l m e t h o d o l o g y a t t h e h i g h e s t l e v e l o fd e s i g no fd i g i t a lh a r d w a r eo ri ca n dc o v e r ss e v e r a lt o p i c ss u c ha sf o r m a ls p e c i f i c a t i o n s ，t e m p o r a ll o g i c , r e f i n e m e n tc a l c u l u s a n df o r m a ls e m a n t i c so fh d l ( h a r d w a r e d e s c r i p t i o nl a n g u a g e ) t h e t h e s i si so r g a n i z e da sf o l l o w s ： ( 1 ) l o o k sb a c k t h e p r o g r e s s a c h i e v e d b y t h ef o r m a l d e s i g n o fs o f t w a r eo r h a r d w a r e ， a n dc o v e r st h ef o u n d a t i o n sf o rf o r m a ld e s i g n , p r e s e n t san e wt w o q e v e lf o r m a l d e s i g n m e t h o d ( 2 ) p r e s e n t st h ef o r m a ls e m a n t i c so fv h d l i nd c ( d u r a t i o n c a l c u l u s ) ( 3 ) d i s c u s s e st h ef o r m a l s p e c i f i c a t i o n s f o rh a r d w a r ef o r m a l d e s i g n a n d p r e s e n t s t h e f o r m a lm o d e lo ff c m h d ( f o r m a l c o m p u t a t i o n a l m o d e lf o rh a r d w a r e d e s i g n ) a n d i t s f o r m a ls e m a n t i c sb a s e do n i t l ( i n t e r v a lt e m p o r a l l o g i c ) i l i i v 婪文摘辱 ( 4 ) p r e s e n t san e w k i n do fh d l c h d l ( c o r e h d l ) a n d g i v e s i t ss e m a n t i c si n f c m h d ( 5 ) g i v e s t h er e f i n e m e n tl a w sf o rf c m h da n d t r a n s f o r m a t i o nf r o mc h d lt ov h d l o r v e r i l o g h d l ( 6 ) e n d su pw i t ha l a r g ee x a m p l e o nt h eb a s eo ft h et h e o r i e sa n dm e t h o d s d i s c u s s e d i nt h ef o r m e r c h a p t e r s k e y w o r d s ：f o r m a l m e t h o d s , f o r m a l d e s i g n ，d i g i t a ls y s t e m s , d e s i g no f i n t e g r a t e d c i r c u i t s , i n t e r v a lt e m p o r a l l o g i c 第1 章引言 1 1系统级设计的挑战 过去几十年来，微电子技术的高速发展所取得的巨大成就和人们对信息技术的强大 需求使得现代集成电路系统的规模和复杂程度日趋提高。这必将导致对未来集成电路系 统的设计、制造提出更高的要求。从目前集成电路的制造技术看，深亚微米制造技术的 突破使得在单一硅片上实现信号采集、转换、存储、处理和输入输出功能的片上系统 ( s y s t e m s o n c h i p ，s o c ) 成为可能。相形之下，集成电路系统级的设计就越来越成为重 要的因素。 有关研究表明【1 l ，最近2 0 年来，集成电路芯片每片上的晶体管的数量每年增长 5 8 ，而相应时间内的设计生产力如果以每个设计师每天设计的晶体管的数量衡量， 只增长了2 1 。该结果将导致在集成电路设计制造业中出现所谓“生产创造力的鸿沟” ( p r o d u c t i v i t yg a p ) 或所谓”设计瓶颈”问题，即出现相对发展缓慢的集成电路的设计能力 落后于先进的集成电路制造技术的现象，设计师将不能有效地在相对短的时间内设计出 各种产品从而无法参与激烈的市场竞争。 文献f 1 】提出了解决以上问题的3 条途径： ( 1 ) 提升系统设计的抽象层次，压缩设计对象的数目。这样，就必须相应地提高设计 规范、体系结构、工具、设计方法学的抽象层次，开发更高层次的设计规范语言、实现 模型以及验证技术。 ( 2 ) 采用设计可重用部件。在系统级设计上尽可能采用知识产权( i n t e l l e c t u a l p r o p e r t i e s 。i p ) 部件，充分利用已有的设计成果。 ( 3 ) 采用系统级综合的方法。直接从系统级的规范进行综合。根据设计规范的要求， 把规范划分为若干组需求并将每组综合为定制或半定制的硬件。在确立了系统结构 1 以后验证该结构是否符合系统规范。最后，编译成代码进而生成定制的实时操作系统 ( r e a l t i m eo p e r a t i n gs y s t e m ，r t o s ) 。 近年来所谓“嵌入式系统”( e m b e d d e ds y s t e m s ) 得到了广泛的应用。所谓嵌入式 系统，就是执行专用功能、但其内部包含了用户所看不见的计算机控制的设备或者系 统【2 1 。 在这样的包含了内嵌软件的软硬件混合系统( h a r d w a r e s o f t w a r e ，h w s w ) 中， 各部件之间的关系或者是同质的( h o m o g e n e o u s ) 或者是非同质的( h e t e r o g e n e o u s ) ，因 此所需要的设计方法将更为困难和复杂。 在嵌入式系统设计过程中，软硬件的边界划分是一个关键的技术 2 1 。如果在设计阶 段过早地对系统的实现进行划分。将导致设计成本增加、设计时间延长。近年来提出的 软硬件的协同设计( h a r d w a r e s o f t w a r ec o d e s i g n ) 的方法就是通过软、硬件的并行设计 达到满足系统设计的目标。并行设计的主要思想是从高层开始建立系统级的抽象行为规 范。详见文献【3 ，4 ，5 】。 从以上分析可见，无论是解决集成电路设计瓶颈问题还是满足软硬件混合系统协同 设计的需要，都要求提高集成电路设计的层次、增加设计的抽象程度。这一要求从目前 集成电路设计的典型流程【6 】来看( 见图1 1 ) ，相当于把设计层次提高到系统级( 或行为设 计级) 。 图1 1 ：集成电路设计流程 当我们提高了数字系统( 或集成电路系统) 的设计层次以后，目前所用的设计方法 学、设计支撑工具等是否还适用? 我们作如下的分析。首先，对于数字系统的行为级而 浙江大学博士学位论文 3 言，一方面，用硬件描述语言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 s ，h d l ) 描述是不合适 的( 原因详见第4 章) ；另一方面，目前的数字系统设计的现状是，系统级的行为描述基 本停留在使用自然语言的阶段【z8 1 。显然，这样的行为描述缺乏严格性、完整性，无疑 是不合适的；其次，无论是这一层次的设计方法学还是设计支撑工具都还是非常缺乏 的1 9 】。这是因为，更高层次的设计规范语言、实现模型以及验证技术的开发都将极大地 依赖于严格的数学方法，尤其是以形式语义及形式规范为主要特征的形式方法。这就要 求研究与开发能够适应系统级设计的理论、设计方法学、设计支撑工具。 另一方面，由于数字硬件系统( 或集成电路系统) 复杂性的快速增长，如何确保系统 设计的正确性也是系统级设计面临的极大的挑战。在主要依靠设计师自身积累的经验的 情况下，现有的设计验证技术也无法有效保证系统设计的正确性。据报道1 1 0 ，”1 ，1 9 9 4 年，i n t e l 公司的p e n t i u m 芯片中的浮点除法运算错误是在其大量进入商用后才被一位 用户发现的，虽然这种错误发生的概率为几亿分之一，但这个设计错误还是为i n t e l 公 司造成4 7 5 亿美圆的经济损失和无形的形象损失。 研究适合于系统级设计的理论，开发新的、适合于系统级设计的工具，不断提高设 计正确性的课题吸引了学者、设计师、生产厂商的大量研究，也进行了许多有益的实践 和验证。其中一个方法就是采用“形式化方法”( f o r m a lm e t h o d s ) 。所谓形式化方法，就 是利用严格的数学方法，给出系统设计的规范( s p e c i f i c a t i o n s ) 逐步地推导或者验证系统 的方法。 1 2 传统的数字系统设计技术 传统的工业设计技术( 包括数字系统的设计) 过程首先是建立相应的数学模型；然后 用数值计算各项参数；在与设计目标反复比较过程中修改或完善这个数学模型。例如， 航空工程师在设计某个飞行器时利用计算流体动力学建立该飞行器的数学模型；经计算 后把结果与预期的相比较，从而修改这个数学模型。这个过程反复进行，直至对结果与 预期的一致。 在数字系统的传统设计中，布尔代数是主要的理论基础或数学模型1 1 2 3 1 。设计者根 据设计的要求写出系统的输入、输出表达式或者状态图，然后采用真值表、卡诺图进行 化简，如果是时序电路，还需要进行状态分配和指定触发器的激励函数，从而得到所需 的数字系统。 对于数字系统的设计师来说系统设计规范( s p e c i f i c a t i o n ) 并不是新鲜的概念。以 集成电路设计领域为例。系统的设计规范包括系统的功能、性能和物理尺寸。此外，集 成电路设计过程中还需考虑选择什么样的设计模式和制造工艺，以最终确定芯片的尺 4第1 章引言 寸、工作速度、功耗和系统功能。 上述的参数计算早期是用手工或简单计算工具完成的。随着计算机辅助设计的应 用，设计领域中出现了许多求解数学模型计算机算法；比如，一些方程的数值解已经无 须人工干预即可在计算机上进行。类似地，现代的电路c a d 工具也能够取代设计师完 成以前需要人工操作的、烦琐的状态化简、状态分配的过程。不可否认，把模型数学化 的做法本身就是一种形式化的过程，数学模型的计算机的算法也是形式化的手段。但 是，请注意，无论在飞行器设计还是在数字系统设计的过程中，如果没有把整个被设计 的对象的行为描述完全数学化( 即形式化) 那么计算机在这里只是起到辅助设计，其设 计方法也不属于形式方法。 传统的设计方法有以下几个方面的弱点： 1 传统的规范缺乏精确的形式语义定义。如前所述，传统的硬件设计方法主要依赖 于经典数学，而经典数学中基本不考虑如何用符号的方法描述时间和系统构造的动态性 质。例如，建立在经典的布尔代数、状态图基础上的硬件设计方法没有能力描述系统中 各种事件复杂的时序关系，也不会考虑系统级的动态的并发特征。 2 系统设计位于底层或趋于较低层。这是因为从函数的角度看，在传统设计过 程中，设计规范和设计对象之间是一种一一对应( o n e - t o o n ec o r r e s p o n d e n c e ) 或双射 ( b i j e c t i o n ) 关系，即一对一( o n e - t o o n e ) 且映上( o n t o ) 的映射关系，两者之间并不存在 冗余的信息。这种关系一方面对设计者而言很容易把握设计对象的特点和性质，但另一 方面也使设计者在系统日趋庞大和复杂的情况下很难看到整个系统的全貌，从而不能承 担复杂系统的有效设计，延误了市场竞争的最佳时机。 1 3 形式方法 如何寻找新技术的突破点? 近代计算机体系结构的理论和实践表明，软件与硬件的 分界线渐趋模糊。许多原来用硬件的设计可以代之以软件，反之亦然。在数字电子计算 机中，硬件代表了实体部件的结构与互相联系，而软件的主体就是程序，它更多地反映 了展现给用户的计算机行为或者功能的能力。对纯粹的硬件设计师而言，这说明了有必 要更多地从行为或者功能的角度观察和设计数字硬件。 h d l 的使用为硬件设计师提供了一个非常好的分析和设计数字硬件的工具，也为 沟通软件和硬件提供了一种方法。然而，这些h d l 一般是为模拟数字硬件的功能而设 计，缺乏对数字硬件推理和证明的机制；对行为描述的能力较弱( 通常只能用输人输出 的关系描述硬件的行为) ；缺乏形式设计或验证的支持工具。 堑兰奎堂壁圭堂竺鲨塞 ! 1 3 1 形式方法概述 与上述传统的设计方法或者单纯利用h d l 设计工具的设计方法不同，这里的“形式 方法”是指建立在一组严格的数学基础和分析之上的技术。尤其是，它利用了非传统数 学的工具( 如时态逻辑等概念) 。它最初来源于软件工程领域。计算机科学技术百科全 书对”形式方法”的定义是i “】： “建立在严格数学基础上的软件开发方法。软件开发的全过程中，从需求分析、规 范、设计、编程、系统集成、测试、文档生成、直至维护各个阶段。凡是采用严格的数 学语言。具有精确的数学语义的方法，都称为形式方法。” 在软件设计与研制中采用形式方法，可以追溯到1 9 5 0 年代后期对于程序设计师语 言编译技术的研究。当时j b a c k u s 提出了b n f ( b a c k u sn o r m a lf o r m ，巴克斯范式) 记 法作为描述程序设计语言语法的元语言t 。 形式方法的一个重要研究内容是形式规范( f o r m a ls p e c i f i c a t i o n ) ，即使用具有精确 语义的形式语言书写的程序功能描述。一旦给出系统的形式规范，就可以推断它是否具 有某种性质。这些性质虽然并不是规范的一部分但由于规范是形式的，所以可以在相 应的形式推理系统中由推导得到。如果用却e c ，p 和s y s 分别表示规范、性质和程序， 用卜和 分别表示推导和满足关系，并假定所用的推理系统是可靠的，那么从 跏e c 卜p 与s y s s p e c 就知道 s y s p 换言之只要规范具有性质p ，则任何正确地实现了该规范的程序都满足尸。这就保证 从设计规范开始到最终阶段，最大限度地避免了设计过程中可能出现的错误。 这里我们试图给出数字电路系统的形式设计的定义如下： 定义1 1 ：建立在严格教学基础上的硬件设计方法。在设计的全过程中，从需求分 析、规范、设计、到推导阶段都采用严格的数学语言，并且具有精确的数学语义的方 法。最后给出的是被设计系统的硬件描述语言( h d l ) 的代码。 形式方法的特点是：把设计集中在系统的最高层次，而不是过早地拘泥于具体的设 计细节问题，这样可以大大缩短设计时间；基于形式方法的设计还可以充分借鉴软件的 形式设计方法，并且能够采用如同编制高级程序设计语言那样的工作方式。 。精确描述程序设计语言的语法的一种形式系统见文献【1 5 ，1 6 】 t 在讨论语言系统时，通常要涉及到2 种语言。一是被讨论的语言，它可称为对象语言；另一是讨论对 象语言时所用的语言，可以称为元语言。两者通常不在一个层次。 6 第1 章引言 试想，如果我们从描述系统级的设计规范开始，运用严格的数学推导的办法，在计 算机系统的支持下，把系统规范逐步精化成为具体的硬件描述语言。在未来，人们将 开发从系统级到算法级的c a d 工具。到那时，系统级设计的瓶颈将可能得到解决；同 时，设计的正确性问题也能有效地得到保证。 我们可以乐观地认为，以形式规范及形式语义学为主要内容的形式设计方法将带来 数字系统硬件方法学上的革命性变化，它将有力地冲击把硬件与软件分别对待的传统观 念，并将极大地提高集成电路c a d 的工作效率。 1 3 ：2 形式方法在数字硬件系统中的应用 尽管形式技术在软件工程领域已经早已得到应用但形式方法在数字硬件系统的应 用是一项全新的技术。一般而言，它可以分为两类，即：形式设计与形式验证。 1 _ 形式设计( f o r m a ld e s i g n ) 数字系统的形式设计的主要思想来源于计算机科学对程序尤其是并发程序可以转换 为电路的核心概念。在系统设计的早期阶段就采用形式方法，而不是象传统设计那样， 在设计阶段的后期在寄存器传输级( r e g i s t e r t r a n s f e rl e v e l ，r t l ) 进行验证，如果不符合 要求，重新开始前端设计。 一个系统设计过程可以看作是把一个设计规范经过一系列的转换步骤成系统实现的 过程。具体地，基于形式方法的设计应当包括以下几个方面： 功能规范。用严格的数学方法描写系统或者子系统的行为功能； 形式系统。一组关于输入、输出、状态之间的关系的性质； 设计约束。设计中必须满足的一些要求。 整个设计过程是：从功能规范出发，把它作为最高层的抽象，然后运用精化 ( r e f i n e m e n t ) 技术，将高层行为规范逐步具体化为比较低层的实现。文献【2 】对此有详细 的阐述。 事实上，在系统的高层，硬件和软件是没有区别的。我们完全可以利用软件设计中 的形式方法进行硬件设计。 2 形式验证( f o r m a lv e r i f i c a t i o n ) 形式验证技术是一种根据逻辑设计的功能和结构的描述，用类似定理证明的方法或 数学的方法来证明逻辑设计正确性的技术。与形式设计的情况不同的是，目前形式验证 技术是一个研究的热点，它的理论和实践不仅在数字电路中有极大的实用性，也引起了 计算机科学理论和软件等学科不少学者的注意，并且有相当好的前景。 传统的集成电路设计只能对它进行在指定环境下的模拟验证。 浙江大学博士学位论文 然而，这种模拟验证技术至少存在着以下2 方面的缺点： ( 1 ) 模拟验证是一项非常耗时的工作。 ( 2 ) 不管如何设计模拟验证的环境，其验证的范围总是有限的，不可能穷尽所有的实 际情况。 所以这种方法已经越来越不适应于目前的工业生产的实际。 w a g n e r l l 7 1 在1 9 7 7 年首先利用一阶逻辑定理证明系统f o l ( f i r s t o r d e r l o g i c ) ，用基 于符号处理的形式推理方法，成功地对一些计数器、寄存器和一个8 位的乘法器等部件 进行了验证。 继w a g n e r 之后，出现了许多新的形式验证系统。例如，h u n t l l 8 1 9 1 运用b o y e r - m o o r e 定理证明器验证了微处理器f m 8 5 0 1 ，其高层次描述用b o y e r - m o o r e 逻辑描述形 式以指令级给出，低层次以门级给出。 英国学者m j c g o r d o n t 如1 利用高阶逻辑h o l ( h i 【g h e r o r d e r l o g i c ) g 寸数字系统的形 式验证作出了贡献。 目前主要存在着以下几种形式验证的技术。 ( 1 ) 模型检验( m o d e lc h e c k i n g ) 首先把验证对象的有限状态变化抽取出来。然后利用搜索技术对状态空间进行检 查，验证是否满足特定的规范( s p e c i f i c a t i o n ) 。 ( 2 ) 定理证明( t h e o r e mp r o v i n g ) 这是一种基于人工智能的技术。 关于较为完整的形式验证技术的综述，请见【2 1 ，2 2 。 两种技术虽然不同。但两者之间存在着不可分割的关系。首先，它们都涉及形式规 范的选择、使用的问题；其次，在形式设计的过程中，可以要求使用形式验证技术来保 证设计的正确性。 1 3 3 形式方法成功的范例 总体上，对形式设计的理论和实践研究较少，运用形式设计的硬件设计的范例不 多。下面仅例举近年来有一些值得一提的设计形式方法在工业界的应用。 1 i b m 公司a s c ib l u e 超级计算机的c a c h e 协议的形式设计 i b m 公司已经成功应用形式方法设计了a s c ib l u e 超级计算机口3 】中c a c h e 存储器 协议控制器。a s c ib l u e 是为美国能源部所属l a w r e n c el i v e r m o r e 国家实验室开发的 系列超级计算机之一。它具有5 1 2 个节点。每个节点包含8 _ 1 6 个处理器。在1 9 9 9 年1 1 8第1 章引言 月的世界超级计算机5 0 0 强排名中位于第2 位+ 。 传统上，c a c h e 存储器协议的方法是从设计协议表格开始然后再转化成逻辑表达 式。这样做的缺点是这类表格表示的需求不准确，而且因为其结构比较复杂在转化时可 能引出一些错误。采用了形式化方法后，设计分为3 层，即高层、流水线层和逻辑层； 各层都建立了相应的形式模型；并利用形式验证系统m u r p h i 对高层和流水线层进行模 型检验。这些措施的使用取得了较好的效果，逻辑层的设计提前完成，并且很少有错误 发生。文献【2 4 】也阐述了这方面的应用。 2 微处理器的形式验证 1 9 9 1 年b o y e r 和y u 针对m o t o r o l a6 8 0 2 0 微处理器设计了一种形式验证所需的规 范瞄1 。他们使用这些规范证明了许多来自高级语言编译器产生的2 进制的机器代码的正 确性。 1 9 9 5 年a p p e n z e l l e r 和k u e h l m a n n 报导了形式方法在p o w e r p c 微处理器设计中 的应用伫6 l 。在设计的顶层，使用v h d l 描述r t l 级的设计规范，而管级的实现则应用 了v e r i t y 形式验证工具【2 7 l 以保证与其设计规范的等价。 1 3 4 形式设计方法与有关概念的区别与联系 从上面关于数字系统形式设计的概念可见，形式设计的主要任务是从用户的需求开 始，用严格的形式语言描述需求，进而使用一系列的精化的方法推导出能满足用户需求 的系统的实现代码或者其他形式的结果。除了满足数字硬件设计以外，还可望应用于 s o c 或h w s w 系统级的设计和精化。 规范与形式规范的联系与区别：共同点：均可表示对系统设计的要求。区别：常见 的数字系统规范所使用的形式可以是布尔表达式、波形、卡诺图、甚至是自然语言；形 式规范的形式一般是逻辑表达式，包括经典的命题逻辑、一阶逻辑、模态逻辑、高阶逻 辑，最常见的可能是时态逻辑( 一种特殊的模态逻辑) 及其众多的变形，如分枝逻辑、线 形时态逻辑( 详见第2 章) 。形式规范所表示的抽象能力大于一般的规范。 硅编译器：硅编译器是一种把数字电路行为级描述直接转换为硅芯片掩膜版图的设 计技术，其转换过程类似于软件编译器，将高级语言转换成机器语言。硅编译的基本思 想就是把v s i 设计的知识算法化，通过翻译程序把高级描述直接地自动地翻译成相应 的几何掩膜设计。 系统的行为级综合：从描述系统的代码开始，直接把代码生成相应的电路或模块。 见h t t p ：w w w t o p s 0 0 o r g 1 i s t 1 9 9 9 1 1 浙江大学博士学位论文 9 1 4 本文的研究动机、目标和范围 虽然数字硬件的形式设计的思想早已存在，并有一些理论与实际工作者的不断研究 成果的积累。但长期以来，由于种种原因，形式方法、尤其是数字硬件的形式设计的理 论及方法都是研究的“冷门”，这些现象对于当前亟待发展的集成电路的系统新的设计方 法是极为不利的。 为了研究集成电路的高层的行为抽象，保证数字系统设计的正确性，本文将试图研 究数字系统形式设计所涉及的主要理论、方法和技术；探讨在系统级的层次应用形式设 计的可行性，并将提出一种新的数字硬件形式化设计方法。 这些理论适用于v l s i 设计的系统设计到功能设计的阶段。在这一阶段，设计师主 要的任务就是按照系统的需求完成系统的功能设计。 超大规模集成电路的设计是形式设计的原始需求，这种需求极大地促进了形式设计 的理论和实践的发展。但是形式设计的理论与实践的应用并不仅仅局限子集成电路设 计本身。本文的研究目标、和结果对普通的数字电路系统也是适合的。 由于本文定位在数字硬件的形式设计。因此，本文的讨论范围是形式设计的主要原 理和方法，但并不涉及嵌入式系统设计或者h w s w 系统设计的具体方法。 1 5 作者获得的主要成果 1 提出了应用于数字系统的形式设计的计算模型f c m h d ( f o r m a lc o m p u t a t i o n a l m o d e lf o rh a r d w a r e d e s i g n ) 。这是一个基于两层的形式设计模型。给出了f c m h d 的 区间时态逻辑( i n t e r v a lt e m p o r a ll o g i c ，i t l ) 语义。 2 以时段演算( d u r a t i o nc a l c u l u s ，d c ) 为工具对v h d l 的子集进行了形式语义分 析；通过分析v h d l 和v e r i l o g h d l 部分语句的形式语义，为硬件描述语言的分析、 设计、编译提供了一个严格的理论基础和新的途径。同时也对本文后半部分提出新的硬 件描述语言c h d l 作好准备。 3 针对目前形式设计过程中存在的问题提出了两层形式设计方法。该方法对于简化 形式设计的过程将有效降低设计过程的复杂性。 4 提出了“基本硬件描述语言”c h d l ( c o r eh a r d w a r ed e s c r i p t i o nl a n g u a g e ) ，该语 言的抽象程度要稍高于目前常见的硬件描述语言，但又很容易将其转换为常见的硬件 描述语言。并给出了c h d l 的形式语义及常用的硬件的语义；提出了把c h d l 转换为 v h d l 或v e r i l o g h d l 的方法。 5 论述了f c m h d 的精化演算并给出了具体的精化规则；论述了i t l 的复合验证。 1 0第1 章引言 6 运用前面讨论的理论和方法，研究了一个比较大的实例。从给出高层设计规范， 利用精化公式逐步导出设计问题的代码。 1 6 本文的组织结构 第1 章为序言，第2 章主要对目前数字集成电路形式设计中形式化方法作一个详尽 的回顾；第3 章针对目前的形式方法的缺点提出作者的新方案。第4 章将讨论f c m h d 形式系统的形式语义；第5 章将讨论f c m h d 系统的精化演算及其规则；第6 章讨论 f c m h d 系统的其他形式设计途径。在第7 章作者给出了一个完整的实例。最后一章给 出了本文的总结，并指出了未来研究的方向。以下是关于各章内容的较为详细的介绍： 第2 章首先介绍数字系统形式设计的早期研究成果，以期对读者有启发作用。之 后，主要对全文所用的形式设计方法的各种逻辑系统、形式规范、精化演算等主要概念 做了系统的回顾；在此基础上，较为详细地分析了几种有关数字系统形式设计的理论和 方法以及它们的特点，以期为后继的章节作一个铺垫。 从第3 章开始，论文将着重讨论作者提出的f c m h d 形式系统的定义。首先，在第 3 章给出作者提出的f c m h d 形式系统在区间时态逻辑( i t l ) 下的形式语义。为了使本 文结果更为一般化，作者提出了比一般硬件设计语言更抽象的所谓“基本硬件描述语言” c h d l 。 第4 章，作者提出两层的形式设计方法。在该方法中，先提出满足设计要求的形 式设计规范然后形式设计规范将被为精化为若干个f c m h d 语句；接着进行第2 次 精化：即把用f c m h d 的代码迸一步精化为c h d l 代码。在这一章中，前面的内容是 使用f c m h d 对c h d l 的各种语句进行形式语义分析，后面的内容主要讨论如何把 c h d l 转换为一般的h d l o 第5 章作者对所用到的精化演算进行了实时的扩充。提出了精化演算的若干条规 则。这些精化规则对于后继章节的形式设计是非常重要的，也是根本的。 接着在第6 章，作者对一个比较大的实例进行了研究。首先根据要求我们提出了它 的设计形式规范，在此基础上利用第3 、4 章提出的f c m h d 计算模型和c h d l 对形式 规范进行精化，逐步推导出接近实际使用的h d l 的代码。 在最后一章，作者对全文所提到的模型与理论进行了简要的总结，指出了其不足之 处；同时还展望了今后的工作。 51 7 本章小结 本章首先分析了现代集成电路中系统级设计所要遇到的2 个挑战，即设计能力落后 浙江大学博士学位论文 1 1 于制造能力；如何确保系统设计的正确性。通过分析可以知道，首先，无论是解决集成 电路设计瓶颈问题，还是满足软硬件混合系统协同设计的需要，都要求提高系统设计的 层次；其次，系统的复杂性对系统级设计的正确性提出了一个极大的挑战。同样，在一 个含有集成电路的复杂系统或者h w s w 内部，作为硬件的设计正确性以及其验证对 整个系统的可靠性具有决定性的意义。形式方法是一种严格的系统方法，其基础建立在 精确的语义模型上，并采取逐步精化系统设计规范的方法，最终推导出系统的h d l 的 描述。 第2 章基于形式方法的系统研究 如前一章所述，对数字硬件的形式设计的需求来自于2 0 世纪9 0 年代的s o c 与 h w s w 的设计，但其基本思想应该还可以追溯到更早些时候。从文献的研究内容及取 得的成果看，其主题较为分散，而且大多来自于计算机科学。为叙述方便，以下我们按 照对形式设计研究的内容主题的不同而分为4 条线索。 2 1 形式设计方法的历史回顾 第1 条线索是对计算机程序和电路关系的研究。早在1 9 7 8 年，著名计算机科学家 c a r h o a r e 就在其关于c s p ( c o m m u n i c a t i n gs e q u e n t i a lp r o c e s s ，通信顺序进程) 的 重要文献 2 8 】中把电路作为研究并发程序的例子。接着在8 0 年代中期，就出现了对程序 直接转换为电路的研究。据作者所知，这可以认为是数字硬件的形式化设计的最早的文 献。在这个时期，美国加州理工学院( c a l i f o m i ai n s t i t u t eo ft e c h n o l o g y ) 的学者a l a i n j m a r t i n 和s t e v e nm b u r n s 发表了有关将计算机的并发程序直接转换为电路或集成电 路的研究成果1 2 9 , 3 0 ；近年来又有学者提出了利用代数精化方法直接把设计需求规范转换 为现场可编程门阵列( f i l e dp r o g r a m m i n gg a t ea r r a y s ，f p g a ) 实现1 3 1 】。后来，出现了 对s d l 等系统规范语言的研究，并提出了把用s d l 转换为v h d l 程序i “。 第2 条线索可以回顾到对实时控制程序系统的需求的形式规范的描述。1 9 8 9 年欧洲 的p r o c o s ( p r o v a b l y c o r r e c t s y s t e m s ) 项目的目标是要寻求一种”可证实正确的系统