# {DUT} 形式化验证总结报告

> **UCAgent 机器可读模板**
>
> - **目的**: 本模板用于在验证总结阶段（verification_review_and_summary）撰写最终的形式化验证总结报告 `05_{DUT}_formal_summary.md`。
> - **来源**: UCAgent (AI) 汇总各阶段产物（avis.log、fanin.rep、env_analysis.md、bug_report.md）生成。

---

## 1. 验证范围与策略

> 从 `01_{DUT}_verification_needs_and_plan.md` 和 `02_{DUT}_basic_info.md` 提取

- **DUT 名称**: {DUT}
- **验证范围**: [列出被验证的功能模块/子系统]
- **逻辑类型**: [组合逻辑 / 时序逻辑]
- **时钟/复位**: [时钟名, 复位名, 极性]
- **验证引擎**: [使用的引擎配置，如 pdrx / bmc -depth 50]
- **验证策略概述**: [简述采用的验证策略——白盒/黑盒、是否用符号化索引等]

---

## 2. 属性统计

> 从 `avis.log` 提取最终属性状态

| 属性类型 | 数量 | 占比 |
|---------|------|------|
| Assert PASS | - | -% |
| Assert FALSE (RTL_BUG) | - | -% |
| Assert FALSE (ENV_FIXED) | - | -% |
| Assert TRIVIALLY_TRUE (ACCEPTED) | - | -% |
| Cover PASS | - | - |
| Cover FALSE | - | - |
| **Total** | - | 100% |

---

## 3. 发现的 RTL 缺陷摘要

> 从 `04_{DUT}_bug_report.md` 提取关键发现

| 缺陷编号 | 缺陷描述 | 影响的属性 | 严重等级 | 根因（一句话） |
|---------|---------|-----------|---------|-------------|
| BG-XXX-001 | - | A_CK_XXX, A_CK_YYY | 严重/中等/低 | - |

> 若无 RTL 缺陷，写明："形式化验证未发现 RTL 设计缺陷。"

---

## 4. COI 覆盖率结果

> 从 `fanin.rep` 提取最终覆盖率数据

| 指标 | 覆盖/总数 | 百分比 |
|------|----------|-------|
| Inputs (输入端口) | -/- | -% |
| Outputs (输出端口) | -/- | -% |
| Dffs (寄存器) | -/- | -% |
| Nets (组合逻辑) | -/- | -% |

- **未覆盖信号处理**: [全部覆盖 / N 个标记为 UNREACHABLE，原因：...]

---

## 5. 验证完备性评估

### 5.1 安全性属性 (Safety)
- 是否覆盖了所有关键功能点的正确性检查？[是/否，如否说明遗漏]
- 正向断言（行为触发）和负向断言（Frame Condition）是否配对？[是/否]

### 5.2 活性属性 (Liveness)
- 是否验证了所有请求-响应通路？[是/否/不适用（纯组合逻辑）]
- 是否存在潜在死锁路径未被覆盖？[是/否]

### 5.3 Cover 属性
- 关键状态（Full/Empty/Error/各 FSM 状态）的可达性是否全部验证？[是/否]
- 是否有可达性证明失败（Cover FALSE）？[是/否，如有说明原因]

### 5.4 环境约束质量
- TRIVIALLY_TRUE 比例是否在可接受范围？[是/否]
- 所有 ACCEPTED 的 TT 是否有充分论证？[是/否]

---

## 6. 改进建议

> 列出后续可增强的验证方向

1. [例如：增加对 XXX 子模块的深度验证]
2. [例如：补充边界条件的 assert]
3. [例如：对 YYY 接口增加协议级 assume]

---

## 7. 结论

[一段话总结：验证达成情况、发现的核心问题、对设计质量的整体评价]
