3

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.

Tudor Timi
  • 7,453
  • 1
  • 24
  • 53

1 Answers1

1

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.

Tudor Timi
  • 7,453
  • 1
  • 24
  • 53
  • 1
    Did you not mean "`P2`1 is strongly satisfied by any one clock cycle long trace, aside from ⊥. `P1` can never be satisfied by traces shorter than two clock cycles" ? Otherwise, you first sentence seems to contradict your fourth paragraph. Or have I misunderstood? – Matthew Taylor Aug 31 '16 at 15:14
  • 1
    @MatthewTaylor It wasn't paying attention when I wrote it. I meant that the sequence-or form can be strongly satisfied by traces shorter than two cycles. I edited the answer. – Tudor Timi Aug 31 '16 at 21:30
  • So you mean that for P1, the "or" operation in the antecedent part won't be completed in the 1st cycle itself (Ideally for "or" operation in assertions, if any of the inputs are satisfied then the assertion checking ends at that point only) ???? – Karan Shah Sep 01 '16 at 03:50
  • @KaranShah Nope. Assuming vacuous passes are turned off, a tool should show pass messages starting with 2 cycles from the start of the simulation. For `P2` it's going to start showing pass message from the very first cycles after the start of the simulation. – Tudor Timi Sep 20 '16 at 08:12
  • 1
    If that is the case, then what's the difference in execution time for P1 = (1 or (1 ##1 1)) |-> 1 and P1 = (1 and (1 ##1 1)) |-> 1. In the 2nd assertion, due to "and" it require 2 cycles to know the result of antecedent and hence 2 cycle for assertion evaluation as well. – Karan Shah Sep 20 '16 at 15:46
  • @KaranShah The difference is that the "or" variant checks the consequent twice (once per evaluation thread of the `or`), whereas the "and" variant checks it only once (at the end of the "and"). – Tudor Timi Sep 21 '16 at 14:24
  • @TudorTimi exactly, "and" will check after 2 cycles only. But "or" will check in 1st cycle & 2nd cycle, and if in the 1st cycle itself, assertion is found to be proven, then it should not go to the 2nd cycle. So my point is that the "or" variant can be completed in 1st cycle itself – Karan Shah Sep 22 '16 at 02:34