第五章证明引擎原理与选择

Proof Orchestration（证明编排）

JasperGold 的 Proof Orchestration 自动管理多个证明引擎的调度和切换，是证明自动化的核心。

为什么需要 Proof Orchestration

不同属性有不同的特征，适合不同的引擎。手动选择引擎需要丰富经验。Proof Orchestration 自动：

在证明过程中动态调整引擎选择、时间限制等设置
同时遵守用户定义的最大 job 数/license 数和全局时间限制
自动编排引擎和每属性时间限制，让你只需关注手头的资源

Proof Orchestration 如何工作

Proof Orchestration 与普通证明相似，区别在于它能基于整个证明过程中的动态学习来优化对属性集的每一轮扫描：它会判断哪些引擎表现良好，以及确定属性平均需要多少时间。因此，在初次扫描证明掉简单属性之后，Proof Orchestration 会在后续扫描中动态调整引擎选择和时间限制，无需你介入。

这是工具在默认设置（prove_orchestration auto 和 engine_mode auto）下的行为。若你希望在使用 Proof Orchestration 的同时指定额外的偏好设置，可以用 set_prove_orchestration on——此时工具会总体上考虑你的设置，但不一定严格遵守。特别地，如果你同时用 set_engine_mode 给出了引擎列表，编排器只会从该列表中选择引擎，但仍然是动态选择的，并且取决于 max_jobs 设置，由于分时的关系它未必会一直用到全部引擎。

想更深入地了解 Proof Orchestration 的行为，可以使用 set_prove_verbosity 7。运行 prove 时，可参考消息 IPF031 来确认 Proof Orchestration 是启用还是禁用。

Proof Orchestration 启用与禁用的条件

启用：prove_orchestration 为 on；或 prove_orchestration 为 auto 且 engine_mode 为 auto（工具默认）
禁用：prove_orchestration 为 off；或 prove_orchestration 为 auto 但 engine_mode 不是 auto

如何控制 Proof Orchestration

# 开启/关闭 Proof Orchestration（全局设置）
set_prove_orchestration on

# 设置引擎模式。注意 set_engine_mode 对所有 task 全局生效，
# 需要按 task 区分时用下面的顺序写法
set_engine_mode {B D}
prove -task task1
set_engine_mode {H}
prove -task task2

# 设置时间限制
set_prove_per_property_time_limit 10s
set_prove_time_limit 2m

引擎概览

JasperGold 的证明引擎基于 SAT（可满足性）和 BDD（二元决策图）以及这些算法的各种变体。工具不公开每个引擎的内部算法名称，官方文档描述的是每个引擎擅长做什么，下表按此整理。

引擎	特性	适用场景
H	并发证明或证伪同一 task 中的多个安全属性；混合安全与活性属性时，先并发证明所有安全属性，再逐个证明活性属性	首轮验证，快速验证属性并识别需要施加在主输入上的接口约束
Hp	引擎 H 的变体，专注于找证明，但也能找反例。不能与引擎 H 组合使用	与 Ht 配合，两者协作同时找证明和反例
Ht	引擎 H 的变体，专注于找反例。不能与引擎 H 组合使用	与 Hp 配合，两者协作同时找证明和反例
B	与引擎 Ht 类似，某些情况下性能更好，但不并发处理属性。永远不会得到穷尽证明，只能给出反例或有界证明	快速识别反例、构建 analysis region
Bm	引擎 B 的多属性版本。与 B 一起选用可在一次证明中同时获得多属性和单属性两种变体	需要多属性并发的 B 类搜索
I	一次处理一个属性。迭代地从影响锥（COI）中加入逻辑，从而最小化证明所需的逻辑量	analysis region 变得过于复杂时的证明；与 C、C2、K、N 组合可加速
K	为寻找有界证明而优化。只搜索 trace，通常不会找到完全证明。一次处理一个属性，迭代地从 COI 加入逻辑	建立有界证明（bounded proof）
N	顺序证明属性。是完全证明方法，不像 B、J、K、L 那样局限于找 trace；对活性属性效果好。能找 trace 但并不擅长	证明有效的断言或不可达的 cover；补充引擎 H 首轮后仍未决的属性
M	顺序证明属性，同样是完全证明方法。最适合 COI 较小、且没有很多复杂（非 pin）约束的属性	证明有效断言或不可达 cover，对活性属性效果好
L	bug-hunting 引擎，目标是在状态空间中深度搜索，找到常规形式引擎难以到达的反例或 cover point。基于有界模型检测算法与状态选择启发式的组合。忽略活性属性	深状态搜索、难以命中的 cover point
Tri	采用与 IFV Trident 引擎类似的证明策略，默认同时使用 8 个进程处理一个属性。可能找到非最短 trace，证明过程中只提供 trace attempt 和 min_length 更新	专注于找证明时性能最好的引擎之一
D	一次证明或证伪一个属性。对证明使用即时压缩（on-the-fly compression），以提升深证明的容量	补充引擎 H 首轮后仍未决的属性
C / C2 / G / G2	一次处理一个属性，适合验证复杂时序属性。C 和 C2 迭代地从 COI 加入逻辑；G 和 G2 使用 COI 中的全部逻辑	数据通路 credit 或 token 管理单元一类的复杂时序属性
AB / AD / AG / AM	抽象引擎，遵循各自非抽象对应引擎（B、D、G、M）的算法，但从少量 flop/gate 开始分析，再逐步加入更多——可理解为自动化的 Design Tunneling	COI 很大但 proof witness 很小的问题

