El error de 10 millones de dólares que escribió la IA — y por qué fundé una empresa para eliminarlo

Recuerdo el momento exacto en que decidí fundar Veriprajna.

No fue un destello de inspiración. Fue una llamada telefónica. De esas en las que nadie habla durante los primeros cinco segundos porque la persona al otro lado intenta averiguar cómo decir lo que necesita decir. Un equipo de diseño —gente a la que respetaba, gente que era genuinamente buena en su trabajo— acababa de recibir el primer silicio de la fundición para un acelerador RISC-V personalizado. El chip estaba muerto. No muerto de «necesita una solución alternativa». No muerto de «podemos parchearlo en firmware». Inservible. Bajo una alineación específica y poco frecuente de limitación térmica y tráfico de memoria de alto ancho de banda, el módulo de arbitraje entró en un estado indefinido y todo el conjunto se bloqueó por completo.

La causa raíz fue una condición de carrera. Un único y sutil desajuste entre asignaciones bloqueantes y no bloqueantes en el RTL: de esas que se simulan a la perfección, pasan el linting sin un susurro, superan todas las pruebas de regresión que les lances y luego te traicionan en el silicio, donde no hay segundas oportunidades.

El juego de máscaras para ese chip de 5 nm costó aproximadamente 10 millones de dólares. Perdido. Pero el daño real no fueron las máscaras. Fueron los seis meses necesarios para diagnosticar, corregir, volver a verificar y volver a fabricar. En el mercado de aceleradores de IA, donde las generaciones de producto duran unos 18 meses, un retraso de seis meses puede erosionar el 50 % del beneficio bruto total de la vida útil de un producto. Para una empresa que apunta a 100 millones de dólares en ingresos, esa condición de carrera no costó 10 millones de dólares. Costó 50 millones.

Y aquí está la parte que me quitaba el sueño: el código que la causó fue generado por un LLM.

La fiebre del oro que nadie cuestiona

En este momento, la industria de los semiconductores está en plena fiebre del oro. Todos —y me refiero a todos— compiten por integrar los grandes modelos de lenguaje (LLM) en el flujo de trabajo de automatización del diseño electrónico (EDA). La propuesta es irresistible: tomar ciclos de diseño que solían durar años y comprimirlos a meses. Democratizar el diseño de chips. Dejar que la IA se encargue de la tediosa codificación a nivel de transferencia de registros para que los ingenieros puedan centrarse en la arquitectura.

Entiendo el atractivo. Yo mismo lo he sentido. La primera vez que vi a un LLM generar un módulo Verilog sintácticamente correcto a partir de una indicación en lenguaje natural, pensé: esto lo cambia todo.

Pero luego empecé a fijarme con más atención en lo que «sintácticamente correcto» significa en realidad cuando escribes hardware en lugar de software. Y me di cuenta de que la industria estaba construyendo sobre cimientos de arena.

Las herramientas que inundan el mercado ahora mismo son lo que yo llamo «Envoltorios». Toman un LLM de propósito general —GPT-4, Claude, Llama—, lo envuelven en una interfaz de chat con algunas indicaciones de sistema con sabor a Verilog y lo venden como un «copiloto de diseño de chips». Algunas son demostraciones genuinamente impresionantes. El código se ve limpio. Compila. Incluso se simula.

Pero esto es lo que son fundamentalmente estas herramientas: predictores estocásticos de tokens con una piel de hardware. No entienden la topología de circuitos. No entienden el cierre de temporización. No entienden la metaestabilidad. Predicen el siguiente token probable basándose en patrones estadísticos de sus datos de entrenamiento.

Cuando un LLM alucina en software, obtienes un error de tiempo de ejecución que puedes parchear por aire. Cuando un LLM alucina en hardware, obtienes un pisapapeles de 10 millones de dólares.

Esa asimetría es toda la razón por la que existe Veriprajna.

¿Por qué la IA escribe mal código de hardware?

Esta es la pregunta que me hacen con más frecuencia, normalmente ingenieros de software que han visto a los LLM escribir Python perfectamente funcional y no entienden por qué Verilog es diferente. La respuesta va más allá de «el hardware es más difícil». Es un desajuste fundamental entre cómo piensan los LLM y cómo funciona el hardware.

