电子设计自动化验证技术概述

1、验证技术概述Introduction to Verification1内容验证技术概述功能验证、等价性验证、静态分析及物理检查3. 模拟4. 形式验证5. 验证方法学2 Cell Library Design Rule. .Spec.Behavior HDLRTL HDLSynthesisNetlistPlacement&RoutingIC LayoutFPGAAreaTimingPowerDFTSimulation and VerificationFPGA Compiler 自 顶 向 下3验证的重要性验证的重要性：占工程设计时间70，代码总量80验证影响：产品的生命产品返工失去顾客成本4验

2、证的目的及其本质验证的目的：原始描述的正确性：SPEC设计结果与原始描述的一致性设计结果是否符合设计规则验证的本质：验证本质上就是保证某种形式的转换符合我们的期望，即保证设计正确的实现了规范所定义的功能和性能要求。 芯片的设计规范(一般是一个文本文件)与其系统级模型（高级语言模型，如C模型）之间的等效通过比较系统级模型与 HDL 实现的输出，可以在规范的系统级模型与其 HDL 实现之间建立等效关系。 HDL实现与门级 (综合后的)之间通过应用“逻辑等效性检查”可以建立等效 5工程对验证的要求验证的完整性：只有充分接近全部功能得到验证，并达到功能覆盖率的要求，才能对产品有信心。验证的自动化：尽可

3、能减少验证时间对产品产出时间的影响，验证才是成功的，这需要EDA工具和先进验证手段的支持。6验证系统验证系统的组成：验证说明：描述目标行为以及不希望出现之行为的设计规范（Specification）成品模型：环境模型：模型类别：硬件：prototype-仿真(Emulation)软件：C or RTL Code-模拟(Simulation)混合：7设计各阶段验证的内容前端设计：功能验证 ：代码是否符合设计规范 等价性验证 ：各层次的功能是否满足原有功能规范 后端设计：功能：门级仿真（后仿真） 性能（setup、hold、驱动）：静态时序分析物理设计 ：规则检查（design rule chec

4、k）电气规则检查 (ERC)、设计规则检查 (DRC)、版图对电路检查 （LVS)信号完整性、干扰、金属迁移、噪声 8功能验证分类：目的性验证：目的是验证设计所试图完成的功能在设计中已正确实现。最典型的情况是在抽象程度最高的层次完成，其最终结果是建立一套“黄金模型”，它可以在整个设计过程中作为设计细节的参考。等价性验证：目的是验证设计过程中产生的不同层次的设计结果功能是否符合“黄金模型”。9目的性验证 1. 动态模拟：将一组输入激励施加到设计模型上，使其工作运行，并观察模型的响应。2. 形式验证：用数学方法验证设计的功能，不需要验证测试向量。3. 模拟形式混合验证：混合验证取两者之优点，模拟能

5、处理的设计规模大，类型多，而形式验证具有完整性。4. 软/硬件协同验证：协同验证可以在硬件开发的同时，让软件在硬件模拟平台上运行，从而硬件和软件可以同时调试，而不是串行进行，大大缩短了产品的开发时间。 10目的性验证（续）5.仿真系统：专门设计的硬件和软件系统，典型的是采用FPGA-与最终设计接近的仿真速度。6.样机系统 ：系统测试、市场开发、演示(1)物理样机：一种目标设计的硬件替代品，它的运行能够“接近”目标设计平台的性能。与目标系统速度相同的数量级，比仿真系统的速度快出许多。 (2)虚拟样机：一个虚拟样机就是一个产品、一个元件或一个系统的计算机模拟模型。 11 物理样机Parterre之

6、FPGA验证平台12等价性验证 1.动态等价验证i)确定模拟：复用高层次模型开发的验证测试向量和测试程序 ii)回归测试：批处理模拟；自动比较结果 2.形式等价验证：完全的等价验证，如Formality 形式等价验证工具生成一个数据结构并比较在相同的输入模式下得出的输出数值模式，如果这些输出数值模式不相同，那么同一设计的两种描述(如门级和 RTL级)就不是等价的。组合等价检验和时序等价检验 13静态分析验证 1）Lint检查：对设计代码进行静态检查，验证语法的正确性。Lint检验对RTL设计代码进行静态检查，是在设计进行综合前的一种预处理，目的是消除代码中的错误，包括语法、可综合性、未初始化的

