{"id":55901,"date":"2006-05-12T00:00:00","date_gmt":"2006-05-12T00:00:00","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/aportaciones-a-la-verificacion-formal-de-circuitos-secuenciales\/"},"modified":"2006-05-12T00:00:00","modified_gmt":"2006-05-12T00:00:00","slug":"aportaciones-a-la-verificacion-formal-de-circuitos-secuenciales","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/tecnologia-electronica\/aportaciones-a-la-verificacion-formal-de-circuitos-secuenciales\/","title":{"rendered":"Aportaciones a la verificaci\u00f3n formal de circuitos secuenciales"},"content":{"rendered":"<h2>Tesis doctoral de <strong> H\u00e9ctor Navarro Botello <\/strong><\/h2>\n<p>A pesar de que la industria se centra \u00fanicamente en general herramientas para facilitar la verificaci\u00f3n funcional, lo cierto es que hoy en d\u00eda las t\u00e9cnicas de verificaci\u00f3n formal est\u00e1n despertando un creciente inter\u00e9s en la comunidad cient\u00edfica. la presente tesis se centra en la generaci\u00f3n de vectores de m\u00e1xima cobertura para la validaci\u00f3n funcional de sistemas secuenciales descritos a nivel rtl. Estos vectores podr\u00e1n ser empleados tanto en el proceso de verificaci\u00f3n como en el test de los microcircuitos fabricados. para generar vectores de calidad, es necesario resolver los siguientes problemas:     1,- modelar el comportamiento del sistema combinacional matem\u00e1ticamente. Se presenta en primer lugar, un estudio te\u00f3rico delos modelso b\u00e1sicos empleados en la caracterizaci\u00f3n lineal de puertas l\u00f3gicas. Con un inter\u00e9s menos te\u00f3rico y m\u00e1s pragm\u00e1tico, se presenta un novedoso modelo de alto nivel para el multiplexor. Este modelo ofrece una complejidad menor que el de referencia y resulta, considerablemente, m\u00e1s eficiente.     2,- describir el problema de justificaci\u00f3n de estados que plantea el circuito secuencial y definir los par\u00e1metros de calidad con el fin de optimizar la bondad de los vectores a obtener. se presenta una metodolog\u00eda que permite obtener en un s\u00f3lo paso, el conjunto de vectores de entrada que permite que el sistema secuencial ejecute la secuencia de estados \u00f3ptima; siendo esta \u00faltima aquella que satisface las condiciones impuestas en el menor n\u00famero de ciclos de reloj. la metodolog\u00eda de paso \u00fanico permite evitar el proceso iterativo que conlleva la forma tradicional de resolver el problema de justificaci\u00f3n de estados.     3,- resolver el problema final que se deriva de la justificaci\u00f3n de estados, y que consta de un problema de optimizaci\u00f3n condicionado a un problema de satisfabildiad. con el fin de reducir sustancialmente la complejidad de este problema se presentan dos aportaicones independientes que eliminan<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Aportaciones a la verificaci\u00f3n formal de circuitos secuenciales<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Aportaciones a la verificaci\u00f3n formal de circuitos secuenciales <\/li>\n<li><strong>Autor:<\/strong>\u00a0 H\u00e9ctor Navarro Botello <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Palmas de gran canaria<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 05\/12\/2006<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<h3>Direcci\u00f3n y tribunal<\/h3>\n<ul>\n<li><strong>Director de la tesis<\/strong>\n<ul>\n<li>Juan  Antonio Montiel Nelson<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: Antonio N\u00fa\u00f1ez ord\u00f3\u00f1ez <\/li>\n<li> Bicho dos santos marcelino (vocal)<\/li>\n<li>eugenio Villar bonet (vocal)<\/li>\n<li>eduardo Torre arnanz (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de H\u00e9ctor Navarro Botello A pesar de que la industria se centra \u00fanicamente en general herramientas para facilitar [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"site-sidebar-layout":"default","site-content-layout":"","ast-site-content-layout":"","site-content-style":"default","site-sidebar-style":"default","ast-global-header-display":"","ast-banner-title-visibility":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","astra-migrate-meta-layouts":"default","ast-page-background-enabled":"default","ast-page-background-meta":{"desktop":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"ast-content-background-meta":{"desktop":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"footnotes":""},"categories":[16629,3706],"tags":[15947,123499,123500,43237,123498,16758],"class_list":["post-55901","post","type-post","status-publish","format-standard","hentry","category-palmas-de-gran-canaria","category-tecnologia-electronica","tag-antonio-nunez-ordonez","tag-bicho-dos-santos-marcelino","tag-eduardo-torre-arnanz","tag-eugenio-villar-bonet","tag-hector-navarro-botello","tag-juan-antonio-montiel-nelson"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/55901","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/comments?post=55901"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/55901\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=55901"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=55901"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=55901"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}