Resumen Técnico: SpecAlign – Un Marco de Alineación Semántica para la Generación de Aserciones en SystemVerilog

1. Enunciado del Problema

La creciente complejidad de los diseños de hardware modernos ha impulsado la adopción de Modelos de Lenguaje Grandes (LLM) para la generación de Aserciones en SystemVerilog (SVA) con el fin de apoyar la Verificación Basada en Aserciones (ABV). Sin embargo, los enfoques actuales de LLM se centran principalmente en la validez sintáctica y los resultados de la verificación formal (FV) (por ejemplo, si una aserción se demuestra o produce un contraejemplo en un RTL dado). Estas métricas no abordan la alineación semántica: si la aserción generada refleja con precisión la intención comportamental descrita en la especificación en lenguaje natural.

Los LLM pueden producir aserciones que son sintácticamente correctas y formalmente demostrables en una implementación RTL específica, pero que son semánticamente ineficaces o alucinan. Por ejemplo, una aserción podría muestrear un reloj en el mismo borde que activa la propiedad, volviéndola vacía a pesar de pasar la FV. En ausencia de un modelo RTL "de referencia" para comparación, la inspección manual de tales aserciones consume tiempo y reduce la confianza. Además, los motores de FV enfrentan problemas de escalabilidad (explosión del espacio de estados) al evaluar grandes conjuntos de aserciones generadas para diseños complejos. Existe una necesidad crítica de un marco que evalúe la consistencia semántica contra la propia especificación, independientemente de los detalles de implementación RTL.

2. Metodología: El Marco SpecAlign

SpecAlign es un marco centrado en la especificación diseñado para evaluar y refinar iterativamente las SVA generadas por LLM sin depender de un RTL de referencia. Opera a través de dos bucles iterativos principales: un Bucle de Alineación de Propiedades y un Bucle de Alineación de SVA. Ambos bucles utilizan tres etapas centrales: Verificación de Alineación, Análisis de Inconsistencias y Extracción de Evidencia.

A. Descripción General de la Arquitectura

El marco normaliza la comparación entre diferentes representaciones de la intención de diseño. Mientras que la entrada consiste en propiedades en lenguaje natural ($P$) y SVA generadas ($A$), el marco convierte cada SVA en un Resumen en Lenguaje Natural ($N$) mediante un proceso de extracción específico. Esta normalización permite que tanto las propiedades como las aserciones se evalúen en el mismo nivel semántico frente a la especificación de diseño ($S$).

B. Componentes Principales

1. Verificación de Alineación:

   • Clasificación: El marco clasifica las descripciones en lenguaje natural ($X_i$) en tres categorías basadas en su relación con la especificación:
     • Implica: Todos los elementos están respaldados por la especificación.
     • Contradice: Al menos un elemento contradice la especificación.
     • Desconocido: Los elementos no están ni respaldados ni contradichos (a menudo debido a suposiciones específicas de implementación no presentes en la especificación).
   • Votación de Autoconsistencia: Para mejorar la fiabilidad, el sistema emplea una estrategia de prompting de Cadenas de Pensamiento (CoT). Genera $k$ caminos de razonamiento para una entrada dada y agrupa los sub-veredictos utilizando votación mayoritaria. En caso de empate, se aplica una prioridad conservadora: Contradice > Desconocido > Implica.
   • Selección de Referencia: El Bucle de Propiedades utiliza la especificación de diseño ($S$) como referencia. El Bucle de SVA utiliza un "Banco de Propiedades Alineadas" (si está disponible) para reducir el ruido de documentos de especificación dispersos; de lo contrario, recurre a $S$.

2. Análisis de Inconsistencias y Refinamiento:

   • Cuando un veredicto es Contradice, el sistema realiza un Análisis de Inconsistencias. Identifica los elementos conflictivos específicos en la descripción, hace referencia al comportamiento correcto en la especificación y genera retroalimentación estructurada y accionable ($F_i$).
   • Esta retroalimentación guía al LLM para regenerar la propiedad o aserción ($P'_i$ o $A'_i$), definiendo explícitamente las condiciones de activación y evitando la introducción de nuevas señales o comportamientos no presentes en la especificación.
   • La salida refinada se reevalúa en el bucle de alineación hasta alcanzar un número fijo de iteraciones o hasta que la salida esté alineada.

3. Extracción de Evidencia:

   • Para los casos de Implica, el sistema extrae evidencia de apoyo (citas y ubicaciones) de la especificación para facilitar la revisión humana y fortalecer la confianza.
   • Para los casos de Desconocido, el sistema categoriza qué elementos son ambiguos o indefinidos, distinguiendo las verdaderas contradicciones de los comportamientos subespecificados.