Los LLM se entrenan de forma abrumadora con software: Python, Java, C++, JavaScript. Estos son lenguajes imperativos y secuenciales. La línea A se ejecuta, luego la línea B. El estado del sistema se define por el orden de las operaciones. Los LLM han interiorizado este paradigma tan profundamente que es prácticamente su lengua materna.

Verilog y VHDL son declarativos y concurrentes. En un módulo de hardware, cada bloque always, cada instrucción assign, cada instanciación de módulo se ejecuta simultáneamente y continuamente. El orden de las líneas en el código fuente a menudo no tiene ninguna relación con el orden de ejecución en el silicio.

Vi cómo esto se desarrollaba en tiempo real durante uno de nuestros primeros experimentos. Pedimos a tres LLM de vanguardia diferentes que implementaran un simple registro de pipeline de tres etapas. Los tres usaron asignaciones bloqueantes (=) en lugar de asignaciones no bloqueantes (<=). El código parecía perfectamente razonable si lo mirabas de reojo como si fuera código C. Pero en hardware, las asignaciones bloqueantes en un bloque sincronizado hacen que stage2 se actualice con el valor de stage1 de forma inmediata, y luego stage3 obtiene el nuevo valor de stage2 — colapsando efectivamente un pipeline de dos ciclos en uno solo.

Una de mis ingenieras, Priya, se quedó mirando la salida durante un minuto y dijo: «Está escribiendo C con los puntos y comas en los lugares equivocados». Tenía toda la razón. El LLM tenía un sesgo secuencial —trataba Verilog como un lenguaje de programación cuando en realidad es un lenguaje de descripción. La distinción es sutil sintácticamente y catastrófica físicamente.

Y va a peor. El diseño de hardware depende de estrictos protocolos de interfaz —AXI, AHB, PCIe, TileLink— con reglas temporales complejas. «Ready no debe esperar a Valid». «Grant debe afirmarse en un plazo de 5 ciclos». Los LLM pueden generar código que respeta estas reglas el 90 % de las veces, lo cual suena estupendo hasta que te das cuenta de que el 10 % que hace mal son precisamente los casos límite que matan chips. Un maestro AXI que afirma WVALID antes de AWREADY en una violación específica de una subcláusula no arrojará un error de sintaxis. Compilará, se simulará y luego se colgará cuando se conecte a un controlador de memoria conforme en el silicio.

El problema de los datos de entrenamiento lo agrava todo. El volumen de Verilog de alta calidad y de nivel de producción disponible para entrenamiento es órdenes de magnitud menor que el de Python o JavaScript. Gran parte del Verilog de código abierto en GitHub son proyectos de estudiantes, prototipos abandonados, implementaciones de juguete que jamás sobrevivirían a una revisión de tape-out. Cuando entrenas con datos mediocres, obtienes resultados mediocres: resultados que parecen profesionales pero que contienen el ADN de errores de aficionado.

La regla que atormenta a todo diseñador de chips

Existe una heurística en el diseño de semiconductores llamada «Regla de Diez» y, una vez que la entiendes, comprendes por qué estoy tan obsesionado con detectar los errores pronto.

El coste de corregir un defecto aumenta 10x en cada etapa posterior del ciclo de vida del diseño. Un error detectado durante el diseño RTL cuesta unos 100 dólares de corregir: alguien edita un archivo y vuelve a ejecutar una comprobación. El mismo error detectado durante la verificación de bloques cuesta 1000 dólares. En la verificación de sistema, 10 000 dólares. Si escapa a la validación posterior al silicio —cuando estás depurando chips reales en un laboratorio— estás ante 10 millones de dólares o más por un respin. ¿Y si llega a los clientes sobre el terreno? Eso es territorio de 100 millones de dólares. Retiradas de producto, demandas, destrucción de la marca. Pregúntale a Intel por el error FDIV del Pentium.

Las herramientas de IA Envoltorio operan casi exclusivamente en la etapa de diseño RTL. Ayudan a los ingenieros a escribir código más rápido. Pero como carecen de cualquier capacidad de verificación más allá de «¿compila?», inyectan errores que atraviesan sin problemas la verificación de bloques y de sistema, solo para detonar en el silicio.

Esta es la cruel ironía: al aumentar la velocidad de generación de código sin aumentar el rigor de la verificación, estas herramientas aceleran la inyección de defectos de alto coste en el pipeline. No solo te mueves rápido y rompes cosas. Te mueves rápido y horneas errores en juegos de máscaras de 10 millones de dólares.

