数字系统设计及VHDL实践专题讲座模拟验证与课件.ppt

《数字系统设计及VHDL实践专题讲座模拟验证与课件.ppt》由会员分享，可在线阅读，更多相关《数字系统设计及VHDL实践专题讲座模拟验证与课件.ppt（59页珍藏版）》请在三一办公上搜索。

1、数字系统设计及VHDL实践,专题一 模拟验证与形式验证,模拟验证与形式验证,学习目标： 主要学习模拟验证的模型和算法问题，包括逻辑模拟算法和VHDL模拟算法。要求深入掌握逻辑模拟的概念、模型与算法，掌握VHDL模拟的基本思想，了解VHDL进程模拟算法与层次式模拟算法。,难点重点：,1. 模拟验证概念与模拟过程,2. 逻辑模拟模型,3. 事件驱动模拟算法,4. VHDL模拟模型,5. 进程模拟算法,模拟验证与形式验证,本章主要内容：,一、模拟验证,1.1 模拟验证概述,1.2 逻辑模拟算法,1.3 VHDL模拟,二、形式验证,模拟验证概述,1.验证的重要性,2.三种验证方法,3.模拟系统的构成,

2、4.逻辑模拟过程,验证的重要性,由于集成电路规模增大，单个芯片已经可以包含整个电路系统，因此设计过程的复杂性迅速增加。解决电路设计复杂性的一种方法是进行层次化设计。这种方法从系统级、行为级、寄存器传输级、功能级、门级以及开关级等不同的级别对设计进行描述，每级还可以细化为许多层次，使得设计对象逐级细化。在如此广阔的设计领域里，每个步骤都有可能发生错误。验证作为保证设计正确性的主要手段，其重要性是不言而喻的，而且，设计人员希望越早发现错误越好，如果要到版图级验证时才发现错误，所造成的损失将是十分巨大的。开发适合于各个设计阶段和设计层次的验证工具，帮助设计人员尽早发现和排除错误，是EDA的一个重要研

3、究课题。在目前流行的设计方法和实际设计流程中，设计正确性的验证通常采用的是模拟验证方法（Simulation Verification Method）。所谓模拟验证，是指从电路描述（语言描述或图形描述）中提取出模型，然后将外部激励信号或数据施加于该模型，进行计算并观察输出结果，判断该电路描述是否实现了预期的功能 。,三种验证方法,1. 模拟（simulation）：从电路的描述（语言描述或图形描述）抽象出模型，然后将外部激励信号或数据施加于此模型，通过观察该模型在外部激励信号作用下的反应来判断该电路系统是否实现预期的功能。模拟方法是目前常用的方法。根据不同的电路级别，有不同的模拟工具。 （目前

4、验证电路正确性的主要手段）,2. 规则检查（Design Rule Checking）：分析电路设计结果中各种数据的关系是否符合设计规则。,3. 形式验证（Formal Verification）：它利用理论证明的方法和数学的方法来验证设计结果的正确性。形式验证基于严密的理论体系，理论上可以证明电路正确与否。,模拟系统的构成,模拟系统的基本数据包括电路模型、外部输入激励波形、输出响应波形三部分组成。,硬件描述语言,模拟数据,数据库,激励波形,控制命令,模拟器,输出波形,原理图输入,编译,转换,模拟系统的构成,1. 电路模型 不用实际元件而用表示电路结构或行为的内部数据表示。设计者可以用硬件描述

5、语言将所设计电路的结构或功能输入计算机，也可以用图形描述的方法输入电路模型。内部模型还可以通过数据库统一管理。2. 在输入端施加作为外部激励波形的数据。3. 计算机根据这些激励波形和内部电路模型计算出各点的响应，得到输出波形数据。,逻辑模拟的过程,原理图编辑,硬件描述语言,激励波形编辑,数据库,启动,读电路数据,生成模拟驱动程序,得到激励波形,模拟,模拟结果,波形显示,观察修改模拟状态,模拟运行,准备工作,编译,转换,编译或转换,继续模拟,逻辑模拟的过程,1. 模拟启动前，须完成的工作： （1）用硬件描述语言描述被模拟电路，经过编译形成中间格式的内部数据。对逻辑电路来说，常用逻辑图编辑器对要模

