第一章形式验证概念导论
什么是形式验证（Formal Verification）
形式验证是一种通过数学方法穷尽证明设计是否满足给定属性的验证技术。与传统的仿真验证（Simulation）不同，形式验证不需要编写测试用例（testbench），而是通过算法遍历设计的所有可能状态空间，从数学上证明属性成立，或找到违反属性的反例（counterexample）。
形式验证的核心优势在于穷尽性：仿真只能覆盖有限的输入组合，而形式验证可以覆盖所有可能的输入序列和状态组合。这使得形式验证特别适合发现那些边角情况下的深层 bug。
关键概念
模型检测（Model Checking）
模型检测是形式验证的核心技术。它将硬件设计建模为状态转换系统（有限状态机），然后使用 SAT（可满足性）或 BDD（二元决策图）等算法，自动检查系统是否满足用时序逻辑表达的属性。
属性（Property）
在 JasperGold 中，属性分为三类：
- 断言（assert）：描述设计必须满足的行为。如果断言失败，表示设计存在 bug。
- 假设（assume）：描述设计输入环境的约束。形式验证工具只考虑满足假设的输入。
- 覆盖（cover）：描述设计应该能够到达的状态或行为。用于衡量验证的完整性。
三者关系：assertion 检查设计输出是否正确，assumption 约束输入环境，cover 确认关键场景被覆盖。
证明结果
运行证明后，每个属性会得到以下状态之一：
| 状态 | 含义 |
|---|---|
proven | 证明成功：属性在所有可达状态下都成立（full proof） |
failed | 证明失败：找到了违反属性的反例（counterexample trace） |
bounded | 有界证明：在设定的时间边界（trace length）内成立，但未证明完整（partial proof） |
unknown | 未知：引擎超时或资源不足，无法确定 |
有界模型检测（BMC）
有界模型检测将证明问题展开为 k 个时间步长内的 SAT 问题。它寻找长度不超过 k 的反例。增大 k 可以增加信心但不能完全证明（除非 k 超过了 completeness bound）。
其他核心术语
- 待验证设计：正在被验证的硬件设计
- 影响锥：影响某个属性的设计逻辑集合，JasperGold 自动缩减 COI 以提高证明效率
- 证明引擎：执行证明的算法模块（如 BMC、PDR、KA、MBP 等）
- 引擎模式：一个或多个引擎的组合配置
- 抽象：移除不相关逻辑以简化证明
- 过约束：假设太强导致排除了合法行为，可能漏检 bug
- 归纳法：一种证明技术，先证基础情况（初始状态），再证归纳步骤
- 证明编排：JasperGold 自动选择和调度多个引擎的策略
形式验证 vs 仿真验证
| 特性 | 仿真验证 | 形式验证 |
|---|---|---|
| 覆盖方式 | 有限测试向量 | 穷尽所有状态 |
| 需要 Testbench | 是 | 否（用断言+约束） |
| 发现 Bug 类型 | 取决于测试质量 | 深度逻辑 bug、边界情况 |
| 运行时间 | 随覆盖率线性增长 | 受状态空间爆炸限制 |
| 适用场景 | 系统级、数据通路 | 控制逻辑、协议、仲裁、FIFO |
| 互补关系 | 形式验证和仿真验证互补使用，形式验证处理控制密集模块，仿真处理数据通路和系统集成 | |
来源文档
glossary.pdfjaspergold_apps_userguide.pdf