附录 DProof Accelerator 选型指南

先分清两类 PA

选型之前必须先理解官方对 PA 的分类，这是最容易搞错的一点：

• Verification Component（验证组件）：内部包含断言，用来证明设计的数据传输是否正确。 例如各个 scoreboard、jasper_datapath 系列、jasper_cache。
• Abstraction Component（抽象组件）：内部不含任何检查，作用是把设计里难啃的大结构 （FIFO、存储器、乘法器、除法器、cache way）替换成简化模型，让形式引擎能够收敛。 例如 jasper_model_* 系列。

选型决策树

先问"我要证明什么"，再问"设计里有什么结构挡住了证明"：

第一步：选验证组件（做检查的）
├── 要证明数据穿过设计不丢失/不重复/不乱序/不损坏
│   ├── 数据包或 data beat 穿过桥接/队列/FIFO → jasper_datapath
│   ├── 最多 8 个 initiator 到最多 8 个 target   → jasper_datapath_1port
│   ├── 同上，且 initiator 与 target 时钟不同     → jasper_datapath_1port_2clk
│   ├── 最多 8 个 initiator 到 8 个 target，异时钟 → jasper_scoreboard
│   ├── initiator/target 数量任意，异时钟         → jasper_scoreboard_2
│   │      （可配置成按序或乱序传输验证）
│   ├── 单个 initiator 到单个 target              → jasper_scoreboard_3
│   ├── 输入数据被约束、或被 DUV 当控制信号用     → jasper_scoreboard_free
│   │      （与 scoreboard_2 类似，但对被检查数据无限制）
│   └── 每个包优先级不同，需在同优先级内保序     → jasper_scoreboard_priority
└── 要证明 cache 对主存接口是透明的               → jasper_cache

第二步：选抽象组件（让证明收敛的）
├── 数据通路里的大 FIFO 拖垮了证明
│   ├── 普通情形                                  → jasper_model_fifo
│   ├── 需要保留包的优先级信息                    → jasper_model_fifo_priority
│   └── 需求由 DUV 中的 FIFO 逻辑驱动             → jasper_datapath_fifo
├── 用来缓存数据包的大存储器拖垮了证明
│   ├── 普通情形                                  → jasper_model_mem
│   ├── 需要保留包的优先级信息                    → jasper_model_mem_priority
│   └── 需求由 DUV 中的存储器逻辑驱动             → jasper_datapath_mem
├── COI 里的存储器让属性不可解
│   ├── 单端口                                    → jasper_model_ram
│   └── 多端口                                    → jasper_model_mpram
├── COI 里的乘法器/除法器让属性不可解
│   ├── 乘法器                                    → jasper_model_multiplier
│   └── 除法器                                    → jasper_model_divider
└── cache 的 tag/data RAM 成为瓶颈                → jasper_model_cache_way
       （与 jasper_cache 配合使用）

其他
├── 低功耗流程中驱动设计走完上电/掉电序列        → jasper_power_sequencer
└── 多时钟域下快慢时钟比值需要在区间内浮动        → jasper_model_frequency_jitter

使用方法

使用 Proof Accelerator 的一般步骤：

1. 在 Tcl 脚本中用 analyze -verilog -req 读入 PA（需求文件）
2. 用 connect 把 PA 的端口连接到 DUT 的对应信号
3. 验证组件内部带断言，连接好后即可 prove；抽象组件不产生断言，只负责替换结构让证明收敛

可参考 proof_accelerators/tutorial_scoreboard_priority/ 和 tutorial_scoreboard_2/ 两个官方教程， 详细解读见第七篇第 15 节。

各 PA 概览