2. Jasper平台与属性验证流程

Jasper 是 Cadence 面向形式化属性验证（Formal Property Verification, FPV）的核心工具平台。要真正用好它，不能只记住几条命令，而要先理解它的应用架构：设计如何被读入、属性如何被编译、证明引擎如何工作、结果如何反馈到调试。本节围绕 Jasper Apps 的架构、属性检查流程，以及从设计读取到属性证明的完整步骤与常用命令展开。

一、Jasper Apps 架构：从设计到证明的分层结构

Jasper 采用“前端读入 + 中间编译 + 后端求解”的分层架构。理解这一分层，有助于在出错时快速判断问题出在哪一层。

• 设计读入层（Elaboration）：负责读取 RTL（Verilog/SystemVerilog/VHDL）、库文件、约束文件（SDC）以及黑盒定义。这一层把设计展开成 Jasper 内部的层次化数据库，并解析模块实例、端口连接、参数覆盖。
• 属性编译层（Property Compilation）：把 SVA/PSL 属性、假设（assume）、断言（assert）、覆盖（cover）编译成内部形式，绑定到具体信号与时钟域。此层会检查属性语法、时钟/复位语义、以及属性引用的信号是否存在。
• 求解引擎层（Proof Engines）：Jasper 内部集成多种引擎，包括 BDD、SAT、ABC、以及针对大规模设计的结构化和抽象引擎。工具会根据属性类型和设计规模自动选择或由用户指定引擎组合。
• 结果与调试层（Debug & Analysis）：输出证明结果（proven / disproven / inconclusive / covered），并提供波形（Waveform）、反例（Counterexample）、属性依赖图（Property Dependency Graph）等调试手段。

这四层之间是单向数据流：设计读入 → 属性编译 → 求解 → 结果反馈。任何一层出错，都会在后续层表现为“证明失败”或“无法编译”，因此定位问题时必须逐层排查。

二、属性检查流程：从设计读取到属性证明

Jasper 的典型属性验证流程可以概括为六个阶段。每个阶段都有明确的输入、操作和判断依据。

阶段 1：环境准备与设计读入。首先设置工作目录和搜索路径，然后读入 RTL。常用命令如下：

# 设置搜索路径
set_search_path {./rtl ./lib}

# 分析并展开设计
analyze -sv09 top.sv
analyze -sv09 sub_module.sv
elaborate -top top

# 读入 SDC 约束
read_sdc ./constraints/top.sdc

# 定义黑盒（如模拟 IP）
set_blackbox -module analog_ip

读入完成后，用 get_design_info 检查模块层次、端口数量和未解析的实例。如果出现“unresolved module”警告，说明有模块未找到，需要补充搜索路径或黑盒定义。

阶段 2：时钟与复位定义。形式化验证必须明确时钟和复位语义，否则属性无法正确采样。例如：

clock -name clk -period 10 -waveform {0 5}
reset -name rst_n -active low -async

这里定义了一个周期 10ns、占空比 50% 的时钟，以及低电平有效的异步复位。时钟和复位定义错误是导致“属性无法证明”的常见原因之一。

阶段 3：属性与假设的编写和读入。属性通常写在独立的 SVA 文件中，通过 read_property 或直接在 RTL 中嵌入。假设（assume）用于约束输入空间，断言（assert）用于描述待证明的行为，覆盖（cover）用于检查场景可达性。例如：

// 假设：请求与授权不会同时有效
assume property (@(posedge clk) disable iff (!rst_n)
  !(req && grant));

// 断言：请求后两个周期内必须授权
assert property (@(posedge clk) disable iff (!rst_n)
  req |-> ##[1:2] grant);

// 覆盖：授权场景可达
cover property (@(posedge clk) disable iff (!rst_n)
  grant);

阶段 4：属性编译与绑定。读入属性后，Jasper 会将其编译并绑定到设计中的具体信号。此时应检查属性是否成功绑定、时钟域是否一致、是否有未驱动的信号。常用命令 get_property_list 可以列出所有已编译属性及其状态。

阶段 5：证明执行。使用 prove 命令启动证明。Jasper 会根据属性类型和设计规模自动选择引擎，也可以手动指定：

# 自动选择引擎
prove -all

# 指定引擎组合
set_engine -sat -bdd
prove -property {req_grant_assert}

# 设置证明时间上限
set_prove_time_limit 3600

证明结果分为四类：proven（在所有合法输入下成立）、disproven（存在反例）、inconclusive（超时或资源不足，无法判定）、covered（覆盖点可达）。

阶段 6：结果分析与调试。对于 disproven 的属性，Jasper 会生成反例波形，展示从初始状态到违反属性的具体输入序列。对于 inconclusive 的属性，需要分析是设计规模过大、假设过强还是引擎选择不当。常用命令：

# 查看属性状态
get_property_status -all

# 查看反例波形
visualize -property req_grant_assert -waveform

# 查看属性依赖关系
get_property_dependency -property req_grant_assert

三、关键命令速查与常见问题定位

总结来说，Jasper 属性验证的核心在于“分层理解、逐层排查”。设计读入层确保设计完整，属性编译层确保语义正确，求解引擎层确保证明能力，调试层确保结果可解释。掌握这四层架构和六阶段流程，就能在遇到证明失败时快速定位问题所在，而不是盲目调整命令或引擎参数。