Given the two properties P1 = (R1 or R2) |-> P and P2 = (R1 |-> P) or (R2 |-> P), where R1 and R2 are sequences and P is a property, is it correct to say that P1 is equivalent to P2?
I did the calculations based on the definitions of tight and neutral satisfiability in Annex F of the LRM and they came up as being equivalent. (I don't want to exclude the possibility of me making a mistake somewhere.)
I ask, because I've seen the two being handled differently by simulation tools.
I did the math again today and the two are not equivalent. There are cases where the property-or form passes, but where the sequence-or form would fail.
A simple example of this would be the properties:
P1 = (1 or (1 ##1 1)) |-> 1
P2 = (1 |-> 1) or (1 ##1 1 |-> 1)
P2 is strongly satisfied by any one clock cycle long trace, aside from ⊥. P1 can never be satisfied by traces shorter than two clock cycles. (This comes out when plugging the conditions of property satisfaction for both forms into the definition of strong satisfaction.)
What this means in plain English is that both threads started in P1 (the one for the R1 part and the one for the R2 part) need to complete until an assertion of this property is deemed successful. For P2, though, only one of the properties is required to "mature" and at this point, the other property's attempt will be discarded.
This seems a bit strange at first glance and not so intuitive, but it stems out of the formal semantics for SVAs. I guess, but I'm not sure, that P3 = first_match(R1 or R2) |-> P is equivalent to P2. One would need to do the math.