跳到正文
半导体开放世界

功能验证

Functional Verification也称 仿真验证

以可追踪规格为判据，系统寻找设计实现与预期行为之间不一致的活动。

基础出处 2 本教材
报告问题

速览

约 1 分钟

验证不是“跑几个波形”，而是把需求拆成场景、激励、检查器、断言和覆盖目标，并用回归持续证明已检查到哪些风险。

系统理解

约 2 分钟

功能验证围绕DUT、参考模型、激励生成、协议监视、检查器和覆盖模型建立闭环。定向仿真适合已知场景，受约束随机有助于探索组合空间，断言表达局部时序性质，形式方法在有限模型和假设下搜索反例。代码覆盖率只说明结构被执行，功能覆盖率只说明预先定义的场景被观察；两者都不能单独证明没有缺陷。

与RTL开发并行，并贯穿综合前后、系统集成和硅后验证。

公式提示

覆盖率可写为C=Ncovered/Neligible，但分母如何定义决定指标含义；未纳入覆盖模型的需求不会因C=100%而自动被验证。

关键参数

关键参数
参数单位含义
需求覆盖%有明确验证目标和结果证据的规格条款比例
功能覆盖%覆盖模型中已命中的场景、交叉项和边界值比例
回归通过率%同一版本与环境下通过检查的测试比例
未关闭缺陷—尚未修复、豁免或确认不可达的有效问题数量

常见误区

  • 把测试平台没有报错当成设计已被证明正确
  • 把代码覆盖率100%等同于规格覆盖完整
  • 混淆设计前功能验证、流片后硅验证与制造测试
  • 只追求随机用例数量而不保留种子、检查机制和需求追踪

工程深入

12 条结论 · 1 道例题

规格、对象与验证闭环

定义

功能验证寻找实现与规格的不一致

功能验证以可追踪需求为判据，对设计模型施加场景并检查可观察结果，目标是尽早发现反例，而不是仅证明若干示例能够运行。12

成立条件 规格需定义正常、边界与异常行为；结论只覆盖已建模并被观察的需求

机制

验证计划把规格拆成可关闭目标

验证计划为需求分配场景、方法、检查器、覆盖点、负责人和关闭准则，使每条结论都能回溯到规格与执行证据。12

成立条件 规格变更必须同步更新计划与覆盖模型；未分配目标的条款不能被默认视为已验证

机制

测试环境由激励、观察和判定共同构成

完整测试环境需要生成合法或故意非法的输入、监视接口事务，并把DUT输出与断言、参考模型或预期结果比较；只有激励而没有自动判定无法形成稳定回归。12

成立条件 观察点必须覆盖关键内部或外部结果；检查器本身也需用已知样例校准

激励、检查与反例

机制

定向与随机激励解决不同搜索问题

定向测试便于复现指定功能和边界条件，随机或受约束随机测试有助于探索交互组合；有效流程通常以场景目标和检查质量约束测试数量。12

成立条件 随机测试需保存种子和配置；约束过强可能屏蔽错误，过弱则可能产生大量无效事务

机制

断言把局部时序规则变成持续检查

断言可表达请求后应答、状态互斥、握手稳定性或禁止事件等性质，在仿真或形式分析中自动报告最早违反规则的轨迹。12

成立条件 断言的时钟、复位和前提假设必须明确；断言成立不表示未表达的需求也成立

机制

参考模型与记分板检查端到端数据

参考模型计算抽象预期结果，记分板按事务身份、顺序或允许重排规则进行比较，从而把长流水、多并发和缓存行为转换为可定位的差异。12

成立条件 参考模型应与RTL保持实现独立；允许的舍入、延迟和乱序窗口需由规格定义

覆盖率与收敛

边界

代码覆盖与功能覆盖回答不同问题

代码覆盖记录语句、分支或条件是否被执行；功能覆盖记录预先定义的场景和交叉组合是否被观察。前者不能识别遗漏需求，后者也不能证明检查器正确。12

成立条件 覆盖豁免需说明不可达或无需覆盖的理由；覆盖模型应与需求追踪表共同评审

公式

覆盖率取决于分母的工程定义

覆盖率是已覆盖目标与纳入统计目标的比值；如果遗漏重要场景、交叉项或边界值，即使数值达到100%也不能推出规格完整。12

C = Ncovered / Neligible

C
给定覆盖模型下的覆盖比例
Ncovered
已满足关闭条件的覆盖项数量
Neligible
纳入统计且未被批准豁免的覆盖项数量

成立条件 分子和分母需采用同一覆盖模型版本；不可达项应通过审查后豁免而不是静默删除

例题：动手算一次教学假设，可复算

某一版功能覆盖模型有1000个纳入统计且未豁免的覆盖项，本轮回归关闭了920项；该版覆盖率和仍未关闭的项数是多少？

已知

  1. Neligible=1000
  2. Ncovered=920
  3. 所有数量来自同一覆盖模型版本
  4. 未把未建模需求计入分母

步骤

  1. C=920/1000=0.92=92%，用已关闭覆盖项除以纳入统计的有效覆盖项
  2. Nopen=1000−920=80，列出仍需生成激励、补检查器或评审豁免的覆盖缺口
结果 该模型版本的覆盖率为92%，仍有80个覆盖项未关闭。

92%只回答当前覆盖模型内的收敛程度；下一步应逐项判断80个缺口是激励不足、检查器缺失、不可达还是规格遗漏。

不能外推到 该数值不能证明设计有92%正确，更不能覆盖模型之外的需求、错误检查器或硅后制造缺陷。

机制

回归必须能够重现失败

回归把相同测试集、检查器和环境持续应用到新版本；失败定位依赖代码版本、配置、随机种子、工具版本和日志被完整保留。12

成立条件 环境变更需与DUT变更分开记录；不稳定测试应修复根因而不是简单重复运行

方法边界与实现衔接

边界

形式验证的完备性受模型和假设限制

形式工具在给定状态空间、性质和环境假设下搜索证明或反例；抽象不当、状态爆炸或错误假设都会限制结论，不能把局部证明外推为整芯片无缺陷。12

成立条件 性质和环境假设需独立评审；复杂设计可采用分块、抽象和有界分析

边界

等价检查不替代规格验证

逻辑等价检查判断RTL与综合或修改后的实现是否保持同一功能关系；如果RTL本身误解规格，等价实现仍会忠实保留该错误。12

成立条件 复位、黑盒、存储器和时钟门控模型需一致；设计变更超出等价假设时需补充功能验证

关联

功能验证与制造测试处于不同生命周期

功能验证在设计阶段检查模型是否满足规格；制造测试在芯片生产后用可观察、可控制结构筛除物理缺陷。两者会共享测试思想，但目标、故障模型和成本约束不同。12

成立条件 硅后验证还需检查真实器件、封装和系统环境；DFT在设计期插入结构以服务制造测试

RTL 用于：RTL是设计期功能验证的主要被测模型。
ATE 对比：ATE面向制造后芯片的可控激励、测量与筛选。

出处

2 本教材 · 2 处引用
  1. 1
  2. 2