第三章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>

# 1) 指定 control point 作为目标（默认不提取任何 control point）
check_xprop -init_control true

# 2) 创建 X-Prop 属性
check_xprop -create -outputs -no_bit_blast
check_xprop -create -control -no_bit_blast
check_xprop -create -clocks_and_resets -no_bit_blast

# 3) 证明
check_xprop -prove -no_decompose -all

X-Prop 行为

$isunknown() 支持

在形式分析中与 X 做比较，要用 X-Prop App 配合 $isunknown 运算符。但注意默认行为：$isunknown(<signal>) 和 $isunknown(<expression>) 默认总是返回 false（1'b0）。要真正启用它，必须使用 elaborate -enable_sva_isunknown。

此外它的支持是部分的——文档的支持表中有若干项明确标注为不支持（如 Tcl 提示符下的二元/一元运算符、嵌套的 $isunknown、SERE）。

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

=== 是 case equality（全等）运算符——注意不要与 wildcard equality 混淆，后者是 ==? / !=?。

关键的默认行为：=== 'Z 在 X-Prop 中需要 -triple_equal 选项才被支持。如果不使用 elaborate -triple_equal，工具会把 === 和 !== 当作 == 和 != 处理——也就是说，默认情况下工具并不遵循 case equality 语义。

X-Prop 专用命令

# X-Prop 专用通用命令
assert -xprop
assume -xprop
assume -xprop -is_x

# control point / data point 的指定（布尔值）
check_xprop -init_control true
check_xprop -init_all_control true
check_xprop -init_data true
check_xprop -init_all_data true

调试 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 属性
check_xprop -waiver

check_xprop 的可用选项为：-abstract、-clear、-create、-export、-get_expression、-highlight_failure_path、-import_cover、-init_control、-prove、-report、-waiver。

X-Propagation 验证界面

X-Prop 方法论

X-optimism 与 X-pessimism：仿真为什么不可信

设计中 X 值的传播若未被发现，会导致仿真与综合不一致（simulation-synthesis mismatch）。由于 HDL 语义的限制，仿真器并不能匹配真实电路的行为，而是给出乐观（optimistic）或悲观（pessimistic）的分析——两者都有各自的缺陷。

乐观分析的例子：

always @ (posedge clk or negedge rst_n)
     if (~rst_n)
           cnt <= 3'd0
     else if (cnt_en)
           cnt <= cnt_nxt

假设 rst_n 为 1、cnt_en 为 X。正确的行为应该是 cnt 要么保持原值、要么更新为 cnt_nxt。而乐观的仿真分析意味着 X 不会通过 if 语句传播，cnt 直接保持原值——真实的不确定性被掩盖了。

悲观分析的例子：

wire output = (~sel & A) | (sel & B);

假设 sel 为 X。Verilog 的仿真语义规定输出为 X。然而在真实电路中，如果 A == B，输出就确定等于 A——仿真报了一个并不存在的问题。

X-optimism 和 X-pessimism 之所以成为问题，是因为它们使 RTL 仿真的行为不同于门级仿真、也不同于真实电路。

X-Prop App 检查 X 值能否传播到那些"本应有确定 0/1 值"的点。工具匹配的是真实电路的行为——如果它在某个用户指定点检测到 X，那么该电路上也确实如此。JasperGold 执行的是穷尽的 X 传播检查：只要存在 X 传播的可能性，工具就会检测到该场景。

指定 control point：-init_control 与 -init_all_control

这两个选项取布尔值 true / false，不是 0/1/2 的档位。它们的作用是指定 control point 作为目标——默认情况下工具不会提取任何 control point，所以不指定就等于什么都不查。

两个修饰选项：

• -sequential：只从时序块（如 always @(posedge clk)）提取 control point。默认时序块和组合块都会提取。
• -expression：只提取 Verilog case 语句中可能产生 X 的那些位；不加此选项则把整个 case 变量（所有位）作为 control point 提取。

X 的来源（Sources of X）

设计中可能存在多种 X 来源，可在 X-Propagation Wizard 中按需勾选。注意每一种的默认开关状态不同——这决定了不勾选时工具到底查不查它：

X-Prop 结果解读

X-Prop 属性失败意味着在某个时钟周期，本应为确定 0/1 的点上出现了 X 值。调试时从该点倒推，对照上表定位 X 的源头，再决定是补复位初始化、改 X 赋值逻辑，还是显式处理 X（如 case 的 default）。