第一章形式验证概念导论
什么是形式验证（Formal Verification）
形式验证是一种通过数学方法穷尽证明设计是否满足给定属性的验证技术。与传统的仿真验证（Simulation）不同，形式验证不需要编写测试用例（testbench），而是通过算法遍历设计的所有可能状态空间，从数学上证明属性成立，或找到违反属性的反例（counterexample）。
形式验证的核心优势在于穷尽性：仿真只能覆盖有限的输入组合，而形式验证可以覆盖所有可能的输入序列和状态组合。这使得形式验证特别适合发现那些边角情况下的深层 bug。
关键概念
模型检测（Model Checking）
官方术语表对模型检测的定义是：证明一个设计与某个行为模型（behavior model）在时序上、功能上等价的过程。
而形式验证本身在术语表中被定义为「一个系统化的数学推理过程，用于验证设计意图（design intent）」；设计意图来源于规格级需求，并在设计创建过程中被保持。形式验证是 JasperGold Apps 所使用的验证类型之一。
属性（Property）
在 JasperGold 中，属性分为三类：
- 断言（assert）：描述设计必须满足的行为。如果断言失败，表示设计存在 bug。
- 假设（assume）：描述设计输入环境的约束。形式验证工具只考虑满足假设的输入。
- 覆盖（cover）：描述设计应该能够到达的状态或行为。用于衡量验证的完整性。
三者关系：assertion 检查设计输出是否正确，assumption 约束输入环境，cover 确认关键场景被覆盖。
证明结果
运行证明后，每个属性会得到一个有效性状态（validity status）。官方把这些状态分成两大类：未定（Undetermined）属性的状态和已定（Determined）属性的状态。
未定属性的状态
| 状态值 | 含义 |
|---|---|
unknown | 初始有效性状态（处理之前） |
undetermined | 证明边界（proof bound）小于目标边界（target bound） |
bounded_proven_auto | 证明边界由工具按既定规则自动提取：带前提条件（precondition）的断言，目标边界 = 前提条件边界；不带前提条件的断言，目标边界 = 1。且证明边界大于或等于目标边界 |
error | 属性编译超时，或证明过程发现该 task 中的假设与设计之间、或假设彼此之间互相矛盾 |
易错点：
unknown 不是「超时/算不出来」，而是属性在被处理之前的初始状态。真正表示「跑了但没收敛」的是 undetermined（证明边界还没达到目标边界）。这两个状态含义完全不同，很容易记反。已定属性的状态
| 状态值 | 含义 |
|---|---|
proven / covered | 证明成功 / 已覆盖 |
cex / unreachable | 找到反例（counterexample found）/ 不可达。CEX 即由 prove 或 Visualize 过程找到的一个证明失败实例；找到 CEX 后，可打开 Visualize 窗口查看相关信号的波形，调试由此开始 |
bounded_proven_user | 证明边界由用户指定。当属性达到由 set_prove_target_bound 指定的目标边界时即被标记为 bounded proven (user)。例如目标边界为 10、当前边界也为 10 时，该断言就被标记为 Bounded Proven (User) |
bounded_unreachable_user | 与上一行同理，用于 cover：达到用户指定的目标边界时标记为 bounded unreachable (user) |
marked_proven | 用户在 SST 流程中手工标记该断言为 proven；此时 Engine 列会显示 User |
ar_cex / ar_covered | 工具生成了一条分析区域（analysis region）内的 trace，违反（ar_cex）或覆盖（ar_covered）了该属性。这条 trace 可能揭示设计中的真实 bug，也可能是与完整设计不一致的伪 trace。注意：属性的有效性仍然是 undetermined |
设定目标边界的命令有两个层级：
set_prove_target_bound 作用于所有属性；assert -set_target_bound（断言）和 cover -set_target_bound（覆盖）作用于指定属性，支持通配符。用
get_property_info 查询时，断言（assertion）的完整 validity_status 取值为：proven、marked_proven、cex、ar_cex、undetermined、bounded_proven_auto、bounded_proven_user、unknown、error；覆盖（cover）的取值为：unreachable、covered、ar_covered、undetermined、bounded_unreachable_user、unknown、error；假设（assumption）则为 temporary 和 approved。注意工具使用的失败状态名是 cex，并不存在名为 “failed” 的状态值。有界证明（Bounded Proof）
有界证明是 JasperGold Apps 中的一种部分证明（partial proof）技术，它只检查从复位状态起 N 个周期以内是否存在 bug，参见命令 set_max_trace_length。增大 N 可以检查更深的行为，但只要没有得到完整证明，就不能断言属性在所有可达状态下都成立。
注意区分两个容易混淆的命令：
set_max_trace_length 限定证明搜索的最大 trace 长度；而目标边界 set_prove_target_bound 决定属性达到多少周期后被判定为 bounded_proven_user（见上文状态表）。与之相对的是状态空间爆炸（state-space explosion）：形式验证工具在证明过程中不断递增时间迭代、为每个时间迭代复制一份设计的分析区域，却既证不出属性（收敛到证明）也找不到反例（CEX）。此时工具要么在设定时间后超时，要么在未设定超时的情况下一直运行到内存耗尽。
其他核心术语
- 待验证设计：代表待形式验证之设计的 RTL 代码，通常就简称为「设计」（the design）
- 影响锥：设计中信号的集合，这些信号的值可能影响属性所涉及信号的值，或影响创建 Visualize trace 时所关注的某个特定信号。COI 的大小可能影响属性的证明性能，但并非总是如此——由于形式验证问题自身的性质，有些属性 COI 很大却很容易证明，而另一些属性 COI 很小却出乎意料地难证
- 证明引擎：用于 Visualize 和运行属性证明的 JasperGold 工具模块。JasperGold Apps 内置多个证明引擎，任意组合使用以在不同类型的设计上得到证明（proof）、见证（witness）或反例（counterexample）。其中既有 SAT（可满足性）类和 BDD（二元决策图）类引擎，也有在这些方法上做变化的其他引擎。引擎以字母命名，如 B、D、H、Hp、Ht、I、J、K、L、M、N 等
- 引擎模式：在 JasperGold Apps 中所选定的、用于 Visualize 和运行属性证明的一个证明引擎或一组证明引擎。引擎模式可通过 GUI 或
set_engine_mode命令选择 - 抽象：把设计的一部分替换为「形式友好」（formal-friendly）版本的过程，以获得更快的形式证明、或得到原本无法完成的证明。抽象通常能大幅减小状态空间、从而降低证明复杂度，且不损害证明的正确性——所有抽象都是安全的。在证明涉及大计数器、存储器、队列等时序深度较大的部件时尤其有用。抽象施加于设计之上，不需要改动任何 RTL 设计代码
- 无关逻辑：设计中不驱动、也不影响证明目标或 Visualize 目标的那部分逻辑（这是与「抽象」不同的另一个术语，注意区分）
- 过约束：施加在设计上的约束减少了工作模式（即减少了可达状态空间），以致所得到的任何证明都不是完整证明（full proof）
- 归纳法：一种数学原理，它使 JasperGold Apps 能够分析有界 trace，再利用有界 trace 的信息推断出关于任意长 trace 的结论
- 证明编排：免去用户挑选引擎和微调证明的负担。该功能在证明过程中动态调整引擎选择、时间限制等，同时遵守用户设定的最大 jobs/licenses 数与全局时间限制
形式验证 vs 仿真验证
| 特性 | 仿真验证 | 形式验证 |
|---|---|---|
| 覆盖方式 | 有限测试向量 | 穷尽所有状态 |
| 需要 Testbench | 是 | 否（用断言+约束） |
| 发现 Bug 类型 | 取决于测试质量 | 深度逻辑 bug、边界情况 |
| 运行时间 | 随覆盖率线性增长 | 受状态空间爆炸限制 |
| 适用场景 | 系统级、数据通路 | 控制逻辑、协议、仲裁、FIFO |
| 互补关系 | 形式验证和仿真验证互补使用，形式验证处理控制密集模块，仿真处理数据通路和系统集成 | |
来源文档
glossary.pdfjaspergold_apps_userguide.pdf