Ahora la comprobación de la secuencia tiene una condición previa Ø
|
1 |
assert propperty (@(negedge clk) req |->##1 grant); |
Se hace una evaluación en cada ciclo . Si la condición de habilitación es falsa , esa evaluación en ese ciclo es abortada y por tanto no puede dar fallo Si la condición es cierta , se comprueba la secuencia que se cumpla
Tipos de implicación
|-> la evaluación de la secuencia empieza en el mismo ciclo que la condición que se contempla en la implicación
|=> la evaluación de la secuencia empieza en el siguiente ciclo que la condición que se contempla en la implicación .
- Equivalente a: |-> ##1