6、拟的电路进行编辑生成内部数据。所生成的内部数据存入数据库中。 （2）用波形描述语言写出输入波形文件或者用波形编辑器编辑波形，并放在当前目录。,2. 在同一个EDA系统中，用硬件描述语言输入的内部数据格式与图形编辑器输入的内部数据是一致的。不同级别的内部数据在结构上往往有较大的差别。例如，逻辑电路的内部数据是有元件模型组成的网表结构，而行为描述的内部数据是复杂的数据结构，用以表示各种语言的组成要素。数据库将各级内部描述有机地组织在一起。,逻辑模拟的过程,3. 启动模拟器运行之后首先从数据库中读入中间格式的内部模型数据及波形数据。,4. 所生成的模拟程序启动运行之后，首先读入激励波形和模拟控制命令

7、，接着就在这些激励波形和模拟控制命令的控制下进行模拟。,5. 模拟结果包括输出波形文件和电路错误报告。电路错误报告保存模拟过程中得到的检查结果，例如竞争冒险情况，时序检查结果，以及由控制命令描述规定的信号状态显示等，供设计者参考。,逻辑模拟算法,1. 内部电路模型,2. 事件驱动模拟算法,内部电路模型,逻辑模拟的对象是由门和功能块等元件组成的逻辑电路。为了对逻辑电路进行模拟，要对被模拟的电路建立模型。模拟模型反映实际电路的特性。越接近于真实电路，模拟结果越精确，但往往也增加了复杂度。选取什么样的模型，取决于模拟的目的和对模拟的精度要求。主讲内容：电路结构模型、信号状态值模型、延迟模型、元件模型

8、。,内部电路模型,电路结构模型：,e1, XOR, (X, Y), S1;e2, XOR, (Cin, S1), Sum;e3, AND, (X, Y), S2;e4, AND, (S1, Cin), S3;e5, OR, (S2, S3), Cout;,在对硬件描述语言描述编译之后，首先产生一个中间数据格式的文件，可放在数据库中，然后由模拟程序读取。这样的中间数据用最基本的信息描述电路。逻辑电路的中间数据模型一般用称为网表(Netlist)的一个元件集合表示电路结构。如果指定了每个元件各端口所连接的信号，就可以唯一确定电路连接关系。此外，每个元件还应指明其元件模型。这样，一个元件E的描述至少

9、应有元件名N、模型M、输入端信号PI、输出端信号PO四部分组成，即 E = (N, M, PI, PO),内部电路模型,电路结构模型：,一般逻辑模拟器中，除了基本门外，还包括三态门、传输门、触发器、寄存器以及自定义功能模块等。每个元件需要纪录其逻辑连接关系，如输入信号，输出信号，还需要纪录其性能特性：所用的模型、延迟时间、最大负载系数等。对于指定功能的逻辑功能模块，还要指定其内部记忆变量、建立时间和保持时间、以及信号值配合的禁止情况等。,内部电路模型,电路结构模型：,网表的连接关系隐含在各元件的信号名中，模拟程序中使用很不便。为此，模拟程序在读入网表之后要对网表进行重新组织。模拟程序中，电路主

10、要由元件表和信号表两个表组成。每个元件的输入信号和输出信号都指向相应的信号节点。在模拟时需要频繁查找每个信号后面所接的元件，称为负载元件或扇出元件。为此，需要找出各信号负载元件表，指向相应的元件节点。信号节点还需要有其性能特性的纪录，以及信号强度、信号值波形等，纪录模拟结果。,内部电路模型,信号状态值模型：,在逻辑电路中，信号值一般用布尔值(0和1)表示。除此之外，为了表示信号波形的各种状态，在模拟系统中经常增加一些特殊用途的值。选取不同值的组合，就构成各种功能的模拟器信号模型。主要讲三种模型：二值模型、三值模型和四值模型。,内部电路模型,信号状态值模型：,二值模型：,只使用0和1两个值的模型

11、称为二值模型。二值模型假定逻辑元件都完成理想的布尔运算，可以检验数字系统的逻辑功能，可以检查电平配合、时序配合等问题。,三值模型：,在二值的基础上再增加一个值X，即形成三值模型。X可以表示下列三种情况：(1)表示不确定状态，如未赋初值的信号值和某些初值。具有相同强度，不同逻辑值的输出端驱动同一个信号节点时，不能区分0或1，该信号值也用X表示。(2)处在跳变过程中的过渡态。信号从一个稳态过渡到另一个稳态，都要经历一段短暂时间。在此期间信号状态值未定，或处于0和1。(3)表示无关紧要的信号。,内部电路模型,信号状态值模型：,信号状态值模型：,高阻值Z常用在CMOS电路中，晶体管截止时常出现高阻状态

