{"id":424,"date":"2020-09-30T16:03:11","date_gmt":"2020-09-30T16:03:11","guid":{"rendered":"http:\/\/dsd.webs.upv.es\/?page_id=424"},"modified":"2025-08-06T17:14:59","modified_gmt":"2025-08-06T17:14:59","slug":"secuencias-en-la-condicion-de-implicacion","status":"publish","type":"page","link":"https:\/\/dsd.webs.upv.es\/?page_id=424","title":{"rendered":"Secuencias en la condici\u00f3n de implicaci\u00f3n"},"content":{"rendered":"\n<p class=\"wp-block-paragraph\">Cada vez que la secuencia se detecte (con solapamiento) la aserci\u00f3n tras la implicaci\u00f3n ser\u00e1 evaluada<\/p>\n\n\n<div class=\"wp-block-syntaxhighlighter-code \"><pre class=\"brush: systemverilog; title: ; notranslate\" title=\"\">\nassert property (@(posedge clk) a ##1 !a ##1 a |-&amp;gt; ##1 grant ##1 !grant)\n<\/pre><\/div>\n\n\n<figure class=\"wp-block-table\"><table><tbody><tr><td>g:<\/td><td><\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">1<\/span><\/td><td class=\"has-text-align-left\" data-align=\"left\"><span class=\"has-inline-color has-vivid-green-cyan-color\">0<\/span><\/td><td><span class=\"has-inline-color has-vivid-red-color\">0<\/span><\/td><td><span class=\"has-inline-color has-vivid-red-color\">0<\/span><\/td><td>1<\/td><td>0<\/td><\/tr><tr><td>a:<\/td><td><\/td><td>0<\/td><td>1<\/td><td>0<\/td><td><span class=\"has-inline-color has-luminous-vivid-amber-color\">1<\/span><\/td><td>0<\/td><td class=\"has-text-align-left\" data-align=\"left\"><span class=\"has-inline-color has-luminous-vivid-amber-color\">1<\/span><\/td><td>0<\/td><td>0<\/td><td>0<\/td><td><span class=\"has-inline-color has-black-color\">1<\/span><\/td><\/tr><tr><td>c:<\/td><td><\/td><td>0<\/td><td>1<\/td><td>2<\/td><td>3<\/td><td>4<\/td><td class=\"has-text-align-left\" data-align=\"left\"><strong><span class=\"has-inline-color has-black-color\">5<\/span><\/strong><\/td><td><strong><span class=\"has-inline-color has-vivid-red-color\">6<\/span><\/strong><\/td><td><strong><span class=\"has-inline-color has-black-color\">7<\/span><\/strong><\/td><td><strong><span class=\"has-inline-color has-black-color\">8<\/span><\/strong><\/td><td><strong><span class=\"has-inline-color has-black-color\">9<\/span><\/strong><\/td><\/tr><\/tbody><\/table><\/figure>\n\n\n\n<ul class=\"wp-block-list\">\n<li>e.a. comenz\u00f3 en 0: abortado en 0<\/li>\n\n\n\n<li>e.a. comenz\u00f3 en 1: coincide en 5<\/li>\n\n\n\n<li>e.a. comenz\u00f3 en 2: abortado en el 2<\/li>\n\n\n\n<li>e.a. comenz\u00f3 en 3: falla en 6 (en.cond. emparejado)<\/li>\n\n\n\n<li>e.a. comenz\u00f3 en 4: abortado en 4<\/li>\n\n\n\n<li>e.a. comenz\u00f3 en 5: abortado en 7<\/li>\n<\/ul>\n\n\n\n<p class=\"wp-block-paragraph\">Si en la habilitaci\u00f3n pongo no una secuencia sino un conjunto de secuencias (mediante por ejemplo un rango de repetici\u00f3n) el funcionamiento pr\u00e1cticamente es el mismo: la aserci\u00f3n se evaluar\u00e1 cada vez que alguna de las secuencias de la habilitaci\u00f3n sea cierta. <\/p>\n\n\n\n<p class=\"wp-block-paragraph\">Por ejemplo si   utilizamos <\/p>\n\n\n<div class=\"wp-block-syntaxhighlighter-code \"><pre class=\"brush: systemverilog; title: ; notranslate\" title=\"\">\nassert property (@(posedge clk) a ##1 !a&#x5B;*0:$] ##1 a |-&gt; ##1 grant ##1 !grant)\n<\/pre><\/div>\n\n\n<p class=\"wp-block-paragraph\">vemos que en la condici\u00f3n de habilitaci\u00f3n hay en realidad infinitas secuencias descritas. Por lo tanto cada vez que alguna de ellas sea cierta, la comprobaci\u00f3n de la aserci\u00f3n deber\u00e1 ser realizada , en este caso la detecci\u00f3n de un paso de \u00abgrand\u00bb  de 1 a 0 un ciclo despu\u00e9s de detectar la secuencia de habilitaci\u00f3n<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Cada vez que la secuencia se detecte (con solapamiento) la aserci\u00f3n tras la implicaci\u00f3n ser\u00e1 evaluada g: 0 0 0 0 1 0 0 0 1 0 a: 0 1 0 1 0 1 0 0 0 1 c: 0 1 2 3 4 5 6 7 8 9 Si en la habilitaci\u00f3n pongo no una secuencia sino un conjunto de secuencias (mediante por ejemplo un rango de repetici\u00f3n) el funcionamiento pr\u00e1cticamente es el mismo: la aserci\u00f3n se evaluar\u00e1 cada vez que alguna de las secuencias de la habilitaci\u00f3n sea cierta. Por ejemplo si utilizamos vemos que en la condici\u00f3n de habilitaci\u00f3n hay en realidad infinitas secuencias descritas. Por lo tanto cada vez que alguna de ellas sea cierta, la comprobaci\u00f3n de la aserci\u00f3n deber\u00e1 ser realizada , en este caso la detecci\u00f3n de un paso de \u00abgrand\u00bb de 1 a 0 un ciclo despu\u00e9s de detectar la secuencia de habilitaci\u00f3n<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":183,"menu_order":13,"comment_status":"closed","ping_status":"closed","template":"","meta":{"ub_ctt_via":"","footnotes":""},"class_list":["post-424","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\/424","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=424"}],"version-history":[{"count":6,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/pages\/424\/revisions"}],"predecessor-version":[{"id":1880,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/pages\/424\/revisions\/1880"}],"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=424"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}