数字系统设计及VHDL实践专题讲座模拟验证与形式验证

数字系统设计及VHDL实践专题一专题一 模拟验证与形式验证模拟验证与形式验证模拟验证与形式验证模拟验证与形式验证学习目标：学习目标：主要学习主要学习模拟验证的模型模拟验证的模型和和算法算法问题，包括问题，包括逻辑模拟算法逻辑模拟算法和和VHDL模拟模拟算法算法。要求深入掌握逻辑模拟的概念、模型与算法，掌握。要求深入掌握逻辑模拟的概念、模型与算法，掌握VHDL模拟的基本模拟的基本思想，了解思想，了解VHDL进程模拟算法进程模拟算法与与层次式模拟算法层次式模拟算法。难点重点：难点重点：1.模拟验证概念与模拟过程模拟验证概念与模拟过程2.逻辑模拟模型逻辑模拟模型3.事件驱动模拟算法事件驱动模拟算法4.VHDL模拟模型模拟模型5.进程模拟算法进程模拟算法模拟验证与形式验证模拟验证与形式验证本章主要内容：本章主要内容：一、模拟验证一、模拟验证1.1模拟验证概述模拟验证概述1.2逻辑模拟算法逻辑模拟算法1.3VHDL模拟模拟二、形式验证二、形式验证模拟验证概述模拟验证概述1.验证的重要性验证的重要性2.三种验证方法三种验证方法3.模拟系统的构成模拟系统的构成4.逻辑模拟过程逻辑模拟过程验证的重要性验证的重要性由于集成电路规模增大，单个芯片已经可以包含整个电路系统，因此设计过由于集成电路规模增大，单个芯片已经可以包含整个电路系统，因此设计过程的复杂性迅速增加。解决电路设计复杂性的一种方法是进行程的复杂性迅速增加。解决电路设计复杂性的一种方法是进行层次化设计层次化设计。这种。这种方法从方法从系统级、行为级、寄存器传输级、功能级、门级以及开关级系统级、行为级、寄存器传输级、功能级、门级以及开关级等不同的级别等不同的级别对设计进行描述，每级还可以细化为许多层次，使得设计对象逐级细化。对设计进行描述，每级还可以细化为许多层次，使得设计对象逐级细化。在如此广阔的设计领域里，每个步骤都有可能发生错误。验证作为保证设计在如此广阔的设计领域里，每个步骤都有可能发生错误。验证作为保证设计正确性的主要手段，其重要性是不言而喻的，而且，设计人员希望越早发现错误正确性的主要手段，其重要性是不言而喻的，而且，设计人员希望越早发现错误越好，如果要到版图级验证时才发现错误，所造成的损失将是十分巨大的。开发越好，如果要到版图级验证时才发现错误，所造成的损失将是十分巨大的。开发适合于各个设计阶段和设计层次的验证工具，帮助设计人员尽早发现和排除错误，适合于各个设计阶段和设计层次的验证工具，帮助设计人员尽早发现和排除错误，是是EDA的一个重要研究课题。的一个重要研究课题。在目前流行的设计方法和实际设计流程中，设计正确性的验证通常采用的是在目前流行的设计方法和实际设计流程中，设计正确性的验证通常采用的是模拟验证方法（模拟验证方法（SimulationVerificationMethod）。所谓模拟验证，是指。所谓模拟验证，是指从电路从电路描述（语言描述或图形描述）中提取出模型，然后将外部激励信号或数据施加于描述（语言描述或图形描述）中提取出模型，然后将外部激励信号或数据施加于该模型，进行计算并观察输出结果，判断该电路描述是否实现了预期的功能该模型，进行计算并观察输出结果，判断该电路描述是否实现了预期的功能。三种验证方法三种验证方法1.模拟（模拟（simulation）：）：从电路的描述（语言描述或图形描述）抽象出模型，从电路的描述（语言描述或图形描述）抽象出模型，然后将外部激励信号或数据施加于此模型，通过观察该模型在外部激励信号然后将外部激励信号或数据施加于此模型，通过观察该模型在外部激励信号作用下的反应来判断该电路系统是否实现预期的功能。模拟方法是目前常用作用下的反应来判断该电路系统是否实现预期的功能。模拟方法是目前常用的方法。根据不同的电路级别，有不同的模拟工具。的方法。根据不同的电路级别，有不同的模拟工具。（目前验证电路正确性（目前验证电路正确性的主要手段）的主要手段）2.规则检查（规则检查（DesignRuleChecking）：）：分析电路设计结果中各种数据分析电路设计结果中各种数据的关系是否符合设计规则。的关系是否符合设计规则。3.形式验证（形式验证（FormalVerification）：）：它利用理论证明的方法和数学的它利用理论证明的方法和数学的方法来验证设计结果的正确性。形式验证基于严密的理论体系，理论上方法来验证设计结果的正确性。形式验证基于严密的理论体系，理论上可以证明电路正确与否。可以证明电路正确与否。模拟系统的构成模拟系统的构成模拟系统的基本数据包括模拟系统的基本数据包括电路模型、外部输入激励波形、输出响应波形电路模型、外部输入激励波形、输出响应波形三部分组成。三部分组成。硬件描述语言硬件描述语言模拟数据模拟数据数据库数据库激励波形激励波形控制命令控制命令模拟器模拟器输出波形输出波形原理图输入原理图输入编译编译转换转换模拟系统的构成模拟系统的构成1.电路模型电路模型 不用实际元件而用表示电路结构或行为的内部数据表示。设计不用实际元件而用表示电路结构或行为的内部数据表示。设计者可以用者可以用硬件描述语言将硬件描述语言将所设计电路的结构或功能输入计算机，也可以用所设计电路的结构或功能输入计算机，也可以用图形描述图形描述的方法输入电路模型。内部模型还可以通过数据库统一管理。的方法输入电路模型。内部模型还可以通过数据库统一管理。2.在输入端施加作为在输入端施加作为外部激励波形外部激励波形的数据。的数据。3.计算机根据这些激励波形和内部电路模型计算出各点的响应，得到输出计算机根据这些激励波形和内部电路模型计算出各点的响应，得到输出波形数据。波形数据。逻辑模拟的过程逻辑模拟的过程原理图编辑原理图编辑硬件描述语言硬件描述语言激励波形编辑激励波形编辑数据库数据库启启动动读读电电路路数数据据生成生成模拟模拟驱动驱动程序程序得到得到激励激励波形波形模模拟拟模模拟拟结结果果波形波形显示显示观察修改观察修改模拟状态模拟状态模拟运行模拟运行准备工作准备工作编译编译转换转换编译或转换编译或转换继续模拟继续模拟逻辑模拟的过程逻辑模拟的过程1.模拟启动前，须完成的工作：模拟启动前，须完成的工作：（1）用硬件描述语言描述被模拟电路，经过编译形成中间格式的内部数据。对）用硬件描述语言描述被模拟电路，经过编译形成中间格式的内部数据。对逻辑电路来说，常用逻辑图编辑器对要模拟的电路进行编辑生成内部数据。所生成逻辑电路来说，常用逻辑图编辑器对要模拟的电路进行编辑生成内部数据。所生成的内部数据存入数据库中。的内部数据存入数据库中。（2）用波形描述语言写出输入波形文件或者用波形编辑器编辑波形，并放在当）用波形描述语言写出输入波形文件或者用波形编辑器编辑波形，并放在当前目录。前目录。2.在同一个在同一个EDA系统中，用硬件描述语言输入的内部数据格式与图形编辑器输入系统中，用硬件描述语言输入的内部数据格式与图形编辑器输入的内部数据是一致的。不同级别的内部数据在结构上往往有较大的差别。的内部数据是一致的。不同级别的内部数据在结构上往往有较大的差别。例如，逻例如，逻辑电路的内部数据是有元件模型组成的网表结构，而行为描述的内部数据是复杂的辑电路的内部数据是有元件模型组成的网表结构，而行为描述的内部数据是复杂的数据结构，用以表示各种语言的组成要素。数据结构，用以表示各种语言的组成要素。数据库将各级内部描述有机地组织在一数据库将各级内部描述有机地组织在一起。起。逻辑模拟的过程逻辑模拟的过程3.启动模拟器运行之后首先启动模拟器运行之后首先从数据库中读入中间格式的内部模型数据及波从数据库中读入中间格式的内部模型数据及波形数据。形数据。4.所生成的模拟程序启动运行之后，首先读入所生成的模拟程序启动运行之后，首先读入激励波形和模拟控制命激励波形和模拟控制命令令，接着就在这些激励波形和模拟控制命令的控制下进行模拟。，接着就在这些激励波形和模拟控制命令的控制下进行模拟。5.模拟结果包括模拟结果包括输出波形文件和电路错误报告。输出波形文件和电路错误报告。电路错误报告保存模拟电路错误报告保存模拟过程中得到的检查结果，例如过程中得到的检查结果，例如竞争冒险情况，时序检查结果，以及由控竞争冒险情况，时序检查结果，以及由控制命令描述规定的信号状态显示制命令描述规定的信号状态显示等，供设计者参考。等，供设计者参考。逻辑模拟算法逻辑模拟算法1.内部电路模型内部电路模型2.事件驱动模拟算法事件驱动模拟算法内部电路模型内部电路模型u逻辑模拟的对象是由逻辑模拟的对象是由门和功能块门和功能块等元件组成的逻辑电路。等元件组成的逻辑电路。u为了对逻辑电路进行模拟，要对被模拟的电路建立模型。模拟模型反为了对逻辑电路进行模拟，要对被模拟的电路建立模型。模拟模型反映实际电路的特性。越接近于真实电路，模拟结果越精确，但往往也映实际电路的特性。越接近于真实电路，模拟结果越精确，但往往也增加了复杂度。增加了复杂度。选取什么样的模型，取决于模拟的目的和对模拟的精选取什么样的模型，取决于模拟的目的和对模拟的精度要求。度要求。u主讲内容：主讲内容：电路结构模型、信号状态值模型、延迟模型、元件模型。电路结构模型、信号状态值模型、延迟模型、元件模型。内部电路模型内部电路模型电路结构模型：电路结构模型：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)内部电路模型内部电路模型电路结构模型：电路结构模型：一般逻辑模拟器中，除了基本门外，还包括三态门、一般逻辑模拟器中，除了基本门外，还包括三态门、传输门、触发器、寄存器以及自定义功能模块等。每个元传输门、触发器、寄存器以及自定义功能模块等。每个元件需要纪录其逻辑连接关系，如输入信号，输出信号，还件需要纪录其逻辑连接关系，如输入信号，输出信号，还需要纪录其性能特性：需要纪录其性能特性：所用的模型、延迟时间、最大负载所用的模型、延迟时间、最大负载系数系数等。对于指定功能的逻辑功能模块，还要指定其等。对于指定功能的逻辑功能模块，还要指定其内部内部记忆变量、建立时间和保持时间、以及信号值配合的禁止记忆变量、建立时间和保持时间、以及信号值配合的禁止情况情况等。等。内部电路模型内部电路模型电路结构模型：电路结构模型：网表的连接关系隐含在各元件的信号名中，模拟程序中网表的连接关系隐含在各元件的信号名中，模拟程序中使用很不便。为此，模拟程序在读入网表之后要对网表进行使用很不便。为此，模拟程序在读入网表之后要对网表进行重新组织。重新组织。模拟程序中，电路主要由元件表和信号表两个表模拟程序中，电路主要由元件表和信号表两个表组成。每个元件的输入信号和输出信号都指向相应的信号节组成。每个元件的输入信号和输出信号都指向相应的信号节点。点。在模拟时需要频繁查找每个信号后面所接的元件，称为在模拟时需要频繁查找每个信号后面所接的元件，称为负载元件负载元件或或扇出元件扇出元件。为此，需要找出各信号负载元件表，。为此，需