12、。三态门在控制信号为0时其输出呈现高阻状态，它相当于把连线断开。在CMOS电路中，常遇到两个或多个输出端直接连接在一起的情况，称为线连接(Wired Connection)，如图所示。这种情况下，通常只允许一个输出端为稳态值，其余端均应为Z。这时线或运算的最后结果就等于该稳态值。,由0,1,X,Z组成的信号值模型称为四值模型，常用来实现对MOS电路的模拟。,四值模型：,内部电路模型,延迟模型：,每个信号在通过元件时都会有延迟。延迟时间的计算是逻辑模拟的重要功能。通过计算延迟时间得到的波形可以更精确地反映实际电路的情况，从而检查时序配合是否满足设计要求，是否能在规定的时间内完成规定的操作。根据需

13、要对元件的延迟赋予不同的值，可以得到不同的延迟模型。延迟模型一般支持传输延迟和惯性延迟。,内部电路模型,延迟模型：,零延迟模型。所有的元件其传输延迟均设定为0。这种模型与实际电路相差很大。使用这种模型可以检验组合逻辑电路的正确性，而不便于处理异步时序电路。,单位延迟模型。电路中所有元件都赋予相同的延迟值，并取值为1，称为单位延迟模型。用这种模型可以模拟异步时序电路。但随着引入功能块作元件，其延迟与简单门的延迟相差甚远，不能正确体现时序关系，目前已很少使用。,标准延迟模型。根据元件特性，对每种元件规定一个标准延迟数值，通常按产品目录中给定的数据为依据。它不考虑同类元件的参数分散性，与真实情况仍有

14、差别。但由于在逻辑设计阶段还不能确定参数分散情况，因而标准延迟模型对于大多数电路已经足够精确。,内部电路模型,延迟模型：,上升/下降延迟模型。进一步区分信号在正跳变和负跳变的不同延迟时间。在对于某些元件上升、下降延迟区别较大的情况下，可以更加精确地反映实际情况。,模糊延迟模型。为了反映参数的分散性，延迟时间不是给定一个值，而是给定一个范围，即给出延迟最小值和最大值。在这个范围内，其信号值不定（用X 表示）。即有一个模糊区域，故称之为模糊延迟模型。这种方式一般适用于小规模电路的精确模拟，也称为最坏情况模拟。,内部电路模型,元件模型：,元件模型给出各类元件的内部功能、参数及特性，如输入输出端个数、

15、延迟时间、扇入扇出系数等。为了提高模拟效率，常把电路中具有一定功能的部分电路网络作为一个模拟元件。这样的元件称为功能块(Functional Block)。功能块的模型用功能和行为来描述，而不关心其内部结构和组成。常见的寄存器、存储器、译码器、加法器、PLA以及其它形式的电路网络均可作为功能块。,事件驱动模拟算法,事件驱动模拟算法(Event Driven Simulation Algorithm)建立在内部表示电路结构的静态数据结构基础上，在外部激励信号的作用下，逐渐得到各级元件的响应。节点信号的每一次变化称为一个事件(Event)。由事件驱动该信号的负载元件，根据元件的功能计算元件输出端的

16、逻辑值，并且得到新的事件。这样逐级传播，直到不再存在新的事件，或者到达指定的结束时刻为止。,事件驱动模拟算法,事件驱动，其意义就是当信号值变化时才去计算该信号作为输入信号的元件（即扇出元件）。如果一个元件的输入端的值均未变化，则该元件没有必要计算。为了表示信号波形和元件延迟的作用，模拟程序建立一个虚拟的模拟时钟（Simulation clock）。起始点是0时刻。 模拟过程从零时刻开始。首先把外部输入激励信号作为原始的事件，驱动相关元件的功能计算。计算得到的元件输出端的信号值并不是当前时刻的值，有一定的延迟，是将来时刻的值，我们称之为将来值。模拟器需要把这些将来值的发生时刻和信号值记录下来。,

