1. Jasper Formal 验证环境搭建

Jasper 是 Cadence 旗下的形式化属性验证（Formal Property Verification, FPV）工具，其核心工作方式不是像仿真那样给激励、跑波形，而是把 RTL 设计转换成数学命题，由求解器穷尽搜索状态空间，证明某条断言在所有合法输入序列下恒成立，或给出反例波形。因此，环境搭建的目标不是"能打开工具"，而是让工具能正确读入设计、绑定时钟与复位、加载属性文件，并输出可判读的证明结果。本章围绕工具链安装、项目初始化、第一个属性验证任务三个环节展开，最终交付一个可复现的最小验证工程。

一、工具链与运行环境

Jasper 通常以 jaspergold（或 jg）命令行的形式调用，配套组件包括：RTL 前端解析器、属性语言前端（SVA / PSL）、形式化引擎（如 prove、superlint、undetermined 等策略）、以及波形与反例查看器。安装后需要确认三件事：

• 许可证可用：形式化求解对 license 依赖较强，启动时若报 license 相关错误，后续所有步骤都无法进行。
• 版本与 RTL 语言匹配：SystemVerilog 断言语法在不同版本支持程度不同，建议在项目初始化时固定工具版本，避免团队间结果不一致。
• 环境变量与路径：确保 jaspergold 在 PATH 中，且工作目录有写权限，因为工具会生成 jgproject 等中间目录。

一个常见的启动检查方式是直接运行工具并查看版本与 license 状态：

$ jaspergold -version
JasperGold Formal Verification Platform, version 2023.09
$ jaspergold -license_status
License: FPV_Formal  ...  OK

如果这一步失败，不要急着写属性，先解决环境问题。形式化验证的调试成本远高于仿真，环境错误会以"证明失败"或"引擎异常退出"的形式出现，容易误导判断。

二、项目初始化：目录结构与最小工程

Jasper 项目通常以一个工作目录为核心，内部包含 RTL 源文件、属性文件、脚本和输出目录。推荐的最小结构如下：

fpv_demo/
├── rtl/
│   └── counter.sv
├── prop/
│   └── counter_prop.sv
├── scripts/
│   └── run.tcl
└── work/          # 工具输出、日志、反例

其中 rtl/ 放待验证设计，prop/ 放属性文件，scripts/run.tcl 是 Jasper 的 Tcl 驱动脚本，work/ 用于隔离工具生成物。项目初始化的关键动作是：在 Tcl 脚本中声明设计顶层、读入 RTL、读入属性、设置时钟与复位、指定证明策略。下面给出一个可直接运行的最小示例。

设计文件 rtl/counter.sv 是一个带使能和复位的 4 位计数器：

module counter (
  input  logic       clk,
  input  logic       rst_n,
  input  logic       en,
  output logic [3:0] cnt
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n)      cnt <= 4'd0;
    else if (en)     cnt <= cnt + 4'd1;
  end
endmodule

属性文件 prop/counter_prop.sv 用 SVA 描述两条性质：复位后计数为 0；使能且未溢出时计数递增。注意这里用 disable iff 处理复位，避免复位期间误判：

module counter_prop (
  input logic       clk,
  input logic       rst_n,
  input logic       en,
  input logic [3:0] cnt
);
  // 复位释放后的第一个时钟沿，计数应为 0
  property p_rst_zero;
    @(posedge clk) disable iff (!rst_n) $rose(rst_n) |=> (cnt == 4'd0);
  endproperty
  a_rst_zero: assert property (p_rst_zero);

  // 使能且未溢出时，下一拍计数加一
  property p_inc;
    @(posedge clk) disable iff (!rst_n)
      (en && cnt != 4'hF) |=> (cnt == $past(cnt) + 4'd1);
  endproperty
  a_inc: assert property (p_inc);
endmodule

驱动脚本 scripts/run.tcl 负责把上述内容串起来：

# 读入 RTL 与属性
analyze -sv rtl/counter.sv
analyze -sv prop/counter_prop.sv
elaborate -top counter

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

# 证明所有断言
prove -all

运行方式为 jaspergold -batch -tcl scripts/run.tcl。工具会依次完成解析、精化、属性提取和证明，并在终端输出每条断言的结果。

三、第一个属性验证任务：从运行到判读

第一次运行后，最需要关注的不是"是否全绿"，而是每条断言的状态分类。Jasper 的典型结果包括：

• proven：在所有合法输入序列下断言恒成立，这是形式化验证的目标状态。
• cex（counterexample）：找到反例，说明设计或属性存在问题，需要查看波形定位。
• undetermined / inconclusive：求解未收敛，通常需要调整策略、增加约束或简化属性。
• unreachable：断言前提永远不成立，属性本身可能写错或约束过强。

在本例中，a_rst_zero 通常会被证明成立；而 a_inc 如果直接运行，很可能出现反例——因为 en 是自由输入，工具会尝试让 en 在复位后立即为 1，但 $past(cnt) 在复位释放后的第一拍可能没有定义，导致属性前提与设计行为不匹配。这正是形式化验证的典型教学点：属性必须与设计的复位语义、时序语义严格对齐。修正方式是在属性中显式约束复位释放后的稳定条件，或把 a_inc 的前提改为 rst_n && $past(rst_n)，确保 $past 有定义。

判读结果时，建议按以下顺序操作：先看 proven 的断言是否覆盖了核心功能；再看 cex 的波形，确认是设计缺陷还是属性过强；最后处理 undetermined，通常通过增加 assume 约束输入空间、或改用更强的证明策略来收敛。第一次任务的目标不是证明全部属性，而是建立"写属性—运行—看结果—修正"的闭环。

四、常见初始化问题与处理

第一次搭建环境时，以下问题出现频率最高，处理方式也相对固定：