{"id":1456,"date":"2023-02-21T12:14:19","date_gmt":"2023-02-21T12:14:19","guid":{"rendered":"https:\/\/dsd.webs.upv.es\/?page_id=1456"},"modified":"2025-08-06T17:34:04","modified_gmt":"2025-08-06T17:34:04","slug":"secuencias","status":"publish","type":"page","link":"https:\/\/dsd.webs.upv.es\/?page_id=1456","title":{"rendered":"Secuencias"},"content":{"rendered":"\n

A veces es eficiente definir la secuencia separadamente<\/p>\n\n\n\n

<\/p>\n\n\n\n

sequence<\/strong> <\/mark>s1<\/strong>;<\/p>\n\n\n\n

  ##1 b [*0:$] ##1 b;<\/p>\n\n\n\n

endsequence<\/strong><\/mark><\/p>\n\n\n\n

sequence <\/mark>s2<\/strong>;<\/p>\n\n\n\n

     $fell(b) ##1 !b ##1 b;<\/p>\n\n\n\n

endsequence<\/mark><\/strong><\/p>\n\n\n\n

De esta forma podemos definir f\u00e1cilmente las aserciones utilizando las secuencias que han sido previamente definidas<\/p>\n\n\n\n

Ejemplos :<\/p>\n\n\n\n

assert propperty<\/mark> (@(negedge clk) s1<\/mark><\/strong> |-> ##2 s2<\/mark><\/strong>)<\/p>\n\n\n\n

assert propperty <\/mark>(@(negedge clk) a==0 |=> s1<\/mark><\/strong> or s2<\/mark><\/strong>)<\/p>\n\n\n\n

assert propperty<\/mark> (@(negedge clk) s1<\/mark><\/strong> ##1 s2<\/mark><\/strong> |-> a==5)<\/p>\n\n\n\n

assert propperty<\/mark> (@(negedge clk) s1<\/mark><\/strong> and s2<\/mark><\/strong> |=> b==1 ##1 b==0)<\/p>\n\n\n\n

<\/p>\n\n\n\n

Utilizacion de variables internas<\/h3>\n\n\n\n

La otra gran ventaja de las secuencias es que pueden tener variables locales<\/p>\n\n\n\n

sequence<\/strong> <\/mark>s1;<\/p>\n\n\n\n

  int cnt;<\/p>\n\n\n\n

  (a==1, cnt=b) ##1 !a [*0:$] ##1 (a && b==cnt+1);<\/p>\n\n\n\n

endsequence<\/mark><\/strong><\/p>\n\n\n\n

la secuencia corresponde : si \u201ca\u201d es 1, guarde el valor de b en cnt, luego espere hasta que \u201ca\u201d suba de nuevo y compruebe que \u201cb\u201d es igual a cnt+1;<\/p>\n\n\n\n

Reglas<\/h4>\n\n\n\n

Siempre necesitamos una condici\u00f3n para hacer una asignaci\u00f3n a una variable local, en caso de que no haya condici\u00f3n podemos utilizar condici\u00f3n trivial \u00ab1\u00bb
<\/p>\n\n\n\n

Puede hacerse varias asignaciones:<\/p>\n\n\n\n

    (1, cnt=b, cnt2=c)<\/p>\n\n\n\n

Incluso puede tener llamadas de funci\u00f3n y $display \u2013 \u00fatil para la depuraci\u00f3n <\/p>\n\n\n\n

##1 (a==1, $display(cnt))<\/p>\n\n\n\n

Ejemplo<\/h4>\n\n\n\n

Supongamos que queremos definir unas aserciones para un contador up-down<\/p>\n\n\n

\nmodule Contador  #(parameter n = 4)\n  (input clk, incr,areset_n, sreset_n,load,up_down ,\n   input [n-1:0] dato, \n   output reg [n-1:0] salida,\n   output TC );\n\/\/localparam width_counter=4;\n  wire  [n-1:0] fin_cuenta= up_down?2**n-1:0;\n  assign TC=(salida==fin_cuenta)?1'b1:1'b0;\nalways @(posedge clk or negedge areset_n)\n  if (!areset_n)\n        salida<=0;\n  else\n         if (sreset_n==1'b0)\n    \t\tsalida<=0;\n  \t else\n          if(load)\n            salida<=dato;\n           else\n             if (incr)\n               if(up_down)\n\t\t          salida<=salida+1;\n  \t        else\n                  salida<=salida-1;\nsequence s1;\n  logic [n-1:0]  aux;\n    (1, aux=salida)  ##1 (salida==aux+1'b1);\nendsequence  \nsequence s2;\n  logic [n-1:0]  aux;\n    (1, aux=salida)  ##1 (salida==aux-1'b1);\nendsequence    \nprueba1:  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");\nprueba2:  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");  \nprueba3:  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");\nprueba4:  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");  \n  \nendmodule\n<\/pre><\/div>\n\n\n
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\u00f3n concurrente prueba1 y en la aserci\u00f3n concurrente prueba2 . Conviene sin embargo detenerse en algunos detalles que vamos a enumerar:<\/p>\n\n\n\n
<\/p>\n\n\n\n