第二章FPV App 流程与 GUI 导览
FPV App 完整流程
Formal Property Verification (FPV) App 是 JasperGold 最核心的应用，也是其他 App 的基础。FPV 的标准工作流程如下：
- 启动 FPV App：
jg -fpv - 分析设计：使用
analyze命令加载 Verilog/VHDL/SVA 文件 - 细化设计：使用
elaborate -top <module>构建设计层次 - 指定时钟和复位：
clock/reset命令 - 配置证明参数：trace length、引擎模式、时间限制等
- 运行证明：
prove -all或 GUI 中点击证明按钮 - 分析结果：查看 proven/failed/bounded 属性，调试反例
- 迭代优化：添加约束、调整抽象、增加引擎时间
FPV App GUI 导览
启动 FPV App 后，GUI 主要分为以下区域：
- Console 区域：Tcl 命令行，可交互式输入命令或查看输出日志
- Property Table（属性表）：显示所有断言/假设/覆盖点及其证明状态
- Source Browser（源码浏览器）：浏览 RTL 源码，标注断言位置
- Proof Progress Bar（证明进度条）：顶部颜色条显示总体证明进度
- Messages Pane（消息面板）：显示编译警告、证明信息等
证明状态指示器
Property Table 中每个属性旁边有状态图标：
| 图标/颜色 | 状态 | 说明 |
|---|---|---|
| 🟢 绿色 | proven | 属性被完整证明 |
| 🔴 红色 | failed | 找到反例，属性被违反 |
| 🟡 黄色 | bounded | 有界证明完成但未完整证明 |
| ⚪ 灰色 | unknown | 引擎超时，未能确定 |
| 🔵 蓝色 | covered | cover 属性被击中（到达了目标状态） |
界面截图
FPV 验证方法论：多轮收敛流程
FPV 不是"跑一次 prove 就结束"的工具，而是一个多轮迭代收敛的过程。理解这个流程是掌握形式验证的关键。
三轮证明策略
1第一轮：快速浅证明
设置较小的 set_max_trace_length（如 10-20），使用默认引擎模式。这一轮的目标不是完整证明，而是快速发现浅层 bug。如果在深度 10 就能找到反例，没必要花时间跑深度证明。
经验：第一轮通常在几分钟内完成，能发现大部分明显的设计错误。
2第二轮：加深证明
增大 trace length（如 50-100），切换到更强的引擎组合（如 {K I N}），设置每个属性的时间限制（如 30s-60s）。这一轮目标是深度证明或找到深层反例。
3第三轮：逐个攻克 remaining 属性
第一轮和第二轮后仍未证明的属性，需要逐个分析：是属性本身有问题？约束不够？还是设计太复杂需要抽象？对难证明的属性单独调整引擎、时间限制或添加辅助不变量。
什么算"验证完成"？
FPV 的 signoff 标准不是"prove 跑完了"，而是以下条件同时满足：
- 关键安全断言 proven：所有必须成立的属性被完整证明（不是 bounded）
- cover 属性被击中：验证环境确实能到达设计的关键状态（证明约束没有过强）
- 覆盖率达标：代码覆盖率和功能覆盖率达到项目要求（参见 Coverage 章节）
- failing 属性已 triaged：所有失败要么确认为设计 bug 并修复，要么确认为假反例（约束缺失）并补充约束
常见误区：看到所有绿色就认为验证完成。但如果约束过强，形式引擎可能在一个被限制得过小的状态空间内"证明"了属性——这是假 proven。一定要用 cover 属性确认约束空间足够大，合法的场景能被覆盖到。
FPV 的局限性
- 状态空间爆炸：设计规模越大（flop 数越多），引擎需要探索的状态空间指数增长，大设计可能需要抽象和分模块验证
- 黑盒边界影响：黑盒化的模块输出是自由变量，可能导致不真实的反例（假 fail）
- 约束正确性依赖：形式验证只证明"在约束条件下属性成立"，如果约束本身写错了，验证结果不可信
- 不是仿真的替代：形式验证和仿真各有优势——形式验证穷尽所有情况但受限于复杂度，仿真可以跑大规模设计但只覆盖有限场景
来源文档
jaspergold_apps_userguide.pdf