7、变量、未支持的语言结构、端口失配等。有些工具还能抽取FSM模型，检测竞争条件，检查可测试性和可重用性规定的一些设计规则等。2）静态时序分析 每个存储元件有时序要求，例如，建立时间、保持时间和各种延时。时序验证要确定电路时序是否满足设计要求。 14物理验证 物理验证就是通过检验图形设计的数据库以确信物理实现确实是原始逻辑设计的正确表述。物理验证包括以下三个部分：电学规则检查、设计规则检查及版图对电路检查。标准的图形数据库形式是GDSII数据流。15物理验证（续）1)电气规则检查 (ERC)：检查是否违反电气设计规则，包括未使用的输出、浮空输入、负载违例、连接违例，如开路和短路等。2)设计规则检查

8、 (DRC)：检查是否违反工艺过程设计规则，包括层与层的间距、特定层上的线条宽度、层与层的重叠等。3)版图对电路检查(LVS)：检验提取的图形数据库是否有与“黄金”网表相违背之处。LVS工具从多边形数据中构建网表以及从物理布局中提取器件模型。提取出的网表需和“黄金”模型保持一致。所有的器件和互连都必须严格地相匹配。4)其他物理验证：包括信号完整性、干扰、金属迁移、噪声等。16模拟基于模拟的验证是功能验证最重要、用得最多的一种方法。它是在模拟器上通过模拟实际电路的工作环境来对设计进行验证。模拟的基本方法：首先根据设计规范和测试规范,建立测试平台，编写测试数据组（testcase）以生成测试激励以

9、及响应检查；然后在模拟器上进行模拟，将测试数据组的激励输入到硬件描述语言代码模型最后对输出同标准输出结果进行比较，从而达到功能验证的目的。 17基于模拟的验证基于模拟的验证结构可分为四个部分：测试数据组（testcase）测试平台（testbench）参考模型（reference model）仿真器 （simulator）18测试数据组测试数据组是对待测模型产生激励的来源。设计测试数据组的关键是确定待测模型需要验证的属性（features），也就是功能验证点。正确识别和详细分析属性，并依此产生相应的测试数据组，决定了验证的功能覆盖率，从而最终决定了待测模型是否充分满足设计规范的要求。测试数据组

10、的生成：是由验证工程师手工编写。目前也出现了自动测试数据组生成工具，如synopsys的半自动测试数据组生成工具Vera。它利用语言定义各种约束，以指导伪随机测试的生成，结合功能覆盖分析，帮助验证工程师建立高效的验证环境，使得到高质量的测试程序。 19测试数据组（续）每一个测试数据组一般包括激励数据和输出响应数据。在实际设计过程中，测试数据组通常分为三部分：接口测试：检验模块接口时序和协议子模块测试：子模块功能验证系统测试：全系统功能验证 2021测试平台 测试平台是为模拟验证而编写的代码，其目的是用来对待测设计产生预先确定的输入序列，然后选择性的观察响应。测试平台可采用硬件描述语言来编写，也

11、可以采用e或OpenVera等验证语言编写。 22结构化的测试平台 可复用的测试基准BFM（Bus-Function Model）概念：将测试数据组提供的测试数据，通过统一的任务接口，按照待测模型端口的时序和协议进行封装组合的程序模块。由子程序以及Task等组成，代替总线的简单模型，可以复用Testcase Reusable Verification Component BusFunction Model Design UnderVerification Bus Function Model Harness23结构化的测试平台 BFM原理：能够使用某种命令语言在总线上产生一系列事务。不含有总线