17、事件驱动模拟算法,事项处理三个要素：信号节点指针、信号值、事项处理发生时间，记为 e = ( s, v, t )其意义为：信号s将要在将来的 t 时刻得到值v。在实际模拟程序中，时间t可以用绝对时间表示，也可以用相对时间表示。记录和管理事项处理采用时间映射的链表。每一时刻的事项处理各排成一个链表，各个时刻排成一个时间队列表(TQ表)。,事件驱动模拟算法,模拟过程：,开始模拟,处理激励信号,事项处理表,结束模拟,活跃元件集合,处理事项处理接收信号值激活负载元件,元件计算,无事件,事件驱动模拟算法,模拟过程：,当一个新的模拟时刻开始后，首先把当前事项处理表中记录的各信号值接收到各信号节点，如果新的

18、值与原来的值相同，表示该信号的值没有变化，实际上不是一个真正的事件，则把该事项处理删除，不再对它进行处理。如果新值与老值不同，则新值构成一个事件，则需要把新值记录在该信号节点的波形表中，同时查找该节点的负载元件，安排这些元件的计算。需要计算的元件称为活跃元件。由于可能有多个信号驱动同一个元件计算，为了避免重复计算，把需要计算的元件放在一个集合中，称为活跃元件集合。待到所有的信号都处理完毕之后，再集中对所有活跃元件进行计算。计算之后又产生新的事项处理，再放到事项处理表中。对每个时刻都重复这个过程，形成模拟周期(Simulation Cycle)。,事件驱动模拟算法,事项处理冲突的处理：,举例:一

19、个非门，其上升延迟为4，下降延迟为2。当给定图b所示的输入端的波形后，得到正常的波形(图c)。当给出图d的输入波形后，则在9时刻安排事项处理e11= ( b, 1, 11 )时发生了事项处理冲突现象（图e）。这时需要把8时刻安排的事项处理e12= ( a, 0, 12 ) 删去，但其后的输入波形得到正常的输出波形。,事件驱动模拟算法,产生冲突的原因：在处理上升/下降延迟时，由于出现了不同的延迟参数，有时会遇到事项处理冲突的情况。在功能块的计算中，由于各端口延迟时间不同，也常常会出现事项处理冲突现象。,处理方法：对于一个信号s, 设前面已安排了一个事项处理e1= (s,v1,t1)尚未处理，现在

20、又安排了一个新事项处理e2= (s,v2,t2)，且t1t2，则称发生了事项处理冲突。处理方法：删去e1，安排新事项处理e2。,总结：,事件驱动模拟算法,惯性延迟冲突的处理：,产生冲突的原因：对于一个信号s, 设前面已安排了一个事项处理e1= ( s,v1,t1)尚未处理，现在又安排了一个新事项处理e2= ( s,v2,t2)，且t1 t2，v1v2 , 则称发生了惯性延迟冲突。,处理方法：把前面安排的事项处理e1 删去，而安排新事项处理e2 。,模拟实例： 下面举一个简单的例子。对图 (a)所示的电路，用事件驱动算法进行模拟，求出图中各点在t0- t30的波形。图 (b)为输入激励波形。设延

21、迟时间为：异或门-4，与或非门-3，非门-2。,事件驱动模拟算法,模拟实例：,当t = 0时，有外部输入的事项处理(a, 0, 0), (b, 0, 0)，还有作为初始值其它各点的信号事项处理(c, 0, 0), (d, 0, 0), (e, 0, 0), (f, 0, 0)。 各信号当前值均为0。事项处理(a, 0, 0), (b, 0, 0)引起C计算，得(c, 1, 3)；(b, 0, 0), 还引起D计算，得(d, 1, 2)；(c, 0, 0), (d, 0, 0)引起E计算，得(e,0, 4)；(c, 0, 0), (e, 0, 0)引起F计算，得(f, 1 3)。计算完毕，将当前

