SoC设计9参考文档

第九章 SoC功能验证 内容大纲 功能验证概述功能验证方法与验证规划系统级功能验证仿真验证自动化形式验证基于断言的验证 内容大纲 功能验证概述功能验证方法与验证规划系统级功能验证仿真验证自动化形式验证基于断言的验证 随着设计的进行 越接近最后的产品 修正一个设计缺陷的成本就会越高 不同设计阶段修正一个设计缺陷所需费用示意图 验证的概念 在IC设计与制造领域 通常所说的验证 Verification 和测试 Test 是两种不同的事验证在设计过程中确认所设计的正确性通过软件仿真 硬件模拟和形式验证等方法进行在流片之前要做的 测试检测芯片是否存在制造或封装过程中产生的缺陷 采用测试设备进行检查 功能验证 功能验证一般是指设计者通过各种方法比较设计完成的电路和设计文档规定的功能是否一致 保证逻辑设计的正确性 通常不包括面积 功耗等硬件实现的性能检测 SoC功能验证的挑战 系统复杂性提高增加验证难度设计层次提高增加了验证工作量发展趋势 内容大纲 功能验证概述功能验证方法与验证规划系统级功能验证仿真验证自动化形式验证基于断言的验证 仿真为基本出发点的功能验证方法 功能验证开发流程 制订验证计划功能验证需求激励产生策略结果检测策略验证开发提高验证的效率 内容大纲 功能验证概述功能验证方法与验证规划系统级功能验证仿真验证自动化形式验证基于断言的验证 系统级功能验证 行为级功能验证测试数据控制流 包括初始化和关闭I O设备 验证软件功能 与外界的通信 等等性能验证通过性能验证可以使设计者清楚地知道整个系统的工作速度 功耗等性能方面的指标 协议验证根据总线协议对各个模块的接口部分进行验证 系统级验证 系统级的测试平台边界条件设计的不连续处出错的条件极限情况系统级的测试平台标准性能指标覆盖率指标 内容大纲 功能验证概述功能验证方法与验证规划系统级功能验证仿真验证自动化形式验证基于断言的验证 仿真验证平台 激励的生成 直接测试激励 检测到测试者所希望检测到的系统缺陷可以快速 准确地产生大量的与实际应用一致的输入向量随机测试激励 检测到测试者没有想到的一些系统缺陷带约束的随机测试激励是指在产生随机测试向量时施加一定的约束 使所产生的随机测试向量满足一定的设计规则 带约束的随机激励生成的例子 x1和x2为系统的两个输入 它们经过独热码编码器编码之后产生与被验证设计 DUV 直接相连的输入输入约束 in 0 in 1 in 2 1这样产生的随机向量就可以保证它们的合法性 用SystemVerilog语言写的带约束随机激励生成例子 输入data的数量限制在1 1000 programautomatictest defineconstraintclassTransaction randbit 31 0 src dst data Dynamicarrayrandcbit 2 0 kind Cyclethroughallkindsconstraintc len data sizeinside 1 1000 LimitarraysizeEndclass instantiationTransactiontr startrandomvectorgenerationinitialbegintr new if tr randomize finish transmit tr endendprogram 响应的检查 可视化的波形检查 直观 但不适用于复杂系统设计自动比对检查 通过相应的检测模型或验证模型来自动完成输出结果的比对 覆盖率的检测 覆盖率数据通常是在多个仿真中收集的覆盖率的模型由针对结构覆盖率 StructuralCoverage 和功能覆盖率 FunctionalCoverage 两种目标而定义的模型所组成 可细化为 限状态机覆盖率 FSMCoverage 表达式覆盖率 ExpressionCoverage 交叉覆盖率 CrossCoverage 断言覆盖率 AssertionCoverage 用SystemVerilog语言写的覆盖率检测的例子 programautomatictest busifc TBifc classTransaction randbit 31 0 src dst data randenum MemRd MemWr CsrRd CsrWr IoRd IoWr Intr Nop kind endclasscovergroupCovKind coverpointtr kind MeasurecoverageendgroupTransactiontr new InstantiatetransactionCovKindck new Instantiategroupinitialbeginrepeat 32 begin Runafewcyclesif tr randomize finish ifc cb kind tr kind transmittransactionifc cb data tr data intointerfaceck sample Gathercoverage ifc cb Waitacycleendendendprogram 内容大纲 功能验证概述功能验证方法与验证规划系统级功能验证仿真验证自动化形式验证基于断言的验证 形式验证 形式验证 FormalVerification 静态形式验证 StaticFormalVerification 和半形式验证 Semi FormalVerification 静态形式验证不需要施加激励 也不需要通过仿真来验证 目前 SoC设计中常用的静态形式验证方法是相等性检查 半形式验证是一种混合了仿真技术与形式验证技术的方法 常用的半形式验证是混合属性检查或模型检查 它将形式验证的完整性与仿真的速度 灵活性相结合 静态形式验证 相等性检查 EquivalentCheck 对设计进行覆盖率100 的快速验证主要是检查组合逻辑的功能相等性不需要测试平台和测试矢量 不需要进行仿真可用于比较RTL与RTL RTL与门级 门级与门级的功能相等性 被广泛应用于版图提取的网表与RTL代码比较 特别是做完ECO后要进行网表和修改后的RTL的相等性检查 半形式验证 半形式验证 Semi FormalVerification 仿真和形式验证形结合 如混合模型检查 ModelChecking 或属性检查 PropertyChecking 的方法 内容大纲 功能验证概述功能验证方法与验证规划系统级功能验证仿真验证自动化形式验证基于断言的验证 基于断言的验证 仿真验证面临的问题 可观测性和可控制性合适的输入矢量能够激活错误错误要能够以某种预期的形式输出采用断言描述设计的行为 在仿真时起到监控作用 当监控的属性出现错误时 立刻触发错误的产生 增加了设计在仿真时的可观测性问题 也可以用在形式属性检查中作为要验证的属性 属性检查 PropertyCheck 时 是对整个状态空间进行搜索 能够控制到每一个信号并能指出错误的具体位置 解决了设计验证时的可控制性和可观察性问题 验证实现所花费的时间与验证的质量 断言的作用 断言的作用 断言语言及工具的使用 断言语言CorSystemCSystemVerilogAssertion SVA PropertySpecificationLanguage PSL IBM basedonSugar OpenVerificationLibrary OVL Verilog VHDL SVA SystemVerilogAssertion 例子 用Verilog实现的检查器 always posedgeA beginrepeat 1 posedgeclk fork A to Bbegin posedgeB display SUCCESS Barrivedintime n time disableA to B endbeginrepeat 1 posedgeclk posedgeB display SUCCESS Barrivedintime n time disableA to B endbeg