2. Jasper环境搭建

Jasper 是业界常用的形式验证工具，主要用于安全属性验证（Security Property Verification）与逻辑等价验证（LEC）。在开始写属性、跑证明之前，第一步是把工具环境、目录结构和基本命令跑通。本节以一个可复现的最小工程为主线，把“装好—建好—跑通—看懂结果”四件事串起来，让读者能独立完成第一个验证任务。

一、安装与授权配置

Jasper 通常以安装包形式分发，安装过程本身不复杂，真正容易卡住的是授权（License）配置。安装完成后，工具目录下会有 bin/、lib/、include/ 等子目录，其中 bin/jaspergold（或 jg）是主入口。授权一般通过环境变量指定：

export JASPER_HOME=/tools/cadence/jasper/2023.09
export PATH=$JASPER_HOME/bin:$PATH
export LM_LICENSE_FILE=27020@license-server
# 或使用 CDS_LIC_FILE
export CDS_LIC_FILE=27020@license-server

配置完成后，用 jaspergold -version 验证工具能否启动，用 jaspergold -help 查看可用选项。如果启动时报 “Cannot connect to license server”，优先检查网络连通性、端口号和 license 文件中的 feature 名称，而不是反复重装工具。建议把上述变量写入 ~/.bashrc 或项目专用的 env.sh，避免每次手动设置。

二、项目目录结构

Jasper 工程没有强制目录规范，但一个清晰的结构能显著降低后续维护成本。推荐按“设计、属性、脚本、结果”四类划分：

my_jasper_proj/
├── rtl/            # 待验证的 RTL 设计文件
│   └── counter.v
├── sva/            # SystemVerilog 断言/属性文件
│   └── counter_sva.sv
├── scripts/        # 运行脚本（.tcl）
│   └── run_counter.tcl
├── results/        # 输出结果、日志、报告
└── env.sh          # 环境变量

其中 rtl/ 放设计源码，sva/ 放属性，scripts/ 放 Tcl 脚本，results/ 用于存放工具生成的日志和证明结果。这种划分让“设计”与“验证意图”分离，便于复用和版本管理。

三、基本命令与 Tcl 脚本

Jasper 支持交互式命令行和 Tcl 脚本两种方式。交互式适合调试，脚本适合回归。核心命令包括：

• analyze：分析并读入 RTL 或属性文件；
• elaborate：精化设计，构建内部模型；
• clock / reset：定义时钟和复位；
• assert / assume / cover：加载属性、约束和覆盖点；
• prove：启动证明；
• report：查看结果。

下面是一个最小 Tcl 脚本示例，用于验证一个 4 位计数器：

# run_counter.tcl
analyze -sv rtl/counter.v
analyze -sv sva/counter_sva.sv
elaborate -top counter

clock clk
reset -expression {!rst_n}

prove -all
report -summary

运行方式为 jaspergold -tcl scripts/run_counter.tcl。脚本中 analyze 负责读入文件，elaborate 指定顶层模块，clock 和 reset 定义时序基准，prove -all 对所有已加载属性发起证明，report -summary 输出汇总结果。

四、第一个验证任务：计数器属性验证

假设设计是一个带同步复位的 4 位递增计数器，RTL 如下：

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

我们想验证两条属性：复位后计数为 0；正常工作时每个时钟周期加 1。对应的 SVA 可以写成：

module counter_sva (
  input logic clk,
  input logic rst_n,
  input logic [3:0] cnt
);
  // 复位后下一拍计数为 0
  property p_reset;
    @(posedge clk) !rst_n |=> cnt == 4'b0;
  endproperty
  a_reset: assert property (p_reset);

  // 非复位时每拍加 1
  property p_inc;
    @(posedge clk) rst_n |=> cnt == $past(cnt) + 1'b1;
  endproperty
  a_inc: assert property (p_inc);
endmodule

运行脚本后，Jasper 会输出每条属性的证明状态。常见状态有：proven（已证明）、cex（发现反例）、unknown（未收敛）、unreachable（不可达）。如果 a_inc 返回 cex，说明设计或属性存在问题，需要查看反例波形定位原因。

五、常见问题与排查

第一个验证任务跑通后，通常会遇到几类问题。第一类是 elaborate 报错，常见原因是顶层模块名写错或 RTL 中有语法错误，此时应先用 analyze 单独检查每个文件。第二类是属性返回 unknown，往往是因为时钟或复位定义不完整，或者属性本身过于复杂导致证明不收敛，可以尝试简化属性或增加 assume 约束。第三类是 cex，需要打开反例波形，逐拍检查信号变化，判断是设计缺陷还是属性写错。