Verificación de equivalencia formal

El proceso de verificación de equivalencia formal forma parte de la automatización del diseño electrónico (EDA, por sus siglas en inglés), comúnmente utilizada durante el desarrollo de circuitos integrados digitales , para demostrar formalmente que dos representaciones de un diseño de circuito presentan exactamente el mismo comportamiento.

En general, existe una amplia gama de posibles definiciones de equivalencia funcional que abarcan comparaciones entre diferentes niveles de abstracción y distintos grados de detalle en cuanto a la temporización.

• El enfoque más común consiste en considerar el problema de la equivalencia de máquinas, que define dos especificaciones de diseño síncronas como funcionalmente equivalentes si, reloj a reloj, producen exactamente la misma secuencia de señales de salida para cualquier secuencia válida de señales de entrada.
• Los diseñadores de microprocesadores utilizan la comprobación de equivalencia para comparar las funciones especificadas en la arquitectura del conjunto de instrucciones (ISA) con una implementación a nivel de transferencia de registros (RTL), asegurando que cualquier programa ejecutado en ambos modelos genere una actualización idéntica del contenido de la memoria principal. Este es un problema más general.
• El flujo de diseño de un sistema requiere la comparación entre un modelo a nivel de transacción (TLM), por ejemplo, escrito en SystemC , y su especificación RTL correspondiente. Esta verificación cobra cada vez más importancia en el entorno de diseño de sistemas en un chip (SoC).

El comportamiento a nivel de transferencia de registros (RTL) de un chip digital se describe generalmente con un lenguaje de descripción de hardware , como Verilog o VHDL . Esta descripción es el modelo de referencia principal que detalla qué operaciones se ejecutarán durante cada ciclo de reloj y por qué componentes de hardware. Una vez que los diseñadores lógicos han verificado la descripción de la transferencia de registros mediante simulaciones y otros métodos, el diseño se convierte en una lista de conexiones mediante una herramienta de síntesis lógica . La equivalencia no debe confundirse con la corrección funcional, que debe determinarse mediante verificación funcional .

La lista de conexiones inicial suele sufrir varias transformaciones, como optimización, adición de estructuras de diseño para pruebas (DFT), etc., antes de utilizarse como base para la colocación de los elementos lógicos en un diseño físico . El software de diseño físico actual también suele realizar modificaciones significativas (como la sustitución de elementos lógicos por elementos similares equivalentes con mayor o menor capacidad de excitación y/o área ) en la lista de conexiones. A lo largo de cada paso de un procedimiento complejo de múltiples etapas, debe mantenerse la funcionalidad original y el comportamiento descrito por el código original. Cuando se realiza la fabricación final de un chip digital, muchos programas EDA diferentes y posiblemente algunas ediciones manuales habrán alterado la lista de conexiones.

En teoría, una herramienta de síntesis lógica garantiza que la primera lista de conexiones sea lógicamente equivalente al código fuente RTL. Todos los programas posteriores que modifiquen la lista de conexiones también garantizan, en teoría, que estos cambios sean lógicamente equivalentes a una versión anterior.

En la práctica, los programas presentan errores y sería un riesgo considerable asumir que todos los pasos, desde el RTL hasta la lista de conexiones final, se han realizado sin fallos. Además, en la vida real, es común que los diseñadores realicen cambios manuales en la lista de conexiones, conocidos como Órdenes de Cambio de Ingeniería (ECO), lo que introduce un importante factor de error adicional. Por lo tanto, en lugar de asumir ciegamente que no se han cometido errores, es necesario un paso de verificación para comprobar la equivalencia lógica de la versión final de la lista de conexiones con la descripción original del diseño (modelo de referencia).

Históricamente, una forma de comprobar la equivalencia era volver a simular, utilizando la lista de conexiones final, los casos de prueba desarrollados para verificar la corrección del RTL. Este proceso se denomina simulación lógica a nivel de compuertas . Sin embargo, el problema radica en que la calidad de la verificación depende de la calidad de los casos de prueba. Además, las simulaciones a nivel de compuertas son notoriamente lentas, lo cual representa un problema importante dado el crecimiento exponencial del tamaño de los diseños digitales .

