QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis

El artículo presenta QiMeng-CodeV-SVA, un marco de síntesis de datos bidireccional que entrena modelos especializados para generar afirmaciones SystemVerilog (SVAs) a partir de RTL, superando las limitaciones de datos existentes y logrando un rendimiento superior al de modelos avanzados como GPT-5 y DeepSeek-R1.

Lo esencial

¡Claro que sí! Imagina que estás construyendo una casa muy compleja (un chip de computadora) y necesitas asegurarte de que todo funcione perfectamente antes de entregarla. En el mundo de la ingeniería, esto se hace escribiendo "reglas de oro" o assertions (afirmaciones) que dicen cosas como: "Si abres la puerta, la alarma debe sonar" o "Si el interruptor está encendido, la luz debe brillar".

En el lenguaje de los ingenieros de hardware, estas reglas se llaman SVAs (SystemVerilog Assertions). El problema es que escribirlas a mano es como intentar traducir un poema de español a un lenguaje de programación alienígena: es difícil, lento y propenso a errores.

Aquí es donde entra el papel QiMeng-CodeV-SVA. Vamos a explicarlo como si fuera una historia de cocina y detectives.

1. El Problema: La Escasez de Recetas

Imagina que quieres entrenar a un chef (una Inteligencia Artificial) para que escriba estas reglas de seguridad. El problema es que no tienes suficientes "recetas" reales (datos) para enseñarle.

• Los libros de texto tienen muy pocas recetas.
• Las recetas que hay en internet a menudo están mal escritas o son demasiado simples.
• Si le das a un chef generalista (como un modelo de IA común) una receta vaga, probablemente cocinará algo que parece bien pero que en realidad es venenoso (la IA escribe una regla que pasa las pruebas pero no protege la casa).

2. La Solución: El Chef Detective (Síntesis de Datos)

Los autores del papel decidieron no buscar recetas en libros viejos, sino crearlas ellos mismos usando una técnica genial llamada Síntesis de Datos Anclada en RTL.

• El Ancla (RTL): Imagina que tienes miles de planos de casas reales (código de hardware abierto). Son reales, complejos y variados.
• El Proceso: En lugar de pedirle a la IA que invente reglas de la nada, le mostraron los planos reales y le dijeron: "Mira esta casa. ¿Qué reglas de seguridad deberían tener?". La IA generó miles de reglas basadas en la realidad.
• El Filtro de Seguridad: Luego, usaron un "inspector de edificios" automático (una herramienta de verificación formal) para asegurarse de que las reglas generadas realmente funcionaran en los planos. Si la regla no pasaba la prueba, ¡a la basura!

3. El Truco Maestro: El Juego del "Teléfono Descompuesto" Bidireccional

Aquí está la parte más creativa. A veces, la IA puede escribir una regla que pasa la prueba del inspector pero que no significa lo que el ingeniero quería decir. Es como si alguien dijera: "Si llueve, abre el paraguas" y la IA escribiera: "Si llueve, abre el paraguas... o si no llueve, también ábrelo". Técnicamente funciona, pero es absurdo.

Para arreglarlo, usaron un juego de traducción bidireccional:

1. La IA toma la regla escrita en código (SVA) y la traduce a lenguaje humano (Inglés/Español).
2. Luego, toma esa descripción humana y la vuelve a traducir a código.
3. La Prueba de Fuego: Si el código final es exactamente igual (o lógicamente equivalente) al código original, ¡significa que la IA entendió perfectamente el mensaje! Si cambió algo, significa que hubo un error de interpretación y se descarta esa pareja de datos.

Es como si un detective tradujera un mensaje secreto, lo volviera a escribir y comparara si el mensaje original y el nuevo son idénticos. Si no coinciden, el mensaje estaba mal interpretado.

4. El Resultado: Un Especialista de Alto Nivel

Gracias a este proceso de "cocinar con ingredientes reales" y "filtrar con un juego de traducción", crearon CodeV-SVA.