22、事项处理删除（图中未做删除标志，但应认为已不存在）。,事件驱动模拟算法,当t = 1时，无外部输入事项处理，也无当前事项处理。于是时钟直接走到下一周期，t = 2。 当t = 2时，有当前事项处理(d, 1, 2)，接收状态值d = 1，其余信号值不变。 该事项处理引起E计算，因此时c=0，故得新事项处理(e, 1,6)。注意此时事项处理表中存在事项处理(e, 0, 4)，属惯性延迟冲突，应将(e, 0, 4)删除，安排(e, 1,6)。 当t = 3时，有(c, 1, 3), (f, 1, 3)两个事项处理，接收新状态值c = 1, f = 1。c引起E, F的计算，得(e,0, 7)，(f

23、, 1 , 6)。这时可看到(e, 1 6)属惯性延迟，删除(e, 1,6)，安排(e, 0, 7)，(f, 1, 6)。 当t = 4时, 无当前事项处理。 当t = 5时, 有外部输入信号事项处理(a, 1, 5)，接收a = 1，引起C计算，得(c, 1,8)。 当t = 6时，有事项处理(f, 1 , 6)。此时f值未变，删除该事项处理。 当t = 7时，有事项处理(e, 0, 7)，此时e值未变，删除该事项处理。 当t = 8时，有事项处理(c, 1 , 8)。此时c值未变，删除该事项处理。,当t = 10时, 有外部输入信号事项处理(b, 1, 10)，接收b = 1，引起C, D

24、计算，得(c,0,13), (d,0,12)。 当t = 12时，有外部输入信号事项处理(a, 0, 12)，有事项处理(d, 0 , 12),接收a = 0, d = 0，引起C, E计算，得(e, 1,16), (c, 1, 15)。这时(c,0,13)属惯性延迟，删除(c,0,13)。 当t = 15时，有事项处理(c, 1, 16)。c值未变，删除。 当t = 16时，有事项处理(e, 1,16)。接收e = 1，引起F计算，得(f, 0,19)。 当t = 18时, 有外部输入信号事项处理(a, 1, 18)，接收a = 1，引起C计算，得(c, 0,21)。 当t = 19时, 有

25、事项处理(f, 0,19)，接收f = 0，无需要计算的元件。 当t = 20时, 有外部输入信号事项处理(b, 0, 20)，接收b = 0，引起C, D计算，得(c,1,23), (d,1,22)。这时(c,0,21)属惯性延迟，删除(c,0,21)。, 当t = 22时, 有事项处理(d, 1, 22)，接收d = 1，引起E计算，得(e, 0,26)。 当t = 23时，有事项处理(c, 1 , 23)。此时c值未变，删除该事项处理。 当t = 26时, 有事项处理(e, 0, 26)，接收e = 0，引起F计算，得(f, 1,29)。 当t = 29时, 有事项处理(f, 1,29)

26、，接收f = 1 。此时，已无任何未处理事项处理，模拟结束。,VHDL模拟,1. VHDL模拟概述,2. VHDL模拟系统的组成,3. VHDL模拟器的实现方法,4. VHDL内部模型,VHDL模拟概述,高层次硬件描述是指比逻辑结构描述更抽象的描述方法, 最主要的有寄存器传输级和行为算法级。 寄存器传输级的基本描述对象是寄存器，包括触发器、存储器、加法器、计数器等。这些元器件的数据一般为由多个位组成的位串，也称为数组。寄存器传输级语言描述数据在这些元件中的传播过程和条件，描述状态的转换。 行为和算法级的描述比寄存器传输级更为抽象。描述时不考虑具体电路元件，只有一些抽象的信号和变量。这些信号和变

27、量具有各种可能的数据结构。可以是二进制位和位串，也可以是任意枚举类型，整数和实数，甚至可以是记录和数组。描述时主要考虑数字系统的行为和动作，描述各种操作，描述系统流程。 硬件描述语言是高层次系统设计的主要描述方法。VHDL 是覆盖多个级别的多级混合的硬件描述语言。本节以VHDL语言为代表，介绍高层次模拟技术。,VHDL模拟系统的组成,一个完整的VHDL模拟系统包括设计的输入、语言的编译、模拟数据的生成、模拟、模拟结果的波形显示，以及功能较强的高级图形调试器等部分。VHDL集成模拟环境的示意图如下。,VHDL模拟器的实现方法,VHDL模拟器有不同的实现方法。大致有以下两种方式。,(1) 解释型模

