第一章JasperGold 平台总览
平台架构
JasperGold Apps 是 Cadence 公司的形式验证平台，采用统一的 GUI 界面和数据库，通过一系列专用的 "App"（应用）覆盖不同的验证需求。所有 App 共享通用的 GUI 组件和底层引擎。
启动 JasperGold
使用命令行启动 JasperGold：
jg -<app> <script.tcl> -proj <project_dir>其中 -fpv、-cdc、-sec 等参数指定要启动的 App。使用 -proj 指定项目数据库目录。
新建/加载数据库
- 新建数据库：首次启动时自动创建新的 JasperGold 数据库（database），包含设计的编译信息、证明结果等
- 加载已有数据库：启动时指定已有项目目录，或在 GUI 中打开已保存的 session
通用 GUI 组件
所有 JasperGold App 共享以下 GUI 组件：
证明进度条（Expandable Proof Progress Bar）
只要有至少一个证明线程在运行，界面底部就会显示可展开的证明进度条。将鼠标悬停在收起状态的进度条上可显示进度详情的浮动提示；点击状态条的某一段可激活弹出面板，展开后工具会显示每个正在运行的证明线程的信息。
进度条用颜色区分属性状态，对应关系如下：
| 颜色 | 包含的状态值 |
|---|---|
| 红色（Red） | cex、unreachable、bounded_unreachable（user） |
| 绿色（Green） | proven、covered、bounded_proven（user） |
| 黄色（Yellow） | unknown、undetermined、bounded_proven（auto） |
注意：有界证明结果并非一律是黄色——由用户设定边界得到的
bounded_proven 归入绿色，由工具自动设定边界得到的才归入黄色。搜索、排序和过滤
Property Table 支持按名称、状态、证明时间等排序，支持文本搜索和按状态过滤，便于在大量属性中快速定位。
JasperGold 各 App 简介
| App | 全称 | 用途 |
|---|---|---|
| FPV | Formal Property Verification | 经典形式属性验证，用户编写 SVA/PSL 断言证明设计行为 |
| XPROP | X-Propagation Verification | 检测设计中未知态（X）传播导致的问题 |
| CONN | Connectivity Verification | 自动验证 IP/SoC 级信号连接正确性，支持 IP-XACT |
| ARCH | Architectural Modeling | 高层抽象架构建模与验证 |
| CSR | Control and Status Register | 当设计的寄存器空间可经由标准接口或专有接口访问时，验证寄存器字段的数据完整性与复位值。CSR map 可来自 XML 或 CSV 格式的 workbook 文件，或 IEEE 1685 IP-XACT 文件 |
| BPS | Behavioral Property Synthesis | 从仿真信息（波形或 testbench）自动综合出断言、约束和覆盖，并可在仿真、形式或仿真加速环境中使用这些生成的属性 |
| Superlint | — | 提供 lint 检查、可测性设计（DFT）检查和形式检查，针对常见设计错误与覆盖率。这些检查不需要任何 trace 文件或 testbench，工具直接从 RTL 中提取关注点 |
| LPV | Low Power Verification | 验证 UPF/CPF 低功耗设计的电源域行为 |
| SEC | Sequential Equivalence Checking | 针对一个设计规格（spec）与一个实现（imp），检查两者是否实现同一组行为。典型应用是时钟门控优化与流水线重定时（pipeline retiming） |
| SPV | Security Path Verification | 验证安全路径（TrustZone、安全子系统等） |
| COV | Coverage App | 形式验证覆盖率度量 |
| UNR | Coverage Unreachability | 分析仿真覆盖点的不可达性，排除伪漏盖 |
| CDC | Clock Domain Crossing Verification | 提供形式与基于仿真的方案以实现全面的 CDC sign-off：自动从设计中推断时钟域交叉意图，全面分析结构（structural）、功能（functional）与重汇聚（reconvergence）三类问题 |
| FSV | Functional Safety Verification | ISO 26262 功能安全验证（故障注入/传播分析） |
RTLD（RTL Development）：JasperGold 也支持在 RTL 开发阶段使用，设计师可以在编写 RTL 时增量验证模块行为。
界面截图
来源文档
jaspergold_apps_userguide.pdf