第二章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/cex/bounded_proven 属性，调试反例
迭代优化：添加约束、调整抽象、增加引擎时间

FPV App GUI 导览

启动 FPV App 后，GUI 主要分为以下区域：

Console 区域：Tcl 命令行，可交互式输入命令或查看输出日志
Property Table（属性表）：显示所有断言/假设/覆盖点及其证明状态
Source Browser（源码浏览器）：浏览 RTL 源码，标注断言位置
Proof Progress Bar（证明进度条）：顶部颜色条显示总体证明进度
Messages Pane（消息面板）：显示编译警告、证明信息等

官方 FPV App 流程图 — 用户指南给出的 FPV App 流程图，把整个流程收敛成五步：**Read design and properties**（`analyze`、`elaborate`）→ **Add basic tie-off constraints**（`stopat`、`assume`）→ **Define proof environment**（`clock`、`reset`）→ **Prove properties**（`prove`）→ **Interactive Debugging**（`visualize`）

和上面那份八步清单对照着看：官方五步把「配置证明参数」并入了 proof environment，把「迭代优化」并入了 Interactive Debugging。另外注意官方在 analyze/elaborate 之后、定义时钟复位之前，专门列了一步 Add basic tie-off constraints（stopat 与 assume）——先把不关心的部分绑定住，再谈证明环境。

证明状态指示器

JasperGold 默认把状态拆成两套：运行状态（run status）和有效性状态（validity status）。Task Tree 顶部的进度条按三种颜色归类有效性状态：

颜色	包含的状态
🔴 红色	`cex`、`unreachable`、`bounded_unreachable (user)`
🟢 绿色	`proven`、`covered`、`bounded_proven (user)`
🟡 黄色	`unknown`、`undetermined`、`bounded_proven (auto)`

注意状态的准确名称：断言被违反时的状态叫 cex（counterexample found），不是 "failed"；有界证明的状态叫 bounded_proven，分 (auto) 和 (user) 两种，其中 bounded_proven (user) 属于绿色而非黄色。covered 也归在绿色里。

各有效性状态的准确含义（Appendix B，Table B-2）：

状态	含义
`unknown`	初始有效性状态（在处理开始之前）
`undetermined`	证明深度（proof bound）小于目标深度（target bound）
`bounded_proven (auto)`	目标深度由工具自动提取；证明深度已达到或超过目标深度
`bounded_proven (user)`	目标深度由用户通过 `set_prove_target_bound` 指定并已达到
`proven` / `covered`	属性已证明 / 覆盖点已命中
`cex` / `unreachable`	找到反例 / 覆盖点不可达
`error`	属性编译超时，或证明过程发现 task 中的假设与设计、或假设彼此之间不一致

运行状态（Table B-1）是另一套独立的取值：unprocessed（尚未开始证明）、queued（排队等待处理）、processing（正在证明）、processed（证明已结束）。

容易混淆的一点：unknown 是"还没开始跑"的初始状态，而不是"跑了但超时"。"跑了但没收敛"对应的是 undetermined；"根本没跑"对应的是运行状态 unprocessed。

界面截图

FPV 验证方法论：多轮收敛流程

FPV 不是"跑一次 prove 就结束"的工具，而是一个多轮迭代收敛的过程。理解这个流程是掌握形式验证的关键。

三轮证明策略

1第一轮：快速浅证明

设置较小的 set_max_trace_length（如 10-20），使用默认引擎模式。这一轮的目标不是完整证明，而是快速发现浅层 bug。如果在深度 10 就能找到反例，没必要花时间跑深度证明。

经验：第一轮通常在几分钟内完成，能发现大部分明显的设计错误。

2第二轮：加深证明

增大 trace length（如 50-100），换一组不同的引擎（官方示例第二轮用的是 {K I N}），并设置每个属性的时间限制（如 30s）。官方示例对这一轮的注释就是"用不同的引擎验证剩余属性"。

3第三轮：逐个攻克 remaining 属性

第一轮和第二轮后仍未证明的属性，需要逐个分析：是属性本身有问题？约束不够？还是设计太复杂需要抽象？对难证明的属性单独调整引擎和时间限制。

还有一个很有用的手段是用已证明的断言去帮助证明更难的断言：一条断言一旦被证明，就可以把它当作假设来使用，工具提供 assume -from_assert 自动完成这个转换。这属于 assume-guarantee 技术——在次要 task 中证明一条属性，然后在主要 task 中假定它成立。

什么算"验证完成"？

FPV 的 signoff 标准不是"prove 跑完了"，而是以下条件同时满足：

关键安全断言 proven：所有必须成立的属性被完整证明（是 proven，而不是 bounded_proven）
cover 属性被击中：验证环境确实能到达设计的关键状态（证明约束没有过强）
覆盖率达标：代码覆盖率和功能覆盖率达到项目要求（参见 Coverage 章节）
每个 cex 都已定性：所有反例要么确认为设计 bug 并修复，要么确认为假反例（约束缺失）并补充约束

常见误区：看到所有绿色就认为验证完成。但如果约束过强，形式引擎可能在一个被限制得过小的状态空间内"证明"了属性——这是假 proven。一定要用 cover 属性确认约束空间足够大，合法的场景能被覆盖到。

FPV 的局限性

状态空间爆炸：设计规模越大（flop 数越多），引擎需要探索的状态空间指数增长，大设计可能需要抽象和分模块验证
黑盒边界影响：黑盒化的模块输出是自由变量，可能导致不真实的反例（假 fail）
约束正确性依赖：形式验证只证明"在约束条件下属性成立"，如果约束本身写错了，验证结果不可信
不是仿真的替代：形式验证和仿真各有优势——形式验证穷尽所有情况但受限于复杂度，仿真可以跑大规模设计但只覆盖有限场景

来源文档

jaspergold_apps_userguide.pdf