问SVA中“or”运算的分配性

EN

我今天又做了一次数学运算，两者并不相等。在某些情况下，属性或表单通过，但序列或表单将失败。

这方面的一个简单示例是属性：

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。一个人需要做数学计算。