Comprobación de equivalencia formal proceso es una parte de automatización de diseño electrónico (EDA), comúnmente utilizado durante el desarrollo de las digitales circuitos integrados , para demostrar formalmente que dos representaciones de un diseño de circuito de exhibición exactamente el mismo comportamiento.
Verificación de equivalencia y niveles de abstracción
En general, existe una amplia gama de posibles definiciones de equivalencia funcional que cubren comparaciones entre diferentes niveles de abstracción y granularidad variable de detalles de tiempo.
- El enfoque más común es considerar el problema de la equivalencia de la máquina, que define dos especificaciones de diseño síncronas 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 verificación de equivalencia para comparar las funciones especificadas para la arquitectura del conjunto de instrucciones (ISA) con una implementación de nivel de transferencia de registro (RTL), lo que garantiza que cualquier programa ejecutado en ambos modelos provocará una actualización idéntica del contenido de la memoria principal. Este es un problema más general.
- Un flujo de diseño de sistema requiere la comparación entre un modelo de nivel de transacción (TLM), por ejemplo, escrito en SystemC y su correspondiente especificación RTL. Esta verificación es cada vez más interesante en un entorno de diseño de sistema en un chip (SoC).
Equivalencia de máquina síncrona
El comportamiento del nivel de transferencia de registro (RTL) de un chip digital generalmente se describe con un lenguaje de descripción de hardware , como Verilog o VHDL . Esta descripción es el modelo de referencia dorado que describe en detalle qué operaciones se ejecutarán durante qué ciclo de reloj y por qué piezas de hardware. Una vez que los diseñadores lógicos, mediante simulaciones y otros métodos de verificación, han verificado la descripción de la transferencia de registros, el diseño generalmente 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 generalmente se someterá a una serie de transformaciones, como optimización, adición de estructuras Design For Test (DFT), etc., antes de que se utilice como base para la ubicación de los elementos lógicos en un diseño físico . El software de diseño físico contemporáneo ocasionalmente también hará modificaciones significativas (como reemplazar elementos lógicos con elementos similares equivalentes que tienen una fuerza y / o área de unidad mayor o menor ) a la lista de conexiones. A lo largo de cada paso de un procedimiento muy complejo y de varios pasos, se debe mantener la funcionalidad original y el comportamiento descrito por el código original. Cuando la grabación final esté hecha 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 en el proceso que realizan cambios en la lista de redes también, en teoría, aseguran que estos cambios sean lógicamente equivalentes a una versión anterior.
En la práctica, los programas tienen errores y sería un gran riesgo asumir que todos los pasos desde RTL hasta la lista de conexiones final se han realizado sin errores. Además, en la vida real, es común que los diseñadores realicen cambios manuales en una lista de conexiones, comúnmente conocida como Órdenes de Cambio de Ingeniería , o ECO, introduciendo así un factor de error adicional importante. Por lo tanto, en lugar de asumir ciegamente que no se cometieron errores, se necesita un paso de verificación para verificar 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 dorado).
Históricamente, una forma de verificar la equivalencia era volver a simular, utilizando la lista de conexiones final, los casos de prueba que se desarrollaron para verificar la exactitud del RTL. Este proceso se denomina simulación lógica a nivel de puerta . Sin embargo, el problema con esto es que la calidad de la verificación es tan buena como la calidad de los casos de prueba. Además, las simulaciones a nivel de puerta son notoriamente lentas de ejecutar, lo cual es un problema importante ya que el tamaño de los diseños digitales continúa creciendo exponencialmente .
Una forma alternativa de resolver esto es probar 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 en el área más amplia de verificación formal .
Se puede realizar una verificación de equivalencia formal entre dos representaciones de un diseño: RTL <> netlist, netlist <> netlist o RTL <> RTL, aunque esta última es poco común en comparación con las dos primeras. Por lo general, una herramienta de verificación de equivalencia formal también indicará con gran precisión en qué punto existe una diferencia entre dos representaciones.
Métodos
Hay dos tecnologías básicas que se utilizan para el razonamiento booleano en los programas de verificación de equivalencia:
- Diagramas de decisión binarios , o BDD: una estructura de datos especializada diseñada para respaldar el razonamiento sobre funciones booleanas. Los BDD se han vuelto muy populares debido a su eficiencia y versatilidad.
- Satisfabilidad de forma normal conjuntiva: los solucionadores de SAT devuelven una asignación a las variables de una fórmula proposicional que la satisface si tal asignación existe. Casi cualquier problema de razonamiento booleano puede expresarse como un problema SAT.
Aplicaciones comerciales para la verificación de equivalencia
Los principales productos del área de comprobación de equivalencia lógica ( LEC ) de EDA son:
- FormalPro por Mentor Graphics
- Questa SLEC por Mentor Graphics
- Conformal por cadencia
- JasperGold por Cadence
- Formalidad por Synopsys
- VC Formal de Synopsys
- 360 EC de OneSpin Solutions
- ATEC por ATEC
Generalizaciones
- Verificación de equivalencia de circuitos reprogramados: a veces es útil mover la lógica de un lado de un registro a otro, y esto complica el problema de verificación.
- Verificación secuencial de equivalencia: a veces, dos máquinas son completamente diferentes en el nivel combinacional, pero deberían dar las mismas salidas si se les dan las mismas entradas. El ejemplo clásico son dos máquinas de estado idénticas con diferentes codificaciones para los estados. Dado que esto no puede reducirse a un problema de combinación, se requieren técnicas más generales.
- Equivalencia de programas de software, es decir, verificar si dos programas bien definidos que toman N entradas y producen M salidas son equivalentes: Conceptualmente, puede convertir el software en una máquina de estado (eso es lo que hace la combinación de un compilador, ya que una computadora más su memoria forman una máquina de estado muy grande). Entonces, en teoría, varias formas de verificación de propiedades pueden garantizar que produzcan el mismo resultado. Este problema es aún más difícil que la verificación de equivalencia secuencial, ya que las salidas de los dos programas pueden aparecer en momentos diferentes; pero es posible y los investigadores están trabajando en ello.
Ver también
Referencias
- Manual de automatización de diseño electrónico para circuitos integrados , por Lavagno, Martin y Scheffer, ISBN 0-8493-3096-3 Un estudio del campo. Este artículo se obtuvo, con autorización, del Volumen 2, Capítulo 4, Comprobación de equivalencia , por Fabio Somenzi y Andreas Kuehlmann.
- RE Bryant, algoritmos basados en gráficos para la manipulación de funciones booleanas , IEEE Transactions on Computers., C-35, págs. 677–691, 1986. La referencia original sobre BDD.
- Verificación secuencial de equivalencia para modelos RTL. Nikhil Sharma, Gagan Hasteer y Venkat Krishnaswamy. EE Times .