{"id":430,"date":"2020-09-30T16:43:20","date_gmt":"2020-09-30T16:43:20","guid":{"rendered":"http:\/\/dsd.webs.upv.es\/?page_id=430"},"modified":"2025-08-06T17:21:35","modified_gmt":"2025-08-06T17:21:35","slug":"aserciones-de-secuencias-combinadas","status":"publish","type":"page","link":"https:\/\/dsd.webs.upv.es\/?page_id=430","title":{"rendered":"Aserciones de secuencias combinadas"},"content":{"rendered":"\n<p class=\"wp-block-paragraph\">Existen varios operadores que nos permiten combinar varias comprobaciones de secuencias . Los efectos son claros si estas secuencias forman parte de la aserci\u00f3n pero no de la habilitaci\u00f3n (solo la <strong>or<\/strong> es plausible en lacondici\u00f3n de la implicaci\u00f3n)  y vamos a describirlos<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li><mark style=\"background-color:rgba(0, 0, 0, 0)\" class=\"has-inline-color has-vivid-cyan-blue-color\">operador or<\/mark>: si nuestra aserci\u00f3n combina dos secuencias con una <strong>or<\/strong>, basta con que una de ellas sea cierta (ocurra) para que se considere que la aserci\u00f3n no falla<\/li>\n\n\n\n<li><mark style=\"background-color:rgba(0, 0, 0, 0)\" class=\"has-inline-color has-vivid-cyan-blue-color\">operador and<\/mark>: si nuestra aserci\u00f3n combina dos secuencias con una <strong>and<\/strong>, las dos secuencias deben ser  ciertas (ocurrir) para que se considere que la aserci\u00f3n no falla<\/li>\n\n\n\n<li><mark style=\"background-color:rgba(0, 0, 0, 0)\" class=\"has-inline-color has-vivid-cyan-blue-color\">operador intersect<\/mark>: si nuestra aserci\u00f3n combina dos secuencias con un <strong>intersect<\/strong>, las dos secuencias deben ser ciertas (ocurrir) para que se considere que la aserci\u00f3n no falla y adem\u00e1s deben finalizar al \u00fan\u00edsono<\/li>\n\n\n\n<li><mark style=\"background-color:rgba(0, 0, 0, 0)\" class=\"has-inline-color has-vivid-cyan-blue-color\">operador within<\/mark>: si nuestra aserci\u00f3n combina dos secuencias con <strong>within<\/strong>, las dos secuencias deben ser ciertas (ocurrir) y adem\u00e1s una de ellas debe contener completamente a la otra<\/li>\n<\/ul>\n\n\n\n<h3 class=\"wp-block-heading\" id=\"ejemplos\">Ejemplos<\/h3>\n\n\n\n<h4 class=\"wp-block-heading\" id=\"ejemplo1\">Ejemplo1<\/h4>\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 g ##1 !g) or (##1 !g&#x5B;*2])\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-pale-cyan-blue-color\">1<\/span><\/td><td><span class=\"has-inline-color has-pale-cyan-blue-color\">0<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">0<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-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><span class=\"has-inline-color has-luminous-vivid-amber-color\">1<\/span><\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>1<\/td><\/tr><tr><td>c:<\/td><td><\/td><td>0<\/td><td>1<\/td><td>2<\/td><td>3<\/td><td>4<\/td><td><strong>5<\/strong><\/td><td><strong>6<\/strong><\/td><td><strong>7<\/strong><\/td><td><strong>8<\/strong><\/td><td><strong>9<\/strong><\/td><\/tr><\/tbody><\/table><\/figure>\n\n\n\n<p class=\"wp-block-paragraph\">Puede observarse que la aserci\u00f3n no falla nunca porque las dos veces que la habilitaci\u00f3n es cierta (ciclos 3 y 5) o bien ha ocurrido una secuencia o la otra de las combinadas mediante la expresi\u00f3n <strong>or<\/strong><\/p>\n\n\n\n<h4 class=\"wp-block-heading\" id=\"ejemplo2\">Ejemplo2<\/h4>\n\n\n<div class=\"wp-block-syntaxhighlighter-code \"><pre class=\"brush: systemverilog; title: ; notranslate\" title=\"\">\nassert property (@(posedge clk) rose(r) |=&amp;gt; (!g&#x5B;*2:$] ##1 g ) and (r &#x5B;*2:$] ##1 !r)\n<\/pre><\/div>\n\n\n<div class=\"wp-block-group\"><div class=\"wp-block-group__inner-container is-layout-flow wp-block-group-is-layout-flow\">\n<figure class=\"wp-block-table\"><table><tbody><tr><td>g:<\/td><td><\/td><td>0<\/td><td>0<\/td><td><span class=\"has-inline-color has-pale-cyan-blue-color\">0<\/span><\/td><td><span class=\"has-inline-color has-pale-cyan-blue-color\">0<\/span><\/td><td><span class=\"has-inline-color has-pale-cyan-blue-color\">1<\/span><\/td><td>1<\/td><td>1<\/td><td>1<\/td><td>1<\/td><td>1<\/td><\/tr><tr><td>r:<\/td><td><\/td><td>0<\/td><td><span class=\"has-inline-color has-luminous-vivid-amber-color\">1<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">1<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">1<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">1<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">1<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">0<\/span><\/td><td>0<\/td><td>0<\/td><td>0<\/td><\/tr><tr><td>c:<\/td><td><\/td><td>0<\/td><td>1<\/td><td>2<\/td><td>3<\/td><td>4<\/td><td><strong>5<\/strong><\/td><td><strong>6<\/strong><\/td><td><strong>7<\/strong><\/td><td><strong>8<\/strong><\/td><td><strong>9<\/strong><\/td><\/tr><\/tbody><\/table><\/figure>\n<\/div><\/div>\n\n\n\n<p class=\"wp-block-paragraph\">Podemos observar que esta aserci\u00f3n tampoco falla porque cuando fue habilitada (ciclo 1) , ambas secuencias que hab\u00eda que comprobar en la aserci\u00f3n ocurrieron. Cierto es que dichas secuencias terminaron de ser ciertas en momentos diferentes; pero eso no es chequeado por la expresi\u00f3n <strong>and<\/strong><\/p>\n\n\n\n<h4 class=\"wp-block-heading\" id=\"ejemplo-3\">Ejemplo 3<\/h4>\n\n\n<div class=\"wp-block-syntaxhighlighter-code \"><pre class=\"brush: systemverilog; title: ; notranslate\" title=\"\">\nassert property (@(posedge clk) rose(r) |=&amp;gt; (!g&#x5B;*2:$] ##1 g ) intersect (r &#x5B;*2:$] ##1 !r)\n<\/pre><\/div>\n\n\n<div class=\"wp-block-group\"><div class=\"wp-block-group__inner-container is-layout-flow wp-block-group-is-layout-flow\">\n<figure class=\"wp-block-table\"><table><tbody><tr><td>g:<\/td><td><\/td><td>0<\/td><td>0<\/td><td><span class=\"has-inline-color has-pale-cyan-blue-color\">0<\/span><\/td><td><span class=\"has-inline-color has-pale-cyan-blue-color\">0<\/span><\/td><td><span class=\"has-inline-color has-pale-cyan-blue-color\">1<\/span><\/td><td>1<\/td><td>1<\/td><td>1<\/td><td>1<\/td><td>1<\/td><\/tr><tr><td>r:<\/td><td><\/td><td>0<\/td><td><span class=\"has-inline-color has-luminous-vivid-amber-color\">1<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">1<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">1<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">1<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">1<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">0<\/span><\/td><td>0<\/td><td>0<\/td><td>0<\/td><\/tr><tr><td>c:<\/td><td><\/td><td>0<\/td><td>1<\/td><td>2<\/td><td>3<\/td><td><strong><span class=\"has-inline-color has-vivid-red-color\">4<\/span><\/strong><\/td><td><strong>5<\/strong><\/td><td><strong>6<\/strong><\/td><td><strong>7<\/strong><\/td><td><strong>8<\/strong><\/td><td><strong>9<\/strong><\/td><\/tr><\/tbody><\/table><\/figure>\n\n\n\n<p class=\"wp-block-paragraph\">Podemos observar que esta aserci\u00f3n si que falla porque cuando fue habilitada (ciclo 1) , ambas secuencias que hab\u00eda que comprobar en la aserci\u00f3n ocurrieron; <span class=\"has-inline-color has-vivid-red-color\">pero<\/span> terminaron de ser ciertas en momentos diferentes. En el ciclo 4 ya observa la aserci\u00f3n que las dos secuencias no han sido ciertas al mismo tiempo y da fallo<\/p>\n\n\n\n<h4 class=\"wp-block-heading\" id=\"ejemplo-4\">Ejemplo 4<\/h4>\n\n\n\n<div class=\"wp-block-urvanov-syntax-highlighter-code-block\"><pre class=\"lang:verilog decode:true \">assert property (@(posedge clk) rose(r) |=&gt; (!g[*2:$] ##1 g ) within (r [*2:$] ##1 !r)<\/pre><\/div>\n\n\n\n<div class=\"wp-block-group\"><div class=\"wp-block-group__inner-container is-layout-flow wp-block-group-is-layout-flow\">\n<figure class=\"wp-block-table\"><table><tbody><tr><td>g:<\/td><td><\/td><td>0<\/td><td>0<\/td><td><span class=\"has-inline-color has-pale-cyan-blue-color\">0<\/span><\/td><td><span class=\"has-inline-color has-pale-cyan-blue-color\">0<\/span><\/td><td><span class=\"has-inline-color has-pale-cyan-blue-color\">1<\/span><\/td><td>1<\/td><td>1<\/td><td>1<\/td><td>1<\/td><td>1<\/td><\/tr><tr><td>r:<\/td><td><\/td><td>0<\/td><td><span class=\"has-inline-color has-luminous-vivid-amber-color\">1<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">1<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">1<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">1<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">1<\/span><\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">0<\/span><\/td><td>0<\/td><td>0<\/td><td>0<\/td><\/tr><tr><td>c:<\/td><td><\/td><td>0<\/td><td>1<\/td><td>2<\/td><td>3<\/td><td><strong><span class=\"has-inline-color has-black-color\">4<\/span><\/strong><\/td><td><strong>5<\/strong><\/td><td><strong>6<\/strong><\/td><td><strong>7<\/strong><\/td><td><strong>8<\/strong><\/td><td><strong>9<\/strong><\/td><\/tr><\/tbody><\/table><\/figure>\n\n\n\n<p class=\"wp-block-paragraph\">Podemos observar que esta aserci\u00f3n no falla porque cuando fue habilitada (ciclo 1) , ambas secuencias que hab\u00eda que comprobar en la aserci\u00f3n ocurrieron;  y la secuencia segunda (en verde) contiene completamente a la primera (en azul)<\/p>\n<\/div><\/div>\n<\/div><\/div>\n\n\n\n<p class=\"wp-block-paragraph\"><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Existen varios operadores que nos permiten combinar varias comprobaciones de secuencias . Los efectos son claros si estas secuencias forman parte de la aserci\u00f3n pero no de la habilitaci\u00f3n (solo la or es plausible en lacondici\u00f3n de la implicaci\u00f3n) y vamos a describirlos Ejemplos Ejemplo1 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 Puede observarse que la aserci\u00f3n no falla nunca porque las dos veces que la habilitaci\u00f3n es cierta (ciclos 3 y 5) o bien ha ocurrido una secuencia o la otra de las combinadas mediante la expresi\u00f3n or Ejemplo2 g: 0 0 0 0 1 1 1 1 1 1 r: 0 1 1 1 1 1 0 0 0 0 c: 0 1 2 3 4 5 6 7 8 9 Podemos observar que esta aserci\u00f3n tampoco falla porque cuando fue habilitada (ciclo 1) , ambas secuencias que hab\u00eda que comprobar en la aserci\u00f3n ocurrieron. Cierto es que dichas secuencias terminaron de ser ciertas en momentos diferentes; pero eso no es chequeado por la expresi\u00f3n and Ejemplo 3 g: 0 0 0 0 1 1 1 1 1 1 r: 0 1 1 1 1 1 0 0 0 0 c: 0 1 2 3 4 5 6 7 8 9 Podemos observar que esta aserci\u00f3n si que falla porque cuando fue habilitada (ciclo 1) , ambas secuencias que hab\u00eda que comprobar en la aserci\u00f3n ocurrieron; pero terminaron de ser ciertas en momentos diferentes. En el ciclo 4 ya observa la aserci\u00f3n que las dos secuencias no han sido ciertas al mismo tiempo y da fallo Ejemplo 4 g: 0 0 0 0 1 1 1 1 1 1 r: 0 1 1 1 1 1 0 0 0 0 c: 0 1 2 3 4 5 6 7 8 9 Podemos observar que esta aserci\u00f3n no falla porque cuando fue habilitada (ciclo 1) , ambas secuencias que hab\u00eda que comprobar en la aserci\u00f3n ocurrieron; y la secuencia segunda (en verde) contiene completamente a la primera (en azul)<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":503,"menu_order":14,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_crdt_document":"","ub_ctt_via":"","footnotes":""},"class_list":["post-430","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\/430","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=430"}],"version-history":[{"count":15,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/pages\/430\/revisions"}],"predecessor-version":[{"id":1888,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/pages\/430\/revisions\/1888"}],"up":[{"embeddable":true,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/pages\/503"}],"wp:attachment":[{"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=430"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}