system-verilog - SVA中“或”运算的分布

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短于两个时钟周期的走线永远无法满足。（当将两种形式的财产满足条件插入到强满足的定义中时，就会出现这种情况。）

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

乍一看，这似乎有点奇怪，也不是那么直观，但它源于 SVA 的形式语义。我想，但我不确定，这P3 = first_match(R1 or R2) |-> P相当于P2. 一个人需要做数学。