{"id":278,"date":"2020-09-24T10:27:24","date_gmt":"2020-09-24T10:27:24","guid":{"rendered":"http:\/\/dsd.webs.upv.es\/?p=278"},"modified":"2025-08-06T17:06:08","modified_gmt":"2025-08-06T17:06:08","slug":"aserciones-concurrentes","status":"publish","type":"page","link":"https:\/\/dsd.webs.upv.es\/?page_id=278","title":{"rendered":"Aserciones concurrentes"},"content":{"rendered":"\n

Nos permite hacer comprobaciones complejas a lo largo de muchos ciclos de reloj.<\/p>\n\n\n\n


Tiene la palabra clave \u00abproperty\u00bb que facilmente te permite indentificar que es una aserci\u00f3n concurrente<\/p>\n\n\n\n

Ejemplos:<\/h2>\n\n\n\n

Ejemplo 1<\/h3>\n\n\n\n

En este primer ejemplo defino \u00abad hoc\u00bb la propiedad que quiero comprobar en la aserci\u00f3n. Escribo menos pero tenemos que tener claro que esa propiedad ya no podr\u00e9 reusarla en otras aserciones.<\/p>\n\n\n

\nassert property @(negedge clk) (estado==lleno &amp;&amp; FULL_N==1\u2019b0) else $error(\u201csalida_control_erronea\u201d);\n<\/pre><\/div>\n\n\n
Ejemplo 2<\/h3>\n\n\n\n
En este segundo ejemplo hago la definici\u00f3n de la propiedad a comprobar (qu\u00e9 y cu\u00e1ndo compruebo) y luego lo utilizo en una aserci\u00f3n. Fij\u00e9monos que tanto la propiedad como la aserci\u00f3n tienen nombre. El que tenga la aserci\u00f3n un nombre me permite identificarla, inhabilitarla y reportarla claramente. Que la propiedad est\u00e9 separada y con nombre me permitir\u00eda reutilizarla f\u00e1cilmente.<\/p>\n\n\n
\nproperty  vaciado ;\/\/opcion para reuso de propiedades\n@(posedge CLOCK) not (READ==1'b1 &amp;&amp; F_EMPTY_N==1'b0 &amp;&amp; WRITE==1'b0);\nendproperty\nsobrevaciado:assert property  (vaciado) else $error("leyendo de una fifo vacia");\n<\/pre><\/div>\n\n\n
Si utilizamos como evento de muestreo (en este ejemplo \u00abposedge CLOCK\u00bb)  el mismo evento que se utiliza para los cambios de las se\u00f1ales queda la duda de si las se\u00f1ales que se muestrean (en este caso WRITE, READ y F_EMPTY ) cambian antes de despu\u00e9s de ser muestreadas. Hay que tener en cuenta que ese orden determinar\u00e1 si la aserci\u00f3n falla o no. Pero ah\u00ed nos indica la norma que el muestreo se realiza en la region \u00abpreponed\u00bb, es decir, un \u00abdelta delay\u00bb 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\u00edan posteriores<\/span>.<\/p>\n\n\n\n
\"\"<\/figure>\n\n\n\n
Si nos fijamos en el cronograma anterior, en el flanco de muestreo resaltado por el cursor, vemos claramente que READ est\u00e1 activo, WRITE esta desactivo y F_EMPTY est\u00e1 a 1’b1. Con lo cual la aserci\u00f3n no falla<\/p>\n","protected":false},"excerpt":{"rendered":"
Nos permite hacer comprobaciones complejas a lo largo de muchos ciclos de reloj. Tiene la palabra clave \u00abproperty\u00bb que facilmente te permite indentificar que es una aserci\u00f3n concurrente Ejemplos: Ejemplo 1 En este primer ejemplo defino \u00abad hoc\u00bb la propiedad que quiero comprobar en la aserci\u00f3n. Escribo menos pero tenemos que tener claro que esa propiedad ya no podr\u00e9 reusarla en otras aserciones. Ejemplo 2 En este segundo ejemplo hago la definici\u00f3n de la propiedad a comprobar (qu\u00e9 y cu\u00e1ndo compruebo) y luego lo utilizo en una aserci\u00f3n. Fij\u00e9monos que tanto la propiedad como la aserci\u00f3n tienen nombre. El que tenga la aserci\u00f3n un nombre me permite identificarla, inhabilitarla y reportarla claramente. Que la propiedad est\u00e9 separada y con nombre me permitir\u00eda reutilizarla f\u00e1cilmente. Si utilizamos como evento de muestreo (en este ejemplo \u00abposedge CLOCK\u00bb) el mismo evento que se utiliza para los cambios de las se\u00f1ales queda la duda de si las se\u00f1ales que se muestrean (en este caso WRITE, READ y F_EMPTY ) cambian antes de despu\u00e9s de ser muestreadas. Hay que tener en cuenta que ese orden determinar\u00e1 si la aserci\u00f3n falla o no. Pero ah\u00ed nos indica la norma que el muestreo se realiza en la region \u00abpreponed\u00bb, es decir, un \u00abdelta delay\u00bb 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\u00edan posteriores. Si nos fijamos en el cronograma anterior, en el flanco de muestreo resaltado por el cursor, vemos claramente que READ est\u00e1 activo, WRITE esta desactivo y F_EMPTY est\u00e1 a 1’b1. Con lo cual la aserci\u00f3n no falla<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":183,"menu_order":4,"comment_status":"open","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-278","page","type-page","status-publish","hentry"],"featured_image_src":null,"_links":{"self":[{"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/pages\/278","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=278"}],"version-history":[{"count":23,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/pages\/278\/revisions"}],"predecessor-version":[{"id":1871,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/pages\/278\/revisions\/1871"}],"up":[{"embeddable":true,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/pages\/183"}],"wp:attachment":[{"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=278"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}