12、设备的实现，亦不需要包含总线设备的全部功能只含有总线、I/O接口的信号，并模拟这些信号的传输过程 24参考模型 参考模型：一种专门面向功能验证而设计的代码，可以在施加于待测设计的相同激励条件下，产生预期的结果，该结果做为testbench检查器的预期响应参与比较。参考模型的主要目的就是生成与目标设计描述进行比较的比对数据。参考模型侧重于设计的逻辑功能，而不是功能实现的细节。 25参考模型Design Under Test （DUT）激励发生器结果检查黄金模型golden model26验证实例：UART验证环境和测试方案testbench根据设计文档确定验证点（testcase）验证文档：描述

13、每个验证点的目的、具体实现步骤验证文档testcase提取覆盖率分析不理想回到第2阶段记录验证结果.log文件27验证环境架构及建立方式基于软件模拟的层次式架构testcase层：由过程（procedure）调用组成行为模型以及BFM：不可综合的代码，描述系统环境中可能的其他电路模型或行为testbench：验证配置testbench组织：configurations装配testcase，行为模型，BFM以及待测模块DUT28UART验证环境架构29确定验证点testcase提取：tasks激励：从单一功能到复杂功能，辅以覆盖率工具响应：针对具体testcase描述检查相关响应30例：数据发送

14、进程testcase生成testcase1:验证UART是否能够正确发送数据a.保持发送时钟基准时钟*8得到的位时钟txtick；b.调用APB_write任务向UART 控制寄存器写入“000101010”；c.调用APB_write任务向UART 发送保持寄存器thold写入“10101010”；d.调用TXD_verify任务，并检测是否正确接收“10101010”testcase2:验证UART能否检验出奇偶校验错，并据此发出中断请求a.保持发送时钟基准时钟*8得到的位时钟txtick；b.调用APB_write任务向UART 控制寄存器写入“000101010”；c. 调用APB_w

15、rite任务向UART 发送保持寄存器thold写入“10101010”；d.调用TXD_verify任务，并检测是否正确接收“10101010”，偶校验无误，并接收到IRQ信号；e.调用APB_write任务向UART 控制寄存器写入“000111010”；f. 调用APB_write任务向UART 发送保持寄存器thold写入“10101010”；g.调用TXD_verify任务，并检测是否正确接收“10101010”，奇校验无误，并接收到IRQ信号；testcase3：溢出错误检查testcase4：发送过程清TEtestcase5：流控制检查testcase提取31testcase实例

16、-simulustask serial_data_input_generater;input7:0 data;input1:0 verify_indicate;input baudrate_clk;output RXD;/ verify_indicate 1=1，表示有校验位，否则无校验位； / verify_indicate 0 =1，表示奇校验，否则为偶校验；wire verify_bit = verify_indicate 0? data:data;begin (posedge baudrate_clk) TXD= 1b0; (posedge baudrate_clk) TXD= dat

17、a0; (posedge baudrate_clk) TXD= data1; (posedge baudrate_clk) TXD= data2; (posedge baudrate_clk) TXD= data3; (posedge baudrate_clk) TXD= data4; (posedge baudrate_clk) TXD= data5; (posedge baudrate_clk) TXD= data6; (posedge baudrate_clk) TXD= data7; (posedge baudrate_clk) TXD= verify_indicate1? verif

18、y_bit:1b1; (posedge baudrate_clk) TXD= 1b1;endendtask 32testcase实例-receiving datamodule testbench_for_UART_RXD;/例化待测模块UART UART u1(RXD, TXD,.); /顺序执行任务序列，进行功能验证initial begin/调用激励产生模块，输入数据8ha5，1位偶校验位serial_data_input_generater(8ha5, 2b10, baudrate, RXD); Endendmodule33testbench1）将上述task在testbench的pro

19、cess中排列组合，分别调度就组成一个面向UART 的 黑盒子testbench generater2）把UART和testbench generater在顶层模块配置指定testbench，则可进行模拟验证 34模拟仿真工具模拟工具：模拟器SimulatorVerilog-XLModelsimNC VerilogVSS（VHDL）VCS（Verilog ）35模拟仿真工具模拟器工作原理：编译法Compiler：将HDL的描述编译成一般软件语言或汇编语言再执行事件表驱动法Event Driven ：对描述进行解释执行Cycle Based NC Verilog：一个时钟周期只采一次数据 ISS

