system-verilog-assertions - System Verilog 断言属性中的符号 '->' 和 '|->' 有什么区别

Question

我遇到了一个在这里工作的示例属性：

property p_a;
    @(posedge clk) $rose(a) -> $rose(b);
endproperty

上面没有语法错误。

然后我尝试修改为此

property p_a;
    @(posedge clk) $rose(a) -> ##2 $rose(b);
endproperty

这给了我语法错误，只是意识到它实际上不是'|->'

property p_a;
    @(posedge clk) $rose(a) |-> ##2 $rose(b);
endproperty

这行得通，那么->属性中的实际符号是什么？我通常知道它用于触发事件。

Answer 1

该->运算符是逻辑蕴涵运算符，适用于逻辑操作数：

逻辑蕴涵表达式1 -> expression2 在逻辑上等价于 (!expression1 || expression2)

|->是用于表达某些时间属性的顺序蕴涵。

蕴涵构造指定属性的检查是根据顺序前件的匹配有条件地执行的……此构造用于对属性表达式的监视进行前置条件，并且在属性级别是允许的。暗示的结果是真或假。左侧操作数 sequence_expr 称为前件，而右侧操作数 property_expr 称为后件...

换句话说，第一个可用于逻辑功能，第二个可用于事件序列。它们非常不同。