Resumen

La verificación de la equivalencia de dos funciones booleanas, o circuitos combinacionales modelados como funciones booleanas, suele ser deseada cuando se requieren componentes de hardware fiables y correctos. Los enfoques más comunes para la verificación de equivalencia se basan en la simulación y la verificación de modelos, que están limitados debido a los populares problemas de memoria y explosión de estados. Además, dichas herramientas suelen no ser amigables para el usuario, lo que hace tedioso verificar la equivalencia de fórmulas o circuitos grandes. Una alternativa es utilizar herramientas matemáticas, llamadas demostradores de teoremas interactivos, para demostrar la equivalencia de dos circuitos; sin embargo, esto requiere esfuerzo humano y experiencia para escribir múltiples funciones de salida y llevar a cabo la prueba interactiva de su equivalencia. En este documento, (1) definimos dos lenguajes de descripción de hardware a nivel de compuerta simples, uno formal y otro informal, (2) diseñamos y desarrollamos una herramienta formal automática de verificación de equivalencia de circuitos combinacionales (

• Materias:Funciones Flujo de información Estudio de población Modelado de sistemas Modelo de campo
• Subjects:Functions Information flow Population study System modeling Field model
• Palabras claves:Verificación de equivalencia; Funciones booleanas; Circuitos combinacionales; Verificación de modelos; Demostradores de teoremas interactivos; CoCEC
• Keywords:Equivalence checking; Boolean functions; Combinational circuits; Model checking; Interactive theorem provers; CoCEC