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.