- $rose(a): “a” es uno y fue cero en el pasado ciclo de reloj
- $fell(a): ): “a” es cero y fue uno en el pasado ciclo de reloj
- $stable(a): “a” mantiene el mismo valor que en el ciclo pasado
- $past(a): el valor que tenia “a” en el pasado ciclo
- $past(a,7): el valor que tenia “a” hace 7 ciclos
| a | 0 | 0 | 1 | 0 | 1 | 1 | 1 | 1 | 0 | 1 | 0 | 0 | 0 | 0 | 1 | 1 | 0 | 0 | |
| $rose(a) | 0 | 0 | 1 | 0 | 1 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | |
| $fell(a) | ? | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 1 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | |
| $stable(a) | ? | 1 | 0 | 0 | 0 | 1 | 1 | 1 | 0 | 0 | 0 | 1 | 1 | 1 | 0 | 1 | 0 | 1 | |
| $past(a) | ? | 0 | 0 | 1 | 0 | 1 | 1 | 1 | 1 | 0 | 1 | 0 | 0 | 0 | 0 | 1 | 1 | 0 | |
| $past(a,2) | ? | ? | 0 | 0 | 1 | 0 | 1 | 1 | 1 | 1 | 0 | 1 | 0 | 0 | 0 | 0 | 1 | 1 |
Ejemplo1
Queremos chequear que “grant” pasa a uno tres ciclos después de que “request” se active. Si lo hacemos mediante:
|
1 |
assert propperty (@(posedge clk) r |-> ##3 $rose(g)) // wrong |
| g: | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | |
| r: | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 | |
| c: | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 |
- la aserción se anulará inmediatamente en 0,1,2,3 porque la condición de habilitación no coincide
- la condición de habilitación coincide a 4, 5, 6, 7…
- El chequeo que se inicia en ciclo 4, es correcto en el 7
- Todos los demás intentos (5, 6, 7, …) fallan
Por tanto para hacerla correctamente vamos a utilizar una función predefinida que solo sea cierta cuando la señal a pasado de 0 a 1
|
1 |
assert propperty (@(posedge clk) $rose(r) |-> ##3 $rose(g)) // good |
| g: | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | |
| r: | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 | |
| c: | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 |
- la aserción se anulará inmediatamente en 0,1,2,3,5,6,7 porque la condición de habilitación no coincide
- la condición de habilitación coincide en 4
- El chequeo que se inicia en ciclo 4, es correcto en el 7
- Sin fallo