Secuencias en la condición de implicación

Cada vez que la secuencia se detecte (con solapamiento) la aserción tras la implicación será evaluada

assert property (@(posedge clk) a ##1 !a ##1 a |-> ##1 grant ##1 !grant)

1	assert property (@(posedge clk) a ##1 !a ##1 a \|-> ##1 grant ##1 !grant)

g:	0	0	0	1	0	0	0	1	0
a:	1	0	1	0	1	0	0	0	1
c:	1	2	3	4	5	6	7	8	9

e.a. comenzó en 0: abortado en 0
e.a. comenzó en 1: coincide en 5
e.a. comenzó en 2: abortado en el 2
e.a. comenzó en 3: falla en 6 (en.cond. emparejado)
e.a. comenzó en 4: abortado en 4
e.a. comenzó en 5: abortado en 7

Si en la habilitación pongo no una secuencia sino un conjunto de secuencias (mediante por ejemplo un rango de repetición) el funcionamiento prácticamente es el mismo: la aserción se evaluará cada vez que alguna de las secuencias de la habilitación sea cierta.

Por ejemplo si utilizamos

assert property (@(posedge clk) a ##1 !a[*0:$] ##1 a |-> ##1 grant ##1 !grant)

1	assert property (@(posedge clk) a ##1 !a[*0:$] ##1 a \|-> ##1 grant ##1 !grant)

vemos que en la condición de habilitación hay en realidad infinitas secuencias descritas. Por lo tanto cada vez que alguna de ellas sea cierta, la comprobación de la aserción deberá ser realizada , en este caso la detección de un paso de “grand” de 1 a 0 un ciclo después de detectar la secuencia de habilitación