第一章JasperGold 平台总览

平台架构

JasperGold Apps 是 Cadence 公司的形式验证平台，采用统一的 GUI 界面和数据库，通过一系列专用的 "App"（应用）覆盖不同的验证需求。所有 App 共享通用的 GUI 组件和底层引擎。

使用命令行启动 JasperGold：

jg -<app> <script.tcl> -proj <project_dir>

其中 -fpv、-cdc、-sec 等参数指定要启动的 App。使用 -proj 指定项目数据库目录。

所有 JasperGold App 共享以下 GUI 组件：

显示所有属性的证明进度，用颜色区分不同状态：绿色表示 proven、红色表示 failed、黄色表示 bounded/unknown。点击可展开查看每个属性的详细状态。

Property Table 支持按名称、状态、证明时间等排序，支持文本搜索和按状态过滤，便于在大量属性中快速定位。

App	全称	用途
FPV	Formal Property Verification	经典形式属性验证，用户编写 SVA/PSL 断言证明设计行为
XPROP	X-Propagation Verification	检测设计中未知态（X）传播导致的问题
CONN	Connectivity Verification	自动验证 IP/SoC 级信号连接正确性，支持 IP-XACT
ARCH	Architectural Modeling	高层抽象架构建模与验证
CSR	Control/Status Register Verification	自动验证寄存器行为（通过 CSV 配置表）
BPS	Behavioral Property Synthesis	从仿真波形自动生成属性候选
Superlint	—	结合 Lint 和形式验证的静态设计检查
LPV	Low Power Verification	验证 UPF/CPF 低功耗设计的电源域行为
SEC	Sequential Equivalence Checking	验证两个设计（如 RTL vs netlist）时序等价
SPV	Security Path Verification	验证安全路径（TrustZone、安全子系统等）
COV	Coverage App	形式验证覆盖率度量
UNR	Coverage Unreachability	分析仿真覆盖点的不可达性，排除伪漏盖
CDC	Clock Domain Crossing Verification	时钟域交叉结构/功能/亚稳态验证
FSV	Functional Safety Verification	ISO 26262 功能安全验证（故障注入/传播分析）

RTLD（RTL Development）：JasperGold 也支持在 RTL 开发阶段使用，设计师可以在编写 RTL 时增量验证模块行为。