附录 DProof Accelerator 选型指南

选型决策树

根据你的设计中包含的硬件结构类型，选择对应的 Proof Accelerator：

设计中有什么硬件结构？
├── 缓存（Cache）
│   ├── 通用缓存验证 → jasper_cache
│   └── 多路组相联 → jasper_model_cache_way
├── FIFO / 缓冲
│   ├── 标准 FIFO → jasper_model_fifo
│   └── 带优先级 FIFO → jasper_model_fifo_priority
├── 存储器
│   ├── 单端口 RAM → jasper_model_ram
│   ├── 多端口 RAM → jasper_model_mpram
│   ├── 通用 Memory → jasper_model_mem
│   └── 带优先级访问 → jasper_model_mem_priority
├── 数据通路
│   ├── 通用 → jasper_datapath
│   ├── 单端口 → jasper_datapath_1port
│   ├── 双时钟（CDC）→ jasper_datapath_1port_2clk
│   ├── 带 FIFO → jasper_datapath_fifo
│   └── 带 Memory → jasper_datapath_mem
├── 算术单元
│   ├── 乘法器 → jasper_model_multiplier
│   └── 除法器 → jasper_model_divider
├── 计分板（Scoreboard）
│   ├── 通用 → jasper_scoreboard
│   ├── 双端口 → jasper_scoreboard_2
│   ├── 多通道 → jasper_scoreboard_3
│   ├── 自由运行 → jasper_scoreboard_free
│   └── 带优先级 → jasper_scoreboard_priority
├── 电源管理
│   └── 电源定序器 → jasper_power_sequencer
└── 其他
    └── 频率抖动/扩频时钟 → jasper_model_frequency_jitter

使用方法

使用 Proof Accelerator 的一般步骤：

1. 在 Tcl 脚本中导入 PA 模型
2. 将 PA 的端口连接到 DUT 的对应信号
3. PA 内部包含预定义的断言，自动验证 DUT 行为是否符合预期模型
4. PA 内部优化了抽象模型，证明速度比手写断言快

各 PA 概览