完整的引擎清单可用 help set_engine_mode 查看，v2020.03 支持的引擎为：B B4 Bm C C2 D G G2 H Hp Hps Ht Hts I J K L M N Oh AB AD AG AM Q3 R Tri U U2 TM QT（共 31 个）。指定单个引擎，或用花括号指定多个引擎。一般来说使用多个引擎能得到整体更快的结果。

多属性引擎 vs 单属性引擎

Proof Settings 对话框的 Engines 标签页把全部引擎分成三组，这个分组对理解引擎行为很有帮助：

分组	引擎
Multi property（多属性）	`Hp` `Ht` `H` `Bm` `J` `Q3` `U` `U2` `L` `R` `Oh`
Single property（单属性）	`B` `K` `AB` `B4` `D` `I` `AD` `M` `N` `AM` `G` `C` `AG` `G2` `C2` `Hps` `Hts` `Tri`
Post processing（后处理）	`QT` `TM`

这个分组解释了几个容易困惑的地方：Bm 归在多属性组，正是因为它是 B 的多属性版本；Hps 和 Hts 归在单属性组，因为它们分别是 Hp 和 Ht 的单属性版本；QT 和 TM 单独成组，因为它们只在已有 trace 的属性上做后处理（分别建立 quiet trace 和最小 trace）。

默认设置下，工具对每个多属性引擎只用一个实例（例如 H），而对单属性引擎使用两个实例（例如 B）。用 set_proofgrid_per_engine_max_jobs 可以增加单属性引擎的实例数。引擎 L、J、Q3 是支持多实例的特殊多属性引擎。

Proof Settings 对话框的 Engines 标签页——默认勾选的正是 Hp、Ht、B、N，与 Proof Orchestration 关闭时的默认引擎模式 `{Hp Ht N B}` 一致

Advanced Engine Settings（高级引擎设置）

除了选择引擎，还可以通过 Advanced Engine Settings 对话框（或对应的 Tcl 命令）微调单个引擎的行为：

对应的常用命令包括：set_engineD_optimization（standard | high，也适用于引擎 I）、set_engineC_optimization 与 set_engineG_optimization（static | dynamic | adaptive）、set_engineCG_max_mem（默认 4096MB）、set_engineJ_single_property、set_engineJ_migrate，以及 set_first_trace_attempt。

Engine Race

除单引擎证明外，JasperGold Apps 支持多个引擎并行证明属性。每个引擎触发一个独立进程，多个引擎同时处理同一条属性、彼此竞速。当其中一个引擎达到以下四种情况之一时，竞速结束、其余引擎全部停止：找到反例、找到witness、得到完整证明，或触及某个限制（例如你设定的时间上限）。当 Proof Orchestration 关闭时，工具默认并行运行引擎 Hp、Ht、N、B。

注意第四种情况：竞速结束并不等于拿到了结论——如果是触及时间上限而结束，该属性仍然是未定状态。

使用多个引擎（或每个引擎多个 job）在远程机器上运行时最为有效，可通过 ProofGrid 指定运行位置和并行度：

# 指定 proof engine job 在哪种 grid 上运行
# 可选值：local | shell | lsf | oge | nc | cluster
set_proofgrid_mode lsf

# 每个引擎的最大 job 数
set_proofgrid_per_engine_max_jobs 3

在 local 模式下使用很多引擎（或很多 job）可能会让机器过载，导致性能低下，或因内存耗尽而崩溃。

Engine Mode 选择指南

官方指南强调：大多数情况下优先使用 Proof Orchestration，它替你免去了微调引擎选择和其他证明设置的负担。只有在某些特定情况下，才需要禁用 Proof Orchestration 转而手动选择引擎。

