verilog - SVA 语法：##1 a |-> b 与 a |-> $past(b) 之间的区别

Question

这两个表达式有什么区别：

##1 a |-> b 

相对

a |-> $past(b)

在第一个中，将b使用当前周期的值还是下一个周期的值？

Answer 1

由于您在这两种情况下都使用重叠蕴涵运算符，因此 LHS(antecedent) 变为 true 的循环与 RHS(consequent) 开始的循环相同。所以在第一个语句中，Botha和b必须在同一个循环中为真。只是将##1整个操作延迟一个周期。

您可能正在考虑重叠和非重叠之间的区别。对于这些简单的属性，以下是等价的：

a |-> b;
a |=> $past(b);