第五章Proof Accelerators 证明加速器库

概述

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

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

先分清 PA 的两种角色：较新的数据手册把 PA 明确分成两类——Verification Component（验证组件，内含断言，用于证明设计行为的正确性）和 Abstraction Component（抽象组件，不含断言，作用是把难以形式化处理的结构替换成更简单的模型，让引擎更容易收敛）。

下表"类型"列只在数据手册本身使用了这两个术语时才标注。较早的几份数据手册（jasper_datapath 系列）用的是另一套说法，把自己称为 "Proof Accelerator™ (also known as a PPM)"，并不使用 Verification/Abstraction Component 的分类；这类按其原文标注为 PPM，并注明它是用来"证明"还是用来"建模"。

Cache 类

PA	类型	用途
`jasper_cache`	Verification	证明数据在缓存间传输的完整性，可用于验证缓存对主存接口是透明的
`jasper_model_cache_way`	Abstraction	安全地抽象 cache way。与 jasper_cache 配合使用，抽象掉设计中的缓存存储；在很多情况下这是让透明性属性收敛的关键

Datapath 类

PA	类型	用途
`jasper_datapath`	PPM（证明用）	证明经过 DUV 传输的数据包或 data beat 的完整性。适用于桥、队列、FIFO 一类的设计，这些设计中必须确保传输过程不丢数据、不损坏、不重复
`jasper_datapath_1port`	PPM（证明用）	证明数据从最多八个 initiator（master）传输到最多八个 target（slave）经过 DUV 时的完整性
`jasper_datapath_1port_2clk`	PPM（证明用）	同上，但用于 initiator 与 target 时钟不同的场景
`jasper_datapath_fifo`	PPM（建模用）	当所证明的需求由 DUV 中的 FIFO 逻辑驱动时，用来对 FIFO 建模。例如用 jasper_datapath 证明桥中的数据完整性，同时用一个 jasper_datapath_fifo 实例对桥内部的队列建模，使验证精力集中在 bug 概率更高的控制逻辑上
`jasper_datapath_mem`	PPM（建模用）	同上，但用来对存储器建模——当所证明的需求由 DUV 中的存储器逻辑驱动时使用

FIFO/Buffer 模型

PA	类型	用途
`jasper_model_fifo`	Abstraction	数据完整性需求的 COI 中的 FIFO 会成为性能瓶颈，该建模 PA 安全地抽象这类 FIFO，只保留 scoreboard 工作所必需的确切行为，让验证环境不易发生状态空间爆炸。仅与 jasper_scoreboard_2 配合使用
`jasper_model_fifo_priority`	Abstraction	在保持被观察数据包的 FIFO 行为之外，还能保留这些数据包的优先级信息。与 `jasper_scoreboard_priority` 配套使用

Memory 模型

PA	类型	用途
`jasper_model_mem`	Abstraction	替换用于缓冲数据包的大存储器。数据完整性需求 COI 中的存储器会成为性能瓶颈，该 PA 安全地抽象它们，只保留 scoreboard 工作所必需的确切行为。设计用于与 `jasper_scoreboard` 或 `jasper_scoreboard_2` 配合
`jasper_model_mem_priority`	Abstraction	替换用于缓冲数据包的大存储器，在保持 load/store 行为之外还保留数据包的优先级信息
`jasper_model_mpram`	Abstraction	多端口 RAM（Multiport RAM）抽象。多个端口同时访问时，写端口先于读端口、编号小的端口先于编号大的端口被服务
`jasper_model_ram`	Abstraction	抽象存储器、替换为更简单的存储模型，提供灵活的抽象让引擎能抽象掉所指定存储器的大部分。支持多个读/写端口

存储器是形式化工具公认的难点结构。通过抽象存储器，形式引擎更有可能提高有界证明的 bound，或为那些 COI 中含有存储器的属性找到完全证明——若保留原始存储器模块，这些属性对形式化方法而言往往是不可解的。

算术模型

PA	类型	用途
`jasper_model_divider`	Abstraction	对含除法器逻辑的属性取得完全的、无界的证明。它提供灵活的抽象，让引擎抽象掉除法器的大部分，同时保留证明所需的那部分行为
`jasper_model_multiplier`	Abstraction	对含乘法器逻辑的属性所做的同类抽象

Scoreboard 类

Cadence Formal Scoreboard 是一组用于验证跨数据通路的端到端数据完整性的 Verification Component PA。这类验证问题的难点在于，属性本身就需要一块很大的存储才能表达设计意图——例如要验证数据包穿过数据通路时永不损坏，就需要一个 FIFO 来跟踪进入的数据，再与另一端观察到的输出数据做比较。Formal Scoreboard PA 正是为克服这类问题而设计的。