场景	官方推荐
Proof Orchestration 被禁用时的默认模式	`{Hp Ht N B}`——用于快速找到反例并构建 analysis region，也是找到第一批功能 bug、识别缺失输入约束或使用 Design Tunneling 的最佳模式
专注于找证明	引擎 `N` 和 `Tri` 性能最好；`Hp`、`Hps`、`AM`、`C`、`I`、`R` 也针对证明做了调优
专注于找 trace	引擎 `B` 和 `Hts` 性能最好；`Ht`、`L`、`U` 也针对 trace 做了调优
analysis region 变得过于复杂	使用 `C`、`C2` 或 `I`——它们在 analysis region 内逐步加入逻辑，通常能用 analysis region 的一个子集完成证明
Design Tunneling 完成后的完整证明	先用默认引擎模式直到 analysis region 完整（或反例变得相当长），再切换到 `D`、`G` 或 `G2`

Single Pass Mode（单遍模式）

如果希望在整个证明过程中使用同一组引擎并持续预定的时长，Proof Orchestration 并不适用（它会在证明期间变换引擎和时间限制）。此时可以选定引擎并禁用 Proof Orchestration：把 prove_property_time_limit_factor 设为 0，每个单属性引擎对每个属性只分析一次。

# 用引擎 B 对一组属性做一次单遍分析，持续 12 小时
prove -property {P1 P2 P3} \
      -orchestration off \
      -engine_mode B \
      -per_property_time_limit_factor 0 \
      -per_property_time_limit 12h

Focus on a Set of Engines（锁定一组引擎）

当已知某组引擎对当前属性集效果很好时，这种先验知识可能比 Proof Orchestration 的动态学习算法给出更好的结果。手动选择引擎可以配合手动指定 per_property_time_limit。

# 已知引擎 AM 和 I 能在 15 分钟内证明这些属性
prove -task my_task \
      -orchestration off \
      -engine_mode {AM I} \
      -per_property_time_limit 15m

Bounded Proof Information

get_property_info -list min_length 返回指定属性在指定引擎模式下 trace 可能具有的最小长度。这个信息告诉你：不存在比它更短的 trace——这就是所谓的有界证明（bounded proof）。

get_property_info -list max_length 返回该属性最小 trace 长度的上界（如果已经建立了这样的界限）；如果没有，则返回 infinite。当 prove 或 visualize 进程在后台运行时，工具也接受这两条命令。

有界证明信息同样列在 Property Table 的 Bound 列中：

Proof Status	Engine	Bound	含义
unprocessed		1-	—
undetermined	B	7-	如果存在 trace，它的长度是 7 个周期或更长
cex	B	18	工具已找到最小长度的 trace，长度为 18 个周期
cex	J	24-32600	工具能证明最短 trace 至少 24 个周期，同时引擎 J 找到了一条 32,600 周期的 trace，成为最短 trace 的上界
proven	D	Infinite	不存在 trace
undetermined	H	13-	经过 13 个周期后状态仍未确定
cex	M	4-21	工具可能在这个区间内找到最短 trace；这两个数字代表最小长度 trace 的长度界限

注意区分：引擎 B 和 K 给出的是有界证明（B 永远不会得到穷尽证明；K 专为寻找有界证明而优化且通常不会找到完全证明）。要得到完全证明，需要使用完全证明方法的引擎，例如 N、M、D、I、Tri。对未决的活性属性，Bound 列显示的是括号中的 proof_effort 值（例如 (17)）；当工具找到循环 trace 时，该列报告 stem + loop 长度，例如 17 + 20。

处理 State-Space Explosion

官方指南指出，一些指标和条件可以帮助你识别证明何时遇到了状态空间爆炸。有了这些信息，你就可以换用另一种引擎模式，或者通过属性分解（把一个复杂属性拆成若干简单属性）来降低证明复杂度。有助于管理状态空间爆炸的特性包括 Design Tunneling、state-space tunneling，以及可直接在 JasperGold Apps 界面中使用的各种抽象。

引擎选择决策：不是记名字，是理解特性

新手最常问的问题是"我应该用哪个引擎？"答案不是记住某个引擎名字，而是理解每个引擎擅长什么，然后根据问题特征选择。

核心引擎特性对比

选引擎的关键，是先分清它找 trace（反例）还是找证明，再看它是单属性还是多属性。

