Hi,
Could someone kindly help me to understand how the following are equivalent?
S #-# P
Is equivalent to
not(S |-> not p)
I know followed by is used for concatenation of sequence and property but are there any other use cases for followed by operators say like to write a special case assertion or something?
Thank you
In reply to curious_learner:
Hi ,
First of all, both cases are different. In the first case, you tried to insert delay and in the second case, the implication is being used which will get you vacuous success at some points for sure.
Now coming to the problem statement, you want to check whether P is not equal to Q at the same sampling time and the property will give the right answer when this condition won’t get satiated.
So, yeah the second one is correct . If u don’t want to go with implication then simply write
sequence sq;
S == !P;
endsequence
property p1;
not sq;
endproperty
- Hope, this would help you.