PA	类型	用途
`jasper_scoreboard`	Verification	证明数据从最多八个 initiator（master）传输到最多八个 target（slave）的完整性，且 initiator 与 target 时钟不同
`jasper_scoreboard_2`	Verification	证明数据从任意数量的 initiator 传输到任意数量的 target 的完整性。可配置为验证按序传输，也可配置为验证乱序传输
`jasper_scoreboard_3`	Verification	Formal Scoreboard 的较新版本（其数据手册专门给出了与 scoreboard_2 的特性对比、参数差异表以及"Migrating from jasper_scoreboard_2"迁移附录）
`jasper_scoreboard_free`	Verification	与 scoreboard_2 非常相似，区别是它对被检查的数据没有任何限制。因此适用于输入数据受约束、或被 DUV 用作控制信号的场合——也就是无法使用 scoreboard_2 的那些情况
`jasper_scoreboard_priority`	Verification	用于每个数据包优先级可以不同的场景，确保在给定优先级内保持顺序。适用于桥、队列、FIFO 等设计

Formal Scoreboard 可捕获四类错误：丢失（两个打了 tag 的数据包/beat 进入 DUV 但只有一个出来）、重复（一个进入但两个出来）、乱序（进入顺序与退出顺序不一致）和损坏（进入的数据包退出时值不同）。

其他

PA	类型	用途
`jasper_model_frequency_jitter`	建模用 PA	在含多时钟域的 DUV 中证明断言时，对频率抖动的影响建模。使用它可以让快慢时钟之间的比值在一个定义好的范围内变化，而不是始终锁定在同一个值
`jasper_power_sequencer`	—	用于低功耗验证流程的加密模块。它实现一个简单的状态机，带领一个 power-aware 设计走完典型的下电与上电序列；序列由一系列状态转换组成，每个状态控制一个具体的电源组件，例如门控时钟、隔离和保持

两类 PA 的用法完全不同：

用于"证明"的 PA——数据手册自称 Verification Component 的 jasper_cache 与各 scoreboard，以及自称 PPM、用途写明是 "to prove the integrity of data" 的 jasper_datapath、jasper_datapath_1port、jasper_datapath_1port_2clk——内含预定义的断言，把它的端口连接到 DUT 对应信号，即可验证 DUT 行为。
Abstraction Component（jasper_model_ram / _mem / _mem_priority / _fifo / _fifo_priority / _mpram / _divider / _multiplier / _cache_way 等）不包含任何断言，它们的作用是替换掉难处理的结构。这类 PA 都随附一条配套的 Tcl 命令，通过该命令的 -connect <port_name> <signal_name> 参数把 PA 边界上的端口连到指定信号，并管理抽象的连接方式、深度等细节——而不是直接实例化连线。

实例：jasper_scoreboard_3 的参数与接口

PA 通过参数配置、通过端口连接。以 jasper_scoreboard_3 为例，每次实例化都必须配置以下强制参数：

参数	默认值	合法取值	说明
`CHUNK_WIDTH`	1	>= 1	DUV 能处理的最小数据块（chunk）
`IN_CHUNKS`	1	>= 1	DUV 输入侧的 chunk 数量
`OUT_CHUNKS`	1	>= 1	DUV 输出侧的 chunk 数量
`SINGLE_CLOCK`	1	0, 1	单时钟还是双时钟。输入输出数据由同一时钟驱动设为 1，处于不同时钟域设为 0
`ORDERING`	`JS3_IN_ORDER	`JS3_IN_ORDER、`JS3_OUT_OF_ORDER	选择按序还是乱序验证
`MAX_PENDING`	4	>= 1	DUV 能存储的最大未完成 chunk 数

要使用 `JS3_* 这些宏，必须在分析使用它们的验证模块之前先运行命令 jasper_scoreboard_3 -init。

主要端口：

端口	位宽	方向	说明
`rstN`	1	input	低有效异步复位。PA 必须先被此信号复位才能开始验证，所有断言和 cover 仅在该信号解除时有效
`clk`	1	input	`SINGLE_CLOCK=1` 时的时钟
`incoming_clk` / `outgoing_clk`	1	input	`SINGLE_CLOCK=0` 时的输入侧/输出侧时钟
`incoming_vld`	`IN_CHUNKS`	input	输入数据有效指示
`incoming_data`	`IN_CHUNKS*CHUNK_WIDTH`	input	输入数据
`outgoing_vld`	`OUT_CHUNKS`	input	输出数据有效指示
`outgoing_data`	`OUT_CHUNKS*CHUNK_WIDTH`	input	输出数据
`halt_latency`	1	input	`LATENCY_HALT_MODE` 不为 0 时，用于暂停延迟计数器
`incoming_selected` / `outgoing_selected`	`IN_CHUNKS` / `OUT_CHUNKS`	output	数据选择信号

