In reply to ben@SystemVerilog.us:
Thanks Ben. I will have a read of your paper.
Please correct me if I have not understood correctly.
Let’s break the first line down:
(state == FSM_SAMPLE) [*1:] |=> (state == FSM_STREAM) [*1:]
So because of the unspecified range, we can say that the antecedent will spawn an arbitrary number of threads N at each sampling event. Only one of these threads would pass for each clocking events, whilst we remain in FSM_SAMPLE and then transition to FSM_STREAM.
Similarly, this can be applied to all of the lines.
Now the trouble is how all of this interacts when there are 2 implication operators in the antecedent. So, I am presuming it’s hard to decipher what case will cause this whole property to fail specifically so such a property can be assumed to never succeed.