第三章X-Propagation 未知态传播验证

什么是 X-Propagation

在 RTL 仿真中，信号的 X 值（未知态）可能导致仿真结果过于乐观（X-optimism）——RTL 仿真中隐藏了实际硬件中可能出现的问题。X-Propagation App 通过形式方法检测 X 在设计中的传播路径，发现那些 X 被 RTL 仿真"吞掉"但在实际硅片中可能导致功能错误的情况。

X-Prop App 流程

1. 加载设计（analyze + elaborate）
2. 声明时钟和复位
3. 运行 X-Prop 分析（自动生成 X-Prop 属性）
4. 查看结果、调试违规

GUI 导览

运行 X-Prop 验证

# 启动 X-Prop 模式
# jg -xprop <script.tcl>

# 在脚本中运行
check_xprop

# 针对特定模块运行
check_xprop -instance top.u_dut

X-Prop 行为

isunknown() 支持

SystemVerilog 的 $isunknown() 系统函数在 X-Prop 验证中被正确支持，用于检测 X 值。

=== 运算符的 X-Prop 行为

case equality 运算符 ===（wildcard equality）在 X 处理上与 == 不同，X-Prop App 正确建模其行为。

X-Prop 专用命令

# X-Prop 专用配置命令
set_xprop_propagation_mode -mode {optimistic|pessimistic}
xprop_assume -reset
xprop_assert -signal <sig>

调试 X-Prop 违规

当 X-Prop 属性失败时：

1. 双击 failed 属性打开 Visualize
2. 查看 X 值传播路径（X-Propagation Graph）
3. 确定 X 的源头（未初始化寄存器、复位不完全、非法输入等）
4. 修复 RTL 或添加复位/约束

X-Propagation Graphs

X-Prop Graph Window 可视化展示 X 值的传播路径：

• Graph Window：图形化显示 X 传播
• Proving Properties：查看证明进度
• Replaying Proof/Violation：重放证明过程/违规
• Filtering Elements：过滤图形元素

Waiving Properties

# 豁免 X-Prop 属性
waive_xprop -property <name> -reason "X resolved by sync"

X-Propagation 验证界面

X-Prop 方法论

RTL 仿真的乐观性问题

RTL 仿真中 X 值的传播遵循 Verilog 语义：X AND 0 = 0（因为 0 AND 任何值都是 0），X OR 1 = 1。这是乐观的——实际电路中 X 可能是 0 也可能是 1，乐观仿真可能漏掉真实 bug。

经典案例：复位后未初始化的状态机在 RTL 仿真中看起来正常（X 被乐观优化掉），但在硅片中可能死锁。

三种 init_control 模式

X-Prop 结果解读

X-Prop 属性失败意味着在某个时钟周期，输出端口/控制信号出现了 X 值。在波形中：

• 红色 X 标记出现在输出信号上 → 从该点倒推，找到 X 的源头（未初始化 flop/X 赋值/跨域）
• 修复方式：添加复位初始化、修改 X 赋值逻辑、添加 X 处理（如 case 的 default）