Latency Check：LATENCY_HALT_MODE 的两种行为

可选参数 LATENCY 指定 DUV 输入与输出之间允许的最大延迟，LATENCY_HALT_MODE 则配置 halt_latency 端口如何暂停延迟计数器（0 = 禁用）：

LATENCY_HALT_MODE=1 的时序 — `LATENCY_HALT_MODE = 1`：`halt_latency` 为高时停住延迟周期计数器（图中计数器停在 1 不再递增）

LATENCY_HALT_MODE=2 的时序 — `LATENCY_HALT_MODE = 2`：`halt_latency` 为高时复位延迟周期计数器（图中计数器归 0 后重新计数）

Proof Accelerator 使用方法论

什么是 PA、为什么需要它

Proof Accelerator（PA）是 Cadence 提供的加密宏，v2020.03 随附的 22 个 PA 分为两大用途：

用于证明的：内含断言，直接用于证明设计行为。包括 Formal Scoreboard 类（端到端数据完整性——数据不丢失/不重复/不乱序/不损坏）、jasper_datapath 类（数据包与 data beat 的传输完整性）和 jasper_cache（缓存对主存接口的透明性）。其中 scoreboard 类与 jasper_cache 的数据手册自称 Verification Component，jasper_datapath 类的数据手册自称 PPM。
用于抽象/建模的：不含断言，用于把 FIFO、存储器、多端口 RAM、cache way、乘法器、除法器等形式化难点结构替换为更简单的模型，从而让引擎收敛。jasper_model_* 中的九个数据手册自称 Abstraction Component；jasper_datapath_fifo 和 jasper_datapath_mem 则以 PPM 的说法描述为"对 FIFO/存储器建模"。

此外还有 jasper_power_sequencer（低功耗验证流程中的上下电序列状态机，数据手册称其为 encrypted module）和 jasper_model_frequency_jitter（多时钟域下的频率抖动建模，数据手册未使用上述任一分类术语）。

注意：这 22 个 PA 中不包含任何总线协议 VIP——没有 AXI、AHB、APB 一类的协议合规 PA。它们全部属于 cache、datapath、model（抽象）、scoreboard 和 power sequencer 五类。

PA 选型思路

验证场景	推荐 PA
数据从最多八个 initiator 到最多八个 target，且两侧时钟不同	`jasper_scoreboard`
任意数量 initiator/target；按序或乱序均可配置	`jasper_scoreboard_2`（新项目可考虑其较新版本 `jasper_scoreboard_3`）
输入数据受约束、或被 DUV 用作控制信号（无法使用 scoreboard_2 时）	`jasper_scoreboard_free`
每个数据包优先级不同，需在给定优先级内保序	`jasper_scoreboard_priority`（配合 `jasper_model_fifo_priority`）
桥/队列/FIFO 中数据包与 beat 的传输完整性	`jasper_datapath`（配合 `jasper_datapath_fifo` 或 `jasper_datapath_mem` 对内部队列/存储建模）
缓存对主存接口是否透明	`jasper_cache`（配合 `jasper_model_cache_way` 抽象缓存存储）
属性 COI 中含乘法器/除法器导致不收敛	`jasper_model_multiplier` / `jasper_model_divider`

核心价值：这类验证问题的难点在于属性本身就需要一块很大的存储才能表达设计意图（例如要验证数据包穿过数据通路时永不损坏，就需要一个 FIFO 跟踪进入的数据再与输出比较）。Formal Scoreboard PA 正是为克服这类问题而设计的，让形式验证在原本很难下手的场景中变得可行。配合 Abstraction Component PA 抽象掉 COI 中的 FIFO 和存储器，验证环境也不易发生状态空间爆炸。

来源文档

proof_accelerators/jasper_cache.pdf
proof_accelerators/jasper_model_cache_way.pdf
proof_accelerators/jasper_datapath.pdf
proof_accelerators/jasper_datapath_1port.pdf
proof_accelerators/jasper_datapath_1port_2clk.pdf
proof_accelerators/jasper_datapath_fifo.pdf
proof_accelerators/jasper_datapath_mem.pdf
proof_accelerators/jasper_model_fifo.pdf
proof_accelerators/jasper_model_fifo_priority.pdf
proof_accelerators/jasper_model_mem.pdf
proof_accelerators/jasper_model_mem_priority.pdf
proof_accelerators/jasper_model_mpram.pdf
proof_accelerators/jasper_model_ram.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_scoreboard_free.pdf
proof_accelerators/jasper_scoreboard_priority.pdf
proof_accelerators/jasper_model_frequency_jitter.pdf
proof_accelerators/jasper_power_sequencer.pdf