Los modelos de lenguaje grandes se acercan a ejecutar una de las tareas más molestas de la verificación del diseño de chips: convertir las especificaciones escritas en lenguaje natural en un conjunto de propiedades formales que puedan utilizarse para juzgar la corrección de una implementación RTL. Entrevistas realizadas por Brian Bailey en Semiconductor Engineering muestran que las herramientas actuales pueden producir un borrador inicial útil, pero aún están lejos de crear un conjunto completo que pueda adoptarse sin una revisión de ingeniería intensiva.
La importancia de este avance radica en que la escritura de propiedades representa desde hace años un cuello de botella en la verificación formal. Las propiedades de SystemVerilog, conocidas como assertions cuando se incluyen en el entorno de verificación, se utilizan para describir las relaciones lógicas y temporales entre señales, como el comportamiento del reset, los handshakes, las condiciones one-hot y las comprobaciones básicas de seguridad. Cuando estas propiedades son completas y precisas, pueden utilizarse para comparar el comportamiento de una implementación RTL con la especificación, sin depender de la forma en que se construyó el diseño.
¿Qué pueden hacer las herramientas hoy?
Una herramienta basada en un modelo de lenguaje grande puede leer un documento de especificaciones, un estándar de protocolo o incluso comentarios dentro del RTL, y después proponer un borrador de propiedades SVA. Ashish Darbari, director ejecutivo de Axiomise, afirma que este uso resulta más viable cuando las especificaciones se basan en estándares estables que no cambian demasiado. En este caso, la herramienta reduce la parte repetitiva de la escritura del código inicial, en lugar de asumir todo el proceso de verificación.
Algunos enfoques intentan mejorar la precisión de los modelos mediante la creación de un knowledge graph, es decir, un grafo de conocimiento que almacena las entidades y las relaciones entre ellas. Los nodos pueden incluir una señal, un módulo, un requisito o un puerto, mientras que las aristas describen relaciones como «conduce», «reinicia» y «responde a». En lugar de recuperar fragmentos de texto que parecen relacionados con la solicitud, el sistema puede remitirse a hechos y vínculos específicos, lo que reduce la probabilidad de inventar el nombre de una señal o de malinterpretar una relación entre componentes del diseño. La fuente menciona en este contexto un estudio titulado RAG-SVA in the Landscape of LLM-Based Assertion Generation, de Cohen y Chibani.
El problema comienza antes de la inteligencia artificial
La herramienta no puede extraer aquello que no se ha escrito o decidido previamente. Ravindra Aneja, director de ingeniería de aplicaciones en Synopsys, afirma que la especificación ideal no ha estado disponible durante las tres últimas décadas; con frecuencia, el desarrollo comienza antes de que la documentación esté completa, y en algunos proyectos puede no existir una especificación completa, especialmente en diseños derivados o cuando los requisitos cambian durante el trabajo.
Este problema no se refiere únicamente a la redacción, sino también a la gestión del cambio. El equipo de marketing puede añadir una nueva función o modificar un requisito existente, y los equipos de diseño y verificación deben determinar el impacto de ese cambio. Abhi Kolpekwa, vicepresidente sénior y director general de Siemens EDA, considera que convertir la especificación en propiedades requiere «inteligencia contextual» que siga el historial y el contexto de los cambios, no un agente que genere texto nuevo cada vez.
El riesgo de una falsa confianza
La mayor limitación del enfoque actual es que una propiedad puede ser sintácticamente correcta, compilarse y superar las herramientas de verificación que intentan demostrarla, pero no probar realmente el comportamiento previsto. Darbari advierte que una propiedad débil o vacua puede tener éxito con facilidad porque permite demasiados comportamientos, porque utiliza la señal equivocada o porque contiene un antecedente ausente o excesivamente restrictivo. Por ello, una «prueba en verde» no significa que el diseño esté libre de errores: la evidencia no es más sólida que la propiedad que se ha demostrado.
La fuente añade que los modelos tienden a rendir mejor en cobertura estructural y sintáctica que en la comprensión de la intención arquitectónica y de la razón de ser de la regla. Por este motivo, una lectura imprecisa de la especificación por parte del modelo puede convertirse en una pieza que parece formal y rigurosa, mientras oculta una brecha en los requisitos. Si esa brecha pasa a trabajos como FMEDA, archivos de seguridad o pruebas de certificación relacionadas con ISO 26262 e ISO 21434, su impacto puede extenderse mucho más allá del proyecto de verificación original.
También destaca la cuestión de separar el diseño de la verificación. Kaye Mao, líder de diseño de productos en Normal Computing, señala la necesidad de limitar los materiales del proyecto a los que pueden acceder los agentes, porque permitir que el agente utilice el propio diseño para generar casos de prueba podría socavar la independencia del proceso de verificación.
¿Qué cambia en la práctica?
La inteligencia artificial puede reducir el tiempo de preparación de los primeros borradores de días a minutos, según Darbari, pero también puede multiplicar el trabajo posterior. Cada propiedad generada necesita comprobarse frente a la especificación, analizarse en términos de cobertura, someterse a pruebas de vacuity y revisarse en relación con las señales del diseño; además, los fallos pueden requerir un análisis de las formas de onda. Si el número de propiedades se multiplica por diez y el nivel de escrutinio requerido para cada una permanece igual, la carga de revisión puede superar la ganancia derivada de la generación rápida.
Desde la perspectiva de certi.news, el cambio real no consiste en sustituir al ingeniero de verificación, sino en desplazar el centro de gravedad desde la escritura de propiedades hacia su evaluación y el seguimiento de su procedencia. Darbari recomienda tratar las propiedades generadas como borradores, no como resultados aprobados, y establecer una puerta de revisión antes de incorporarlas a la regression suite. También debería registrarse el origen de cada propiedad —el párrafo de la especificación, el requisito o el elemento RTL que la produjo— para que el ingeniero pueda comprobar la correspondencia.
Este enfoque puede reducir la barrera de entrada para los ingenieros de verificación que desean utilizar formal verification, afirma Yaron Ilani, ingeniero de soluciones de verificación en Normal Computing. Sin embargo, no resuelve la cuestión del retorno de la inversión. Kaye Mao considera que el tiempo dedicado a verificar las salidas del agente debe contabilizarse como parte del coste, mientras que Arvind Srinivasan, jefe de ingenieros de soluciones en Normal Computing, señala que la escalabilidad no depende únicamente del cálculo, sino también de la integridad de los datos y del coste de la revisión humana.
La conclusión es que los modelos de lenguaje grandes ya son capaces de acelerar la parte automática y repetitiva de la formulación de propiedades, pero todavía no han resuelto los problemas de la integridad de la especificación y de la comprensión de la intención del diseño. El valor de estas herramientas seguirá dependiendo de la existencia de un ingeniero que comprenda el diseño y de mecanismos independientes para medir la cobertura y detectar propiedades vacías o inadecuadas, no del número de propiedades que el modelo pueda producir.