{"id":1601,"date":"2025-03-11T13:55:52","date_gmt":"2025-03-11T13:55:52","guid":{"rendered":"https:\/\/dsd.webs.upv.es\/?p=1601"},"modified":"2025-03-11T13:58:50","modified_gmt":"2025-03-11T13:58:50","slug":"verificacion-formal-i","status":"publish","type":"post","link":"https:\/\/dsd.webs.upv.es\/?p=1601","title":{"rendered":"Verificaci\u00f3n Formal (I)"},"content":{"rendered":"\n<h2 class=\"wp-block-heading\">\u00bfQu\u00e9 es verificaci\u00f3n formal?<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">La verificaci\u00f3n formal (FV) consiste en el uso de herramientas que analizan matem\u00e1ticamente el espacio de comportamientos posibles de un dise\u00f1o, en lugar de calcular resultaos para valores particulares. Es decir, una herramienta de FV examina el conjunto completo de posibles simulaciones utilizando t\u00e9cnicas matem\u00e1ticas, en contraste con la simulaci\u00f3n, que eval\u00faa puntos individuales en ese espacio.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">Para definir qu\u00e9 estados del dise\u00f1o son legales y cu\u00e1les no, se utilizan:<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li>\u00abAssertions\u00bb: Una aserci\u00f3n es una declaraci\u00f3n sobre el dise\u00f1o, la cual se espera que siempre sea verdadera. Suelen definir el comportamiento de los outputs de DUT.<\/li>\n\n\n\n<li>\u00abAssumptions\u00bb: Son parecidas a las aserciones, pero las asunciones especifican un comportamiento del DUT. Normalmente, definen condiciones que representan alg\u00fan tipo de restricci\u00f3n. Suelen definir el comportamiento de los inputs del DUT.<\/li>\n\n\n\n<li>\u00abCover properties\u00bb: Mientras que las aserciones y las asunciones se espera que siempre sean verdaderas, los \u00abcover properties\u00bb es algo que ocasionalmente es verdadero. Suele definir alguna condici\u00f3n interesante que se quiera confirmar que se est\u00e1 testando.<\/li>\n<\/ul>\n\n\n\n<h2 class=\"wp-block-heading\">Simulaci\u00f3n VS. Verificaci\u00f3n formal<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">Este tipo de construcciones tambi\u00e9n se utilizan cuando se est\u00e1 verificando un dise\u00f1o a trav\u00e9s de simulaciones, pero la herramienta de simulaci\u00f3n y la de verificaci\u00f3n formal no tratan del mismo modo a las \u00abassertions\u00bb, \u00abassumptions\u00bb y \u00abcover properties\u00bb. A continuaci\u00f3n, vamos a ver qu\u00e9 diferencias hay con estas propiedades cuando se utilizan en un entorno de simulaci\u00f3n y en un entorno de verificaci\u00f3n formal.<\/p>\n\n\n\n<figure class=\"wp-block-table aligncenter is-style-regular\"><table class=\"has-fixed-layout\"><tbody><tr><td>                                                                       <\/td><td class=\"has-text-align-left\" data-align=\"left\"><strong>Verificaci\u00f3n formal<\/strong><\/td><td><strong>Simulaci\u00f3n tradicional<\/strong><\/td><\/tr><tr><td><strong>\u00abAssertions\u00bb<\/strong><\/td><td class=\"has-text-align-left\" data-align=\"left\">Define un estado ilegal. La herramienta prueba que el dise\u00f1o nunca puede violar la aserci\u00f3n. Si falla, ofrece un contraejemplo de c\u00f3mo ha fallado.<\/td><td>Si falla para la simulaci\u00f3n con un error.<\/td><\/tr><tr><td><strong>\u00abAssumptions\u00bb<\/strong><\/td><td class=\"has-text-align-left\" data-align=\"left\">Restringe las entradas para eliminar estados irreales.<\/td><td>Si falla para la simulaci\u00f3n con un error.<\/td><\/tr><tr><td><strong>\u00abCover properties\u00bb<\/strong><\/td><td class=\"has-text-align-left\" data-align=\"left\">Comprueba si el estado definido se puede alcanzar.<\/td><td>La informaci\u00f3n se guarda en una base de datos y al final de la simulaci\u00f3n se puede comprobar el coverage.<\/td><\/tr><\/tbody><\/table><\/figure>\n\n\n\n<p class=\"wp-block-paragraph\">Si observamos la siguiente imagen, d\u00f3nde los c\u00edrculos representan los posibles estados alcanzables en el dise\u00f1o, podemos apreciar claramente la diferencia fundamental entre <strong>simulaci\u00f3n<\/strong> y <strong>verificaci\u00f3n formal<\/strong>. <\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li>En <strong>simulaci\u00f3n<\/strong> (izquierda), el proceso parte desde un estado inicial y avanza en funci\u00f3n de los est\u00edmulos que recibe el dise\u00f1o. Solo se exponen algunos estados espec\u00edficos, dependiendo de los casos de prueba definidos. Como resultado, es dif\u00edcil garantizar que se haya cubierto todo el rango de estados posibles, ya que solo se recorren trayectorias individuales dentro del espacio de estados. <\/li>\n\n\n\n<li>En <strong>verificaci\u00f3n formal<\/strong> (derecha), en cambio, se analiza todo el espacio de estados de manera matem\u00e1tica y sistem\u00e1tica. Cada c\u00edrculo representa los estados alcanzables en distintos ciclos de reloj, y el m\u00e9todo permite explorarlos todos simult\u00e1neamente, sin necesidad de est\u00edmulos concretos<\/li>\n<\/ul>\n\n\n<div class=\"wp-block-image\">\n<figure class=\"aligncenter size-full is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"1017\" height=\"623\" src=\"https:\/\/dsd.webs.upv.es\/wp-content\/uploads\/2025\/02\/image.png\" alt=\"\" class=\"wp-image-1605\" style=\"width:644px;height:auto\" srcset=\"https:\/\/dsd.webs.upv.es\/wp-content\/uploads\/2025\/02\/image.png 1017w, https:\/\/dsd.webs.upv.es\/wp-content\/uploads\/2025\/02\/image-300x184.png 300w, https:\/\/dsd.webs.upv.es\/wp-content\/uploads\/2025\/02\/image-768x470.png 768w\" sizes=\"auto, (max-width: 1017px) 100vw, 1017px\" \/><\/figure>\n<\/div>\n\n\n<p class=\"wp-block-paragraph\">Por lo tanto, haciendo uso de la simulaci\u00f3n tradicional puede que haya alg\u00fan error en el dise\u00f1o que no se llegue a cumplir porque puede que no se ha llegado a pensar en ese estado y no se ha hecho un test directo para verificarlo. En el siguiente supuesto, podemos ver como hay bugs en cinco estados distintos, pero que mediante las simulaciones realizadas solo se llega a cubrir uno de ellos. En la verificaci\u00f3n formal, hay m\u00e1s posibilidades de que la herramienta sea capaz de detectar que estos estados contienen un error de comportamiento.<\/p>\n\n\n<div class=\"wp-block-image\">\n<figure class=\"aligncenter size-full is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"747\" height=\"622\" src=\"https:\/\/dsd.webs.upv.es\/wp-content\/uploads\/2025\/02\/image-1.png\" alt=\"\" class=\"wp-image-1608\" style=\"width:466px;height:auto\" srcset=\"https:\/\/dsd.webs.upv.es\/wp-content\/uploads\/2025\/02\/image-1.png 747w, https:\/\/dsd.webs.upv.es\/wp-content\/uploads\/2025\/02\/image-1-300x250.png 300w\" sizes=\"auto, (max-width: 747px) 100vw, 747px\" \/><\/figure>\n<\/div>","protected":false},"excerpt":{"rendered":"<p>\u00bfQu\u00e9 es verificaci\u00f3n formal? La verificaci\u00f3n formal (FV) consiste en el uso de herramientas que analizan matem\u00e1ticamente el espacio de comportamientos posibles de un dise\u00f1o, en lugar de calcular resultaos para valores particulares. Es decir, una herramienta de FV examina el conjunto completo de posibles simulaciones utilizando t\u00e9cnicas matem\u00e1ticas, en contraste con la simulaci\u00f3n, que eval\u00faa puntos individuales en ese espacio. Para definir qu\u00e9 estados del dise\u00f1o son legales y cu\u00e1les no, se utilizan: Simulaci\u00f3n VS. Verificaci\u00f3n formal Este tipo de construcciones tambi\u00e9n se utilizan cuando se est\u00e1 verificando un dise\u00f1o a trav\u00e9s de simulaciones, pero la herramienta de simulaci\u00f3n y la de verificaci\u00f3n formal no tratan del mismo modo a las \u00abassertions\u00bb, \u00abassumptions\u00bb y \u00abcover properties\u00bb. A continuaci\u00f3n, vamos a ver qu\u00e9 diferencias hay con estas propiedades cuando se utilizan en un entorno de simulaci\u00f3n y en un entorno de verificaci\u00f3n formal. Verificaci\u00f3n formal Simulaci\u00f3n tradicional \u00abAssertions\u00bb Define un estado ilegal. La herramienta prueba que el dise\u00f1o nunca puede violar la aserci\u00f3n. Si falla, ofrece un contraejemplo de c\u00f3mo ha fallado. Si falla para la simulaci\u00f3n con un error. \u00abAssumptions\u00bb Restringe las entradas para eliminar estados irreales. Si falla para la simulaci\u00f3n con un error. \u00abCover properties\u00bb Comprueba si el estado definido se puede alcanzar. La informaci\u00f3n se guarda en una base de datos y al final de la simulaci\u00f3n se puede comprobar el coverage. Si observamos la siguiente imagen, d\u00f3nde los c\u00edrculos representan los posibles estados alcanzables en el dise\u00f1o, podemos apreciar claramente la diferencia fundamental entre simulaci\u00f3n y verificaci\u00f3n formal. Por lo tanto, haciendo uso de la simulaci\u00f3n tradicional puede que haya alg\u00fan error en el dise\u00f1o que no se llegue a cumplir porque puede que no se ha llegado a pensar en ese estado y no se ha hecho un test directo para verificarlo. En el siguiente supuesto, podemos ver como hay bugs en cinco estados distintos, pero que mediante las simulaciones realizadas solo se llega a cubrir uno de ellos. En la verificaci\u00f3n formal, hay m\u00e1s posibilidades de que la herramienta sea capaz de detectar que estos estados contienen un error de comportamiento.<\/p>\n","protected":false},"author":56,"featured_media":1608,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_crdt_document":"","ub_ctt_via":"","footnotes":""},"categories":[64],"tags":[],"class_list":["post-1601","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-verificacion-formal"],"featured_image_src":"https:\/\/dsd.webs.upv.es\/wp-content\/uploads\/2025\/02\/image-1.png","author_info":{"display_name":"Mireia Segu\u00ed P\u00e9rez","author_link":"https:\/\/dsd.webs.upv.es\/?author=56"},"_links":{"self":[{"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/posts\/1601","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/users\/56"}],"replies":[{"embeddable":true,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=1601"}],"version-history":[{"count":6,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/posts\/1601\/revisions"}],"predecessor-version":[{"id":1609,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/posts\/1601\/revisions\/1609"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/media\/1608"}],"wp:attachment":[{"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=1601"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=1601"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=1601"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}