列举一个复杂逻辑表达式中的断言无法被检查的示例

本文举一个复杂逻辑表达式中的断言无法被检查的示例。

function bit legal_state( bit [0:3] current, bit valid）
bit_ok: assert #0 (!valid || (current ! = '0));
legal_state = valid && $onehot(current);
endfunction
...
always_comb begin
if (status || legal_state(valid, state)) . . .
根据定义，always_comb 中if括号里面的逻辑表达式在每次变量发生变化时都会进行判断。代码的开发者可能觉得逻辑表达式中的断言bit_ok每次都能够得到执行。

但实际上，仿真器对于SystemVeilog的这种情况会进行优化的。对于逻辑表达式

status || legal_state(valid, state)
仿真器不会傻傻地计算出所有的逻辑项，如果仿真器觉得status 已经是1’b1了，那么它就会觉得再计算函数legal_state(valid, state)是没有意义的，自然也就没有执行其中的

bit_ok: assert #0 (!valid || (current ! = '0));

同理，对于and逻辑，如果第一个逻辑项是1’b0，仿真器自然也不会计算其后的逻辑项。
这个问题很容易解决，那就是将这个修改成

legal_state(valid, state) || status

但是，如果你有多个类似legal_state() 这样的函数呢？你就只能小心地进行多次函数判断，以确保每个带有这种断言的函数得到计算执行。

原作者：验证哥布林