{"id":410,"date":"2020-09-30T13:54:43","date_gmt":"2020-09-30T13:54:43","guid":{"rendered":"http:\/\/dsd.webs.upv.es\/?page_id=410"},"modified":"2025-08-06T17:18:56","modified_gmt":"2025-08-06T17:18:56","slug":"funciones-predefinidas","status":"publish","type":"page","link":"https:\/\/dsd.webs.upv.es\/?page_id=410","title":{"rendered":"Funciones predefinidas"},"content":{"rendered":"\n<ul class=\"wp-block-list\">\n<li>$rose(a): \u201ca\u201d es uno y\u00a0 fue cero en el pasado ciclo de reloj <\/li>\n\n\n\n<li>$fell(a): ): \u201ca\u201d es cero y\u00a0 fue uno en el pasado ciclo de reloj <\/li>\n\n\n\n<li>$stable(a): \u201ca\u201d mantiene el mismo valor que en el ciclo pasado <\/li>\n\n\n\n<li>$past(a): el valor que tenia \u201ca\u201d en el pasado ciclo <\/li>\n\n\n\n<li>$past(a,7): el valor que tenia \u201ca\u201d hace 7 ciclos<\/li>\n<\/ul>\n\n\n\n<p class=\"wp-block-paragraph\"><\/p>\n\n\n\n<figure class=\"wp-block-table is-style-regular\"><table><tbody><tr><td>a<\/td><td><\/td><td>0<\/td><td>0<\/td><td>1<\/td><td>0<\/td><td>1<\/td><td>1<\/td><td>1<\/td><td>1<\/td><td>0<\/td><td>1<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>1<\/td><td>1<\/td><td>0<\/td><td>0<\/td><\/tr><tr><td>$rose(a)&nbsp;<\/td><td><\/td><td>0<\/td><td>0<\/td><td>1<\/td><td>0<\/td><td>1<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>1<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>1<\/td><td>0<\/td><td>0<\/td><td>0<\/td><\/tr><tr><td>$fell(a)<\/td><td><\/td><td>?<\/td><td>0<\/td><td>0<\/td><td>1<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>1<\/td><td>0<\/td><td>1<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>1<\/td><td>0<\/td><\/tr><tr><td>$stable(a)<\/td><td><\/td><td>?<\/td><td>1<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>1<\/td><td>1<\/td><td>1<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>1<\/td><td>1<\/td><td>1<\/td><td>0<\/td><td>1<\/td><td>0<\/td><td>1<\/td><\/tr><tr><td>$past(a)<\/td><td><\/td><td>?<\/td><td>0<\/td><td>0<\/td><td>1<\/td><td>0<\/td><td>1<\/td><td>1<\/td><td>1<\/td><td>1<\/td><td>0<\/td><td>1<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>1<\/td><td>1<\/td><td>0<\/td><\/tr><tr><td>$past(a,2)<\/td><td><\/td><td>?<\/td><td>?<\/td><td>0<\/td><td>0<\/td><td>1<\/td><td>0<\/td><td>1<\/td><td>1<\/td><td>1<\/td><td>1<\/td><td>0<\/td><td>1<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>0<\/td><td>1<\/td><td>1<\/td><\/tr><\/tbody><\/table><\/figure>\n\n\n\n<h3 class=\"wp-block-heading\">Ejemplo1<\/h3>\n\n\n\n<p class=\"wp-block-paragraph\">Queremos chequear que \u201cgrant\u201d pasa a uno tres ciclos despu\u00e9s de que \u201crequest\u201d se active. Si lo hacemos mediante:<\/p>\n\n\n<div class=\"wp-block-syntaxhighlighter-code \"><pre class=\"brush: systemverilog; title: ; notranslate\" title=\"\">\nassert propperty (@(posedge clk) r |-&amp;gt; ##3 $rose(g)) \/\/ wrong\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>0<\/td><td>0<\/td><td>0<\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">1<\/span><\/td><td>1<\/td><td>1<\/td><\/tr><tr><td>r:<\/td><td><\/td><td>0<\/td><td>0<\/td><td>0<\/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-luminous-vivid-amber-color\">1<\/span><\/td><td><span class=\"has-inline-color has-luminous-vivid-amber-color\">1<\/span><\/td><td><span class=\"has-inline-color has-luminous-vivid-amber-color\">1<\/span><\/td><td><span class=\"has-inline-color has-luminous-vivid-amber-color\">1<\/span><\/td><td><span class=\"has-inline-color has-luminous-vivid-amber-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><span class=\"has-inline-color has-vivid-red-color\"><strong>5<\/strong><\/span><\/td><td><span class=\"has-inline-color has-vivid-red-color\"><strong>6<\/strong><\/span><\/td><td><span class=\"has-inline-color has-vivid-red-color\"><strong>7<\/strong><\/span><\/td><td><span class=\"has-inline-color has-vivid-red-color\"><strong>8<\/strong><\/span><\/td><td><span class=\"has-inline-color has-vivid-red-color\"><strong>9<\/strong><\/span><\/td><\/tr><\/tbody><\/table><\/figure>\n\n\n\n<ul class=\"wp-block-list\">\n<li>la aserci\u00f3n se anular\u00e1 inmediatamente en 0,1,2,3 porque la condici\u00f3n de habilitaci\u00f3n no coincide<\/li>\n\n\n\n<li>la condici\u00f3n de habilitaci\u00f3n coincide a 4, 5, 6, 7&#8230;<\/li>\n\n\n\n<li>El chequeo que se inicia en ciclo 4, es correcto en el 7<\/li>\n\n\n\n<li>Todos los dem\u00e1s intentos (5, 6, 7, &#8230;) fallan<\/li>\n<\/ul>\n\n\n\n<p class=\"wp-block-paragraph\">Por tanto para hacerla correctamente vamos a utilizar una funci\u00f3n predefinida que solo sea cierta cuando la se\u00f1al a pasado de 0 a 1<\/p>\n\n\n<div class=\"wp-block-syntaxhighlighter-code \"><pre class=\"brush: systemverilog; title: ; notranslate\" title=\"\">\nassert propperty (@(posedge clk) $rose(r) |-&amp;gt; ##3 $rose(g)) \/\/ good\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>0<\/td><td>0<\/td><td>0<\/td><td><span class=\"has-inline-color has-vivid-green-cyan-color\">1<\/span><\/td><td>1<\/td><td>1<\/td><\/tr><tr><td>r:<\/td><td><\/td><td>0<\/td><td>0<\/td><td>0<\/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-black-color\">1<\/span><\/td><td><span class=\"has-inline-color has-black-color\">1<\/span><\/td><td><span class=\"has-inline-color has-black-color\">1<\/span><\/td><td><span class=\"has-inline-color has-black-color\">1<\/span><\/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><strong><span class=\"has-inline-color has-black-color\">5<\/span><\/strong><\/td><td><strong><span class=\"has-inline-color has-black-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>la aserci\u00f3n se anular\u00e1 inmediatamente en 0,1,2,3,5,6,7 porque la condici\u00f3n de habilitaci\u00f3n no coincide<\/li>\n\n\n\n<li>la condici\u00f3n de habilitaci\u00f3n coincide en 4<\/li>\n\n\n\n<li>El chequeo que se inicia en ciclo 4, es correcto en el 7<\/li>\n\n\n\n<li>Sin fallo<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>a 0 0 1 0 1 1 1 1 0 1 0 0 0 0 1 1 0 0 $rose(a)&nbsp; 0 0 1 0 1 0 0 0 0 1 0 0 0 0 1 0 0 0 $fell(a) ? 0 0 1 0 0 0 0 1 0 1 0 0 0 0 0 1 0 $stable(a) ? 1 0 0 0 1 1 1 0 0 0 1 1 1 0 1 0 1 $past(a) ? 0 0 1 0 1 1 1 1 0 1 0 0 0 0 1 1 0 $past(a,2) ? ? 0 0 1 0 1 1 1 1 0 1 0 0 0 0 1 1 Ejemplo1 Queremos chequear que \u201cgrant\u201d pasa a uno tres ciclos despu\u00e9s de que \u201crequest\u201d se active. Si lo hacemos mediante: g: 0 0 0 0 0 0 0 1 1 1 r: 0 0 0 0 1 1 1 1 1 1 c: 0 1 2 3 4 5 6 7 8 9 Por tanto para hacerla correctamente vamos a utilizar una funci\u00f3n predefinida que solo sea cierta cuando la se\u00f1al a pasado de 0 a 1 g: 0 0 0 0 0 0 0 1 1 1 r: 0 0 0 0 1 1 1 1 1 1 c: 0 1 2 3 4 5 6 7 8 9<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":503,"menu_order":12,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_crdt_document":"","ub_ctt_via":"","footnotes":""},"class_list":["post-410","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\/410","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=410"}],"version-history":[{"count":10,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/pages\/410\/revisions"}],"predecessor-version":[{"id":1885,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/pages\/410\/revisions\/1885"}],"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=410"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}