第五章Proof Accelerators 证明加速器库

概述

证明加速器是 Cadence 预构建的形式验证模型，封装了常见硬件结构（Cache、FIFO、Scoreboard、Memory 等）的验证逻辑。使用 PA 可以：

大幅减少编写断言的工作量
利用 Cadence 优化的抽象模型加速证明
避免手写断言可能的错误

Cache 类

PA	用途
`jasper_cache`	通用缓存验证加速器
`jasper_model_cache_way`	Cache way 模型（多路组相联）

Datapath 类

PA	用途
`jasper_datapath`	通用数据通路验证
`jasper_datapath_1port`	单端口数据通路
`jasper_datapath_1port_2clk`	双时钟单端口数据通路（CDC）
`jasper_datapath_fifo`	带 FIFO 的数据通路
`jasper_datapath_mem`	带存储器的数据通路

FIFO/Buffer 模型

PA	用途
`jasper_model_fifo`	标准 FIFO 模型
`jasper_model_fifo_priority`	带优先级的 FIFO

Memory 模型

PA	用途
`jasper_model_mem`	通用存储器模型
`jasper_model_mem_priority`	带优先级访问的存储器
`jasper_model_mpram`	多端口 RAM 模型
`jasper_model_ram`	单端口 RAM 模型

算术模型

PA	用途
`jasper_model_divider`	除法器验证模型
`jasper_model_multiplier`	乘法器验证模型

Scoreboard 类

PA	用途
`jasper_scoreboard`	通用 Scoreboard 模型
`jasper_scoreboard_2`	双端口 Scoreboard
`jasper_scoreboard_3`	三端口/多通道 Scoreboard
`jasper_scoreboard_free`	自由运行 Scoreboard
`jasper_scoreboard_priority`	带优先级 Scoreboard

其他

PA	用途
`jasper_model_frequency_jitter`	频率抖动模型（扩频时钟验证）
`jasper_power_sequencer`	电源定序器模型

使用 PA 时，将 PA 模型的端口连接到 DUT 对应信号即可，PA 内部包含预定义的断言和抽象，自动验证 DUT 的行为是否符合预期模型。

Proof Accelerator 模型架构图

Proof Accelerator 模型架构图 — 第 7 页截图

Proof Accelerator 模型架构图 — 第 7 页截图

Proof Accelerator 模型架构图 — 第 14 页截图

Proof Accelerator 模型架构图 — 第 15 页截图

Proof Accelerator 使用方法论

什么是 PA、为什么需要它

Proof Accelerator（PA）是预构建的形式验证 IP，封装了常见验证场景的 SVA、约束和抽象逻辑：

Scoreboard PA：数据完整性（数据从输入到输出不丢失/不重复/不乱序）
Data Path PA：数据通路验证（简化宽数据路径的抽象）
各种协议 PA：AXI/AHB/APB/Wishbone 等总线协议的断言和约束
特殊功能 PA：FIFO、仲裁器、缓存等常见结构的验证

不用 PA，你需要自己写几百行 SVA 实现 scoreboard 逻辑；用 PA，几行 connect 命令搞定。

PA 选型思路

验证场景	推荐 PA
FIFO/队列数据按序传输	jasper_scoreboard_priority
数据流完整性（乱序允许）	jasper_scoreboard_2 / scoreboard_3
宽数据通路验证	jasper_datapath
AMBA 总线协议合规	对应协议 PA（AXI4/AHB-Lite/APB）

核心价值：PA 内部已经做了数据抽象（将宽数据路径简化为符号变量），大幅降低证明复杂度。同样的 scoreboard 手写 SVA 可能跑几个小时都不收敛，用 PA 几分钟就 proven。

来源文档

proof_accelerators/jasper_cache.pdf
proof_accelerators/jasper_datapath.pdf
proof_accelerators/jasper_model_fifo.pdf
proof_accelerators/jasper_model_mem.pdf
proof_accelerators/jasper_model_divider.pdf
proof_accelerators/jasper_model_multiplier.pdf
proof_accelerators/jasper_scoreboard.pdf
proof_accelerators/jasper_scoreboard_2.pdf
proof_accelerators/jasper_scoreboard_3.pdf
proof_accelerators/jasper_model_frequency_jitter.pdf
proof_accelerators/jasper_power_sequencer.pdf