Ocho pruebas formales en verde pasaron a ser cinco aptas para sign-off al auditar las aserciones de SystemVerilog
Observé cómo un panel formal sintético reportaba 8/8 PROVEN, y luego vi cómo su propia auditoría certificaba solo 5/8 como TRUSTWORTHY. Esa reversión es la premisa de Proof Firewall, nuestra demostración ejecutable de gobernanza para aserciones de SystemVerilog (SVA) generadas por IA, y cambió el estándar que espero que cumpla una prueba formal en verde antes de llegar a una revisión de sign-off para tape-out.
Construí el panel con propiedades de banco de pruebas creadas como «autoría de LLM» sobre un árbitro sintético, un pipeline de dos etapas y un cruce de dominios de reloj (CDC), porque el caso incómodo merece ser visible. Una aserción puede parecer perfectamente respetable en un registro de propiedades. Un motor formal puede devolver un resultado en verde. Sin embargo, es posible que la implicación nunca haya tenido que hacer ningún trabajo, o que siga pasando después de que el comportamiento relevante del diseño se haya roto. Había estado tratando la palabra PROVEN como un destino. Construir esta demo me obligó a tratarla como el inicio de una revisión de evidencias.
La demo de Proof Firewall no reemplaza un motor formal, no ingesta RTL real ni llama a un LLM en vivo en su ruta predeterminada. Es deliberadamente más pequeña y fácil de inspeccionar: un model checker de estados explícitos en Python puro evalúa una representación intermedia (IR) sintética de sistema de transiciones; luego, una compuerta de gobernanza verifica la alcanzabilidad del antecedente, la eliminación de mutaciones (mutation kills) y el cono de influencia (COI). La salida es o bien un motivo para registrar un certificado de demostración firmado, o bien una razón para retener el resultado para revisión humana.
Comencé con el tipo de verde equivocado
Recuerdo que la primera versión del panel resultaba tranquilizadora precisamente por ser tan limpia. Ocho propiedades, ocho distintivos verdes y una vista del flujo básico que hacía parecer que el trabajo estaba terminado. Mi primer instinto fue hacer que la demo explicara mejor ese resultado limpio. Pensé que la tarea de ingeniería era la presentación: mostrar las pruebas formales, exhibir las aserciones y hacer que el panel fuera más fácil de confiar. El resultado en verde era real, pero respondía a una pregunta mucho menor que la que un revisor necesita plantear.
Luego sometí las mismas ocho propiedades a las comprobaciones que una conversación de sign-off realmente exige. ¿Llegó a ser verdadero el antecedente en algún momento? ¿Protestaría la aserción si se cambiara una parte relevante del diseño? ¿Restringe un COI significativo? Esas preguntas son menos halagadoras que un distintivo verde porque indagan qué se ha ganado la prueba formal, no simplemente qué devolvió el solver.
Tuve que abandonar el planteamiento inicial del desarrollo. Una pantalla que mostraba 8/8 PROVEN era una vista fiel del flujo básico de referencia, pero resultaba incompleta como historia de sign-off. Tras la auditoría del cortafuegos, el mismo panel sintético fijo tiene cinco resultados TRUSTWORTHY, un resultado VACUOUS y dos resultados WEAK. Los tres restantes no se reclasifican como éxito: quedan retenidos junto con la evidencia que explica el porqué. Una etiqueta de prueba formal y una decisión de sign-off son artefactos distintos.
Elegí la palabra «gobernanza» con mucho cuidado. Las comprobaciones deterministas de la demo hacen que la decisión de sign-off sea auditable. Un autor opcional de SVA puede proponer una aserción, pero el model checker y la compuerta de políticas determinan el veredicto. Los agentes aconsejan, el código decide. Intentaba hacer que la compuerta fuera lo suficientemente legible como para que el resultado negativo fuera útil en lugar de simplemente vergonzoso. Un resultado retenido necesita una razón que un ingeniero de verificación pueda inspeccionar, reproducir y cuestionar.
ARB3 hizo que el problema fuera imposible de ignorar
Encontré el fallo más claro en ARB3, la propiedad del árbitro sintético assert (g0 && g1) |-> (turn == 0). En el flujo básico está en verde. Cuando abrí su forma de onda y la evidencia de alcanzabilidad, el antecedente g0 && g1 era inalcanzable en ese árbitro sintético. La implicación se había demostrado solo en el sentido estricto de que nunca se vio obligada a responder por el estado que describía. El antecedente nunca se activa.
Esa distinción es fácil de expresar y difícil de tener presente cuando un panel de verificación está repleto de verde. Inicialmente interpreté la implicación como una afirmación sobre el comportamiento de arbitraje. El resultado de alcanzabilidad cambió lo que estaba observando: era una afirmación cuya condición de activación nunca ocurría. Calificar eso de VACUOUS es más útil que preservar una etiqueta verde, porque orienta al revisor hacia la suposición o el estímulo que dejó vacía la prueba formal.
Volvía continuamente a este panel mientras trabajaba en las etiquetas de las políticas. VACUOUS puede sonar como un resultado severo hasta que se considera la alternativa. Si un registro de sign-off conserva una prueba sin registrar que su antecedente nunca se activa, la revisión habrá recibido una conclusión sin la condición que le da sentido. El mejor registro es aquel que hace explícita la limitación y le proporciona a una persona algo concreto que interrogar. Ese registro de alcanzabilidad debe figurar junto al veredicto.
También tuve que resistirme a tratar la vacuidad como una advertencia cosmética. Si la propiedad está pensada para restringir una condición de arbitraje, un comportamiento de activación inalcanzable es evidencia crucial sobre si la propiedad realmente ejercitó el comportamiento previsto. El panel de control no debería pedirle a un revisor que infiera eso a partir de un resultado en verde. Debe preservar el hallazgo de alcanzabilidad, desviar el resultado fuera de la ruta de certificación y hacer evidente la siguiente acción de revisión.
El contexto de la industria aumentó la trascendencia del problema para mí. El estudio de 2024 de Wilson Research Group / Siemens EDA citado en la especificación de la demo reporta un 14% de éxito en silicio a la primera. Esa no es una medición de Veriprajna, y este panel sintético no pretende explicar esa cifra. Pero sí hace que esté mucho menos dispuesto a tratar un estado agradable del panel como evidencia por sí mismo.
La propiedad del pipeline sobrevivió a la rotura que esperaba que detectara
Me topé con el segundo fallo mientras probaba PIPE3, una propiedad de pipeline sintético de dos etapas: assert v2 |-> (s2 == s2). Quería un ejemplo conciso de una aserción que se leyera con suficiente sentido como para colarse en una revisión superficial. El consecuente es una tautología: dice que s2 es igual a sí mismo. El consecuente no restringe nada.
El paso importante en la demo no es solo detectar la tautología en el texto. La compuerta de gobernanza inyecta mutaciones de diseño puntuales y relevantes y comprueba si la propiedad las elimina. Para el caso destacado del pipeline débil, PIPE3 registra un resultado de 0/6 mutaciones eliminadas. La propiedad sobrevive a las variantes rotas relevantes. Por eso la política asigna WEAK en lugar de permitir que el resultado PROVEN básico se mantenga como evidencia para sign-off. El resultado de mutación evalúa una sensibilidad útil.
Aprendí algo incómodo al intentar que este ejemplo pareciera menos obvio. Un ser humano puede leer s2 == s2 y descartarlo rápidamente. Muchas debilidades no se anunciarán con tanta claridad. Por eso no quería que la demo dependiera de que el operador detectara una cadena sospechosa. El artefacto verdaderamente útil es el procedimiento: alcanzabilidad, una prueba relevante de eliminación por mutación, COI y una decisión de política que registra su motivo.
Llegué a ver la verificación de mutaciones como una forma disciplinada de rechazar una interpretación demasiado complaciente de una prueba formal. El objetivo no es fabricar un fallo dramático, sino preguntar si la propiedad advertiría un cambio local relevante en el comportamiento que se supone que debe restringir. Cuando no lo hace, el resultado le dice al revisor algo accionable: esta aserción necesita reforzarse o seguir una ruta de revisión diferente antes de poder respaldar el registro de sign-off.
Esta es también la razón por la que el benchmark de la demo necesita una descripción precisa. Su ejecución local con python -m backend.bench obtiene una puntuación de 18/18 frente a un conjunto fijo y etiquetado de aserciones sintéticas, e identifica 6 pruebas formales que la línea base sin compuertas de la propia demo habría aprobado automáticamente sin cuestionar. Esas cifras son una comprobación de reproducibilidad sobre los bancos de pruebas etiquetados de esta demo; no representan una tasa de producción, ni una afirmación general sobre las aserciones creadas por IA, ni una comparación con herramientas formales comerciales.
Dejé de intentar que la compuerta pareciera permisiva
Tuve que tomar una decisión de diseño tras los primeros resultados de la auditoría: suavizar los veredictos retenidos para que el panel pareciera más optimista, o dejar que el panel se negara a certificar lo que no podía defender. Elegí lo segundo porque una revisión real de sign-off necesita la capacidad de distinguir una prueba formal completa de una acotada, un antecedente inalcanzable de una propiedad significativa, y una comprobación débil de una que reacciona ante un comportamiento anómalo relevante. Retener un resultado es un desenlace de revisión, no un callejón sin salida.
Esa elección se refleja en el vocabulario de las políticas. TRUSTWORTHY obtiene el certificado de demostración firmado. BOUNDED-PROVEN, VACUOUS, WEAK, DEAD y VIOLATED preservan diferentes motivos para retener dicho certificado o escalar el resultado. En el banco de pruebas de CDC, por ejemplo, la propiedad más estricta assert (req && !ack) |-> ##1 req resulta VIOLATED y produce una forma de onda concreta de contraejemplo sintético. Ilustra una clase de fallo por transacción perdida o CDC. No dice nada sobre un chip de producción de un cliente.
No veo esto como una propuesta para reemplazar el motor existente de un equipo de verificación. El enfoque para producción es agnóstico al motor: situar una compuerta alrededor del flujo formal existente y hacer que sus criterios de aceptación sean inspeccionables. Los adaptadores para motores reales y la ingesta de RTL se posponen en esta demo. El alcance demostrado es intencionadamente acotado. Ese límite es importante porque mantiene la afirmación proporcional a lo que realmente se está ejecutando.
Ahora quiero el comprobante junto al veredicto
Sigo pensando en el artefacto que necesita una reunión de sign-off cuando el autor de la aserción contó con asistencia de IA. No es una puntuación de confianza del autor: es un registro que detalle qué comprobaciones se ejecutaron, cuál fue el resultado de alcanzabilidad, qué mutaciones se eliminaron, qué contenía el COI y por qué la política permitió o retuvo la certificación. La revisión necesita evidencias que se puedan volver a auditar.
Eso es lo que la demo exporta en signoff_certificate.json: veredictos por propiedad, alcanzabilidad, resultados de mutaciones, COI, registros de contraejemplos cuando corresponda y un campo SHA-256. Construí el certificado como un registro de demostración porque un revisor debería poder reconstruir la decisión sin tener que aceptar un distintivo verde por simple fe. Un certificado debe preservar el camino que condujo a su veredicto.
Y si prefiere verlo en lugar de leerme describiéndolo, aquí está todo funcionando de principio a fin.
Hice que la demo fuera ejecutable para que la reversión de 8/8 a 5/8 pueda inspeccionarse en lugar de repetirse como un eslogan. La conclusión que extraigo es modesta pero sólida: una prueba formal que vale la pena firmar para sign-off incluye evidencias de qué restringió, a qué sobrevivió y por qué alguien puede confiar en ella. El verde sigue siendo útil; simplemente necesita un registro que permita al siguiente revisor decidir si merece avanzar más allá.
