附录 C示例工程索引
💡 详细验证流程请查看：第七篇：官方示例工程详解，对每个示例包含 Tcl 逐行解读、验证流程（Setup→约束→引擎→证明→结果）和 GUI 操作指引。
以下是 JasperGold 安装包中提供的示例工程索引，按 App 分类。
| App 目录 | Tcl 脚本 | 说明 |
|---|---|---|
| ARCH | ARCH_example.tcl | Quick introduction to the Architectural Modeling (ARCH) App using |
| BPS | BPS_vhdl_sva_example.tcl, BPS_verilog_sva_example.tcl | A quick introduction to the Behavioral Property Synthesis (BPS) App using |
| CDC | CDC_verilog_example.tcl | A quick introduction to the Clock Domain Crossing (CDC) App: |
| CONN | CONN_verilog_example.tcl, CONN_vhdl_example.tcl, CONN_reverse_vhdl_example.tcl ...（共 4 个） | Quick introduction to the Connectivity Verification (CONN) App + Blackbox Assist |
| COV | COV_vhdl_sva_example.tcl, COV_verilog_sva_example.tcl | Quick introduction to the Coverage (COV) App. |
| CSR | CSR_verilog_example.tcl | Quick introduction to the CSR Verification (CSR) App. |
| FPV | FPV_vhdl_psl_example.tcl, FPV_verilog_sva_example.tcl, FPV_vhdl_sva_example.tcl ...（共 4 个） | Quick introduction to the Formal Property Verification (FPV) App. |
| FSV | FSV_example.tcl, fsv_utils.tcl | Quick introduction to the Functional Safety Verification (FSV) App. |
| IPXACT | IPXACT_csr_example.tcl, IPXACT_consistency_connectivity_example.tcl | Quick introduction to leveraging IPXACT meta-data in JasperGold Apps. |
| LPV | LPV_verilog_example.tcl | Quick introduction to the Low Power Verification (LPV) App: |
| RTLD | RTLD_continue_vhdl_example.tcl, RTLD_start_verilog_example.tcl, RTLD_continue_verilog_example.tcl ...（共 4 个） | Example of how to start using JasperGold Apps for RTL Development |
| SEC | SEC_verilog_example.tcl, SEC_verilog_fixed.tcl | Quick introduction to the Sequential Equivalence Checking (SEC) App: |
| SPV | SPV_verilog_example.tcl, SPV_vhdl_example.tcl | Quick introduction to the Security Path Verification (SPV) App. |
| Superlint | Superlint_vhdl_example.tcl, Superlint_verilog_example.tcl | A quick introduction to the Superlint App using the |
| UNR | Contents: | |
| XPROP | XPROP_vhdl_example.tcl, XPROP_verilog_example.tcl | Quick introduction to the X-Propagation Verification (XPROP) App. |
| designs | ||
| proof_accelerators | About the Proof Accelerator kits... |
Designs 目录
example_jaspergold_apps/designs/ 包含共享的 RTL 设计文件：
| 目录 | 说明 |
|---|---|
reference_design/ | FPV 参考设计（Verilog/VHDL + SVA/PSL） |
cdc_design/ | CDC 示例设计（多时钟域、FIFO、同步器） |
fsv_design/ | FSV 功能安全示例设计 |
ipxact_design/ | IP-XACT 连接性验证示例 |
lpv_design/ | 低功耗验证示例设计 |
spv_design/ | 安全路径验证示例设计 |
uart_design/ | UART 设计示例 |
RTLD 流程
RTLD（RTL Development）示例展示了在 RTL 开发阶段增量使用 JasperGold：
- 先运行
RTLD_start_verilog_example.tcl创建初始数据库 - 再运行
RTLD_continue_verilog_example.tcl增量验证修改后的 RTL
来源文档
example_jaspergold_apps/