20、 （Instruction Set Simulation）- 指令级模拟器： 用于有CPU的系统模拟 363738模拟仿真工具仿真（Emulation）： FPGA 把设计从RTL综合后写入FPGA中, 与周边芯片连成系统进行板级仿真. 特点: 验证功能及接口 速度快：界于实物芯片和模拟之间 只模拟功能，不模拟速度39基于模拟的验证方法 组合逻辑MEMnmn+m2n+m121010241001.26E+3010001.07E+30110238.99E+307穷举模拟？可能的状态转换 2n+m40基于模拟的验证方法测试向量生成：规范一致性测试：所有“指令”、“控制模式”边角测试 （Corner

21、Case）随机测试 无向随机模拟 有向随机模拟 设计错误模型实代码 (Real Code)回归测试(Regression testing) 41基于模拟的验证衡量方法 代码覆盖率 通过硬件代码覆盖率分析工具来评定验证测试序列的覆盖率指标。把特定的测试验证序列输入到特定设计中，通过代码覆盖率分析就有可能得出功能覆盖率的某些方面的信息。分析工具可以提供以下信息：每个被评估属性的百分比的覆盖率值设计中没有执行或者只是部分执行的区域的列表可进行有目的的状态覆盖尝试改变原始模拟踪迹，进行指导42代码覆盖的类型 语句覆盖：表示多少语句已被执行过，或者每个语句执行过的次数。翻转覆盖：表示信号中哪些位已经过0

22、1和10翻转。触发覆盖：每个进程是否被敏感表中每个信号独立地触发。分支覆盖：“if”或 “case”语句中的哪些分支己被执行表达式覆盖：“if”语句中条件布尔表达式的覆盖情况路径覆盖：由“if”和 “Case”语句构成的所有可能的路径是否己被验证。变量覆盖：信号或地址的覆盖情况，是翻转覆盖的扩充。FSM代码覆盖 43基于模拟的验证衡量方法功能覆盖率：由用户定义的、反映在验证过程中被运行到的功能点的范围的衡量方法。功能点可以是对用户而言可视的体系结构特点，也可以是主要的微结构特征。通常情况下，这些特征不能从实现中自动生成，因此需要在验证testbench中的一些规范。功能覆盖率数据一般是一些时序

23、行为（如总线的交易）和一些数据（如交易源、目的和优先级等）的交叉组合。附加覆盖率信息可以从功能覆盖率点的交叉引用中得到。比如，在一个器件的两个引脚之间进行的数据处理的相互关系，或者在一个处理器中指令和中断的关系等。 44基于模拟的验证衡量方法period1 period2BUG RATETime（effort） ready to ship ship？Bug rate with code coverage45基于模拟的验证的问题RTL模拟： 一个月 一个月功能仿真：一天 一个月电路仿真：一分钟 一小时芯片： 一秒 一分钟Validity Test：108矢量Boot Unix：1010矢量46形

24、式验证 形式验证：利用数学方法对设计结果的功能进行验证。由于它依赖于对设计的数学分析，因此无需使用验证测试向量。目前包括如下几种技术： 模型检查定理证明形式等价检验 47模型检查模型检查将设计描述及其部份规范的特性作为输入，以证明该设计是否具有某种特性。其过程是搜索一个设计在所有可能条件下的状态空间，寻找不符合某特性的点，如果找到这样的点，则可证明该特性不正确。 模型检查不需要设置任何验证测试，所需验证的特性以队列形式用特性说明语言描述。当模型检查工具发现一个错误，工具可从初始状态开始，进行完全的状态跟踪，直至出错的状态。48定理证明在定理证明的过程中特性被表述为数学命题，而设计则表述为数学实

25、体，该实体表示为若干公理。证明的过程就是看数学命题是否可从公理中演绎得到。如果得到，则该特性存在；否则，该特性则不存在。 定理证明的主要缺点：用户必须用定理证明器的命令来构造证明过程；当证明结论为不成立，只能用人工方法分析其原因，不能自动跟踪。 49 静态时序分析（STA）：发现使芯片时序失效和对芯片性能起决起决定作用的电路关键路径。 性能验证：时序分析ClkD1Q1bD2CQ250 在同步时序电路中，2个寄存器之间组合电路延迟之和（建立时间、保持时间、寄存器间的信号传播延迟）决定了最大时钟频率。设其中： setup=20ns； hold=30ns；not（b）=15ns；and（d）=25n