28、拟方式,(2) 编译型模拟方式,VHDL模拟器的实现方法,解释型：,基本保持描述风格，按内部的层次化结构模型，做成内部静态数据结构。 整个电路系统由若干模块组成，模块可以嵌套，形成类树型结构。 每个基本模块（叶结点）为纯行为模型。 需要预先做的工作是根据配置的指定将各模块组成一个完整的电路描述。在模拟时，对这些数据分析、解释、执行，实现模拟。,VHDL内部模型,VHDL中各个实体(Entity)及其结构体(Architecture)由一系列并行语句组成。从模拟实现的角度来看，并行语句可分为三类： (1) 进程类语句：进程语句(Process)、并行信号赋值语句(=)、并行过程调用语句、并行断言

29、语句(Assert)。后三种简单并行语句可看做简化的进程语句，在行为模型中作为进程对待。 (2) 模块调用类语句：元件例化语句、块语句(Block)。 (3) 生成语句：条件生成语句(If Generate)、循环生成语句(For Generate)。,根据模拟算法的不同，可以将层次化描述的电路做成展开的平面化纯行为进程模型和层次化的结构模型两种模型。,纯行为的进程模型：,VHDL内部模型,由此可见，一个电路系统实质上是进程的集合。每个进程定义一个完整的独立操作。一个数字系统由若干独立的、并行执行的进程组成。每个进程是由一组顺序语句组成的过程，相当于一段程序。 信号是协调各进程之间通讯机制的数

30、据通路，由信号的值控制各进程的运行，并确定系统的输入和输出，得到各信号的新状态值，即得到新的信号事件。 进程有挂起和激活两种状态。设计者可以在进程中安排挂起和激活的位置和条件，包括挂起时间、激活条件和等待某些信号的事件。激活进程的信号即敏感信号，反映了系统的状态。,上图为进程模型示意图。它是一个主从链表，主链表是进程链表，每个进程结点各挂有一个顺序语句链表。,VHDL内部模型,层次化结构模型：,VHDL内部模型,子模块层次结构： 在VHDL中，子模块层次结构一般通过模块的例化调用(Instance Reference)和配置(Configuration)描述。 配置指明各例化语句所使用的模块(

31、Entity及其某一Architecture)。 由例化语句、元件模板说明(Component)与配置三个方面唯一确定一个电路系统的层次结构和组成。 经过配置，将若干个独立的实体Entity(Architecture)按照配置的指定链接起来，构成一个完整的电路。,简化层次结构： Block语句是一种复合并行语句，是在Architecture中的并行语句嵌套描述，是一种简化的层次结构描述。 整个Block语句相当于一个元件模块，语句的端口和类属参数相当于元件模块的端口和类属参数，端口匹配和类属参数匹配相当于元件例化调用的端口匹配和类属参数匹配。因而Block语句和实体描述用统一模型表示。,层次化

32、结构模型：,VHDL内部模型,VHDL内部模型,VHDL模拟算法,基于进程的事件驱动算法：,进程模型是VHDL描述的基本模型。在纯行为模型中，整个电路的行为用进程的集合来表示。在层次化结构模型中，通过调用，最终是一个纯行为的模块。 进程之间是并行执行的。对进程模型的模拟算法用顺序执行各进程来模拟其并行性。保证并行性的方法是采用与逻辑模拟类似的事件驱动算法。它同样采用基于时间顺序的时间映射的事件驱动方法，所不同的是以进程为驱动对象。 与逻辑模拟算法类似，一个信号的变化形成一个事件。所不同的是：事件不是驱动元件的计算，而是激活进程。被激活的进程在运行之后又产生新的事件，并在遇到等待语句后挂起。每一

33、次处理事件、激活和执行进程组成一个模拟周期。 进程计算的并行性与逻辑元件的并行性的实现基本是相同的。但进程计算比较复杂。其关键一点是进程激活条件比逻辑模拟器中激活元件计算的条件复杂得多。,形式验证,模拟验证的不足： 模拟验证采用仿真运行的手段，为设计人员提供了可行的判别数据，在实际设计中发挥着巨大的作用。但是，这种技术的不足之处也是十分明显的，主要表现在： 1. 模拟方法严重依赖于测试向量的选取。合理而充分地选取测试向量本身就是一个十分艰巨的课题。 2. 模拟方法的效率不高。 VLSI的设计常常需要反复修改，而每次修改后都需要模拟，以确认本次修改达到了预期目的且没有引入新的错误，因此设计人员用

