In reply to Timus:
1800 says: An evaluation attempt of a property of the form property_expr1 and property_expr2 is nonvacuous if, and only if, either the underlying evaluation attempt of property_expr1 is nonvacuous or the underlying evaluation attempt of property_expr2 is nonvacuous.
Thus, P1 and P2 is nonvacuous if either P1 or P2 is nonvacuous.
The assertions address all the requirements for the RTL model.
For the model to be correct it is necessary that ALL properties described
in the checking unit are correct. Each property describes a different
aspect of the requirements, thus you cannot say that under all test conditions
it is OK if one of them fails (you get that with the P1 or P2.
first_match($rose(state==ABS) ##1 state==ABS[*1:99] ##0 ack) |-> state==BBS);
// if the antecedent is a match then
// in the SAME cycle as ack state mus tb ==BBS
// If it does not, then it fails.
// The other property can still pass.
// BTW, you may want
first_match($rose(state==ABS) ##1 state==ABS[*1:99] ##0 ack) |-> ##1 state==BBS);