Los datos de la industria lo confirman. Solo el 32 % de los diseños logran el éxito al primer silicio. El 68 % restante requiere al menos un respin, y la causa principal son fallos lógicos y funcionales: exactamente el tipo de errores que generan los LLM cuando alucinan protocolos o malinterpretan la concurrencia.

Le expliqué esto a un inversor una vez, al principio de nuestra ronda de financiación. Escuchó con paciencia y luego dijo: «¿No puedes simplemente usar GPT-4 con mejores indicaciones?»

Saqué el ejemplo del registro de pipeline. Le mostré el error de la asignación bloqueante. Le mostré que pasaba el linting, pasaba la simulación, pasaba todas las comprobaciones automáticas que ofrecían las herramientas Envoltorio. Luego le mostré lo que haría en el silicio.

No volvió a preguntar por mejores indicaciones.

¿Y si pudieras demostrar que el código es correcto en lugar de solo probarlo?

Aquí es donde la historia da un giro. Porque la respuesta al problema de la alucinación de los LLM no son mejores indicaciones, modelos más grandes ni más datos de entrenamiento. Es un enfoque fundamentalmente diferente de la verificación.

La verificación tradicional se basa en la simulación: escribes bancos de pruebas, ejecutas millones de ciclos y compruebas si el diseño hace lo que esperas. Es como probar los frenos de un coche conduciendo alrededor de la manzana mil veces. Si los frenos no fallan, supones que son seguros. Pero ¿y si solo fallan cuando llueve, vas exactamente a 62 mph y la radio está sintonizada en una frecuencia específica? La simulación solo puede verificar los escenarios que prueba explícitamente. Todo lo demás es una plegaria.

La verificación formal no ejecuta el diseño en absoluto. Convierte todo el diseño en una fórmula matemática y utiliza solucionadores de Teorías de Satisfacibilidad Módulo (SMT) —herramientas como Z3 de Microsoft— para demostrar exhaustivamente que una propiedad se cumple bajo cada posible combinación de entradas y estado interno. Absolutamente todas. No una muestra. No una aproximación estadística. Una demostración matemática.

La simulación pregunta: «¿Funciona esto en los casos que probé?». La verificación formal pregunta: «¿Existe algún caso posible en el que esto falle?». La diferencia es la diferencia entre la esperanza y la demostración.

Cuando el solucionador devuelve «UNSAT» —insatisfacible— significa que no existe ningún contraejemplo. La propiedad está garantizada matemáticamente. Cuando devuelve «SAT», te entrega una secuencia específica de entradas que rompe tu diseño, hasta el ciclo de reloj exacto.

La verificación formal existe desde hace décadas. La razón por la que no se ha impuesto en la industria es que escribir las propiedades formales —las aserciones de SystemVerilog, o SVA— es notoriamente difícil. Requiere un conjunto de habilidades especializadas que la mayoría de los equipos de diseño no tienen. Las aserciones son el «contrato» del hardware: «Si request sube, grant debe seguirlo en un plazo de N ciclos». «Los datos leídos de la dirección X deben coincidir con los últimos datos escritos en la dirección X». «El pipeline nunca debe bloquearse». Escribirlas correctamente es una forma de arte, y no hay suficientes practicantes para abastecer la demanda.

Que es exactamente donde la IA se vuelve útil: no para escribir el código de hardware, sino para escribir la demostración.

El «Sándwich Formal»: cómo lo construimos en realidad

Pasé meses discutiendo con mi equipo sobre la arquitectura correcta. El debate fue feroz y, en retrospectiva, esclarecedor. Un bando quería ajustar (fine-tune) un LLM hasta que generara Verilog correcto por defecto. El otro bando —con el que finalmente me alié— sostenía que la corrección por entrenamiento era una fantasía. No puedes eliminar la alucinación con entrenamiento. Solo puedes detectarla.

Nos decidimos por lo que llamamos el «Sándwich Formal» —una arquitectura neuro-simbólica donde el LLM es el motor creativo y un solucionador de verificación formal es el crítico inflexible. Ninguno funciona por separado. Juntos, hacen algo que ninguno puede hacer de forma independiente.

Así es como funciona en la práctica. Un diseñador proporciona una especificación —«Diseña un puente APB-a-AXI» o incluso una captura de pantalla de un diagrama de tiempos—. Nuestro agente Analizador de Especificaciones la descompone en requisitos funcionales. Luego viene la innovación clave: en lugar de generar solo código, el LLM genera dos artefactos simultáneamente.

