A veces es eficiente definir la secuencia separadamente
sequence s1;
##1 b [*0:$] ##1 b;
endsequence
sequence s2;
$fell(b) ##1 !b ##1 b;
endsequence
De esta forma podemos definir fácilmente las aserciones utilizando las secuencias que han sido previamente definidas
Ejemplos :
assert propperty (@(negedge clk) s1 |-> ##2 s2)
assert propperty (@(negedge clk) a==0 |=> s1 or s2)
assert propperty (@(negedge clk) s1 ##1 s2 |-> a==5)
assert propperty (@(negedge clk) s1 and s2 |=> b==1 ##1 b==0)
Utilizacion de variables internas
La otra gran ventaja de las secuencias es que pueden tener variables locales
sequence s1;
int cnt;
(a==1, cnt=b) ##1 !a [*0:$] ##1 (a && b==cnt+1);
endsequence
la secuencia corresponde : si “a” es 1, guarde el valor de b en cnt, luego espere hasta que “a” suba de nuevo y compruebe que “b” es igual a cnt+1;
Reglas
Siempre necesitamos una condición para hacer una asignación a una variable local, en caso de que no haya condición podemos utilizar condición trivial “1”
Puede hacerse varias asignaciones:
(1, cnt=b, cnt2=c)
Incluso puede tener llamadas de función y $display – útil para la depuración
##1 (a==1, $display(cnt))
Ejemplo
Supongamos que queremos definir unas aserciones para un contador up-down
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 |
module Contador #(parameter n = 4) (input clk, incr,areset_n, sreset_n,load,up_down , input [n-1:0] dato, output reg [n-1:0] salida, output TC ); //localparam width_counter=4; wire [n-1:0] fin_cuenta= up_down?2**n-1:0; assign TC=(salida==fin_cuenta)?1'b1:1'b0; always @(posedge clk or negedge areset_n) if (!areset_n) salida<=0; else if (sreset_n==1'b0) salida<=0; else if(load) salida<=dato; else if (incr) if(up_down) salida<=salida+1; else salida<=salida-1; sequence s1; logic [n-1:0] aux; (1, aux=salida) ##1 (salida==aux+1'b1); endsequence sequence s2; logic [n-1:0] aux; (1, aux=salida) ##1 (salida==aux-1'b1); endsequence prueba1: assert property (@(posedge clk) disable iff (areset_n===1'bx ||areset_n==1'b0 ) load==1'b0&&incr==1'b1&&up_down==1'b1&&sreset_n==1'b1|->s1) else $error("el contador va mal"); prueba2: assert property (@(posedge clk) disable iff (areset_n!=1'b1) load==1'b0&&incr==1'b1&&up_down==1'b1&&sreset_n==1'b1|=>salida==$past(salida)+1'b1) else $error("el contador va mal2"); prueba3: assert property (@(posedge clk) disable iff (areset_n!=1'b1) load==1'b0&&incr==1'b1&&up_down==1'b0&&sreset_n==1'b1|->s2) else $error("el contador va mal3"); prueba4: assert property (@(posedge clk) disable iff (areset_n!=1'b1) load==1'b0&&incr==1'b1&&up_down==1'b0&&sreset_n==1'b1|=>salida==$past(salida)-1'b1) else $error("el contador va mal4"); endmodule |
En este ejemplo observamos dos secuencias definidas, una de las cuales utilizaremos para comprobar los incrementos (s1) y la otra para comprobar los decrementos (s2). Posteriormente esas secuencias son utilizadas en la aserción concurrente prueba1 y en la aserción concurrente prueba2 . Conviene sin embargo detenerse en algunos detalles que vamos a enumerar:
- Las secuencias están llamadas después de una implicación que determine cuando esas secuencias deben de ser ciertas.
- La aserciónes que las utilizan deben de ser convenientemente inhabilitadas cuando el reset es desconocido o es activo
- La sintaxis de expresiones que implican esas variables locales debe de ser muy estricta. Por ejemplo colocar (salida==aux+1) en lugar de (salida==aux+1’b1) hace que la aserción falle porque al incrementar aux con un literal de tipo integer, automáticamente la parte derecha de la expresión de comparación se hace de 32 bits, con lo cual nunca será igual a la parte izquierda
- Se han colocado comprobaciones equivalentes mediante el uso de la función predefinida $past en las aserciones denominadas prueba2 (hace la misma función que prueba1) y prueba4 (hace la misma función que prueba3)
Laboratorio Virtual