34、在模拟验证上的时间常常是设计时间的2至3倍。,形式验证的引出： 电路规模较小的时候，这些不足所造成的影响还不太明显；随着电路规模的迅速增长，模拟验证的不足便突出地摆在了设计人员面前，如测试向量的选择愈加困难，测试向量集的规模呈指数级增加，模拟时间变得不可忍受等。人们开始认识到，必须提供多种设计正确性的验证手段，来解决设计人员所处的这种不利环境。于是，人们提出了一种新的验证方法形式验证（Formal Verification）。 所谓形式验证，是指从数学上完备地证明或验证电路的实现方案（简称实现）是否确实实现了电路设计描述（简称描述）的功能。,形式验证,形式验证的优点： 1. 首先，由于形式验证

35、技术是借用数学上的方法将待验证电路和功能描述或参考设计直接进行比较，因此测试者不必考虑如何获得测试向量。2. 其次，形式验证是对指定描述的所有可能的情况进行验证，而不是仅仅对其中的一个子集进行多次试验，因此有效地克服了模拟验证的不足。3. 此外，形式验证可以进行从系统级到门级的验证，而且验证时间短，有利于尽早、尽快地发现和改正电路设计中的错误，有可能缩短设计周期。,形式验证,形式验证,形式验证的缺点： 形式验证到目前为止仍然不能有效的验证电路的性能，如电路的时延和功耗等。然而，形式验证的作用正是补充了模拟验证的不足，二者各有优势，互为补充，缺一不可。,形式验证的发展： 1、针对组合电路的形式验

36、证，已有一些商用软件出现，如Compass Design Automation(San Jose, CA)公司的VFormal，Chrysalis Symbolic Design(Andover MA)公司的Design VERIFYer等。 2、而时序电路的形式验证，目前尚无成熟的方法和相应软件问世，还处于高校实验室的研究阶段，比较典型的系统有Univ. California at Berkeley的VIS系统，Carnegie-Mellon Univ。(CMU, Pittsburgh, PA)的SMV系统等。,形式验证,形式验证的基本方法,形式验证一般分为两种：1. 等价性验证：等价性验证

37、主要指验证两个方案之间的等价性，一般用于底层验证，如逻辑综合前后方案的验证。在进行不同描述层次的等价性验证时，需要解决如何从低层描述抽象出有用信息，进而与高层设计方案比较等问题。2. 性质验证：性质验证指对一个实现方案，不是去验证它所有的行为，而是验证它是否满足某些规则或性质。性质验证可以用于高层，如行为级验证。性质验证所用的规则和性质需要用户或设计人员给出，这就存在要验证多少性质才算足够的问题。,等价性验证和性质验证都属于功能性的验证。等价性验证往往是针对两个电路描述证明他们在功能上是等价的。比如逻辑最小化后与原电路等价，对电路结构作局部修改后需证明与原电路等价，从较高级别的描述综合为较低级

38、别的描述，也需要证明其所实现的电路与原来的描述等价，例如行为级到寄存器传输级，寄存器传输级到门级。,形式验证的基本方法,形式验证的基本方法,对组合电路来说，不存在状态寄存器，其输出值Zt为输入向量Xt的函数，而不依赖于前面的输入值Xt-i, ( 1 i t )。这时只需要对每个输入向量证明其输出向量相同。 在组合验证领域中出现的大多数方法大致可以分为两类。(1) 转换为单一抽象模型比较。CA和CB的输出布尔函数都转化为某一种单一形式。通过对这种单一表示的结构进行比较得出其功能等价的结论。在最坏情况下，布尔函数的正则表示随输入个数指数增加，其过大的内存需求限制了一般布尔函数的验证能力。(2)利用测试输入向量进行验证。探寻使两个电路具有不同输出值的输入测试向量。若不存在这样的测试向量，则电路在功能上等价。在最坏情况下，这种方法需要穷举所有可能的输入测试向量，使得由于运行时间问题而限制了一般电路网络的验证能力。,成功的系统中用第一类方法较多。IBM的SAS(Static Analysis System)是基于类似于二叉判决图BDD(Binary Decision Diagrams)的方法的验证大型逻辑设计的程序，成功地应用于计算机设计中。 时序电路的验证较复杂，还处于实验室阶段，略。,形式验证的基本方法,