A menudo las aserciones toman la forma: después de r es uno, entonces r irá a cero y permanecerá en cero durante al menos un ciclo, entonces se pondrá a 1.
assert propperty (@(negedge clk) r |-> ##1 !r [*1:$] ##1 r)
Esta es la aserción que chequea que r va a cero al menos un ciclo y luego vuelve a subir
Supongamos ahora que queremos comprobar que cond1 es cierto para todos los ciclos en los que r es cero. Lo hariamos mediante la siguiente aserción
assert propperty (@(negedge clk) r |-> ##1 (cond1 throughout (!r [*1:$])) ##1 r)
Fijémonos que hacemos un chequeo de una secuencia que sigue la señal r y además comprobamos que otra condición se cumple en determinados momentos de esta secuencia