验证技术概述课件

验证技术概述 内容 验证技术概述功能验证 等价性验证 静态分析及物理检查3 模拟4 形式验证5 验证方法学 CellLibraryDesignRule 自顶向下 验证的重要性 验证的重要性 占工程设计时间 70 代码总量 80 验证影响 产品的生命产品返工失去顾客成本 验证的目的及其本质 验证的目的 原始描述的正确性 SPEC设计结果与原始描述的一致性设计结果是否符合设计规则验证的本质 验证本质上就是保证某种形式的转换符合我们的期望 即保证设计正确的实现了规范所定义的功能和性能要求 芯片的设计规范 一般是一个文本文件 与其系统级模型 高级语言模型 如C模型 之间的等效通过比较系统级模型与HDL实现的输出 可以在规范的系统级模型与其HDL实现之间建立等效关系 HDL实现与门级 综合后的 之间通过应用 逻辑等效性检查 可以建立等效 工程对验证的要求 验证的完整性 只有充分接近全部功能得到验证 并达到功能覆盖率的要求 才能对产品有信心 验证的自动化 尽可能减少验证时间对产品产出时间的影响 验证才是成功的 这需要EDA工具和先进验证手段的支持 验证系统 验证系统的组成 验证说明 描述目标行为以及不希望出现之行为的设计规范 Specification 成品模型 环境模型 模型类别 硬件 prototype 仿真 Emulation 软件 CorRTLCode 模拟 Simulation 混合 设计各阶段验证的内容 前端设计 功能验证 代码是否符合设计规范等价性验证 各层次的功能是否满足原有功能规范后端设计 功能 门级仿真 后仿真 性能 setup hold 驱动 静态时序分析物理设计 规则检查 designrulecheck 电气规则检查 ERC 设计规则检查 DRC 版图对电路检查 LVS 信号完整性 干扰 金属迁移 噪声 功能验证 分类 目的性验证 目的是验证设计所试图完成的功能在设计中已正确实现 最典型的情况是在抽象程度最高的层次完成 其最终结果是建立一套 黄金模型 它可以在整个设计过程中作为设计细节的参考 等价性验证 目的是验证设计过程中产生的不同层次的设计结果功能是否符合 黄金模型 目的性验证 1 动态模拟 将一组输入激励施加到设计模型上 使其工作运行 并观察模型的响应 2 形式验证 用数学方法验证设计的功能 不需要验证测试向量 3 模拟 形式混合验证 混合验证取两者之优点 模拟能处理的设计规模大 类型多 而形式验证具有完整性 4 软 硬件协同验证 协同验证可以在硬件开发的同时 让软件在硬件模拟平台上运行 从而硬件和软件可以同时调试 而不是串行进行 大大缩短了产品的开发时间 目的性验证 续 5 仿真系统 专门设计的硬件和软件系统 典型的是采用FPGA 与最终设计接近的仿真速度 6 样机系统 系统测试 市场开发 演示 1 物理样机 一种目标设计的硬件替代品 它的运行能够 接近 目标设计平台的性能 与目标系统速度相同的数量级 比仿真系统的速度快出许多 2 虚拟样机 一个虚拟样机就是一个产品 一个元件或一个系统的计算机模拟模型 物理样机 Parterre之FPGA验证平台 等价性验证 1 动态等价验证i 确定模拟 复用高层次模型开发的验证测试向量和测试程序ii 回归测试 批处理模拟 自动比较结果2 形式等价验证 完全的等价验证 如Formality 形式等价验证工具生成一个数据结构并比较在相同的输入模式下得出的输出数值模式 如果这些输出数值模式不相同 那么同一设计的两种描述 如门级和RTL级 就不是等价的 组合等价检验和时序等价检验 静态分析验证 1 Lint检查 对设计代码进行静态检查 验证语法的正确性 Lint检验对RTL设计代码进行静态检查 是在设计进行综合前的一种预处理 目的是消除代码中的错误 包括语法 可综合性 未初始化的变量 未支持的语言结构 端口失配等 有些工具还能抽取FSM模型 检测竞争条件 检查可测试性和可重用性规定的一些设计规则等 2 静态时序分析每个存储元件有时序要求 例如 建立时间 保持时间和各种延时 时序验证要确定电路时序是否满足设计要求 物理验证 物理验证就是通过检验图形设计的数据库以确信物理实现确实是原始逻辑设计的正确表述 物理验证包括以下三个部分 电学规则检查 设计规则检查及版图对电路检查 标准的图形数据库形式是GDSII 数据流 物理验证 续 1 电气规则检查 ERC 检查是否违反电气设计规则 包括未使用的输出 浮空输入 负载违例 连接违例 如开路和短路等 2 设计规则检查 DRC 检查是否违反工艺过程设计规则 包括层与层的间距 特定层上的线条宽度 层与层的重叠等 3 版图对电路检查 LVS 检验提取的图形数据库是否有与 黄金 网表相违背之处 LVS工具从多边形数据中构建网表以及从物理布局中提取器件模型 提取出的网表需和 黄金 模型保持一致 所有的器件和互连都必须严格地相匹配 4 其他物理验证 包括信号完整性 干扰 金属迁移 噪声等 模拟 基于模拟的验证是功能验证最重要 用得最多的一种方法 它是在模拟器上通过模拟实际电路的工作环境来对设计进行验证 模拟的基本方法 首先根据设计规范和测试规范 建立测试平台 编写测试数据组 testcase 以生成测试激励以及响应检查 然后在模拟器上进行模拟 将测试数据组的激励输入到硬件描述语言代码模型最后对输出同标准输出结果进行比较 从而达到功能验证的目的 基于模拟的验证 基于模拟的验证结构可分为四个部分 测试数据组 testcase 测试平台 testbench 参考模型 referencemodel 仿真器 simulator 测试数据组 测试数据组是对待测模型产生激励的来源 设计测试数据组的关键是确定待测模型需要验证的属性 features 也就是功能验证点 正确识别和详细分析属性 并依此产生相应的测试数据组 决定了验证的功能覆盖率 从而最终决定了待测模型是否充分满足设计规范的要求 测试数据组的生成 是由验证工程师手工编写 目前也出现了自动测试数据组生成工具 如synopsys的半自动测试数据组生成工具Vera 它利用语言定义各种约束 以指导伪随机测试的生成 结合功能覆盖分析 帮助验证工程师建立高效的验证环境 使得到高质量的测试程序 测试数据组 续 每一个测试数据组一般包括激励数据和输出响应数据 在实际设计过程中 测试数据组通常分为三部分 接口测试 检验模块接口时序和协议子模块测试 子模块功能验证系统测试 全系统功能验证 测试平台 测试平台是为模拟验证而编写的代码 其目的是用来对待测设计产生预先确定的输入序列 然后选择性的观察响应 测试平台可采用硬件描述语言来编写 也可以采用e或OpenVera等验证语言编写 结构化的测试平台 可复用的测试基准 BFM Bus FunctionModel 概念 将测试数据组提供的测试数据 通过统一的任务接口 按照待测模型端口的时序和协议进行封装组合的程序模块 由子程序以及Task等组成 代替总线的简单模型 可以复用 结构化的测试平台 BFM原理 能够使用某种命令语言在总线上产生一系列事务 不含有总线设备的实现 亦不需要包含总线设备的全部功能只含有总线 I O接口的信号 并模拟这些信号的传输过程 参考模型 参考模型 一种专门面向功能验证而设计的代码 可以在施加于待测设计的相同激励条件下 产生预期的结果 该结果做为testbench检查器的预期响应参与比较 参考模型的主要目的就是生成与目标设计描述进行比较的比对数据 参考模型侧重于设计的逻辑功能 而不是功能实现的细节 参考模型 DesignUnderTest DUT 激励发生器 结果检查 黄金模型goldenmodel 验证实例 UART 验证环境和测试方案 testbench根据设计文档确定验证点 testcase 验证文档 描述每个验证点的目的 具体实现步骤验证文档 testcase提取覆盖率分析 不理想 回到第2阶段记录验证结果 log文件 验证环境架构及建立方式 基于软件模拟的层次式架构testcase层 由过程 procedure 调用组成行为模型以及BFM 不可综合的代码 描述系统环境中可能的其他电路模型或行为testbench 验证配置testbench组织 configurations装配testcase 行为模型 BFM以及待测模块DUT UART验证环境架构 确定验证点 testcase提取 tasks激励 从单一功能到复杂功能 辅以覆盖率工具响应 针对具体testcase描述检查相关响应 例 数据发送进程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 write任务向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提取 testcase实例 simulus taskserial data input generater input 7 0 data input 1 0 verify indicate inputbaudrate clk outputRXD verify indicate 1 1 表示有校验位 否则无校验位 verify indicate 0 1 表示奇校验 否则为偶校验 wireverify bit verify indicate 0 data data begin posedgebaudrate clk TXD 1 b0 posedgebaudrate clk TXD data 0 posedgebaudrate clk TXD data 1 posedgebaudrate clk TXD data 2 posedgebaudrate clk TXD data 3 posedgebaudrate clk TXD data 4 posedgebaudrate clk TXD data 5 posedgebaudrate clk TXD data 6 posedgebaudrate clk TXD data 7 posedgebaudrate clk TXD verify indicate 1 verify bit 1 b1 posedgebaudrate clk TXD 1 b1 endendtask testcase实例 receivingdata moduletestbench for UART RXD 例化待测模块UARTUARTu1 RXD TXD 顺序执行任务序列 进行功能验证initialbegin 调用激励产生模块 输入数据8 ha5 1位偶校验位serial data input generater 8 ha5 2 b10 baudrate RXD End endmodule testbench 1 将上述task在testbench的process中排列组合 分别调度就组成一个面向UART的黑盒子testbenchgenerater2 把UART和testbenchgenerater在顶层模块配置指定 testbench 则可进行模拟验证 模拟仿真工具 模拟工具 模拟器 SimulatorVerilog XLModelsimNCVerilogVSS VHDL VCS Verilog 模拟仿真工具 模拟器工作原理 编译法 Compiler 将HDL的描述编译成一般软件语言或汇编语言再执行事件表驱动法 EventDriven 对描述进行解释执行CycleBased NCVerilog 一个时钟周期只采一次数据ISS InstructionSetSimulation 指令级模拟器 用于有CPU的系统模拟 模拟仿真工具 仿真 Emulation FPGA把设计从RTL综合后写入FPGA中 与周边芯片连成系统进行板级仿真 特点 验证功能及接口 速度快 界于实物芯片和模拟之间 只模拟功能 不模拟速度 基于模拟的验证方法 组合逻辑 MEM n m 穷举模拟 可能的状态转换 2n m 基于模拟的验证方法 测试向量生成 规范一致性测试 所有 指令 控制模式 边角测试 CornerCase 随机测试无向随机模拟有向随机模拟设计错误模型实代码 RealCode 回归测试 Regressiontesting 基于模拟的验证衡量方法 代码覆盖率通过硬件代码覆盖率分析工具来评定验证测试序列的覆盖率指标 把特定的测试验证序列输入到特定设计中 通过代码覆盖率分析就有可能得出功能覆盖率的某些方面的信息 分析工具可以提供以下信息 每个被评估属性的百分比的覆盖率值设计中没有执行或者只是部分执行的区域的列表可进行有目的的状态覆盖尝试改变原始模拟踪迹 进行指导 代码覆盖的类型 语句覆盖 表示多少语句已被执行过 或者每个语句执行过的次数 翻转覆盖 表示信号中哪些位已经过0 1和1 0翻转 触发覆盖 每个进程是否被敏感表中每个信号独立地触发 分支覆盖 if 或 case 语句中的哪些分支己被执行表达式覆盖 if 语句中条件布尔表达式的覆盖情况路径覆盖 由 if 和 Case 语句构成的所有可能的路径是否己被验证 变量覆盖 信号或地址的覆盖情况 是翻转覆盖的扩充 FSM代码覆盖 基于模拟的验证衡量方法 功能覆盖率 由用户定义的 反映在验证过程中被运行到的功能点的范围的衡量方法 功能点可以是对用户而言可视的体系结构特点 也可以是主要的微结构特征 通常情况下 这些特征不能从实现中自动生成 因此需要在验证testbench中的一些规范 功能覆盖率数据一般是一些时序行为 如总线的交易 和一些数据 如交易源 目的和优先级等 的交叉组合 附加覆盖率信息可以从功能覆盖率点的交叉引用中得到 比如 在一个器件的两个引脚之间进行的数据处理的相互关系 或者在一个处理器中指令和中断的关系等 基于模拟的验证衡量方法 period1period2 BUGRATE Time effort readytoshipship Bugratewithcodecoverage 基于模拟的验证的问题 RTL模拟 一个月 一个月功能仿真 一天 一个月电路仿真 一分钟 一小时芯片 一秒 一分钟 ValidityTest 108矢量 BootUnix 1010矢量 形式验证 形式验证 利用数学方法对设计结果的功能进行验证 由于它依赖于对设计的数学分析 因此无需使用验证测试向量 目前包括如下几种技术 模型检查定理证明形式等价检验 模型检查 模型检查将设计描述及其部份规范的特性作为输入 以证明该设计是否具有某种特性 其过程是搜索一个设计在所有可能条件下的状态空间 寻找不符合某特性的点 如果找到这样的点 则可证明该特性不正确 模型检查不需要设置任何验证测试 所需验证的特性以队列形式用特性说明语言描述 当模型检查工具发现一个错误 工具可从初始状态开始 进行完全的状态跟踪 直至出错的状态 定理证明 在定理证明的过程中特性被表述为数学命题 而设计则表述为数学实体 该实体表示为若干公理 证明的过程就是看数学命题是否可从公理中演绎得到 如果得到 则该特性存在 否则 该特性则不存在 定理证明的主要缺点 用户必须用定理证明器的命令来构造证明过程 当证明结论为不成立 只能用人工方法分析其原因 不能自动跟踪 静态时序分析 STA 发现使芯片时序失效和对芯片性能起决起决定作用的电路关键路径 性能验证 时序分析 在同步时序电路中 2个寄存器之间组合电路延迟之和 建立时间 保持时间 寄存器间的信号传播延迟 决定了最大时钟频率 设其中 setup 20ns hold 30ns not b 15ns and d 25ns 则从D1到D2Totaldelay 20 30 15 25 90ns 性能验证 时序分析 性能验证 时序分析 建立时间 setup 信号S1高电平相对S2上升边之前应保持稳定的时间 保持时间 hold 信号S1高电平相对S2上升边之后应保持稳定的时间 S2 hold setup hold时间为从clk到来时 D Q的传输时间 Setup为防止时钟歪斜等不定因数 S1 长路径错误设其中 setup 20ns hold 30ns not b 15ns and d 25ns 则从D1到D2Totaldelay 20 30 15 25 90ns要求 时钟周期 90ns频率 1 90 11MHz如时钟周期 90ns即发生长路径错误 setup违背 性能验证 时序分析 短路径错误由于时钟歪斜 skew 太大而引起 在一个周期内信号穿过两个寄存器 从而产生逻辑错误 性能验证 时序分析 静态时序分析 STA STA工作原理 采用穷尽分析方法 提取出所有时序路径计算信号在这些路径上的传播延迟检查信号的建立和保持时间是否满足时序要求通过对最大路径延迟和最小路径延迟的分析 找出违背时序约束的错误 STA优点 如果采用模拟的方法 由于输入矢量的局限性 可能无法检查出某些路径存在的时序失效STA不要求输入矢量 能很快得到分析结果 节省了很多的设计时间 性能验证 后仿真 集成电路设计的验证方法学 验证规划验证和设计分离原则周密的验证计划设计验证方法学 根据不同性质的项目可以采用不同的验证方法学 抽象级和模型 定义设计的各个抽象级 以及相应的 说明 和 实现 以便决定采用合适的验证技术 此外 要准备好验证时所需的相应的合适电路模型 验证技术和工具 不同层次的验证需要选用不同的技术及其相应的EDA工具 验证测试 不同抽象级的验证相应有不同的测试 关键是要产生各种测试程序 如何应用这些测试程序 以及测试程序如何在各层次中移植等 构成测试的元素应包括 测试激励 对于动态模拟 可以是各种类型的测试向量 而对于形式验证 则要定义设计的特性和约束等 测试检查器 包括期望的测试响应 协议 黄金模型等 测试评估 包括能力测度 如运行时间 存储器规模等 以及质量测度 如功能覆盖 代码覆盖等 验证流程 往往是迭代的和并行的 而非单调和串行的 此外包括验证的跟踪 所发现的设计错误处埋以及验证文档等 验证方法学 自顶向下的验证方法 1 系统级验证 系统的行为由顶层系统说明规定 系统的行为用行为模拟测试程序进行验证 然后系统映射到合适的体系结构 利用IP模块进行硬件和软件划分 该体系结构的功能和性能用系统行为模拟中建立的测试程序进行验证 系统级的测试程序还不是时钟精度和引线精度上的测试 但系统级的测试程序应当能转换为适当的格式 供硬件RTL模拟和软件验证使用 2 SOC硬件RTL验证 通过系统设计 得到硬件RTL代码和测试程序 然后进行RTL硬件功能验证 包括Lint检查 逻辑模拟 代码覆盖分析 基于事务的验证 形式模型检验等 3 SOC软件验证 软件验证中 软件和测试文件从软件设计团队得到 并针对系统设计中得到的软件设计说明进行软件验证 根据验证要求 软件验证和软 硬件集成验证可以采用软件原型 快速原型 仿真 软 硬件协同验证等方法 4 网表验证 RTL设计经综合后 得到门级网表 门级设计验证可采用RTL 门级形式等价验证 保证两者逻辑上的等价性 接下来由于时钟树和可测试性设计扫描链的插入 网表必须再通过等价验证 以确保设计的正确性 此外 从这里开始 静态时序分析验证在以后各阶段需要反复进行 以