第四章CSR 寄存器验证
概述
寄存器验证App 通过 CSV（逗号分隔值）配置表自动生成断言，验证寄存器的读写行为、复位值、访问权限等，无需手动编写大量 SVA。
CSR App 工作流程
- 准备 CSV 工作表描述寄存器映射
- 加载设计和 CSV
- CSR App 自动生成断言和假设
- 运行证明验证寄存器行为
寄存器行为建模
只读寄存器
| 类型 | CSV 标记 | 说明 |
|---|---|---|
| 常量值 | RO_const | 字段值恒定不变 |
| 设计更新状态 | RO_hw | 字段由硬件逻辑更新 |
| 忽略数据检查 | RO_ignore | 只读但不验证数据值 |
只写寄存器
WO：只能写入，读取值不检查或返回固定值。
同时读写
处理寄存器在同一时钟周期被读和写的情况。
锁定行为
- Register Writes are Locked：写操作被锁定（如锁定后写入无效）
- Register Read Data is Locked or Ignored：读数据被锁定或忽略
其他行为
- Register Aliasing：多个地址映射到同一寄存器
- Preventing Reads/Writes：阻止特定寄存器的读写验证
- Value Range：验证寄存器值在指定范围内
- Reset Value Expression：复位值表达式
扩展文件
对于标准 CSV 无法表达的特殊行为，可以使用扩展文件（Extension File）：
# 生成模板扩展文件
generate_csr_extension_template -output ext.tcl
# 合并扩展文件
merge_csr_extensions -ext ext1.tcl -ext ext2.tclSupporting Details
| 主题 | 内容 |
|---|---|
| Instance Interface | CSR App 与 RTL 的接口信号约定 |
| Worksheet Format | CSV 文件格式定义（列名、数据类型） |
| Access Types | 支持的访问类型：RO/RW/WO/RC/W1C/W1S 等 |
| Bus Write/Read Enable | 支持总线级写/读使能信号 |
| Direct Write/Read | 直接读写接口支持 |
| Latencies | 读写延迟支持 |
| Modified Write Value | 写值被硬件修改的情况 |
| Masks | 写屏蔽/读屏蔽支持 |
| Register Maps | Secure/Non-Secure 映射、Remap States |
| Address Blocks | 地址块和保留地址 |
| Windowed CSRs | 窗口化寄存器（间接寻址） |
附录
关于如何将专有总线（非标准 APB/AHB/AXI）适配到 CSR 证明加速器，请参考官方文档附录。
CSR 验证方法论
CSR 验证的核心问题
寄存器验证最容易出错也最容易被忽略。常见 bug 包括：
- 地址映射错误（寄存器偏移量不对）
- 访问类型错误（RO 寄存器可写、W1C 行为不对）
- 复位值错误
- 字段位域定义错误
- 影子寄存器不更新
手动写 SVA 检查几十上百个寄存器非常繁琐且容易遗漏。CSR App 从 CSV/IP-XACT 定义自动生成所有断言。
CSV 格式要点
CSV 定义寄存器规格，关键列包括：寄存器名、地址偏移、字段名、位域、访问类型（RW/RO/W1C/W1S/W0C 等）、复位值、硬件行为。
验证策略
- 接口约束：CSR 验证需要总线协议约束（如 Wishbone/APB 的 assume），确保总线事务合法
- Task 链接：将总线约束 task 链接到 CSR task，约束和检查在同一证明环境中
- 自动覆盖：CSR App 自动生成 cover 点验证每个寄存器可读写
实践建议：将 CSV 寄存器定义作为设计规格文档维护，不仅用于验证，也是文档。设计变更时先更新 CSV，CSR App 自动验证 RTL 符合新规格。
来源文档
jaspergold_csr_userguide.pdfexample_jaspergold_apps/CSR/