• La Magia: Entrenaron a un modelo de IA (CodeV-SVA) con estos datos ultra-puros.
• El Logro: Este modelo, aunque es más pequeño y barato que los "gigantes" de IA (como GPT-5 o DeepSeek-R1), es mejor en esta tarea específica.
  • En pruebas reales, CodeV-SVA-14B acertó el 75.8% de las veces en crear reglas perfectas, superando a los modelos más grandes y costosos.
  • Es como tener un chef que, aunque no es famoso mundialmente, es el mejor del mundo para cocinar solo ese tipo de plato específico.

En Resumen

Este papel nos dice que no necesitas el cerebro más grande del mundo para resolver un problema de ingeniería difícil. Lo que necesitas es:

1. Datos reales (planos de casas reales, no de dibujos animados).
2. Un método inteligente para limpiar esos datos (el juego de traducción bidireccional para detectar mentiras).
3. Entrenar a un especialista en lugar de un generalista.

El resultado es una herramienta que ayuda a los ingenieros a verificar chips de computadora de forma más rápida, barata y segura, evitando que fallos costosos lleguen al mercado. ¡Es como tener un asistente que nunca se cansa de revisar las reglas de seguridad de tu casa digital!

Resumen técnico

1. Planteamiento del Problema

La verificación formal basada en aserciones es fundamental en el flujo de diseño de hardware digital. Los ingenieros deben formular Aserciones de SistemaVerilog (SVAs) basándose en especificaciones en lenguaje natural (NL) y código de Nivel de Transferencia de Registro (RTL). Sin embargo, existen dos desafíos críticos que dificultan la automatización de esta tarea mediante Modelos de Lenguaje Grandes (LLMs):

