第四章BPS 行为属性综合

概述

行为属性综合App 从仿真波形（SHM/FSDB 或 VCD）自动学习设计行为，生成候选属性（property candidate），帮助用户快速发现设计中隐含的不变量和协议规则。

Exploring the Console

BPS Console 提供 POI（Point of Interest）浏览器和属性候选面板。

指定环境

# 启动 BPS App
# jg -bps script.tcl

# 若从其他 JasperGold App 切换进 BPS（而非用 jg -bps 启动），
# 需要显式初始化
check_bps -init

# 分析设计
analyze -verilog rtl/*.v
elaborate -top top

# 指定时钟和复位
clock clk
reset ~rstN

行为属性综合流程

1. 加载波形：导入仿真波形文件
2. POI Browser：选择感兴趣的信号/模块作为 POI
3. 扫描波形：BPS 分析波形中的模式
4. Property Candidates：生成候选属性列表
5. 审查和选择：用户筛选有意义的属性
6. 形式证明：用 JasperGold 证明选中的属性是否在所有情况下成立

扫描波形

扫描通过 check_bps -scan -trace 完成。注意 -fsdb 和 -vcd 接文件，而 -shm 接目录：

# 扫描 FSDB 波形，限定 POI 范围和时间窗口
check_bps -scan -trace -fsdb sim.fsdb -scope <id_tcl_list> \
          -start_time 0 -end_time 10000

# 扫描 SHM 目录
check_bps -scan -trace -shm waves.shm

# 不依赖仿真波形，直接从形式搜索中综合属性
check_bps -scan -no_sim -from_formal_search -depth 5

# 清除扫描历史
check_bps -scan -clear

生成 SHM 配置文件

可以导出一份 SHM dump 配置文件，直接交给 Xcelium 使用，让仿真按 BPS 需要的方式 dump 波形：

# 在 JasperGold 中导出配置文件
scope -export -format shm_dump_configuration

生成的配置文件通过 Xcelium 的 xrun -bps_cfg <configuration_file> 传入。默认从 top 开始、把所有对象当作 instance、dump 全部信号，并把 shm_dump.cfg 导出到当前目录。

附录

• Appendix A：Jasper Property Macros for BPS — BPS 使用的属性宏定义
• Appendix B：Handshake Protocols — 支持的握手协议模板
• Appendix C：User-Defined POIs from XML — 通过 XML 文件自定义 POI
• Appendix D：Jasper Property Templates — 属性模板规范
• Appendix E：BPS Progress Report — 进度报告功能

BPS 行为属性综合界面

BPS 使用方法论

BPS 适合什么场景

• 遗留设计无断言：老代码没人写 SVA，从仿真波形自动提取行为属性
• 理解陌生设计：通过波形学习模块的行为模式
• 文档化设计行为：将综合出的属性作为设计文档
• 发现覆盖率漏洞：BPS 发现仿真中未出现的行为模式

属性分类与处理

BPS 用两个独立的维度描述候选属性，不要混为一谈。

维度一：Classification（分类）——这是你自己给属性打的评级，工具不会自动填写。所有提取出来的属性初始状态都是 unclassified，需要人工 review 后用 check_bps <id> -set_class 归类：

维度二：Type（类型）——描述属性本身是什么，用 check_bps <id> -set_type 设置。合并后（collapsed）的取值共五个：assert、assume、exercised_cover、coverage_hole、assert_assume。（未合并的底层维度是 Observer type hole/exercised 与 Type assert/assume/cover。）其中 coverage_hole 表示波形中未被激励到的行为，提示你补充仿真激励；工具用启发式给出默认类型，例如 stuck_at 情形默认就是 coverage hole。