PINMUX_Spec与Testplan.md
PINMUX — 功能 Spec 与验证 Testplan（详细版）
工程路径：
/project/SOC_V1.1/To_Customer/PINMUX/
验证形态：形式验证（VC Formal）+ SystemVerilog Assertions
关联：IP验证环境资料.md
第一部分：功能 Spec
1. 概述
1.1 功能定义
PINMUX 子系统完成两类功能：
- IO 复用（
pin_mux）：根据每路 pad 的 3bit 复用配置，将片内 SPI0/SPI1、UART、I2C0/I2C1 等信号映射到pad[20:1]（及专用时钟/复位 pad）。 - 复用寄存器（
pin_mux_rf+pin_mux_rf_top）：通过 APB 类接口 配置r_io_reuse_pad1~r_io_reuse_pad20。
另含 IO Pad 单元（gnrl_io_pad.v、TPPADLRCMCUDB.v）处理电气特性。
1.2 模块层次
pin_mux_rf_top
└── pin_mux_rf # 配置寄存器
pin_mux # 组合复用逻辑（大 case）
gnrl_io_pad / TPPADLRCMCUDB # PAD 原语
sva_checker (FPV) # 断言模块 pinmux.sva
FPV 顶层：read_file -top pin_mux（见 FPV/solution/batch.tcl）。
2. 端口 Spec — pin_mux
2.1 片内侧信号（输入到 mux 的“功能信号”）
| 组 | 信号（节选） | 方向（相对 mux） |
|---|---|---|
| SPI0 | spi0_clk, spi0_csn0~3, spi0_sdo0~3, spi0_oe0~3, spi0_sdi0~3 |
主机侧 |
| SPI1 | spi1_* |
同上 |
| UART | ua_txd（出）, ua_rxd（入） |
串口 |
| I2C0/1 | i2c*_scl/sda_pad_o, *_padoen_o（出）, *_pad_i（入） |
开漏 IO |
| 时钟/复位 | cpu_clk, cpu_reset_n, apb_clk, apb_reset_n |
输出到专用 pad |
| 配置 | r_io_reuse_pad1 ~ r_io_reuse_pad20 |
每路 3bit |
2.2 片外侧 — pad[20:1]
- inout 双向 pad 总线。
- SoC 集成时
soc_top为pad[24:1]，与验证包 20 路 子集或扩展映射以 RTL 为准。
2.3 专用时钟/复位输出
| 输出 | 来源 |
|---|---|
clk_cpu |
cpu_clk |
rst_n_cpu |
cpu_reset_n |
pclk |
apb_clk |
prest_n |
apb_reset_n |
3. 复用编码 Spec（全局）
每个 r_io_reuse_padN[2:0] 选择该 物理 pad N 上承载的功能：
编码 reuse[2:0] |
功能组 | 说明 |
|---|---|---|
3'b000 |
SPI0 | 该 pad 用作 SPI0 的某一信号（clk/csn/sdo/sdi 等，依 pad 编号而定） |
3'b001 |
SPI1 | SPI1 对应信号 |
3'b010 |
I2C0 | I2C0 SCL/SDA（开漏，含 padoen） |
3'b011 |
I2C1 | I2C1 |
3'b100 |
UART | TX 或 RX（依 pad） |
| 其它 | 保留/高阻 | default 多为输出 0、oe=0 |
重要：同一编码在不同 pad 上对应 不同的具体信号（由 pin_mux.v 内 per-pad case 决定），不能理解为“全局一根线”。
4. 典型 Pad 复用表（摘自 RTL 行为）
以下为实现级摘要，便于对照波形与 SVA（非全部 pad）：
4.1 SPI0 相关（reuse==3'b000）
| Pad | 复用为 SPI0 | 方向 |
|---|---|---|
| 1 | spi0_clk |
输出 |
| 2 | spi0_csn0 |
输出 |
| 3 | spi0_sdo0 |
输出（oe 随 spi0_oe0） |
| 4 | spi0_sdi0 |
输入 |
| 7 | spi0_sdo1 / sdi1 等 |
依 case |
| … | 更多 SDO/SDI | 见 pin_mux.v |
输入汇聚（当某 pad 配置为 SPI0 的 SDI 角色时）：
spi0_sdi0 = (r_io_reuse_pad4==0) ? pad4 : (r_io_reuse_pad17==0) ? pad17 : 0- 即 同一 SDI 功能可映射到 pad4 或 pad17（二选一）。
4.2 SPI1 相关（reuse==3'b001）
| Pad | 示例功能 |
|---|---|
| 2 | spi1_clk |
| 3 | spi1_csn0 |
| 5 | spi1_sdi0（与 pad17 可选） |
4.3 I2C0（reuse==3'b010）
| Pad | 信号 |
|---|---|
| 3 | i2c0_sda |
| 4 | i2c0_scl |
环境假设（FPV assume_i2c_signal）：若 pad3 为 I2C0，则 pad4 也为 I2C0。
4.4 I2C1（reuse==3'b011）
| Pad | 信号 |
|---|---|
| 5 | i2c1_sda |
| 6 | i2c1_scl |
4.5 UART（reuse==3'b100）
| Pad | 信号 |
|---|---|
| 3 | ua_txd 输出 |
| 4 | ua_rxd 输入 |
输入：ua_rxd = (pad4==UART) ? pad4 : (pad20==UART) ? pad20 : 0
4.6 pad1 / pad2 示例（理解 case 结构）
pad1（r_io_reuse_pad1）：
| reuse | pad1 输出 |
|---|---|
| 000 | spi0_clk |
| 001~100 | 高阻/0 |
pad2（r_io_reuse_pad2）：
| reuse | pad2 输出 |
|---|---|
| 000 | spi0_csn0 |
| 001 | spi1_clk |
5. 配置寄存器 Spec — pin_mux_rf
5.1 接口
经 pin_mux_rf_top 转 APB：
| APB 信号 | 宽度 | 说明 |
|---|---|---|
paddr[15:0] |
16 | 字节地址 |
pwdata[7:0] |
8 | 写数据 |
prdata[7:0] |
8 | 读数据 |
pwrite/psel/penable |
— | 标准 APB 相位 |
内部转为 sft_adr_i / sft_dat_i / sft_wr_i / sft_rd_i。
5.2 寄存器地址映射（字地址 sft_adr_i）
每地址 8bit 写数据 打包 两个 pad 的 3bit 复用域：
| 地址 (hex) | 写入位域 | 控制的 pad |
|---|---|---|
0x00 |
[6:4] → pad2；[2:0] → pad1 |
pad1, pad2 |
0x01 |
[6:4] → pad4；[2:0] → pad3 |
pad3, pad4 |
0x02 |
pad6, pad5 | |
0x03 |
pad8, pad7 | |
0x04 |
pad10, pad9 | |
0x05 |
pad12, pad11 | |
0x06 |
pad14, pad13 | |
0x07 |
pad16, pad15 | |
0x08 |
pad18, pad17 | |
0x09 |
pad20, pad19 |
复位值：各 reg_io_reuse_pad* 复位为 3'h0（默认 SPI0 组）。
5.3 读回
读操作时 sft_dat_o 返回对应地址的 8bit 寄存器镜像（实现见 pin_mux_rf.v 读多路选择）。
6. FPV / SVA Spec — pinmux.sva
模块 sva_checker 端口与 pin_mux 侧信号对齐（SPI0/1、I2C、UART、reuse、pad、时钟复位）。
6.1 断言（Assert）
| 名称 | 语义（自然语言） |
|---|---|
assert_spi0_csn0_pad_2_15 |
当 spi0_csn0 有效且 r_io_reuse_pad15==0 时，应有 pad[15] 参与（与 pad2 映射场景相关，需结合 RTL） |
assert_spi0_csn0_cannot_map_to_pad_3 |
spi0_csn0 有效且 pad15 为 SPI0 时，不应错误出现在 pad[3] |
说明：交付包内断言为 示例/子集；完整 pinmux 需按项目补全“每个功能信号仅出现在合法 pad 集合”类属性。
6.2 假设（Assume）— 约束输入空间
| 名称 | 语义 |
|---|---|
assume_i2c_signal |
r_io_reuse_pad3==2 → r_io_reuse_pad4==2（I2C0 成对） |
assume_qspi0_signal |
r_io_reuse_pad3==1 → pad4/5/6 均为 SPI1 组（编码 1） |
6.3 覆盖（Cover）
| 名称 | 意图 |
|---|---|
cov_spi0_csn0_pad2 |
SPI0 CSn 出现在 pad2 配置 |
cov_spi0_csn0_pad15 |
SPI0 CSn 出现在 pad15 配置 |
7. 与 SoC test.v 的关系
SoC 片级仿真 固定 部分 pad（不通过软件改 reuse）：
| pad | SoC test.v 连接 |
|---|---|
| 21 | clk_cpu |
| 22 | rst_n_cpu |
| 1~13 | SPI0 四线等 |
FPV 验证的是 pin_mux 逻辑；集成时若 force pad，需在 review 时区分 “静态 testbench 约束” 与 “软件可配 reuse”。
第二部分：验证 Testplan（形式验证）
8. 验证目标
| # | 目标 |
|---|---|
| 1 | 证明关键 SPI0 片选信号 仅映射到合法 pad |
| 2 | 在合理 assume 下 无断言失败 |
| 3 | cover 点可达（证明环境非过约束） |
| 4 | 为 SoC 管脚约束提供形式化依据 |
9. 验证策略
| 项 | 选择 |
|---|---|
| 工具 | Synopsys VC Formal（vcf） |
| 顶层 | pin_mux |
| 读入 | rtl/filelist + bind SVA |
| 时钟 | cpu_clk、apb_clk period=100 |
| 复位 | cpu_reset_n、apb_reset_n 高有效 |
| 引擎 | check_fv -block |
非目标：动态仿真、APB 总线 UVM、电气特性（ESD/驱动能力）。
10. 形式验证用例（“形式 test”）
| Case ID | 类型 | 对象 | 步骤 | 通过准则 |
|---|---|---|---|---|
| PM-F01 | assert | assert_spi0_csn0_* |
vcf -f batch.tcl |
无 counterexample |
| PM-F02 | assume | I2C/QSPI 组假设 | 同上 | 证明完成且 assumptions 合理 |
| PM-F03 | cover | cov_spi0_csn0_pad2/15 |
查看 cover 报告 | 非 vacuous |
| PM-F04 | 复位 | sim_save_reset |
batch.tcl | reset 状态下无违例 |
11. 详细执行步骤（PM-F01 主流程）
| 步 | 操作 | 检查点 |
|---|---|---|
| 1 | cd PINMUX/FPV/solution |
路径正确 |
| 2 | 确认 ../../rtl/filelist 可读 |
RTL+SVA 齐全 |
| 3 | vcf -verdi -f batch.tcl 或批处理 vcf -f batch.tcl |
license OK |
| 4 | 等待 check_fv -block 完成 |
无 FAIL assert |
| 5 | 打开 results.txt |
列表全 PASS 或 expected |
| 6 | 若有 FAIL | Verdi 看 counterexample 波形，区分 RTL bug / 过弱 assume / 错误属性 |
12. 属性评审清单（扩展用）
建议在后续版本补充的形式属性（当前交付未全部实现）：
| ID | 属性描述 | 优先级 |
|---|---|---|
| PM-A01 | 任一时刻每个 SPI0 功能信号最多驱动一个 pad | P0 |
| PM-A02 | UART TX 仅在 reuse=100 的 pad 上驱动 | P1 |
| PM-A03 | I2C pad 必须成对出现（已有 assume 子集） | P0 |
| PM-A04 | 非法 reuse 编码不导致 X 传播到 pad | P1 |
| PM-A05 | 复位后 reuse 寄存器为 0 | P2 |
13. 覆盖率（形式）
| 类型 | 说明 |
|---|---|
cover property |
已定义 pad2/pad15 CSn 场景 |
| 证明 depth | 由 sim_run -stable 与工具默认决定 |
| 出口 | 所有 assert proven；cover 非空 |
14. 出口准则
| # | 准则 |
|---|---|
| 1 | batch.tcl 跑通无 assert failure |
| 2 | results.txt 归档 |
| 3 | assume 已评审（不过强导致 vacuous proof） |
| 4 | 与 SoC pad 表、数据手册 pinout 交叉核对 |
15. 与动态仿真的分工
| 验证层 | PINMUX FPV | SoC soc/test.v |
|---|---|---|
| 方法 | 全状态空间属性 | 固定 pad + CPU 跑程序 |
| 优点 | 穷举连接关系 | 真实系统场景 |
| 缺点 | 依赖 assume | 不覆盖所有 reuse 组合 |
建议：FPV PASS + SoC 至少 1 个 SPI/UART 场景 PASS，再签核 pinmux 相关风险。