'or' 操作在 SVA 中的分布
Distributivity of 'or' operation in SVA
给定 P1 = (R1 or R2) |-> P 和 P2 = (R1 |-> P) or (R2 |-> P) 这两个属性，其中 R1 和 R2 是序列，P 是 属性，是正确地说 P1 等同于 P2?
我根据 LRM 的附件 F 中紧和中性可满足性的定义进行了计算，结果发现它们是等价的。 （我不想排除我在某处犯错的可能性。）
我问，因为我看到模拟工具对这两者的处理方式不同。
今天又算了一下，两者不等价。在某些情况下，属性-or 形式通过，但 sequence-or 形式失败。
一个简单的例子就是属性：
P1 = (1 or (1 ##1 1)) |-> 1
P2 = (1 |-> 1) or (1 ##1 1 |-> 1)
P2 除了 ⊥ 之外，任何一个时钟周期长的跟踪都强烈满足。 P1 永远无法满足短于两个时钟周期的跟踪。 （当将两种形式的 属性 满意度条件插入到强烈满意度的定义中时，就会出现这种情况。）
用简单的英语来说，这意味着在 P1 中启动的两个线程（一个用于 R1 部分和一个用于 R2 部分）需要完成直到此 属性 的断言被视为成功。但是，对于 P2，"mature" 只需要一个属性，此时，另一个 属性 的尝试将被丢弃。
乍一看这似乎有点奇怪而且不太直观，但它源于 SVA 的形式语义。我想，但我不确定，P3 = first_match(R1 or R2) |-> P 等同于 P2。需要算一算。
给定 P1 = (R1 or R2) |-> P 和 P2 = (R1 |-> P) or (R2 |-> P) 这两个属性，其中 R1 和 R2 是序列，P 是 属性，是正确地说 P1 等同于 P2?
我根据 LRM 的附件 F 中紧和中性可满足性的定义进行了计算，结果发现它们是等价的。 （我不想排除我在某处犯错的可能性。）
我问，因为我看到模拟工具对这两者的处理方式不同。
今天又算了一下，两者不等价。在某些情况下，属性-or 形式通过，但 sequence-or 形式失败。
一个简单的例子就是属性：
P1 = (1 or (1 ##1 1)) |-> 1
P2 = (1 |-> 1) or (1 ##1 1 |-> 1)
P2 除了 ⊥ 之外，任何一个时钟周期长的跟踪都强烈满足。 P1 永远无法满足短于两个时钟周期的跟踪。 （当将两种形式的 属性 满意度条件插入到强烈满意度的定义中时，就会出现这种情况。）
用简单的英语来说，这意味着在 P1 中启动的两个线程（一个用于 R1 部分和一个用于 R2 部分）需要完成直到此 属性 的断言被视为成功。但是，对于 P2，"mature" 只需要一个属性，此时，另一个 属性 的尝试将被丢弃。
乍一看这似乎有点奇怪而且不太直观，但它源于 SVA 的形式语义。我想，但我不确定，P3 = first_match(R1 or R2) |-> P 等同于 P2。需要算一算。