安徽淮北发现一例无排名优化

 SystemVerilog 断言（SVA）中 内建系统函数 $onehot、$onehot0、$isunknown 和 $countones 。

1. $onehot(expression)

功能与定义

• 作用：检查表达式在指定时钟沿是否 只有 1 位为高电平（1），其他位必须为低电平（0）。

  • 若表达式为多热码（multiple-hot）或全零，返回 0（断言失败）。

• 语法：$onehot(signal)

示例与波形

property check_onehot;@(posedge clk) valid |-> $onehot(ctrl_bus); // ctrl_bus 必须为独热码
endpropertyassert property (check_onehot);

波形分析：

周期： 0   1   2   3
ctrl_bus: 0010  0100  1000  0011
valid  : 1      1      1      1

• 周期 0-2：ctrl_bus 仅有一位为高 → 断言通过。

• 周期 3：ctrl_bus 为 0011（两位为高）→ 断言失败。

2. $onehot0(expression)

功能与定义

• 作用：检查表达式在指定时钟沿是否 最多 1 位为高电平（1），允许全零。

  • 若表达式为多热码（multiple-hot），返回 0。

• 语法：$onehot0(signal)

示例与波形

property check_onehot0;@(posedge clk) valid |-> $onehot0(ctrl_bus); // ctrl_bus 可为全零或独热码
endpropertyassert property (check_onehot0);

波形分析：

周期： 0   1   2   3
ctrl_bus: 0000  0010  1000  0011
valid  : 1      1      1      1

• 周期 0：ctrl_bus 全零 → 断言通过。

• 周期 1-2：ctrl_bus 仅有一位为高 → 断言通过。

• 周期 3：ctrl_bus 为 0011 → 断言失败。

3. $isunknown(expression)

功能与定义

• 作用：检查表达式中 是否存在未知值（X 或 Z）。

  • 若有任意位为 X/Z，返回 1（断言失败）；否则返回 0。

• 语法：$isunknown(signal)

示例与波形

property check_unknown;@(posedge clk) valid |-> !$isunknown(data_bus); // data_bus 不得有 X/Z 值
endpropertyassert property (check_unknown);

波形分析：

周期： 0   1   2   3
data_bus: 8'hA5  8'hX1  8'hFF  8'hZZ
valid  : 1      1      1      1

• 周期 0,2：data_bus 无 X/Z → 断言通过。

• 周期 1,3：data_bus 存在 X/Z → 断言失败。

4. $countones(expression)

功能与定义

• 作用：计算表达式中 为高电平（1）的位数，返回无符号整数。

  • 常用于动态检查有效信号的数量。

• 语法：$countones(signal)

示例与波形

property check_countones;@(posedge clk) valid |-> ($countones(enable_bus) <= 2); // enable_bus 最多 2 位为高
endpropertyassert property (check_countones);

波形分析：

周期： 0   1   2   3
enable_bus: 0011  0101  1000  1110
valid    : 1      1      1      1

• 周期 0：2 位为高 → 断言通过。

• 周期 1：2 位为高 → 断言通过。

• 周期 2：1 位为高 → 断言通过。

• 周期 3：3 位为高 → 断言失败。

5. 对比总结

函数	功能	返回值	典型应用场景
$onehot	检查独热码（仅 1 位为高）	1（真）/0（假）	仲裁器、多路选择器控制信号
$onehot0	检查零或独热码	1（真）/0（假）	可屏蔽中断信号、低功耗模式
$isunknown	检测 X/Z 值	1（存在 X/Z）	总线稳定性检查、仿真 X 传播防护
$countones	统计高电平位数	无符号整数	并行资源管理、冗余设计检查