Finite time FSM .Assertion

In reply to ben@SystemVerilog.us:

In reply to Timus:
Those 2 assertions have each a property; i just put the property content within the assertion statement.
Thus, declare the properties with property declaration.
Then write assert properly (P1 and P2) ;
It’s a AND because both properties must be true.
I believe that for a nonvacuity pass one of the 2 must be nonvacuous.
In general I prefer to have multiple smaller assertions, so I would not do this ANDing.
Do simulate the model.

After Anding P1 and P2 in assertion.
its showing Success all overr simularion time and same with the OR