4. Métrica Cuantitativa:

   • El marco define una Puntuación de Alineación ($a_t$) calculada como la relación entre las aserciones que implican ($E$) y el número total de aserciones ($n$) en una iteración dada ($a_t = E/n$). El objetivo del proceso de refinamiento es maximizar esta puntuación.

C. Extracción de Resumen en Lenguaje Natural

Un paso de preprocesamiento crítico implica convertir las SVA formales en resúmenes estructurados en lenguaje natural. Se solicita al LLM que identifique componentes específicos de la SVA (Activador, Antecedente, Operador de Implicación, Consecuente y Deshabilitar Si) y los mapee a frases equivalentes en lenguaje natural. Esto asegura que la intención semántica del código formal se preserve para la comparación.

3. Contribuciones Clave

El artículo describe las siguientes contribuciones:

• Marco de Evaluación Semántica: Un enfoque novedoso para evaluar las SVA generadas por LLM frente a especificaciones en lenguaje natural sin depender de la verificación formal aplicada a un RTL de referencia.
• Pipeline de Refinamiento Iterativo: Un marco estructurado que comprende Verificación de Alineación, Análisis de Inconsistencias y Extracción de Resúmenes de SVA, diseñado para integrarse en flujos de trabajo de generación basados en LLM existentes.
• Métrica de Alineación Cuantitativa: Una métrica de puntuación de alineación basada en la clasificación de implicación semántica para medir la consistencia de la especificación, ofreciendo una alternativa escalable a la evaluación tradicional de corrección mediante FV.
• Mecanismo de Análisis de Inconsistencias: Un método para generar retroalimentación específica y accionable para propiedades y aserciones contradictorias, apoyando tanto la revisión manual como el refinamiento automatizado.
• Validación Empírica: Resultados experimentales que demuestran la reducción de aserciones contradictorias en diseños APB y UART mediante refinamiento semántico.

4. Resultados Experimentales

Los autores evaluaron SpecAlign en dos diseños de hardware: APB (Interfaz de APB a I2C) y UART (Interfaz de UART a Bus). El marco se comparó con AssertionForge, un método de referencia que utiliza un grafo de conocimiento e incorpora RTL en la generación.

• Resultados de APB:
  • Línea Base (AssertionForge): Generó 442 SVA con una puntuación de alineación de 0.02. Solo 8 fueron implicadas, mientras que 148 fueron contradictorias.
  • SpecAlign: Mantuvo 442 SVA pero aumentó la puntuación de alineación a 0.15. Crucialmente, el número de aserciones contradictorias cayó a 0, con 66 aserciones implicadas. Las 376 restantes se clasificaron como Desconocidas.
• Resultados de UART:
  • Línea Base: Generó 325 SVA con una puntuación de alineación de 0.06 (21 implicadas, 142 contradictorias).
  • SpecAlign: Generó 319 SVA con una puntuación de alineación de 0.28. Las aserciones contradictorias se redujeron a 6, mientras que las aserciones implicadas aumentaron a 92.

Análisis de Resultados:
Los experimentos revelaron que los métodos de referencia a menudo generan aserciones que son o bien contradictorias con la especificación o dependen en gran medida de detalles específicos de implementación (RTL) no encontrados en la especificación en lenguaje natural. SpecAlign filtra eficazmente estas contradicciones. El aumento en las clasificaciones "Desconocido" en SpecAlign (por ejemplo, 376 para APB) se interpreta no como un fracaso, sino como una estrategia de clasificación más conservadora y precisa que separa las suposiciones específicas de implementación del comportamiento respaldado por la especificación. Esta distinción previene el etiquetado de falsos positivos de comportamientos no respaldados como "implicados".

5. Significado y Afirmaciones

El artículo afirma que SpecAlign proporciona un complemento escalable a la verificación formal tradicional. Al separar la corrección semántica de los resultados de prueba RTL, aborda la limitación de que la verificación formal por sí sola no puede determinar si una aserción captura el comportamiento intencionado descrito en la especificación.

Los autores enfatizan que, aunque la verificación formal es necesaria para probar que las aserciones se mantienen en el RTL, es insuficiente para evaluar la calidad de la intención de la aserción. SpecAlign mejora la confianza en las aserciones generadas por LLM mediante:

1. Detectar inconsistencias semánticas que las herramientas formales podrían pasar por alto (por ejemplo, verdades vacías).
2. Reducir los esfuerzos de depuración al identificar contradicciones antes de la simulación RTL o la prueba formal.
3. Proporcionar un mecanismo para refinar aserciones iterativamente sin requerir un modelo de referencia.

El artículo concluye con modestia, señalando que, aunque el marco mejora la alineación, se necesita trabajo futuro para refinar las metodologías de clasificación, capturar mejor los errores sintácticos y extender el enfoque a otras tareas de automatización de diseño de hardware, como la generación y depuración de RTL.