El artefacto A es la implementación RTL: el propio código Verilog. El artefacto B es la especificación formal: un conjunto de propiedades SVA derivadas de los mismos requisitos. Si la especificación dice «Grant debe seguir a Request», el LLM genera la máquina de estados y la aserción que demuestra que la máquina de estados hace lo que afirma.

Luego desatamos el solucionador. Toma el artefacto A e intenta romperlo usando el artefacto B. Primero, una comprobación de vacuidad: para asegurarse de que las aserciones no sean trivialmente verdaderas (una generación «perezosa» en la que la condición de disparo nunca se activa). Luego, la comprobación acotada de modelos, explorando espacios de estados profundos —50, 100 ciclos de profundidad— en busca de bloqueos, condiciones de carrera y violaciones de protocolo.

Si el solucionador encuentra un error, no se limita a señalarlo. Produce una traza de contraejemplo —una forma de onda precisa que muestra exactamente cómo se manifiesta el error. Y aquí es donde se cierra el bucle: introducimos esa traza de vuelta en el LLM como una indicación. «Tu diseño falló. Aquí está la traza: Ciclo 1, Reset se desactiva. Ciclo 2, Request sube. Ciclo 10, Grant sigue en bajo. El grant nunca llegó. Corrige la máquina de estados».

El LLM analiza la traza, identifica la transición de estado que falta y reescribe el código. El solucionador vuelve a comprobar. Este bucle se repite automáticamente hasta que se demuestra que el diseño es correcto.

Escribí sobre esta arquitectura con mucha más profundidad en la versión interactiva de nuestra investigación, pero la idea central es sencilla: usamos la IA para escribir la demostración y las matemáticas para comprobar la IA. Ninguna confía en la otra. Ambas mejoran a la otra.

Los errores que me convirtieron en creyente

Me convertí en un verdadero creyente de este enfoque no a través de la teoría, sino a través de errores concretos que detectamos y que nada más habría encontrado.

La comunidad de RISC-V de código abierto ha producido núcleos de procesador genuinamente excelentes: Ibex (usado en el chip de seguridad OpenTitan de Google), la plataforma PULP de la ETH de Zúrich. Son diseños sumamente escrutados con verdadero talento de ingeniería detrás. Y aun así contienen errores que solo la verificación formal puede encontrar.

Axiomise, una consultoría de verificación formal, encontró un error en el núcleo Ibex donde una solicitud de depuración que llegaba en un ciclo específico durante una instrucción de bifurcación podía hacer que el núcleo se bloqueara o ejecutara la instrucción equivocada. Piénsalo: un núcleo crítico para la seguridad, revisado por decenas de ingenieros, y una herramienta formal encontró un error que la simulación pasó por alto por completo.

En la plataforma PULP, se encontró un error donde la interconexión AXI podía privar de recursos a un maestro de bus indefinidamente bajo un patrón «ocupado» específico de interacciones AWVALID y AWREADY. Un clásico fallo de vivacidad: el sistema no se cuelga, simplemente deja de avanzar. Nunca escribirías una prueba dirigida para ese patrón de interacción específico. Hay demasiados patrones posibles para enumerarlos.

Cuando apuntamos Veriprajna a una unidad de carga y almacenamiento (Load-Store Unit) de RISC-V, genera automáticamente aserciones de conformidad de interfaz («si valid se afirma, debe permanecer en alto hasta ready»), integridad de datos («los datos leídos de la dirección X coinciden con la última escritura en la dirección X») y progreso hacia adelante («la unidad debe finalmente devolver una respuesta»). No son ocurrencias tardías atornilladas al código. Se generan junto con el código, a partir de la misma especificación, y se hacen cumplir antes de que una sola línea de RTL salga de nuestro sistema.

Para el desglose técnico completo de nuestra metodología y el motor de verificación formal, consulta nuestro documento de investigación detallado.

«Pero la verificación formal no escala»

La gente siempre pone objeciones en este punto, y entiendo por qué. La verificación formal tiene fama de ser computacionalmente explosiva: el espacio de estados de un SoC moderno es astronómicamente grande, y los enfoques formales ingenuos se atragantan con cualquier cosa más grande que un diseño de juguete.