• Escasez de Datos de Alta Calidad: Los corpus públicos de SVAs escritos por humanos son limitados (principalmente libros de texto o repositorios pequeños), mientras que existen grandes cantidades de código RTL de código abierto. Los LLMs de propósito general (como GPT-5 o DeepSeek-R1) suelen tener un rendimiento deficiente en la traducción NL2SVA debido a la falta de conocimiento especializado y datos de entrenamiento específicos.
• Falta de Métodos de Validación Semántica: Es difícil validar automáticamente si un par (NL, SVA) es semánticamente equivalente.
  • Las herramientas de verificación formal pueden aprobar aserciones triviales o vacías (ej. assert property (1'b1)) que no se alinean con la descripción en lenguaje natural.
  • Los métodos de "LLM como juez" fallan debido a la ambigüedad del lenguaje natural y la sintaxis compleja de los SVAs (ej. precedencia de operadores).

2. Metodología Propuesta

Los autores proponen un marco de trabajo de síntesis de datos para crear un conjunto de datos masivo y de alta calidad, seguido del entrenamiento de modelos especializados (CodeV-SVA). El proceso consta de cuatro etapas principales:

A. Síntesis de SVA a partir de RTL del Mundo Real

En lugar de buscar SVAs existentes, utilizan código RTL de código abierto (del dataset CodeV) como "Dispositivo Bajo Prueba" (DUT).

1. Se utiliza un LLM de propósito general (DeepSeek-V3.1) para analizar el RTL y generar múltiples propiedades de verificación en lenguaje natural.
2. El mismo LLM traduce estas propiedades a SVAs.
3. Se emplea una herramienta de verificación formal (JasperGold) para filtrar y retener solo los SVAs que son formalmente verificables bajo el RTL dado. Esto genera un conjunto inicial de 159k instancias.

B. Selección Bidireccional de Pares NL-SVA (Núcleo de la Innovación)

Para asegurar que el SVA generado capture fielmente la semántica de la propiedad en lenguaje natural, se aplica una traducción bidireccional:

1. SVA $\to$ NL: Se traduce el SVA generado de nuevo a lenguaje natural.
2. NL $\to$ SVA: Se traduce ese nuevo texto a un SVA de nuevo.
3. Verificación de Equivalencia: Se compara el SVA original con el SVA regenerado mediante herramientas formales. Solo se conservan los pares donde ambos SVAs son lógicamente equivalentes.
   • Lógica: Si la información se pierde en la traducción (debido a errores de alineación o ambigüedad), el SVA regenerado no será equivalente al original. Este método elimina errores sutiles que engañan a la verificación formal directa o a los LLMs como jueces.
   • Resultado: Reducción del conjunto de datos a 105k pares de alta calidad.

C. Refinamiento Adicional de la Calidad de Datos

Se aplican técnicas adicionales para pulir el dataset:

• Juez LLM con Priors de Expertos: Se identifican y eliminan errores específicos (desalineación lógica, inconsistencia de señales) que la selección bidireccional no capturó.
• Filtrado por Dificultad: Se utiliza un LLM más débil (Qwen3-8B) para generar múltiples SVA; si todos son triviales o incorrectos, el dato se descarta.
• Augmentación de Trayectorias de Razonamiento: Se utiliza un modelo de razonamiento avanzado (DeepSeek-R1) para generar trayectorias de pensamiento (CoT) junto con la respuesta final, mejorando la capacidad de inferencia del modelo.

D. Ajuste Fino Supervisado (SFT)

Se entrena el modelo CodeV-SVA (basado en Qwen3-8B y Qwen3-14B) utilizando el dataset sintetizado de 83k instancias. El formato de entrada incluye el código RTL y la propiedad NL, y la salida incluye la trayectoria de razonamiento seguida del SVA.

3. Contribuciones Clave

1. Marco de Síntesis de Datos RTL-Anclado: Demuestra que es posible generar un corpus masivo de SVAs de alta calidad utilizando RTL abierto como base, superando la limitación de datos existentes.
2. Selección Bidireccional: Introduce un método robusto y automatizado para validar la equivalencia semántica entre NL y SVA, resolviendo el problema de la validación de datos sintéticos sin depender exclusivamente de expertos humanos.
3. Modelos Especializados Eficientes: Desarrolla CodeV-SVA, una serie de modelos que superan a LLMs de propósito general masivos (como GPT-5 y DeepSeek-R1) en tareas específicas de hardware, con un costo de despliegue significativamente menor.
4. Recursos Abiertos: Los autores planean liberar el dataset, los modelos y la tubería de entrenamiento.

4. Resultados Experimentales

Los modelos se evaluaron en el benchmark FVEval-NL2SVA (Human y Machine) utilizando la métrica de corrección funcional (Func.@k).

• Rendimiento Superior:
  • CodeV-SVA-14B logró un 75.8% en Func.@1 (NL2SVA-Human) y 84.0% en (NL2SVA-Machine).
  • Estos resultados igualan o superan a modelos propietarios avanzados como GPT-5 y DeepSeek-R1, a pesar de que CodeV-SVA es un modelo de 14B parámetros (mucho más pequeño y barato de ejecutar).
• Comparación con Líneas Base:
  • Superó significativamente a los modelos base (Qwen3-14B) y a modelos especializados en generación de RTL.
  • En el estudio de ablación, se demostró que la selección bidireccional fue el componente que más mejoró el rendimiento (un aumento del 12.3% en Func.@1 para NL2SVA-Human), validando su eficacia para filtrar datos ruidosos.
• Flujo de Verificación End-to-End:
  • Integrado en un flujo de verificación automatizado (modificación de AssertionForge), CodeV-SVA-8B generó hasta 3.5 veces más SVAs verificables que DeepSeek-R1 en diseños complejos (ej. OPENMSP430).

5. Significado e Impacto

Este trabajo aborda un cuello de botella crítico en la industria de semiconductores: la verificación formal. Al demostrar que es posible entrenar modelos especializados de tamaño moderado que superan a los gigantes de propósito general mediante una síntesis de datos inteligente y validada formalmente, el artículo ofrece una ruta viable y económica para automatizar la generación de aserciones.

La metodología propuesta no solo resuelve el problema de la escasez de datos, sino que establece un nuevo estándar para la validación de datos sintéticos en dominios técnicos donde la precisión semántica es crítica, permitiendo que las empresas de hardware adopten IA sin los costos prohibitivos de los modelos más grandes o la necesidad de grandes cantidades de datos etiquetados manualmente.