Una forma alternativa de resolver esto es demostrar formalmente que el código RTL y la lista de conexiones sintetizada a partir de él tienen exactamente el mismo comportamiento en todos los casos (relevantes). Este proceso se denomina verificación de equivalencia formal y es un problema que se estudia dentro del ámbito más amplio de la verificación formal .

Se puede realizar una comprobación de equivalencia formal entre dos representaciones cualesquiera de un diseño: RTL <> netlist, netlist <> netlist o RTL <> RTL, aunque esta última es menos frecuente que las dos primeras. Normalmente, una herramienta de comprobación de equivalencia formal también indicará con gran precisión en qué punto existe una diferencia entre las dos representaciones.

Existen dos tecnologías básicas que se utilizan para el razonamiento booleano en los programas de comprobación de equivalencia:

• Diagramas de decisión binaria (BDD): Estructura de datos especializada diseñada para facilitar el razonamiento sobre funciones booleanas. Los BDD se han vuelto muy populares debido a su eficiencia y versatilidad.
• Satisfacibilidad mediante la forma normal conjuntiva: Los solucionadores SAT devuelven una asignación a las variables de una fórmula proposicional que la satisface, si existe tal asignación. Casi cualquier problema de razonamiento booleano puede expresarse como un problema SAT.

Los principales productos en el área de verificación de equivalencia lógica ( LEC ) de EDA son:

• FormalPro de Mentor Graphics
• Questa SLEC de Mentor Graphics
• Conforme por Cadence
• Jasper de Cadence
• Formalidad por Synopsys
• VC Formal de Synopsys
• 360 EC de OneSpin Solutions
• ATEC por ATEC

• Verificación de equivalencia de circuitos con temporización modificada: En ocasiones, resulta útil trasladar la lógica de un lado de un registro a otro, lo que complica el problema de la verificación.
• Verificación de equivalencia secuencial: En ocasiones, dos máquinas son completamente diferentes a nivel combinacional, pero deberían generar las mismas salidas si reciben las mismas entradas. El ejemplo clásico son dos máquinas de estados idénticas con codificaciones diferentes para los estados. Dado que esto no se puede reducir a un problema combinacional, se requieren técnicas más generales.
• Equivalencia de programas informáticos, es decir, comprobar si dos programas bien definidos que reciben N entradas y producen M salidas son equivalentes: conceptualmente, se puede convertir el software en una máquina de estados (que es lo que hace un compilador, ya que un ordenador y su memoria forman una máquina de estados muy grande). Entonces, en teoría, diversas formas de comprobación de propiedades pueden asegurar que produzcan la misma salida. Este problema es incluso más difícil que la comprobación de equivalencia secuencial, puesto que las salidas de los dos programas pueden aparecer en momentos diferentes; pero es posible, y los investigadores están trabajando en ello.

• Métodos formales

• Manual de automatización del diseño electrónico para circuitos integrados , por Lavagno, Martin y Scheffer, ISBN 0-8493-3096-3Un análisis del campo. Este artículo se basa, con permiso, en el Volumen 2, Capítulo 4, Verificación de Equivalencia , de Fabio Somenzi y Andreas Kuehlmann.
• RE Bryant, Algoritmos basados ​​en grafos para la manipulación de funciones booleanas , IEEE Transactions on Computers., C-35, pp.  677–691, 1986. La referencia original sobre BDD.
• Verificación de equivalencia secuencial para modelos RTL. Nikhil Sharma, Gagan Hasteer y Venkat Krishnaswamy. EE Times .

• CADP: proporciona herramientas de verificación de equivalencia para diseños asíncronos.
• OneSpin 360 EC-FPGA: Corrección funcional de la síntesis de FPGA desde el código RTL hasta la lista de conexiones final.