代号	找证明还是找 trace	擅长	限制
B	找 trace（性能最好之一）	快速识别反例、构建 analysis region	永远不会得到穷尽证明，只能给出反例或有界证明；不并发处理属性
Bm	找 trace	引擎 B 的多属性版本，可与 B 同时选用	与 B 同样是有界的
K	找 trace	为寻找有界证明而优化；迭代地从 COI 加入逻辑，最小化搜索时用到的逻辑	只搜索 trace，通常不会找到完全证明；一次只处理一个属性
L	找 trace	bug-hunting 引擎，深度搜索状态空间，能到达常规有界模型检测难以到达的深状态	找到的 trace 不一定是最短的；忽略活性属性
I	找证明（也可找反例）	迭代地从 COI 加入逻辑，最小化证明所需逻辑；与 C、C2、K、N 交换信息加速	一次只处理一个属性
N	找证明（性能最好之一）	完全证明方法，对活性属性效果好；比 M 更能容忍复杂约束	能找 trace 但并不擅长；找到的 trace 不一定最短
Tri	找证明（性能最好之一）	类似 IFV Trident 策略，默认用 8 个进程处理一个属性	可能给出非最短 trace；只提供 trace attempt 和 min_length 更新
Hp	找证明	引擎 H 的变体，专注找证明，也能找反例	不能与引擎 H 组合使用
Ht	找 trace	引擎 H 的变体，专注找反例；与 Hp 协作可同时得到证明与反例	不能与引擎 H 组合使用

引擎选择策略

1先用默认设置（Proof Orchestration）

保持工具默认的 prove_orchestration auto 和 engine_mode auto，让 Proof Orchestration 在初次扫描证明掉简单属性后，基于动态学习自动调整引擎选择和时间限制。官方指南明确指出，大多数情况下这都是首选做法。

2对 remaining 属性换引擎

第一轮后剩下的属性，按目标换引擎：想找反例用 B、Hts（Ht、L、U 也针对 trace 调优过），想要证明用 N、Tri（Hp、Hps、AM、C、I、R 也针对证明调优过）。analysis region 太复杂时改用 C、C2 或 I。

3对特别难的属性手动调优

少量 remaining 属性可能需要：增大时间限制、添加辅助不变量、黑盒化部分逻辑、数据路径抽象。

状态空间爆炸的信号与对策

官方指南给出了一组可观察的症状，以及每种症状对应的处理动作：

症状	动作
证明耗尽内存	换一个引擎模式，或降低证明复杂度。例如识别并抽象 analysis region 中的队列/FIFO 或计数器
使用引擎 D、AD 或 I 时证明停止并出现 "Ran out of gates"	说明触及了内部限制、引擎无法继续。试用 `set_engineD_optimization high` 看能否得到更好结果。若并未使用 D/AD/I 却收到此消息，可换用其他引擎，或用 stopat、黑盒、假设、helper property 等降低属性复杂度
证明已经跑了超过 24 小时	完成的可能性很小。停止证明并换引擎模式，例如用 C 或 C2 代替 G 或 G2，用 I 代替 D 或 H
两次 attempt 之间的运行时间超过 1000 秒，且每次 attempt 还在增加	停止证明并换引擎模式，例如用 G 或 G2 代替 H 或 D
每个周期的 structure size 非常大（例如引擎 G 下达到 2,000,000，或引擎 D 下达到 100,000）	换引擎模式，或降低证明复杂度（识别并抽象队列/FIFO 或计数器）
使用引擎 G、G2、C 或 C2 时，消息显示某些信号的 structure size 偏高（超过 500）	若证明无法完成，换到包含 D 或 I 的引擎模式，或降低复杂度。可用 `get_design_info` 分析该信号及其 fanin 的复杂度——例如大的多路选择器就是很好的抽象目标
周期数很高，而两次 attempt 之间的运行时间看起来恒定	计数器可能在 analysis region 中，需要被抽象

注意：structure size 反映的是引擎在 trace 或 proof attempt 推进过程中建模复杂度的总体指标，是官方指南采用的复杂度度量。

复杂度控制手段

黑盒：不参与当前属性的模块黑盒化（analyze -bbox_m）
stopat：用 stopat 降低属性的复杂度
假设与 helper property：用 assumption 和 helper property 约束问题规模
属性分解：把一个复杂属性拆分成若干简单属性（property decomposition）
抽象：Design Tunneling、state-space tunneling 以及可直接在界面中使用的各种抽象
假设-保证（assume-guarantee）：验证施加在设计上的假设是否正确的过程。可以对照设计规格来检查假设的有效性，也可以把假设转换成断言再对其做形式化证明。它是 design tunneling 过程中使用的一种技术：一个属性先在次要 task 中被证明，然后在主要 task 中被假定为真

来源文档

jaspergold_engine_selection.pdf