26、s；则从D1 到 D2 Total delay =20+30+15+25=90nsClkD1Q1bD2CQ2Clk性能验证：时序分析51性能验证：时序分析建立时间（setup）：信号S1高电平相对S2上升边之前应保持稳定的时间。保持时间（hold）： 信号S1 高电平相对S2上升边之后应保持稳定的时间。S2holdsetup hold 时间为从clk到来时，D Q 的传输时间，Setup为防止时钟歪斜等不定因数S152 长路径错误设其中： setup=20ns； hold=30ns； not（b）=15ns； and（d）=25ns；则从D1 到 D2 Total delay =20+30+1

27、5+25=90ns要求： 时钟周期 90ns 频率 1/90 11MHz如 时钟周期 90ns 即发生长路径错误：setup违背性能验证：时序分析53 短路径错误 由于时钟歪斜（skew）太大而引起，在一个周期内 信号穿过两个寄存器，从而产生逻辑错误clk1clk2Q1Q2”Q2性能验证：时序分析54静态时序分析（STA）STA工作原理：采用穷尽分析方法，提取出所有时序路径计算信号在这些路径上的传播延迟检查信号的建立和保持时间是否满足时序要求通过对最大路径延迟和最小路径延迟的分析，找出违背时序约束的错误。 STA优点：如果采用模拟的方法，由于输入矢量的局限性，可能无法检查出某些路径存在的时序失

28、效STA不要求输入矢量，能很快得到分析结果，节省了很多的设计时间。 55性能验证：后仿真56集成电路设计的验证方法学 验证规划 验证和设计分离原则 周密的验证计划设计验证方法学：根据不同性质的项目可以采用不同的验证方法学。抽象级和模型：定义设计的各个抽象级，以及相应的说明和 实现，以便决定采用合适的验证技术。此外，要准备好验证时所需的相应的合适电路模型。验证技术和工具：不同层次的验证需要选用不同的技术及其相应的EDA工具。验证测试：不同抽象级的验证相应有不同的测试，关键是要产生各种测试程序、如何应用这些测试程序，以及测试程序如何在各层次中移植等。构成测试的元素应包括：测试激励：对于动态模拟，可

29、以是各种类型的测试向量，而对于形式验证，则要定义设计的特性和约束等。测试检查器：包括期望的测试响应、协议、黄金模型等。测试评估：包括能力测度，如运行时间、存储器规模等，以及质量测度，如功能覆盖、代码覆盖等。验证流程：往往是迭代的和并行的，而非单调和串行的。此外包括验证的跟踪，所发现的设计错误处埋以及验证文档等。 57验证方法学：自顶向下的验证方法 (1)系统级验证：系统的行为由顶层系统说明规定，系统的行为用行为模拟测试程序进行验证。然后系统映射到合适的体系结构，利用IP模块进行硬件和软件划分。该体系结构的功能和性能用系统行为模拟中建立的测试程序进行验证。系统级的测试程序还不是时钟精度和引线精度

30、上的测试。但系统级的测试程序应当能转换为适当的格式，供硬件RTL模拟和软件验证使用。(2)SOC硬件RTL验证：通过系统设计，得到硬件RTL代码和测试程序，然后进行RTL硬件功能验证，包括Lint检查、逻辑模拟、代码覆盖分析、基于事务的验证、形式模型检验等。(3)SOC软件验证：软件验证中，软件和测试文件从软件设计团队得到，并针对系统设计中得到的软件设计说明进行软件验证。根据验证要求，软件验证和软/硬件集成验证可以采用软件原型、快速原型、仿真、软/硬件协同验证等方法。 58(4)网表验证：RTL设计经综合后，得到门级网表，门级设计验证可采用RTL-门级形式等价验证，保证两者逻辑上的等价性。接下来由于时钟树和可测试性设计扫描链的插入，