A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking

1. El Problema

La verificación formal de hardware, específicamente mediante el algoritmo IC3/PDR (Inductive Clause-based 3 / Property Directed Reachability), es la técnica más avanzada para verificar propiedades de seguridad en diseños RTL. Sin embargo, la eficiencia de IC3 depende críticamente de la generalización inductiva: el proceso de convertir un contraejemplo a la inducción (CTI) en una cláusula más amplia que bloquee un conjunto mayor de estados no alcanzables.

• Limitación actual: Las estrategias de generalización existentes (como CtgDown, EXCTG o DynAMic) suelen ser fijas o se basan en reglas de conmutación estáticas y predefinidas.
• El desafío: El entorno de verificación es altamente dinámico y no estacionario. Un CTI generado en un nivel de marco (frame) bajo con una densidad de cláusulas específica requiere una estrategia diferente a uno generado más tarde en la prueba.
  • Una generalización demasiado agresiva puede generar cláusulas que no se pueden propagar a marcos superiores, llenando la cola de obligaciones de prueba (PO queue) y desperdiciando recursos.
  • Una generalización demasiado conservadora bloquea muy pocos estados, lo que lleva a una convergencia lenta.
• Brecha: No existe un mecanismo ligero y en línea que pueda adaptar la estrategia de generalización en tiempo real basándose en el estado evolutivo de la prueba, sin incurrir en el alto costo computacional de los modelos de aprendizaje profundo entrenados offline.

2. Metodología: A-IC3

Los autores proponen A-IC3, un marco ligero basado en aprendizaje que trata la selección de la estrategia de generalización como un problema de Brazo Multi-Arma Contextual (Contextual Multi-Armed Bandit - MAB).

Componentes Clave:

1. Formulación como MAB Contextual:

   • Agentes: Un agente PA-LinUCB (Proof-Aware Linear Upper Confidence Bound) toma las decisiones.
   • Brazos (Arms): Cada "brazo" representa una configuración específica de estrategia de generalización con diferentes niveles de agresividad (desde Básico hasta Agresivo). Estas configuraciones controlan parámetros como la profundidad de recursión, el número de intentos de CTG (Counterexample to Generalization) y el presupuesto de EXCTG.
   • Contexto ($x_t$): Antes de cada generalización, el sistema extrae un vector de características del estado interno de IC3. Este vector combina:
     • Características Locales: Tamaño del cubo, profundidad de recursión actual, puntuación de actividad del CTI y longitud de la cola de obligaciones de prueba.
     • Características Globales: Nivel del marco actual, nivel del marco frontera, saturación del marco (número de cláusulas) y tasa de crecimiento de la cola.
   • Recompensa ($r_t$): Se calcula después de intentar propagar la cláusula generalizada. Combina:
     • Reducción de tamaño: Qué tanto se simplificó la cláusula.
     • Calidad de empuje (Push): Si la cláusula se propagó exitosamente a marcos superiores y a qué distancia.
     • Bonificaciones/Penalizaciones: Por eventos extremos (ej. alcanzar la frontera, generalización excesiva).

2. Integración en IC3:

   • El agente PA-LinUCB se integra directamente en el bucle interno de bloqueo de IC3.
   • En cada paso de generalización, el agente observa el contexto, selecciona el brazo óptimo (estrategia) utilizando el algoritmo LinUCB, ejecuta la generalización, observa el resultado y actualiza sus parámetros en línea.
   • No requiere entrenamiento previo ni conjuntos de datos externos; aprende durante la ejecución de la verificación.

3. Diseño de Estrategias (Brazos):

   • Se definen cuatro estrategias estáticas (Básico, Conservador, Equilibrado, Agresivo) y tres dinámicas que ajustan sus parámetros basándose en la puntuación de actividad del CTI. El agente elige entre estas opciones en tiempo real.

3. Contribuciones Clave

1. Primera adaptación basada en aprendizaje: A-IC3 es el primer controlador adaptativo basado en aprendizaje para la selección de estrategias de generalización dentro de IC3.
2. Representación de contexto consciente de la prueba: Diseñaron un vector de características que captura tanto la dificultad local del CTI como el progreso global de la prueba, permitiendo que un agente estándar (LinUCB) guíe decisiones complejas con sobrecarga mínima.
3. Función de recompensa multifacética: Crearon una función de recompensa que equilibra la reducción de tamaño de la cláusula con la capacidad de propagación, incentivando estrategias que no solo son fuertes, sino también útiles para el avance de la prueba.
4. Integración eficiente: Demostraron que un algoritmo de banda multi-brazo puede ejecutarse millones de veces dentro del bucle interno de IC3 sin degradar el rendimiento, superando las limitaciones de los enfoques de aprendizaje profundo pesados.

4. Resultados Experimentales

Los autores evaluaron A-IC3 implementado sobre rIC3 (el verificador de estado actual) en una suite de 914 instancias extraídas de las colecciones HWMCC'20, HWMCC'24 y HWMCC'25.

• Comparativa: Se comparó contra tres líneas base:
  1. rIC3-Standard (configuración por defecto).
  2. rIC3-CtgDown (estrategia estática mejorada).
  3. rIC3-DynAMic (conmutación dinámica predefinida).
• Métricas de Éxito:
  • Instancias Resueltas: A-IC3 resolvió 653 casos en total, superando a la línea base estándar en 50 casos (+35 en casos seguros, +15 en casos inseguros). Esto representa un aumento significativo sobre las otras variantes.
  • Puntuación PAR-2: Logró la puntuación PAR-2 más baja (2151.76), mejorando en un rango de 194 a 389 puntos respecto a las líneas base. Una puntuación PAR-2 más baja indica un mejor rendimiento global (tiempo promedio de resolución).
  • Tiempo de Ejecución: En casos no triviales (difíciles), A-IC3 mostró el tiempo promedio de ejecución más bajo.
• Análisis de Curvas Cactus: Las gráficas muestran que A-IC3 resuelve instancias difíciles que las líneas base no pueden resolver dentro del límite de tiempo (3600s), y mantiene un rendimiento competitivo en casos fáciles, demostrando que la sobrecarga del aprendizaje es insignificante.
• Niveles de Terminación: A-IC3 tiende a terminar en niveles de marco más bajos que las líneas base, lo que indica que encuentra invariantes inductivos o contraejemplos más rápido, mejorando la trayectoria de la prueba.

5. Significado e Impacto

• Paradigma de Verificación: El trabajo marca un cambio de las heurísticas estáticas a procesos de generalización adaptativos y guiados por el aprendizaje.
• Eficiencia Práctica: Demuestra que el aprendizaje automático ligero (Online MAB) es viable y beneficioso en el núcleo de algoritmos de verificación formal, donde la latencia es crítica, evitando los costos de los modelos grandes de Deep Learning.
• Escalabilidad: Al mejorar la calidad de las cláusulas generadas, A-IC3 acelera la convergencia de la verificación, permitiendo verificar diseños más complejos o reducir el tiempo de validación en flujos de diseño industrial.
• Futuro: Abre la puerta a integrar mecanismos de aprendizaje en otras fases de la verificación formal, sugiriendo que la "inteligencia" en la selección de estrategias puede ser tan importante como la potencia del motor SAT/SMT subyacente.

En resumen, A-IC3 resuelve el problema de la rigidez en la generalización de IC3 mediante un agente de aprendizaje en línea que ajusta dinámicamente su estrategia según el contexto de la prueba, logrando mejoras sustanciales en la capacidad de resolución y la eficiencia computacional.