Verificación funcional - Functional verification

En la automatización del diseño electrónico , la verificación funcional es la tarea de verificar que el diseño lógico se ajuste a la especificación. En términos cotidianos, la verificación funcional intenta responder a la pregunta "¿Este diseño propuesto hace lo que se pretende?" Esta es una tarea compleja y requiere la mayor parte del tiempo y esfuerzo en la mayoría de los grandes proyectos de diseño de sistemas electrónicos. La verificación funcional es parte de una verificación de diseño más integral , que, además de la verificación funcional, considera aspectos no funcionales como el tiempo, el diseño y la potencia.

La verificación funcional es muy difícil debido al gran volumen de posibles casos de prueba que existen incluso en un diseño simple. Con frecuencia, hay más de 10 ^ 80 posibles pruebas para verificar exhaustivamente un diseño, un número que es imposible de lograr en toda la vida. Este esfuerzo es equivalente a la verificación del programa , y es NP-difícil o incluso peor, y no se ha encontrado una solución que funcione bien en todos los casos. Sin embargo, puede ser atacado por muchos métodos. Ninguno de ellos es perfecto, pero todos pueden ser útiles en determinadas circunstancias:

  • La simulación lógica simula la lógica antes de que se construya.
  • La aceleración de simulación aplica hardware de propósito especial al problema de simulación lógica.
  • La emulación crea una versión del sistema utilizando lógica programable. Esto es caro y aún mucho más lento que el hardware real, pero órdenes de magnitud más rápido que la simulación. Se puede utilizar, por ejemplo, para iniciar el sistema operativo en un procesador.
  • La verificación formal intenta demostrar matemáticamente que se cumplen ciertos requisitos (también expresados ​​formalmente), o que no pueden ocurrir ciertos comportamientos no deseados (como un punto muerto).
  • La verificación inteligente utiliza la automatización para adaptar el banco de pruebas a los cambios en el código de nivel de transferencia del registro .
  • Las versiones de lint específicas de HDL y otras heurísticas se utilizan para encontrar problemas comunes.

La verificación basada en simulación (también llamada ' verificación dinámica ') se usa ampliamente para "simular" el diseño, ya que este método se escala muy fácilmente. Se proporciona un estímulo para ejercitar cada línea en el código HDL. Se construye un banco de pruebas para verificar funcionalmente el diseño al proporcionar escenarios significativos para verificar que, dada cierta entrada, el diseño se desempeña según las especificaciones.

Un entorno de simulación suele estar compuesto por varios tipos de componentes:

  • El generador genera vectores de entrada que se utilizan para buscar anomalías que existen entre la intención (especificaciones) y la implementación (Código HDL). Este tipo de generador utiliza un tipo NP-complete de SAT Solver que puede ser computacionalmente costoso. Otros tipos de generadores incluyen vectores creados manualmente, generadores patentados de generadores basados ​​en gráficos (GBM). Los generadores modernos crean estímulos aleatorios dirigidos y aleatorios que se controlan estadísticamente para verificar partes aleatorias del diseño. La aleatoriedad es importante para lograr una alta distribución en el enorme espacio de los estímulos de entrada disponibles. Con este fin, los usuarios de estos generadores subespecifican intencionalmente los requisitos para las pruebas generadas. El papel del generador es llenar este vacío al azar. Este mecanismo permite al generador crear entradas que revelan errores que el usuario no busca directamente. Los generadores también sesgan los estímulos hacia casos de esquina de diseño para enfatizar aún más la lógica. El sesgo y la aleatoriedad sirven a diferentes objetivos y existen compensaciones entre ellos, por lo que los diferentes generadores tienen una combinación diferente de estas características. Dado que la entrada para el diseño debe ser válida (legal) y se deben mantener muchos objetivos (como el sesgo), muchos generadores utilizan la técnica del problema de satisfacción de restricciones (CSP) para resolver los complejos requisitos de prueba. Se modela la legalidad de las entradas de diseño y el arsenal de sesgos. Los generadores basados ​​en modelos utilizan este modelo para producir los estímulos correctos para el diseño objetivo.
  • Los controladores traducen los estímulos producidos por el generador en las entradas reales para el diseño bajo verificación. Los generadores crean entradas con un alto nivel de abstracción, es decir, como transacciones o lenguaje ensamblador. Los controladores convierten esta entrada en entradas de diseño reales como se define en la especificación de la interfaz de diseño.
  • El simulador produce las salidas del diseño, basándose en el estado actual del diseño (el estado de los flip-flops) y las entradas inyectadas. El simulador tiene una descripción de la lista de redes de diseño. Esta descripción se crea sintetizando el HDL en una lista de red de nivel de puerta bajo.
  • El monitor convierte el estado del diseño y sus resultados a un nivel de abstracción de transacciones para que pueda almacenarse en una base de datos de "tablas de puntuación" para su verificación más adelante.
  • El verificador valida que el contenido de los 'marcadores' es legal. Hay casos en los que el generador crea los resultados esperados, además de las entradas. En estos casos, el verificador debe validar que los resultados reales coincidan con los esperados.
  • El director de arbitraje gestiona todos los componentes anteriores juntos.

Se definen diferentes métricas de cobertura para evaluar que el diseño se ha ejercido adecuadamente. Estos incluyen cobertura funcional (¿se han ejercido todas las funciones del diseño?), Cobertura de declaraciones (¿se ha ejercido cada línea de HDL?) Y cobertura de sucursales (¿se ha ejercido cada dirección de cada sucursal?).

Herramientas

Ver también

Referencias