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

数字系统设计及VHDL实践专题一专题一 模拟验证与形式验证模拟验证与形式验证数字系统设计及VHDL实践专题一 模拟验证与形式验证1模拟验证与形式验证模拟验证与形式验证学习目标：学习目标：主要学习主要学习模拟验证的模型模拟验证的模型和和算法算法问题，包括问题，包括逻辑模拟算法逻辑模拟算法和和VHDL模拟模拟算法算法。要求深入掌握逻辑模拟的概念、模型与算法，掌握。要求深入掌握逻辑模拟的概念、模型与算法，掌握VHDL模拟的基本模拟的基本思想，了解思想，了解VHDL进程模拟算法进程模拟算法与与层次式模拟算法层次式模拟算法。难点重点：难点重点：1.模拟验证概念与模拟过程模拟验证概念与模拟过程2.逻辑模拟模型逻辑模拟模型3.事件驱动模拟算法事件驱动模拟算法4.VHDL模拟模型模拟模型5.进程模拟算法进程模拟算法模拟验证与形式验证学习目标：难点重点：1.模拟验证概念与模2模拟验证与形式验证模拟验证与形式验证本章主要内容：本章主要内容：一、模拟验证一、模拟验证1.1模拟验证概述模拟验证概述1.2逻辑模拟算法逻辑模拟算法1.3VHDL模拟模拟二、形式验证二、形式验证模拟验证与形式验证本章主要内容：一、模拟验证1.1 模拟验3模拟验证概述模拟验证概述1.验证的重要性验证的重要性2.三种验证方法三种验证方法3.模拟系统的构成模拟系统的构成4.逻辑模拟过程逻辑模拟过程模拟验证概述1.验证的重要性2.三种验证方法3.模拟系统的构4验证的重要性验证的重要性由于集成电路规模增大，单个芯片已经可以包含整个电路系统，因此设计过由于集成电路规模增大，单个芯片已经可以包含整个电路系统，因此设计过程的复杂性迅速增加。解决电路设计复杂性的一种方法是进行程的复杂性迅速增加。解决电路设计复杂性的一种方法是进行层次化设计层次化设计。这种。这种方法从方法从系统级、行为级、寄存器传输级、功能级、门级以及开关级系统级、行为级、寄存器传输级、功能级、门级以及开关级等不同的级别等不同的级别对设计进行描述，每级还可以细化为许多层次，使得设计对象逐级细化。对设计进行描述，每级还可以细化为许多层次，使得设计对象逐级细化。在如此广阔的设计领域里，每个步骤都有可能发生错误。验证作为保证设计在如此广阔的设计领域里，每个步骤都有可能发生错误。验证作为保证设计正确性的主要手段，其重要性是不言而喻的，而且，设计人员希望越早发现错误正确性的主要手段，其重要性是不言而喻的，而且，设计人员希望越早发现错误越好，如果要到版图级验证时才发现错误，所造成的损失将是十分巨大的。开发越好，如果要到版图级验证时才发现错误，所造成的损失将是十分巨大的。开发适合于各个设计阶段和设计层次的验证工具，帮助设计人员尽早发现和排除错误，适合于各个设计阶段和设计层次的验证工具，帮助设计人员尽早发现和排除错误，是是EDA的一个重要研究课题。的一个重要研究课题。在目前流行的设计方法和实际设计流程中，设计正确性的验证通常采用的是在目前流行的设计方法和实际设计流程中，设计正确性的验证通常采用的是模拟验证方法（模拟验证方法（SimulationVerificationMethod）。所谓模拟验证，是指。所谓模拟验证，是指从电路从电路描述（语言描述或图形描述）中提取出模型，然后将外部激励信号或数据施加于描述（语言描述或图形描述）中提取出模型，然后将外部激励信号或数据施加于该模型，进行计算并观察输出结果，判断该电路描述是否实现了预期的功能该模型，进行计算并观察输出结果，判断该电路描述是否实现了预期的功能。验证的重要性 由于集成电路规模增大，5三种验证方法三种验证方法1.模拟（模拟（simulation）：）：从电路的描述（语言描述或图形描述）抽象出模型，从电路的描述（语言描述或图形描述）抽象出模型，然后将外部激励信号或数据施加于此模型，通过观察该模型在外部激励信号然后将外部激励信号或数据施加于此模型，通过观察该模型在外部激励信号作用下的反应来判断该电路系统是否实现预期的功能。模拟方法是目前常用作用下的反应来判断该电路系统是否实现预期的功能。模拟方法是目前常用的方法。根据不同的电路级别，有不同的模拟工具。的方法。根据不同的电路级别，有不同的模拟工具。（目前验证电路正确性（目前验证电路正确性的主要手段）的主要手段）2.规则检查（规则检查（DesignRuleChecking）：）：分析电路设计结果中各种数据分析电路设计结果中各种数据的关系是否符合设计规则。的关系是否符合设计规则。3.形式验证（形式验证（FormalVerification）：）：它利用理论证明的方法和数学的它利用理论证明的方法和数学的方法来验证设计结果的正确性。形式验证基于严密的理论体系，理论上方法来验证设计结果的正确性。形式验证基于严密的理论体系，理论上可以证明电路正确与否。可以证明电路正确与否。三种验证方法1.模拟（simulation）：从电路的描6模拟系统的构成模拟系统的构成模拟系统的基本数据包括模拟系统的基本数据包括电路模型、外部输入激励波形、输出响应波形电路模型、外部输入激励波形、输出响应波形三部分组成。三部分组成。硬件描述语言硬件描述语言模拟数据模拟数据数据库数据库激励波形激励波形控制命令控制命令模拟器模拟器输出波形输出波形原理图输入原理图输入编译编译转换转换模拟系统的构成模拟系统的基本数据包括电路模型、外部输入激励波7模拟系统的构成模拟系统的构成1.电路模型电路模型 不用实际元件而用表示电路结构或行为的内部数据表示。设计不用实际元件而用表示电路结构或行为的内部数据表示。设计者可以用者可以用硬件描述语言将硬件描述语言将所设计电路的结构或功能输入计算机，也可以用所设计电路的结构或功能输入计算机，也可以用图形描述图形描述的方法输入电路模型。内部模型还可以通过数据库统一管理。的方法输入电路模型。内部模型还可以通过数据库统一管理。2.在输入端施加作为在输入端施加作为外部激励波形外部激励波形的数据。的数据。3.计算机根据这些激励波形和内部电路模型计算出各点的响应，得到输出计算机根据这些激励波形和内部电路模型计算出各点的响应，得到输出波形数据。波形数据。模拟系统的构成1.电路模型 不用实际元件而用表示电路结构或8逻辑模拟的过程逻辑模拟的过程原理图编辑原理图编辑硬件描述语言硬件描述语言激励波形编辑激励波形编辑数据库数据库启启动动读读电电路路数数据据生成生成模拟模拟驱动驱动程序程序得到得到激励激励波形波形模模拟拟模模拟拟结结果果波形波形显示显示观察修改观察修改模拟状态模拟状态模拟运行模拟运行准备工作准备工作编译编译转换转换编译或转换编译或转换继续模拟继续模拟逻辑模拟的过程原理图编辑硬件描述语言激励波形编辑数据库启读生9逻辑模拟的过程逻辑模拟的过程1.模拟启动前，须完成的工作：模拟启动前，须完成的工作：（1）用硬件描述语言描述被模拟电路，经过编译形成中间格式的内部数据。对）用硬件描述语言描述被模拟电路，经过编译形成中间格式的内部数据。对逻辑电路来说，常用逻辑图编辑器对要模拟的电路进行编辑生成内部数据。所生成逻辑电路来说，常用逻辑图编辑器对要模拟的电路进行编辑生成内部数据。所生成的内部数据存入数据库中。的内部数据存入数据库中。（2）用波形描述语言写出输入波形文件或者用波形编辑器编辑波形，并放在当）用波形描述语言写出输入波形文件或者用波形编辑器编辑波形，并放在当前目录。前目录。2.在同一个在同一个EDA系统中，用硬件描述语言输入的内部数据格式与图形编辑器输入系统中，用硬件描述语言输入的内部数据格式与图形编辑器输入的内部数据是一致的。不同级别的内部数据在结构上往往有较大的差别。的内部数据是一致的。不同级别的内部数据在结构上往往有较大的差别。例如，逻例如，逻辑电路的内部数据是有元件模型组成的网表结构，而行为描述的内部数据是复杂的辑电路的内部数据是有元件模型组成的网表结构，而行为描述的内部数据是复杂的数据结构，用以表示各种语言的组成要素。数据结构，用以表示各种语言的组成要素。数据库将各级内部描述有机地组织在一数据库将各级内部描述有机地组织在一起。起。逻辑模拟的过程1.模拟启动前，须完成的工作：2.在同一个10逻辑模拟的过程逻辑模拟的过程3.启动模拟器运行之后首先启动模拟器运行之后首先从数据库中读入中间格式的内部模型数据及波从数据库中读入中间格式的内部模型数据及波形数据。形数据。4.所生成的模拟程序启动运行之后，首先读入所生成的模拟程序启动运行之后，首先读入激励波形和模拟控制命激励波形和模拟控制命令令，接着就在这些激励波形和模拟控制命令的控制下进行模拟。，接着就在这些激励波形和模拟控制命令的控制下进行模拟。5.模拟结果包括模拟结果包括输出波形文件和电路错误报告。输出波形文件和电路错误报告。电路错误报告保存模拟电路错误报告保存模拟过程中得到的检查结果，例如过程中得到的检查结果，例如竞争冒险情况，时序检查结果，以及由控竞争冒险情况，时序检查结果，以及由控制命令描述规定的信号状态显示制命令描述规定的信号状态显示等，供设计者参考。等，供设计者参考。逻辑模拟的过程3.启动模拟器运行之后首先从数据库中读入中间11逻辑模拟算法逻辑模拟算法1.内部电路模型内部电路模型2.事件驱动模拟算法事件驱动模拟算法逻辑模拟算法 1.内部电路模型2.事件驱动模拟算法12内部电路模型内部电路模型u逻辑模拟的对象是由逻辑模拟的对象是由门和功能块门和功能块等元件组成的逻辑电路。等元件组成的逻辑电路。u为了对逻辑电路进行模拟，要对被模拟的电路建立模型。模拟模型反为了对逻辑电路进行模拟，要对被模拟的电路建立模型。模拟模型反映实际电路的特性。越接近于真实电路，模拟结果越精确，但往往也映实际电路的特性。越接近于真实电路，模拟结果越精确，但往往也增加了复杂度。增加了复杂度。选取什么样的模型，取决于模拟的目的和对模拟的精选取什么样的模型，取决于模拟的目的和对模拟的精度要求。度要求。u主讲内容：主讲内容：电路结构模型、信号状态值模型、延迟模型、元件模型。电路结构模型、信号状态值模型、延迟模型、元件模型。内部电路模型逻辑模拟的对象是由门和功能块等元件组成的逻辑电路13内部电路模型内部电路模型电路结构模型：电路结构模型：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;u在对硬件描述语言描述编译之后，首先产生一个在对硬件描述语言描述编译之后，首先产生一个中间数据格式的文件中间数据格式的文件，可放，可放在数据库中，然后在数据库中，然后由模拟程序读取。由模拟程序读取。这样的中间数据用最基本的信息描述电这样的中间数据用最基本的信息描述电路。路。逻辑电路的中间数据模型一般用称为网表逻辑电路的中间数据模型一般用称为网表(Netlist)的一个元件集合表示的一个元件集合表示电路结构。电路结构。如果指定了每个元件各端口所连接的信号，就可以唯一确定电路如果指定了每个元件各端口所连接的信号，就可以唯一确定电路连接关系。此外，每个元件还应指明其元件模型。这样，连接关系。此外，每个元件还应指明其元件模型。这样，一个元件一个元件E的描述至的描述至少应有元件名少应有元件名N、模型、模型M、输入端信号、输入端信号PI、输出端信号、输出端信号PO四部分组成，即四部分组成，即E=(N,M,PI,PO)内部电路模型电路结构模型：e1,XOR,(X,Y),14内部电路模型内部电路模型电路结构模型：电路结构模型：一般逻辑模拟器中，除了基本门外，还包括三态门、一般逻辑模拟器中，除了基本门外，还包括三态门、传输门、触发器、寄存器以及自定义功能模块等。每个元传输门、触发器、寄存器以及自定义功能模块等。每个元件需要纪录其逻辑连接关系，如输入信号，输出信号，还件需要纪录其逻辑连接关系，如输入信号，输出信号，还需要纪录其性能特性：需要纪录其性能特性：所用的模型、延迟时间、最大负载所用的模型、延迟时间、最大负载系数系数等。对于指定功能的逻辑功能模块，还要指定其等。对于指定功能的逻辑功能模块，还要指定其内部内部记忆变量、建立时间和保持时间、以及信号值配合的禁止记忆变量、建立时间和保持时间、以及信号值配合的禁止情况情况等。等。内部电路模型电路结构模型：一般15内部电路模型内部电路模型电路结构模型：电路结构模型：网表的连接关系隐含在各元件的信号名中，模拟程序中网表的连接关系隐含在各元件的信号名中，模拟程序中使用很不便。为此，模拟程序在读入网表之后要对网表进行使用很不便。为此，模拟程序在读入网表之后要对网表进行重新组织。重新组织。模拟程序中，电路主要由元件表和信号表两个表模拟程序中，电路主要由元件表和信号表两个表组成。每个元件的输入信号和输出信号都指向相应的信号节组成。每个元件的输入信号和输出信号都指向相应的信号节点。点。在模拟时需要频繁查找每个信号后面所接的元件，称为在模拟时需要频繁查找每个信号后面所接的元件，称为负载元件负载元件或或扇出元件扇出元件。为此，需要找出各信号负载元件表，。为此，需要找出各信号负载元件表，指向相应的元件节点。信号节点还需要有其性能特性的纪录，指向相应的元件节点。信号节点还需要有其性能特性的纪录，以及信号强度、信号值波形等，纪录模拟结果。以及信号强度、信号值波形等，纪录模拟结果。内部电路模型电路结构模型：网表的连接关系隐含16内部电路模型内部电路模型信号状态值模型：信号状态值模型：u在逻辑电路中，信号值一般用布尔值在逻辑电路中，信号值一般用布尔值(0和和1)表示。除此之外，为了表表示。除此之外，为了表示信号波形的各种状态，在模拟系统中经常增加一些特殊用途的值。示信号波形的各种状态，在模拟系统中经常增加一些特殊用途的值。选取不同值的组合，就构成各种功能的模拟器信号模型。选取不同值的组合，就构成各种功能的模拟器信号模型。u主要讲三种模型：主要讲三种模型：二值模型、三值模型和四值模型。二值模型、三值模型和四值模型。内部电路模型信号状态值模型：在逻辑电路中，信号值一般用布尔值17内部电路模型内部电路模型信号状态值模型：信号状态值模型：u二值模型：二值模型：只使用只使用0和和1两个值的模型称为二值模型。两个值的模型称为二值模型。二值模型假定逻辑元件都完成理想二值模型假定逻辑元件都完成理想的布尔运算，可以的布尔运算，可以检验数字系统的逻辑功能检验数字系统的逻辑功能，可以，可以检查电平配合、时序配合检查电平配合、时序配合等问等问题。题。内部电路模型信号状态值模型：二值模型：只使用18u三值模型：三值模型：在二值的基础上再增加一个值在二值的基础上再增加一个值X，即形成三值模型。，即形成三值模型。X可以表示下列三种情况：可以表示下列三种情况：(1)表示不确定状态，如未赋初值的信号值和某些初值。表示不确定状态，如未赋初值的信号值和某些初值。具有相同强度，不同逻辑具有相同强度，不同逻辑值的输出端驱动同一个信号节点时，不能区分值的输出端驱动同一个信号节点时，不能区分0或或1，该信号值也用，该信号值也用X表示。表示。(2)处在跳变过程中的过渡态。处在跳变过程中的过渡态。信号从一个稳态过渡到另一个稳态，都要经历一段信号从一个稳态过渡到另一个稳态，都要经历一段短暂时间。在此期间信号状态值未定，或处于短暂时间。在此期间信号状态值未定，或处于0和和1。(3)表示无关紧要的信号。表示无关紧要的信号。内部电路模型内部电路模型信号状态值模型：信号状态值模型：三值模型：在二值的基础上再增加一个值X，即形成三值模型。X可19信号状态值模型：信号状态值模型：l高阻值高阻值Z常用在常用在CMOS电路中，晶体管截止时常出现高阻状态。电路中，晶体管截止时常出现高阻状态。三态门在控制三态门在控制信号为信号为0时其输出呈现高阻状态，它相当于把连线断开。时其输出呈现高阻状态，它相当于把连线断开。l在在CMOS电路中，常遇到两个或多个输出端直接连接在一起的情况，称为线电路中，常遇到两个或多个输出端直接连接在一起的情况，称为线连接连接(WiredConnection)，如图所示。这种情况下，如图所示。这种情况下，通常只允许一个输出端通常只允许一个输出端为稳态值，其余端均应为为稳态值，其余端均应为Z。这时线或运算的最后结果就等于该稳态值。这时线或运算的最后结果就等于该稳态值。由由0,1,X,Z组成的信号值模型称为四值模型，常用来实现对组成的信号值模型称为四值模型，常用来实现对MOS电路的模拟。电路的模拟。u四值模型：四值模型：信号状态值模型：高阻值Z常用在CMOS电路中，晶体管截止时常20内部电路模型内部电路模型延迟模型：延迟模型：u每个信号在通过元件时都会有延迟。每个信号在通过元件时都会有延迟。延迟时间的计算是逻辑模拟的重延迟时间的计算是逻辑模拟的重要功能。要功能。通过计算延迟时间得到的波形可以更精确地反映实际电路的通过计算延迟时间得到的波形可以更精确地反映实际电路的情况，从而检查时序配合是否满足设计要求，是否能在规定的时间内情况，从而检查时序配合是否满足设计要求，是否能在规定的时间内完成规定的操作。完成规定的操作。u根据需要对元件的延迟赋予不同的值，可以得到不同的延迟模型。根据需要对元件的延迟赋予不同的值，可以得到不同的延迟模型。延延迟模型一般支持传输延迟和惯性延迟。迟模型一般支持传输延迟和惯性延迟。内部电路模型延迟模型：每个信号在通过元件时都会有延迟。延迟时21内部电路模型内部电路模型延迟模型：延迟模型：l零延迟模型。零延迟模型。所有的元件其传输延迟均设定为所有的元件其传输延迟均设定为0。这种模型与实际电路相差很。这种模型与实际电路相差很大。使用这种模型可以检验组合逻辑电路的正确性，而不便于处理异步时序电大。使用这种模型可以检验组合逻辑电路的正确性，而不便于处理异步时序电路。路。l单位延迟模型。单位延迟模型。电路中所有元件都赋予相同的延迟值，并取值为电路中所有元件都赋予相同的延迟值，并取值为1，称为单位，称为单位延迟模型。用这种模型可以模拟异步时序电路。但随着引入功能块作元件，其延迟模型。用这种模型可以模拟异步时序电路。但随着引入功能块作元件，其延迟与简单门的延迟相差甚远，不能正确体现时序关系，目前已很少使用。延迟与简单门的延迟相差甚远，不能正确体现时序关系，目前已很少使用。l标准延迟模型。标准延迟模型。根据元件特性，对每种元件规定一个标准延迟数值，通常按产根据元件特性，对每种元件规定一个标准延迟数值，通常按产品目录中给定的数据为依据。它不考虑同类元件的参数分散性，与真实情况仍品目录中给定的数据为依据。它不考虑同类元件的参数分散性，与真实情况仍有差别。但由于在逻辑设计阶段还不能确定参数分散情况，因而标准延迟模型有差别。但由于在逻辑设计阶段还不能确定参数分散情况，因而标准延迟模型对于大多数电路已经足够精确。对于大多数电路已经足够精确。内部电路模型延迟模型：零延迟模型。所有的元件其传输延迟均设定22内部电路模型内部电路模型延迟模型：延迟模型：l上升上升/下降延迟模型。下降延迟模型。进一步区分信号在正跳变和负跳变的不同延迟时间。进一步区分信号在正跳变和负跳变的不同延迟时间。在对于某些元件上升、下降延迟区别较大的情况下，可以更加精确地反映在对于某些元件上升、下降延迟区别较大的情况下，可以更加精确地反映实际情况。实际情况。l模糊延迟模型。模糊延迟模型。为了反映参数的分散性，延迟时间不是给定一个值，而为了反映参数的分散性，延迟时间不是给定一个值，而是给定一个范围，即给出延迟最小值和最大值。在这个范围内，其信号值是给定一个范围，即给出延迟最小值和最大值。在这个范围内，其信号值不定（用不定（用X表示）。即有一个模糊区域，故称之为模糊延迟模型。这种表示）。即有一个模糊区域，故称之为模糊延迟模型。这种方式一般适用于小规模电路的精确模拟，也称为方式一般适用于小规模电路的精确模拟，也称为最坏情况模拟。最坏情况模拟。内部电路模型延迟模型：上升/下降延迟模型。进一步区分信号在正23内部电路模型内部电路模型元件模型：元件模型：u元件模型给出元件模型给出各类元件的内部功能、参数及特性，各类元件的内部功能、参数及特性，如如输入输出端个数、延迟时输入输出端个数、延迟时间、扇入扇出系数间、扇入扇出系数等。等。u为了提高模拟效率，为了提高模拟效率，常把电路中具有一定功能的部分电路网络作为一个模拟元常把电路中具有一定功能的部分电路网络作为一个模拟元件。这样的元件称为功能块件。这样的元件称为功能块(FunctionalBlock)。功能块的模型用功能和行为功能块的模型用功能和行为来描述，而不关心其内部结构和组成。常见的来描述，而不关心其内部结构和组成。常见的寄存器、存储器、译码器、加法寄存器、存储器、译码器、加法器、器、PLA以及其它形式的电路网络以及其它形式的电路网络均可作为功能块。均可作为功能块。内部电路模型元件模型：元件模型给出各类元件的内部功能、参数及24事件驱动模拟算法事件驱动模拟算法u事件驱动模拟算法事件驱动模拟算法(EventDrivenSimulationAlgorithm)建立在内部表示电建立在内部表示电路结构的静态数据结构基础上，在外部激励信号的作用下，逐渐得到各级元路结构的静态数据结构基础上，在外部激励信号的作用下，逐渐得到各级元件的响应。件的响应。u节点信号的每一次变化称为一个事件节点信号的每一次变化称为一个事件(Event)。由事件驱动该信号的负载元。由事件驱动该信号的负载元件，根据元件的功能计算元件输出端的逻辑值，并且得到新的事件。这样逐件，根据元件的功能计算元件输出端的逻辑值，并且得到新的事件。这样逐级传播，直到不再存在新的事件，或者到达指定的结束时刻为止。级传播，直到不再存在新的事件，或者到达指定的结束时刻为止。事件驱动模拟算法事件驱动模拟算法(Event Driven 25事件驱动模拟算法事件驱动模拟算法u事件驱动，其意义就是事件驱动，其意义就是当信号值变化时才去计算该信号作为输入信号的元件当信号值变化时才去计算该信号作为输入信号的元件（即扇出元件）。（即扇出元件）。如果一个元件的输入端的值均未变化，则该元件没有必要如果一个元件的输入端的值均未变化，则该元件没有必要计算。计算。u为了表示信号波形和元件延迟的作用，模拟程序建立一个虚拟的模拟时钟为了表示信号波形和元件延迟的作用，模拟程序建立一个虚拟的模拟时钟（Simulationclock）。）。起始点是起始点是0时刻。时刻。u模拟过程从零时刻开始。模拟过程从零时刻开始。首先把外部输入激励信号作为原始的事件，驱动相首先把外部输入激励信号作为原始的事件，驱动相关元件的功能计算。计算得到的元件输出端的信号值并不是当前时刻的值，关元件的功能计算。计算得到的元件输出端的信号值并不是当前时刻的值，有一定的延迟，是将来时刻的值，我们称之为将来值。有一定的延迟，是将来时刻的值，我们称之为将来值。u模拟器需要把这些将来值的发生时刻和信号值记录下来。模拟器需要把这些将来值的发生时刻和信号值记录下来。事件驱动模拟算法事件驱动，其意义就是当信号值变化时才去计算该26事件驱动模拟算法事件驱动模拟算法u事项处理三个要素：事项处理三个要素：信号节点指针、信号值、信号节点指针、信号值、事项处理发生时间事项处理发生时间，记为，记为e=(s,v,t)u其意义为：其意义为：信号信号s将要在将来的将要在将来的t时刻得到值时刻得到值v。在实际模拟程序中，时间在实际模拟程序中，时间t可以用绝对时间表示，可以用绝对时间表示，也可以用相对时间表示也可以用相对时间表示。u记录和管理事项处理采用记录和管理事项处理采用时间映射的链表。时间映射的链表。u每一时刻的事项处理各排成一个链表，各个时每一时刻的事项处理各排成一个链表，各个时刻排成一个刻排成一个时间队列表时间队列表(TQ表表)。事件驱动模拟算法事项处理三个要素：信号节点指针、信号值、事项27事件驱动模拟算法事件驱动模拟算法模拟过程：模拟过程：开开始始模模拟拟处理处理激励激励信号信号事事项项处处理理表表结束结束模拟模拟活跃活跃元件元件集合集合处理事项处理处理事项处理接收信号值接收信号值激活负载元件激活负载元件元元件件计计算算无事件无事件事件驱动模拟算法模拟过程：开处理事结束活跃处理事项处理元无事28事件驱动模拟算法事件驱动模拟算法模拟过程：模拟过程：l当一个新的模拟时刻开始后，首先把当一个新的模拟时刻开始后，首先把当前事项处理表中记录的各信号值接收到各当前事项处理表中记录的各信号值接收到各信号节点，信号节点，如果新的值与原来的值相同，表示该信号的值没有变化，如果新的值与原来的值相同，表示该信号的值没有变化，实际上不是一实际上不是一个真正的事件，则把该事项处理删除，不再对它进行处理。个真正的事件，则把该事项处理删除，不再对它进行处理。如果新值与老值不同，如果新值与老值不同，则新值构成一个事件，则则新值构成一个事件，则需要把新值记录在该信号节点的波形表中，同时查找该节需要把新值记录在该信号节点的波形表中，同时查找该节点的负载元件，安排这些元件的计算。点的负载元件，安排这些元件的计算。l需要计算的元件称为需要计算的元件称为活跃元件。活跃元件。由于可能有多个信号驱动同一个元件计算，由于可能有多个信号驱动同一个元件计算，为了为了避免重复计算，把需要计算的元件放在一个集合中，称为活跃元件集合。避免重复计算，把需要计算的元件放在一个集合中，称为活跃元件集合。待到所有待到所有的信号都处理完毕之后，再集中对所有活跃元件进行计算。的信号都处理完毕之后，再集中对所有活跃元件进行计算。l计算之后又产生新的事项处理，再放到事项处理表中。计算之后又产生新的事项处理，再放到事项处理表中。对每个时刻都重复这个过对每个时刻都重复这个过程，形成模拟周期程，形成模拟周期(SimulationCycle)。事件驱动模拟算法模拟过程：当一个新的模拟时刻开始后，首先把29事件驱动模拟算法事件驱动模拟算法事项处理冲突的处理：事项处理冲突的处理：l举例举例:一个非门，其上升延迟为一个非门，其上升延迟为4，下降延迟为，下降延迟为2。当给定图。当给定图b所示的输入端的波形后，得到正所示的输入端的波形后，得到正常的波形常的波形(图图c)。当给出图。当给出图d的输入波形后，则在的输入波形后，则在9时刻安排事项处理时刻安排事项处理e11=(b,1,11)时发生了时发生了事项处理冲突现象（图事项处理冲突现象（图e）。这时需要把）。这时需要把8时刻安排的事项处理时刻安排的事项处理e12=(a,0,12)删去，但其后删去，但其后的输入波形得到正常的输出波形。的输入波形得到正常的输出波形。事件驱动模拟算法事项处理冲突的处理：举例:一个非门，其上升延30事件驱动模拟算法事件驱动模拟算法产生冲突的原因：产生冲突的原因：在处理上升在处理上升/下降延迟时，由于出现了不同的延迟参数，有下降延迟时，由于出现了不同的延迟参数，有时会遇到事项处理冲突的情况。在功能块的计算中，由于各端口延迟时间不时会遇到事项处理冲突的情况。在功能块的计算中，由于各端口延迟时间不同，也常常会出现事项处理冲突现象。同，也常常会出现事项处理冲突现象。处理方法：处理方法：对于一个信号对于一个信号s,设前面已安排了一个事项处理设前面已安排了一个事项处理e1=(s,v1,t1)尚未尚未处理，现在又安排了一个新事项处理处理，现在又安排了一个新事项处理e2=(s,v2,t2)，且，且t1t2，则称发生了事，则称发生了事项处理冲突。处理方法：删去项处理冲突。处理方法：删去e1，安排新事项处理，安排新事项处理e2。总结：总结：事件驱动模拟算法产生冲突的原因：在处理上升/下降延迟时，由于31事件驱动模拟算法事件驱动模拟算法惯性延迟冲突的处理：惯性延迟冲突的处理：产生冲突的原因：产生冲突的原因：对于一个信号对于一个信号s,设前面已安排了一个事项处理设前面已安排了一个事项处理e1=(s,v1,t1)尚未处理，现在又安排了一个新事项处理尚未处理，现在又安排了一个新事项处理e2=(s,v2,t2)，且，且t1t2，v1v2,则则称发生了惯性延迟冲突。称发生了惯性延迟冲突。处理方法：处理方法：把前面安排的事项处理把前面安排的事项处理e1删去，而安排新事项处理删去，而安排新事项处理e2。事件驱动模拟算法惯性延迟冲突的处理：产生冲突的原因：对于一个32模拟实例：模拟实例：下面举一个简单的例子。对图下面举一个简单的例子。对图(a)所示的电路，用事件驱动算法进行模拟，所示的电路，用事件驱动算法进行模拟，求出图中各点在求出图中各点在t0-t30的波形。图的波形。图(b)为输入激励波形。设延迟时间为：异为输入激励波形。设延迟时间为：异或门或门-4，与或非门，与或非门-3，非门，非门-2。事件驱动模拟算法事件驱动模拟算法模拟实例：事件驱动模拟算法33模拟实例：模拟实例：模拟实例：34l 当当t=0时，时，有外部输入的事项处理有外部输入的事项处理(a,0,0),(b,0,0)，还有作为初始，还有作为初始值其它各点的信号事项处理值其它各点的信号事项处理(c,0,0),(d,0,0),(e,0,0),(f,0,0)。各各信号当前值均为信号当前值均为0。l事项处理事项处理(a,0,0),(b,0,0)引起引起C计算，得计算，得(c,1,3)；l(b,0,0),还引起还引起D计算，得计算，得(d,1,2)；l(c,0,0),(d,0,0)引起引起E计算，得计算，得(e,0,4)；l(c,0,0),(e,0,0)引起引起F计算，得计算，得(f,13)。l计算完毕，将当前事项处理删除（图中未做删除标志，但应认为已不存在）。计算完毕，将当前事项处理删除（图中未做删除标志，但应认为已不存在）。事件驱动模拟算法事件驱动模拟算法 当t=0时，有外部输入的事项处理(a,0,035l 当当t=1时，时，无外部输入事项处理，也无当前事项处理。于是时钟直接走到下一周期，无外部输入事项处理，也无当前事项处理。于是时钟直接走到下一周期，t=2。l当当t=2时，时，有当前事项处理有当前事项处理(d,1,2)，接收状态值，接收状态值d=1，其余信号值不变。，其余信号值不变。l该事项处理引起该事项处理引起E计算，因此时计算，因此时c=0，故得新事项处理，故得新事项处理(e,1,6)。注意此时事项处理表中。注意此时事项处理表中存在事项处理存在事项处理(e,0,4)，属惯性延迟冲突，应将，属惯性延迟冲突，应将(e,0,4)删除，安排删除，安排(e,1,6)。l当当t=3时，时，有有(c,1,3),(f,1,3)两个事项处理，接收新状态值两个事项处理，接收新状态值c=1,f=1。c引起引起E,F的计算，得的计算，得(e,0,7)，(f,1,6)。这时可看到。这时可看到(e,16)属惯性延迟，删除属惯性延迟，删除(e,1,6)，安排，安排(e,0,7)，(f,1,6)。l当当t=4时时,无当前事项处理。无当前事项处理。l当当t=5时时,有外部输入信号事项处理有外部输入信号事项处理(a,1,5)，接收，接收a=1，引起，引起C计算，得计算，得(c,1,8)。l当当t=6时，时，有事项处理有事项处理(f,1,6)。此时。此时f值未变，删除该事项处理。值未变，删除该事项处理。l当当t=7时，时，有事项处理有事项处理(e,0,7)，此时，此时e值未变，删除该事项处理。值未变，删除该事项处理。l当当t=8时时，有事项处理，有事项处理(c,1,8)。此时。此时c值未变，删除该事项处理。值未变，删除该事项处理。当t=1时，无外部输入事项处理，也无当前事项处理。于36l当当t=10时时,有外部输入信号事项处理有外部输入信号事项处理(b,1,10)，接收，接收b=1，引起，引起C,D计算，得计算，得(c,0,13),(d,0,12)。l当当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)。l当当t=15时，时，有事项处理有事项处理(c,1,16)。c值未变，删除。值未变，删除。l当当t=16时，时，有事项处理有事项处理(e,1,16)。接收。接收e=1，引起，引起F计算，得计算，得(f,0,19)。l当当t=18时时,有外部输入信号事项处理有外部输入信号事项处理(a,1,18)，接收，接收a=1，引起，引起C计算，得计算，得(c,0,21)。l当当t=19时时,有事项处理有事项处理(f,0,19)，接收，接收f=0，无需要计算的元件。，无需要计算的元件。l当当t=20时时,有外部输入信号事项处理有外部输入信号事项处理(b,0,20)，接收，接收b=0，引起，引起C,D计算，得计算，得(c,1,23),(d,1,22)。这时。这时(c,0,21)属惯性延迟，删除属惯性延迟，删除(c,0,21)。当t=10时,有外部输入信号事项处理(b,1,37 当当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)，接收，接收f=1。此时，已无任何未处理事。此时，已无任何未处理事项处理，模拟结束。项处理，模拟结束。数字系统设计及VHDL实践专题讲座1-模拟验证与课件38VHDLVHDL模拟模拟1.VHDL模拟概述模拟概述 2.VHDL模拟系统的组成模拟系统的组成 3.VHDL模拟器的实现方法模拟器的实现方法4.VHDL内部模型内部模型VHDL模拟1.VHDL模拟概述 2.VHDL模拟系统的39VHDLVHDL模拟概述模拟概述l高层次硬件描述是指比逻辑结构描述更抽象的描述方法高层次硬件描述是指比逻辑结构描述更抽象的描述方法,最主要的有最主要的有寄存器传输级寄存器传输级和和行为算法级。行为算法级。l寄存器传输级寄存器传输级的基本描述对象是寄存器，包括触发器、存储器、加法器、计数器等。的基本描述对象是寄存器，包括触发器、存储器、加法器、计数器等。这些元器件的数据一般为由多个位组成的位串，也称为数组。寄存器传输级语言描述这些元器件的数据一般为由多个位组成的位串，也称为数组。寄存器传输级语言描述数据在这些元件中的传播过程和条件，描述状态的转换。数据在这些元件中的传播过程和条件，描述状态的转换。l行为和算法级的描述行为和算法级的描述比寄存器传输级更为抽象。描述时不考虑具体电路元件，只有比寄存器传输级更为抽象。描述时不考虑具体电路元件，只有一些抽象的信号和变量。这些信号和变量具有各种可能的数据结构。可以是二进制位一些抽象的信号和变量。这些信号和变量具有各种可能的数据结构。可以是二进制位和位串，也可以是任意枚举类型，整数和实数，甚至可以是记录和数组。描述时主要和位串，也可以是任意枚举类型，整数和实数，甚至可以是记录和数组。描述时主要考虑数字系统的行为和动作，描述各种操作，描述系统流程。考虑数字系统的行为和动作，描述各种操作，描述系统流程。l硬件描述语言是高层次系统设计的主要描述方法。硬件描述语言是高层次系统设计的主要描述方法。VHDL是覆盖多个级别的多级混是覆盖多个级别的多级混合的硬件描述语言。本节以合的硬件描述语言。本节以VHDL语言为代表，介绍高层次模拟技术。语言为代表，介绍高层次模拟技术。VHDL模拟概述 高层次硬件描述是指比逻辑结构描述更抽象40VHDLVHDL模拟系统的组成模拟系统的组成一个完整的一个完整的VHDL模拟系统包括模拟系统包括设计的输入、语言的编译、模拟数据的生成、模设计的输入、语言的编译、模拟数据的生成、模拟、模拟结果的波形显示，以及功能较强的高级图形调试器等部分。拟、模拟结果的波形显示，以及功能较强的高级图形调试器等部分。VHDL集成模拟集成模拟环境的示意图如下。环境的示意图如下。VHDL模拟系统的组成 一个完整的VHDL模拟系41VHDLVHDL模拟器的实现方法模拟器的实现方法VHDL模拟器有不同的实现方法。大致有以下两种方式。模拟器有不同的实现方法。大致有以下两种方式。(1)解释型模拟方式解释型模拟方式(2)编译型模拟方式编译型模拟方式 VHDL模拟器的实现方法VHDL模拟器有不同的实现方法。大42VHDLVHDL模拟器的实现方法模拟器的实现方法解释型：解释型：l基本保持描述风格，按内部的层次化结构模型，做成基本保持描述风格，按内部的层次化结构模型，做成内部静态数据结构。内部静态数据结构。l整个电路系统由若干模块组成，模块可以嵌套，形成整个电路系统由若干模块组成，模块可以嵌套，形成类树型结构。类树型结构。l每个基本模块（叶结点）为纯行为模型。每个基本模块（叶结点）为纯行为模型。l需要预先做的工作是根据配置的指定将各模块组成一需要预先做的工作是根据配置的指定将各模块组成一个完整的电路描述。在模拟时，对这些数据分析、解释、个完整的电路描述。在模拟时，对这些数据分析、解释、执行，实现模拟。执行，实现模拟。VHDL模拟器的实现方法解释型：基本保持描述风格，按内部的43VHDLVHDL内部模型内部模型VHDL中各个实体中各个实体(Entity)及其结构体及其结构体(Architecture)由一系列并行语句组成。由一系列并行语句组成。从模拟实现的角度来看，并行语句可分为三类：从模拟实现的角度来看，并行语句可分为三类：(1)进程类语句：进程类语句：进程语句进程语句(Process)、并行信号赋值语句、并行信号赋值语句(=)、并行过程调用语、并行过程调用语句、并行断言语句句、并行断言语句(Assert)。后三种简单并行语句可看做简化的进程语句，在行为模。后三种简单并行语句可看做简化的进程语句，在行为模型中作为进程对待。型中作为进程对待。(2)模块调用类语句：模块调用类语句：元件例化语句、块语句元件例化语句、块语句(Block)。(3)生成语句：生成语句：条件生成语句条件生成语句(IfGenerate)、循环生成语句、循环生成语句(ForGenerate)。根据模拟算法的不同，可以将层次化描述的电路做成展开的平面化根据模拟算法的不同，可以将层次化描述的电路做成展开的平面化纯行为进纯行为进程模型程模型和和层次化的结构模型层次化的结构模型两种模型。两种模型。VHDL内部模型 VHDL中各个实体(Entity44纯行为的进程模型：纯行为的进程模型：VHDLVHDL内部模型内部模型l由此可见，由此可见，一个电路系统实质上是进程的集合。一个电路系统实质上是进程的集合。每个进程定义一个完整的独立操每个进程定义一个完整的独立操作。作。一个数字系统由若干独立的、并行执行的进程组成。一个数字系统由若干独立的、并行执行的进程组成。每个进程是由一组顺序语句每个进程是由一组顺序语句组成的过程，相当于一段程序。组成的过程，相当于一段程序。l信号是协调各进程之间通讯机制的数据通路，由信号的值控制各进程的运行，并信号是协调各进程之间通讯机制的数据通路，由信号的值控制各进程的运行，并确定系统的输入和输出，得到各信号的新状态值，即得到新的信号事件。确定系统的输入和输出，得到各信号的新状态值，即得到新的信号事件。l进程有进程有挂起挂起和和激活激活两种状态。设计者可以在进程中安排挂起和激活的位置和条件，两种状态。设计者可以在进程中安排挂起和激活的位置和条件，包括包括挂起时间、激活条件挂起时间、激活条件和和等待某些信号的事件。等待某些信号的事件。激活进程的信号即敏感信号，反映激活进程的信号即敏感信号，反映了系统的状态。了系统的状态。纯行为的进程模型：VHDL内部模型由此可见，一个电路系统实45上图为进程模型示意图。它是一个主从链表，主链表是进程链表，每个进上图为进程模型示意图。它是一个主从链表，主链表是进程链表，每个进程结点各挂有一个顺序语句链表。程结点各挂有一个顺序语句链表。VHDLVHDL内部模型内部模型 上图为进程模型示意图。它是一个主从链表，主链表是进46层次化结构模型：层次化结构模型：VHDLVHDL内部模型内部模型子模块层次结构：子模块层次结构：l在在VHDL中，子模块层次结构一般通过中，子模块层次结构一般通过模块的例化调用模块的例化调用(InstanceReference)和和配置配置(Configuration)描述。描述。l配置指明各例化语句所使用的模块配置指明各例化语句所使用的模块(Entity及其某一及其某一Architecture)。l由由例化语句、元件模板说明例化语句、元件模板说明(Component)与配置与配置三个方面三个方面唯一确定一个电路系统唯一确定一个电路系统的层次结构和组成。的层次结构和组成。l经过配置，将若干个独立的实体经过配置，将若干个独立的实体Entity(Architecture)按照配置的指定链接起来，按照配置的指定链接起来，构成一个完整的电路。构成一个完整的电路。层次化结构模型：VHDL内部模型子模块层次结构：47简化层次结构：简化层次结构：lBlock语句是一种语句是一种复合并行语句复合并行语句，是在，是在Architecture中的并行语句嵌套描述，中的并行语句嵌套描述，是是一种一种简化的层次结构描述。简化的层次结构描述。l整个整个Block语句相当于一个元件模块，语句的端口和类属参数相当于元件模块的端语句相当于一个元件模块，语句的端口和类属参数相当于元件模块的端口和类属参数，端口匹配和类属参数匹配相当于元件例化调用的端口匹配和类属参数口和类属参数，端口匹配和类属参数匹配相当于元件例化调用的端口匹配和类属参数匹配。因而匹配。因而Block语句和实体描述用统一模型表示。语句和实体描述用统一模型表示。层次化结构模型：层次化结构模型：VHDLVHDL内部模型内部模型简化层次结构：层次化结构模型：VHDL内部模型48VHDLVHDL内部模型内部模型VHDL内部模型49VHDLVHDL模拟算法模拟算法基于进程的事件驱动算法：基于进程的事件驱动算法：l进程模型是进程模型是VHDL描述的基本模型。描述的基本模型。在纯行为模型中，整个电路的行为用进程的集在纯行为模型中，整个电路的行为用进程的集合来表示。在层次化结构模型中，通过调用，最终是一个纯行为的模块。合来表示。在层次化结构模型中，通过调用，最终是一个纯行为的模块。l进程之间是并行执行的。进程之间是并行执行的。对进程模型的模拟算法用顺序执行各进程来模拟其并行性。对进程模型的模拟算法用顺序执行各进程来模拟其并行性。保证并行性的方法是采用与逻辑模拟类似的事件驱动算法。它同样采用基于时间顺序保证并行性的方法是采用与逻辑模拟类似的事件驱动算法。它同样采用基于时间顺序的时间映射的事件驱动方法，的时间映射的事件驱动方法，所不同的是以进程为驱动对象。所不同的是以进程为驱动对象。l与逻辑模拟算法类似，一个信号的变化形成一个事件。与逻辑模拟算法类似，一个信号的变化形成一个事件。所不同的是：事件不是驱动所不同的是：事件不是驱动元件的计算，而是激活进程。被激活的进程在运行之后又产生新的事件，并在遇到等元件的计算，而是激活进程。被激活的进程在运行之后又产生新的事件，并在遇到等待语句后挂起。每一次处理事件、激活和执行进程组成一个模拟周期。待语句后挂起。每一次处理事件、激活和执行进程组成一个模拟周期。l进程计算的并行性与逻辑元件的并行性的实现基本是相同的。进程计算的并行性与逻辑元件的并行性的实现基本是相同的。但进程计算比较复杂。但进程计算比较复杂。其关键一点是进程激活条件比逻辑模拟器中激活元件计算的条件复杂得多。其关键一点是进程激活条件比逻辑模拟器中激活元件计算的条件复杂得多。VHDL模拟算法基于进程的事件驱动算法：进程模型是VHDL50形式验证形式验证模拟验证的不足：模拟验证的不足：模拟验证采用仿真运行的手段，为设计人员提供了可行的判别数据，在实际设模拟验证采用仿真运行的手段，为设计人员提供了可行的判别数据，在实际设计中发挥着巨大的作用。但是，这种技术的不足之处也是十分明显的，主要表计中发挥着巨大的作用。但是，这种技术的不足之处也是十分明显的，主要表现在：现在：1.模拟方法严重依赖于测试向量的选取。模拟方法严重依赖于测试向量的选取。合理而充分地选取测试向量本身合理而充分地选取测试向量本身就是一个十分艰巨的课题。就是一个十分艰巨的课题。2.模拟方法的效率不高。模拟方法的效率不高。VLSI的设计常常需要反复修改，而每次修改后都需要模拟，以确认本次修改达的设计常常需要反复修改，而每次修改后都需要模拟，以确认本次修改达到了预期目的且没有引入新的错误，因此设计人员用在模拟验证上的时间常常到了预期目的且没有引入新的错误，因此设计人员用在模拟验证上的时间常常是设计时间的是设计时间的2至至3倍。倍。形式验证模拟验证的不足：51形式验证的引出：形式验证的引出：电路规模较小的时候，这些不足所造成的影响还不太明显；随着电路规模电路规模较小的时候，这些不足所造成的影响还不太明显；随着电路规模的迅速增长，模拟验证的不足便突出地摆在了设计人员面前，如测试向量的选的迅速增长，模拟验证的不足便突出地摆在了设计人员面前，如测试向量的选择愈加困难，测试向量集的规模呈指数级增加，模拟时间变得不可忍受等。人择愈加困难，测试向量集的规模呈指数级增加，模拟时间变得不可忍受等。人们开始认识到，必须提供多种设计正确性的验证手段，来解决设计人员所处的们开始认识到，必须提供多种设计正确性的验证手段，来解决设计人员所处的这种不利环境。于是，人们提出了一种新的验证方法这种不利环境。于是，人们提出了一种新的验证方法形式验证（形式验证（FormalVerification）。）。所谓形式验证，是指所谓形式验证，是指从数学上完备地证明或验证电路的实现方案（简称实从数学上完备地证明或验证电路的实现方案（简称实现）是否确实实现了电路设计描述（简称描述）的功能。现）是否确实实现了电路设计描述（简称描述）的功能。形式验证形式验证 形式验证的引出：形式验证52形式验证的优点：形式验证的优点：1.首先，由于形式验证技术是借用数学上的方法将待验证电路和功能描述或首先，由于形式验证技术是借用数学上的方法将待验证电路和功能描述或参考设计直接进行比较，因此参考设计直接进行比较，因此测试者不必考虑如何获得测试向量。测试者不必考虑如何获得测试向量。2.其次，形式验证是对指定描述的所有可能的情况进行验证，而不是仅仅对其次，形式验证是对指定描述的所有可能的情况进行验证，而不是仅仅对其中的一个子集进行多次试验，因此其中的一个子集进行多次试验，因此有效地克服了模拟验证的不足。有效地克服了模拟验证的不足。3.此外，形式验证可以进行从系统级到门级的验证，而且验证时间短，此外，形式验证可以进行从系统级到门级的验证，而且验证时间短，有利有利于尽早、尽快地发现和改正电路设计中的错误，有可能缩短设计周期。于尽早、尽快地发现和改正电路设计中的错误，有可能缩短设计周期。形式验证形式验证形式验证的优点：1.首先，由于形式验证技术是借用数53形式验证形式验证形式验证的缺点：形式验证的缺点：形式验证到目前为止仍然不能有效的验证电路的性能，如电路的时延形式验证到目前为止仍然不能有效的验证电路的性能，如电路的时延和功耗等。然而，形式验证的作用正是补充了模拟验证的不足，二者各有和功耗等。然而，形式验证的作用正是补充了模拟验证的不足，二者各有优势，互为补充，缺一不可。优势，互为补充，缺一不可。形式验证形式验证的缺点：54形式验证的发展：形式验证的发展：1、针对组合电路的形式验证，已有一些商用软件出现，如、针对组合电路的形式验证，已有一些商用软件出现，如CompassDesignAutomation(SanJose,CA)公司的公司的VFormal，ChrysalisSymbolicDesign(Andover