第四章CSR 寄存器验证

概述

寄存器验证App 读入寄存器映射（register map），自动生成断言，验证寄存器的读写行为、复位值、访问权限等，无需手动编写大量 SVA。寄存器映射来自 workbook 文件，支持 XML 或 CSV 格式，也支持 IEEE 1685 IP-XACT。每个 workbook 对应一个 instance，工具按字段的访问类型为每个字段生成属性。

CSR App 工作流程

准备 workbook（CSV/XML）或 IP-XACT 文件描述寄存器映射
加载设计，并用 check_csr -load（CSV）或 check_csr -load_ipxact（IP-XACT）挂接寄存器定义
CSR App 自动生成断言和假设
运行证明验证寄存器行为

寄存器行为建模

只读寄存器的三种情形

三种只读行为都以访问类型 RO 为基础，再按需要附加属性行（CSV 用 ATTR 行，IP-XACT 用 cadence: 厂商扩展）来区分。

情形	建模方式	说明
字段值恒定	仅标为 `RO` 即可	如器件/版本 ID、cache 大小等固定能力位
由设计更新的状态位	CSV 加 `ATTR, DIRECT_WRITE, <write_enable_signal>, <data>, <latency>, <modified write value>`	典型的 status 字段：复位到某值，之后由设计更新。IP-XACT 对应 `<cadence:hwAccessWriteEnable>`、`<cadence:hwAccessWriteData>` 等扩展
忽略数据检查	CSV 加 `ATTR, BUS_READ_CHECK, read_undefined`	读回值难以预测或不关心时，工具关闭读检查，改为生成一个 cover 观察是否读到与复位值不同的值。IP-XACT 侧可用 `<spirit:volatile>true</spirit:volatile>`

只写寄存器

WO：写入无法从总线接口观察到，CSR App 因此建立一份寄存器值的影子模型（shadow），在看到总线写时更新，再与设计内部信号比较。CSV 中用 ATTR, DIRECT_READ, <compare_enable>, <field_data>, <latency> 指定比较对象；把 compare_enable 设为 1'b1 即可每拍连续比较。

同时读写

处理寄存器在同一时钟周期被读和写的情况。

锁定行为

Register Writes are Locked：写操作被锁定（如锁定后写入无效）
Register Read Data is Locked or Ignored：读数据被锁定或忽略

其他行为

Register Aliasing：多个地址映射到同一寄存器
Preventing Reads/Writes：阻止特定寄存器的读写验证
Value Range：寄存器忽略指定范围之外的写值——写值超范围时不更新影子值
Reset Value Expression：复位值表达式

扩展文件

当基础的 IP-XACT 或 CSV 寄存器描述无法表达某些特殊行为时，可以把额外建模放进扩展文件（Extension File）。扩展文件本身是 CSV 格式，先基于原文件生成模板，再在加载时一并读入：

# 基于 IP-XACT 生成扩展文件模板
check_csr -generate_extension <output_ext_csv_file> -ipxact <base_IP-XACT_file>

# 基于 CSV 生成扩展文件模板
check_csr -generate_extension <output_ext_csv_file> -csv <base_csv_file>

# 加载基础描述 + 扩展文件
check_csr -load_ipxact <IP-XACT_file> -load_extension <extension_csv_file>
check_csr -load <csv_file> -load_extension <extension_csv_file>

Supporting Details

主题	内容
Instance Interface	CSR App 与 RTL 的接口信号约定
Worksheet Format	CSV 文件格式定义（列名、数据类型）
Access Types	支持的访问类型共 8 种，见下表
Bus Write/Read Enable	支持总线级写/读使能信号
Direct Write/Read	直接读写接口支持
Latencies	读写延迟支持
Modified Write Value	写值被硬件修改的情况
Masks	写屏蔽/读屏蔽支持
Register Maps	Secure/Non-Secure 映射、Remap States
Address Blocks	地址块和保留地址
Windowed CSRs	窗口化寄存器（间接寻址）

支持的访问类型

必须为每个寄存器指定访问类型，它会成为该寄存器所有字段的默认值；若某个字段单独指定了访问类型，则覆盖该默认值。CSR Verification App 目前支持的访问类型正好是以下 8 种：

访问类型	含义	说明
`RW`	READ-WRITE	可通过接口写入和读出
`RO`	READ-ONLY	只读，接口无法写入
`RC`	READ-CLEAR	读操作把寄存器每一位置 0
`RS`	READ-SET	读操作把寄存器每一位置 1
`RR`	READ-RESET	读操作把寄存器置回复位值
`WO`	WRITE-ONLY	只写，读只能借助其他寄存器在地址别名场景下验证
`R1`	READ-ONES	读操作每一位都返回 1
`RZ`	READ-ZEROS	读操作每一位都返回 0

易错点：其他寄存器工具里常见的 W1C、W1S、W0C 不是 CSR App 的访问类型，不要直接照搬。"写 1 清零"这类语义属于 Modified Write Value 范畴，通过 <cadence:hwAccessModifiedWriteValue> 或 IP-XACT 的 <spirit:modifiedWriteValue> 元素表达。

附录

关于如何将专有总线（非标准 APB/AHB/AXI）适配到 CSR 证明加速器，请参考官方文档附录。

CSR 验证方法论

CSR 验证的核心问题

寄存器验证最容易出错也最容易被忽略。常见 bug 包括：

地址映射错误（寄存器偏移量不对）
访问类型错误（RO 寄存器可写、RC 读清零行为不对）
复位值错误
字段位域定义错误
影子寄存器不更新

手动写 SVA 检查几十上百个寄存器非常繁琐且容易遗漏。CSR App 从 CSV/IP-XACT 定义自动生成所有断言。

CSV 格式要点

CSV 定义寄存器规格，以 CSR 行描述寄存器、FIELD 行描述字段、ATTR 行附加额外属性。例如：

CSR, ,REG1,32,0x0,RO
,FIELD,OVERFLOW,0,0,RO
,ATTR, DIRECT_WRITE, dut.write_status, dut.status,

寄存器行依次给出名称、位宽、复位值和访问类型；字段行给出字段名、位域和访问类型。访问类型只能取上文列出的 8 种之一。

验证策略

接口约束：CSR 验证需要总线协议约束（如 Wishbone/APB 的 assume），确保总线事务合法
Task 链接：将总线约束 task 链接到 CSR task，约束和检查在同一证明环境中
自动覆盖：CSR App 除断言和假设外还自动生成 cover 点，例如 COV_BUS_WRITE 验证总线写、COV_READ 验证读访问

实践建议：将 CSV 寄存器定义作为设计规格文档维护，不仅用于验证，也是文档。设计变更时先更新 CSV，CSR App 自动验证 RTL 符合新规格。

来源文档

jaspergold_csr_userguide.pdf
example_jaspergold_apps/CSR/