Nos permite hacer comprobaciones complejas a lo largo de muchos ciclos de reloj.
Tiene la palabra clave «property» que facilmente te permite indentificar que es una aserción concurrente
Ejemplos:
Ejemplo 1
En este primer ejemplo defino «ad hoc» la propiedad que quiero comprobar en la aserción. Escribo menos pero tenemos que tener claro que esa propiedad ya no podré reusarla en otras aserciones.
|
1 |
checkFULL: assert property @(negedge clk) (estado==lleno && FULL_N==1’b0) else $error(“salida_control_erronea”); |
Ejemplo 2
En este segundo ejemplo hago la definición de la propiedad a comprobar (qué y cuándo compruebo) y luego lo utilizo en una aserción. Fijémonos que tanto la propiedad como la aserción tienen nombre. El que tenga la aserción un nombre me permite identificarla, inhabilitarla y reportarla claramente. Que la propiedad esté separada y con nombre me permitiría reutilizarla fácilmente.
|
1 2 3 4 |
property vaciado ;//opcion para reuso de propiedades @(posedge CLOCK) not (READ==1'b1 && F_EMPTY_N==1'b0 && WRITE==1'b0); endproperty sobrevaciado:assert property (vaciado) else $error("leyendo de una fifo vacia"); |
Si utilizamos como evento de muestreo (en este ejemplo «posedge CLOCK») el mismo evento que se utiliza para los cambios de las señales queda la duda de si las señales que se muestrean (en este caso WRITE, READ y F_EMPTY ) cambian antes de después de ser muestreadas. Hay que tener en cuenta que ese orden determinará si la aserción falla o no. Pero ahí nos indica la norma que el muestreo se realiza en la region «preponed», es decir, un «delta delay» antes del flanco de reloj gastado para el muestreo y por tanto se presupone que los cambios de READ, WRITE y F_EMPTY, si se produjeran en ese flanco, serían posteriores.
Si nos fijamos en el cronograma anterior, en el flanco de muestreo resaltado por el cursor, vemos claramente que READ está activo, WRITE esta desactivo y F_EMPTY está a 1’b1. Con lo cual la aserción no falla