name: verification-strategy
description: "verification_workflow 流水线的第 3 步。根据第 2 步生成的测试点列表，为每条测试点确定最优的验证手段——回答每条测试点"应使用何种手段验证"。可用手段只有两种：动态仿真（SIM）或形式化验证（FORMAL）。输出为测试点到验证手段的映射策略表，并附带决策依据。触发条件：由 verification_workflow 在第 3 步调用，或用户直接需要为一组测试点规划验证策略时触发。"
验证策略规划（第 3 步）
概述
本 skill 是 verification_workflow 流水线的第 3 步。
目标：针对 verification-testpoints.md 中的每条测试点，决定采用哪种验证手段来证明它，并记录决策依据。
输入：
- DUT Spec 文档
- RTL 源代码
verification-targets.md（来自第 1 步）verification-testpoints.md（来自第 2 步）
输出：verification-strategy.md —— 测试点到验证手段的映射策略表，附带决策依据
可用验证手段
本流程只区分两种验证手段，不在仿真内部细分定向/随机：
手段一：动态仿真（SIM）
定义：通过运行 RTL 仿真驱动激励、观察响应来验证行为。测试用例的具体实现形式（定向序列、约束随机、UVM 等）由后续实施阶段决定，本阶段不关心。
适合：
- 功能行为验证（需要运行设计才能观察到的行为）
- 需要参考模型 / 记分板进行数据比对的测试点
- 性能/吞吐量测量（需要跑足够长时间的仿真）
- 状态空间大、需要覆盖率驱动的测试点
- 复杂协议交互、数据通路变换
局限：概率性，不能穷举；验证完备性依赖覆盖率收敛。
手段二：形式化验证（FORMAL）
定义：使用模型检查（BMC、k-归纳、PDR/IC3）对 SVA 属性进行数学穷举证明，对所有可能的输入序列进行验证。
适合：
- 可表述为"对所有输入，属性 P 恒成立"的测试点
- 结构性不变式：One-hot、互斥、无死锁
- 协议握手不变式（如：VALID 拜高期间 DATA 稳定）
- 复位后状态正确性
- 随机仿真极难命中的深度角落（概率 < 1/2^20）
- DUT 子范围较小（状态位数 < ~50K）且无复杂数据变换
局限：状态空间爆炸，不适合大型数据通路；需 SVA 属性编写能力。
决策框架
为每条测试点按以下顺序判断：
规则 1 —— 优先考虑 FORMAL
若测试点同时满足以下所有条件，选 FORMAL：
- 可以写成"对所有输入/序列，某属性成立"的命题
- 所涉及的 DUT 子结构较小（无大型数据通路或存储阵列）
- 不需要参考模型进行逐拍数据比对
否则，进入规则 2。
规则 2 —— 其余情况使用 SIM
不满足 FORMAL 条件的测试点，一律选 SIM：
- 功能行为（需要实际运行观察输出）
- 数据通路正确性（需要参考模型比对）
- 性能与吞吐量
- 大状态空间的协议场景
规则 3 —— 高优先级测试点可双重覆盖
若测试点标记为 P0，且同时满足 FORMAL 条件，可分配 FORMAL + SIM 以获得最高置信度。
规则 4 —— 标记不在范围内的测试点
若测试点关联的目标在第 1 步中被标记为"不在范围内"，将手段标记为 N/A（不在范围内） 并附注说明。
优先级分类
同时为每条测试点分配优先级：
| 优先级 | 含义 |
|---|
| P0 | 流片前必须通过。若未通过，设计正确性存在风险。 |
| P1 | 高价值。应在硅片 bring-up 前通过。 |
| P2 | 建议完成。应在最终 sign-off 前完成。 |
| P3 | 锦上添花。尽力完成。 |
默认分配启发式规则：
[CLK_RST] 和 [SAFETY] 测试点 → P0- 所有引用核心 Spec 需求的
[FUNC] 测试点 → P1
[INTF] 协议合规性 → P1[CORNER] 和 [PERF] → P2[LOW_PWR] 和 [INTEG] → 根据设计意图为 P1 或 P2[LOW_PWR] 若功耗预算是硬性 Spec 要求 → P0/P1
输出格式
生成 verification-strategy.md，结构如下：
# 验证策略 — <DUT 名称>
## 摘要
| 验证手段 | 测试点数量 |
|----------|------------|
| FORMAL | <n> |
| SIM | <n> |
| FORMAL + SIM | <n> |
| N/A（不在范围内） | <n> |
| **合计** | **<N>** |
## 策略表
| 测试点 ID | 简要描述 | 类别 | 手段 | 优先级 | 决策依据 |
|----------|---------|------|------|--------|----------|
| TP-FUNC-001 | <简要> | FUNC | SIM | P1 | 需运行仿真观察数据通路输出 |
| TP-CLK_RST-001 | <简要> | CLK_RST | FORMAL | P0 | 结构性不变式，需穷举证明 |
| TP-INTF-001 | <简要> | INTF | FORMAL + SIM | P0 | P0 协议属性，双重覆盖 |
...
## 备注与假设
<依赖用户输入做出的决策，或权衡取舍说明>
输出交接
本步骤完成后：
- 向用户展示策略摘要表供审阅。
- 重点标出所有 P0 测试点，并确认其手段分配。
- 询问："是否需要调整任何手段分配？是否需要升级或降级某些测试点的优先级？"
- 确认后，保存为
verification-strategy.md。
- 告知用户："第 3 步已完成。验证策略已全部定义。您可以根据此策略开始构建验证环境和测试用例。"
