system-verilog - SVA中 'or'操作的分布

Question

给定两个属性 P1 = (R1 or R2) |-> P 和 P2 = (R1 |-> P) or (R2 |-> P) ，其中 R1 和 R2 是序列，P 是一个属性，说 P1 是等价的是否正确到 P2?

我根据 LRM 的附件 F 中的严格和中性可满足性的定义进行了计算，结果发现它们是等价的。 (我不想排除我在某处犯错的可能性。)

我问，因为我看到模拟工具对这两者的处理方式不同。

Answer 1

我今天又算了一下，两者不等价。在某些情况下，属性或形式会通过，但序列或形式会失败。

一个简单的例子就是属性:

P1 = (1 or (1 ##1 1)) |-> 1
P2 = (1 |-> 1) or (1 ##1 1 |-> 1)

P2 对除 ⊥ 之外的任何一个时钟周期长的轨迹都非常满意。 P1 永远不能被短于两个时钟周期的跟踪满足。 (当将两种形式的属性(property)满意度条件插入到强烈满意度的定义中时，就会出现这种情况。)

用简单的英语来说，这意味着两个线程都从 P1 开始(一个用于 R1 部分，一个用于 R2部分)需要完成，直到此属性的断言被视为成功。但是，对于 P2，只有一个属性需要“成熟”，此时，另一个属性的尝试将被丢弃。

乍一看这似乎有点奇怪而且不太直观，但它源于 SVA 的形式语义。我想，但我不确定，P3 = first_match(R1 or R2) |-> P 等同于 P2。需要算一算。