La comprobación del comportamiento deseado afecta varios ciclos
|
1 |
assert propperty (@(negedge clk) a==2 ##1 a==4); |
| a: | 2 | 4 | 2 | 2 | 4 |
| c: | 0 | 1 | 2 | 3 | 4 |
- La comprobación se realiza igualmente en todos los ciclos (con solapamiento)
- La aserción falla tan pronto se comprueba que dicha secuencia no puede ocurrir
- En el ciclo 0: la comprobación es cierta en el primer elemento de la secuencia
- En el ciclo 1: la comprobación es cierta en el segundo elemento de la secuencia; sin embargo hay fallo por una nueva secuencia que se inicializa y en la que ya no hay coincidencia en el primer elemento de la secuencia. En 1 sabemos que la secuencia nunca coincidirá y ya damos el fallo y abortamos dicha comprobación de esta secuencia
- En el ciclo 2: falla en ciclo 3. En 2 creemos que la secuencia podría coincidir (puesto que el primer elemento coincide) y al ciclo 3 nos damos cuenta de que estábamos equivocados
- En el ciclo 3: Finaliza la comprobación de la secuencia que falla en su segundo elemento y comienza la comprobación de una nueva secuencia en la cual el primer elemento es correcto y el segundo coincidirá en ciclo 4