3. Jasper形式验证签核环境搭建

Jasper 形式验证的签核环境不是“打开工具、读入 RTL、点 Run”这么简单。一个可复现、可回归、可交付的 Jasper 工程，本质上是一套把设计、约束、属性、证明策略和结果数据库绑定在一起的工程化配置。签核时评审人关心的不是某一次证明是否通过，而是：约束是否完整且可解释、属性是否覆盖了签核目标、证明策略是否可复现、结果数据库能否追溯到具体版本。本节围绕这四件事展开。

一、工程创建：目录结构与工程文件

Jasper 工程通常以 .tcl 脚本驱动，配合一个工程目录。推荐的结构是：rtl/ 放设计源文件，tb/ 放形式验证专用的绑定文件与假设，props/ 放 SVA 属性，scripts/ 放工程脚本，db/ 放结果数据库，logs/ 放运行日志。工程入口脚本一般命名为 run.tcl，其核心动作是清空环境、设置分析模式、读入设计、读入属性、施加约束、配置证明策略、启动证明并保存数据库。

# run.tcl —— Jasper 工程入口（示例）
clear -all
analyze -sv09 ./rtl/arb_core.sv
analyze -sv09 ./props/arb_props.sv
elaborate -top arb_core -create_related_covers

# 时钟与复位
clock clk
reset -expression {!rst_n}

# 属性与假设
assume -name a_req_stable {req_valid |-> ##1 req_valid || grant_valid}
assert -name p_no_double_grant {!(grant0 && grant1)}

# 证明策略
set_prove_time_limit 2h
set_engine_mode {Hp Ht N M B}
prove -all
save -db ./db/arb_core_$(date +%Y%m%d_%H%M).db

这里有两个容易踩坑的点。第一，analyze 与 elaborate 的顺序必须正确，属性文件若依赖设计中的信号名，必须在 elaborate 之后才能被正确解析。第二，-create_related_covers 会为每条 assert 自动生成对应的 cover，用于检查属性是否真的被激活过；如果某条 assert 从未被触发，它“通过”是没有意义的。

二、时钟与复位约束：形式验证的“时间基准”

形式验证没有仿真时间轴，所有时序行为都建立在时钟和复位定义之上。Jasper 中 clock 命令定义采样时钟，reset 命令定义复位表达式。对于多时钟设计，需要为每个时钟域分别声明，并明确跨时钟域属性的采样关系。复位通常用 -expression {!rst_n} 表示低有效异步复位，若复位是同步的，则需配合 -sync 选项或在属性中显式建模。

时钟复位约束写错，会导致两类典型问题：一是属性在复位释放前就被检查，产生大量假失败；二是复位被过度约束，导致某些合法状态永远无法到达，证明“通过”但实际不成立。签核环境中，建议把时钟复位约束单独放在 tb/clk_rst.tcl 中，并在评审时逐条确认其与设计规格的一致性。

三、属性加载与假设管理

属性加载的核心是区分 assert 与 assume。assert 是待证明的设计属性，assume 是对环境的约束。签核环境中，assume 必须来自可追溯的接口协议或规格，不能为了“让证明通过”而随意添加。Jasper 支持 assume -name 命名管理，建议每条 assume 都带名称和注释，便于在结果数据库中定位。

属性加载后，应先用 get_property_list 或 check_assumptions 检查假设之间是否矛盾。如果假设集合本身不可满足，整个证明会退化为“空证明”，所有 assert 都会通过，这是形式验证中最危险的假通过。签核流程中必须包含“假设一致性检查”这一步。

四、证明策略：引擎组合与时间预算

Jasper 提供多种证明引擎，常见的有 Hp（高性能）、Ht（层次化）、N（归纳）、M（多路）、B（有界）等。不同引擎适合不同属性：有界属性适合 B 引擎快速收敛，深层时序属性需要 N 引擎做归纳，复杂数据路径适合 Hp 引擎。签核环境通常采用 set_engine_mode {Hp Ht N M B} 组合模式，让工具自动调度。

时间预算方面，set_prove_time_limit 控制单条属性的证明时间。签核场景建议按属性复杂度分层设置：简单属性 10 分钟，复杂属性 2 小时，并配合 set_per_property_time_limit 做细粒度控制。证明结束后，必须区分三种结果：proven（已证明）、covered（已覆盖但未证明）、undetermined（未确定）。只有 proven 才能进入签核结论，undetermined 需要人工分析或调整策略后重跑。

五、结果数据库管理：签核的“证据链”

Jasper 的结果数据库（.db）保存了属性状态、反例波形、覆盖率信息和运行元数据。签核环境中，数据库管理要解决三个问题：可追溯、可对比、可归档。可追溯是指每个 .db 都能对应到具体的 RTL 版本、属性版本和约束版本；可对比是指回归时能自动比较两次运行的属性状态差异；可归档是指按签核里程碑保存数据库，而不是每次运行都覆盖。

推荐的做法是在 run.tcl 中用日期和版本号命名数据库，例如 save -db ./db/arb_core_v1.2_20250612.db。回归时用 compare -db old.db new.db 生成差异报告，重点关注从 proven 变为 undetermined 或 failed 的属性。签核评审时，数据库中的反例波形是定位问题的关键证据，必须确保波形文件与数据库一起归档。

六、一个可复用的签核检查清单

把上述五件事固化到脚本和检查清单中，Jasper 形式验证才从“个人调试”变成“团队签核”。工程创建决定了环境能否复现，时钟复位约束决定了时间基准是否正确，属性加载决定了证明目标是否清晰，证明策略决定了收敛效率，结果数据库决定了签核证据是否完整。五者缺一，签核结论都不可靠。