3. Jasper验证环境搭建

形式验证工程与仿真工程最大的差别之一，是它高度依赖“环境先行”。Jasper 本身只提供证明引擎，真正决定一次验证能否顺利跑通、能否被复现的，是围绕它搭建的目录、配置、脚本、时钟复位定义和验证 IP。本节围绕一个可落地的工程骨架展开，所有路径、文件名和参数均为教学示例，可按实际项目替换。

一、项目目录结构：让证明可复现

形式验证的输入包括 RTL、约束、断言、脚本和工具配置，输出包括证明结果、覆盖报告和反例波形。若这些内容散落各处，几周后连自己都无法复现一次证明。推荐按“源码与验证分离、输入与输出分离”的原则组织目录：

proj_fv/
├── rtl/                 # 待验证设计源码（只读引用）
│   ├── fifo_ctrl.v
│   └── fifo_top.v
├── fv/
│   ├── setup/           # 工具与编译配置
│   │   ├── jasper.tcl
│   │   └── compile.tcl
│   ├── clocks/          # 时钟与复位定义
│   │   └── clk_rst.tcl
│   ├── sva/             # 断言与假设
│   │   ├── fifo_props.sva
│   │   └── fifo_assume.sva
│   ├── vip/             # 验证 IP（接口模型、抽象模型）
│   │   └── axi_lite_vip/
│   ├── scripts/         # 运行与回归脚本
│   │   └── run_prove.tcl
│   └── work/            # 工具输出（证明库、日志、波形）
└── docs/                # 验证计划与结果记录

关键约定有三点：rtl/ 只读，验证人员不修改设计源码，避免“改设计迁就证明”；work/ 可整目录删除，任何一次干净复现都从空 work 开始；setup、clocks、sva、vip 分目录，使配置、时序定义、断言和模型各自独立演进，便于多人协作与版本管理。

二、Jasper 工具配置与编译脚本

Jasper 通过 Tcl 命令驱动。工程级配置通常写在 jasper.tcl 中，负责设定证明模式、求解器资源、日志与并行策略；编译脚本 compile.tcl 负责读入 RTL、定义顶层、指定时钟复位并完成 elaboration。二者分离的好处是：编译一次后可反复加载不同属性集，节省大量时间。

# jasper.tcl —— 工程级配置（示例）
set_prove_mode -bmc_depth 50
set_engine_mode {Hp Ht}
set_proofgrid_max_jobs 8
set_proofgrid_per_engine_max_local_jobs 4
set_logfile ./work/jasper.log
set_proof_effort high

# compile.tcl —— 编译与顶层定义（示例）
analyze -sv09 ./rtl/fifo_ctrl.v
analyze -sv09 ./rtl/fifo_top.v
elaborate -top fifo_top -bbox_mul 64
source ./fv/clocks/clk_rst.tcl
source ./fv/sva/fifo_assume.sva
clock clk
reset ~rst_n

这里 analyze 只做语法与语义分析，elaborate 才真正展开层次并绑定顶层。-bbox_mul 64 用于把乘法器抽象为黑盒，避免位宽较大时证明状态爆炸——这是工程中非常常见的取舍。若设计含大量存储器，可配合 -bbox_i 或抽象模型替代，而不是让工具直接展开。

三、时钟与复位定义

形式验证没有仿真时间轴，时钟与复位必须显式声明，否则工具无法建立时序语义。定义内容包括：时钟周期、边沿、复位有效电平、同步或异步、以及复位释放后的初始状态。示例：

# clk_rst.tcl —— 时钟与复位（示例）
clock -name clk -period 10 -waveform {0 5}
reset -name rst_n -active low -async
# 复位释放后，从第 1 个时钟上升沿开始检查属性
set_reset_sequence -reset rst_n -clock clk -cycles 2

需要特别注意：异步复位必须用 -async 声明，否则工具会按同步复位建模，导致复位期间的属性检查行为与真实电路不符；set_reset_sequence 指定复位保持的周期数，决定了属性从哪个时刻开始被检查。若设计有多个时钟域，应分别声明时钟，并用 set_clock_groups 或 set_clock_domain 说明跨域关系，避免工具对不存在的跨域路径做无意义证明。

四、验证 IP 集成方法

验证 IP（VIP）在形式验证中通常不是仿真用的总线功能模型，而是接口协议假设 + 抽象模型。集成方式有三种：

• 假设型 VIP：用 SVA 描述接口必须遵守的协议，如 AXI 的握手不能提前撤销。它约束输入空间，使证明聚焦于合法激励。
• 抽象模型型 VIP：用 bbox 或 model 替代复杂子模块，只保留行为契约，降低证明复杂度。
• 绑定型 VIP：通过 bind 把断言模块挂到设计内部信号上，无需修改 RTL 即可观察内部节点。

集成时建议把 VIP 放在独立目录，并在编译脚本中按“先模型、后设计、再绑定”的顺序加载。若 VIP 自带时钟复位假设，需确认其与工程 clk_rst.tcl 一致，否则会出现“假设冲突”导致证明无法收敛。

五、一次完整的环境搭建流程

把上述内容串起来，一次可复现的搭建流程如下：

1. 建立 proj_fv/ 目录树，把设计源码放入 rtl/，确认只读。
2. 编写 setup/jasper.tcl，设定证明模式、引擎、并行度和日志路径。
3. 编写 setup/compile.tcl，用 analyze 读入 RTL，用 elaborate -top 指定顶层，必要时对复杂模块做黑盒抽象。
4. 编写 clocks/clk_rst.tcl，声明时钟周期、边沿、复位有效电平与同步/异步属性，并设置复位序列。
5. 把协议假设写入 sva/，把接口模型或抽象模型放入 vip/，按“模型 → 设计 → 绑定”顺序加载。
6. 运行 scripts/run_prove.tcl，在 work/ 中查看日志、证明状态和反例波形。

判断环境是否搭建成功，不看“有没有报错”，而看三件事：elaborate 后层次与顶层正确、时钟复位被工具识别且无冲突假设、至少一条已知为真的属性能被证明为 Proven。若一条简单属性都返回 Undetermined，通常说明时钟复位定义或 VIP 假设存在问题，应先排查环境，而不是急着加深证明深度。