Hemos dedicado un esfuerzo considerable a esto. Nuestro sistema utiliza técnicas de abstracción automatizadas para hacer la verificación formal tratable a escala. El encapsulado en caja negra nos permite verificar la lógica de pegamento tratando grandes subbloques como las RAM o las ALU complejas como entidades abstractas con interfaces definidas. Los puntos de corte rompen las rutas de handshake valid/ready para que podamos verificar el control de flujo independientemente del procesamiento de datos. La reducción por simetría nos permite demostrar una propiedad para un canal de un router multipuerto e inducirla matemáticamente para todos los N canales.

¿Está resuelto por completo? No. La física analógica siempre presentará desafíos que los métodos formales no pueden abordar. Pero los errores lógicos —las condiciones de carrera, los bloqueos, las violaciones de protocolo— se vuelven matemáticamente imposibles en el código generado. Y esos son los errores que provocan los respins.

La otra objeción que escucho es sobre la velocidad. «¿No ralentiza el proceso de diseño ejecutar un solucionador formal?». Sí, añade coste computacional. Pero cambiaré tiempo de cómputo por certeza de calendario todos y cada uno de los días. Un solucionador formal ejecutándose una hora extra es infinitamente más barato que un respin de seis meses.

La incómoda verdad sobre los «chips diseñados por IA»

Hay una narrativa que gana terreno en la industria: que la IA pronto diseñará chips de extremo a extremo, que estamos pasando del Diseño Asistido por Computadora al Diseño Automatizado por Computadora. Creo que esa narrativa es direccionalmente correcta pero peligrosamente incompleta.

Estamos avanzando hacia flujos de trabajo agénticos donde agentes de IA autónomos colaboran: un agente Arquitecto para el particionado de alto nivel, un Codificador RTL para la implementación, un Ingeniero de Verificación para escribir bancos de pruebas y aserciones, y un Gestor para orquestar el flujo frente a las restricciones de potencia, rendimiento y área. Usamos la generación aumentada por recuperación (RAG) no solo para el código sino para el conocimiento: extrayendo reglas de protocolo específicas, restricciones del kit de diseño de procesos y estándares de codificación internos para que el LLM genere código conforme sin alucinar.

Pero nada de esto funciona —nada de ello — sin una columna vertebral de verificación formal. Cuanto más autónoma se vuelve la IA, más crítico es que cada salida se verifique matemáticamente antes de avanzar aguas abajo. Un agente de IA que genera código más rápido solo es valioso si ese código es correcto. ¿Un agente de IA que genera código más rápido y demuestra que es correcto? Ese es el futuro.

El problema de la industria de los semiconductores no es que la IA sea demasiado lenta escribiendo código de hardware. Es que la IA es demasiado rápida escribiendo código de hardware que es sutilmente incorrecto.

No somos un copiloto. No somos un chatbot. Somos una fundición de verificación formal que resulta que usa IA generativa como interfaz de entrada. La distinción importa porque determina para qué estás optimizando. Los copilotos optimizan la velocidad. Nosotros optimizamos la corrección. En un mundo donde un único error que se escapa cuesta 10 millones de dólares en máscaras y 50 millones de dólares en ingresos perdidos, sé qué optimización elegiría yo.

La elección ya está tomada

La industria de los semiconductores ya no puede permitirse el enfoque de «generar y rezar». La Regla de Diez no es una sugerencia: es la física y la economía conspirando para castigar a cualquiera que envíe silicio sin verificar. A 5 nm y por debajo, con juegos de máscaras que se acercan a los 20 millones de dólares, el margen de error se ha desplomado a cero.

Cada semana hablo con equipos de diseño que están entusiasmados con lo que los LLM pueden hacer por su productividad y aterrorizados por lo que los LLM podrían hacer a su calendario de tape-out. Tienen razón en sentir ambas cosas simultáneamente. La tecnología es genuinamente transformadora. También es genuinamente peligrosa sin una red de seguridad.

Veriprajna es esa red de seguridad. Te damos la velocidad de la IA con la certeza de las matemáticas. No «probablemente correcto». No «pasó la regresión». Demostrado correcto, a través de cada entrada posible, cada estado posible, cada caso límite posible que una simulación jamás pensaría en probar.

La elección a la que se enfrenta hoy todo diseñador de chips no es si usar IA. Ese barco ya zarpó. La elección es si usar una IA que pueda demostrar su propio trabajo, o una IA que simplemente espera lo mejor.

Sé por cuál apostaría 10 millones de dólares.