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

Resumo Técnico: A-IC3

1. O Problema

A verificação formal de hardware, especificamente através do algoritmo IC3/PDR (Property Directed Reachability), é a técnica mais avançada (SOTA) para verificar propriedades de segurança em designs RTL. No entanto, a eficiência do IC3 depende criticamente de uma etapa chamada generalização indutiva.

Nesta etapa, o algoritmo tenta generalizar um "contraexemplo à indução" (CTI) — um estado que leva a um estado inválido — em uma cláusula lógica que bloqueia um conjunto maior de estados indesejados. O desafio central é o trade-off entre:

• Generalização Agressiva: Remove muitos literais, criando cláusulas fortes que bloqueiam muitos estados, mas que podem não ser válidas em frames superiores (não podem ser "empurradas" ou pushed), gerando novas obrigações de prova e aumentando o custo computacional.
• Generalização Conservadora: Mantém muitos literais, criando cláusulas fracas que bloqueiam poucos estados, levando a uma convergência lenta e à geração de muitos CTIs similares.

Abordagens existentes (como CtgDown, EXCTG e DynAMic) utilizam estratégias fixas ou regras de troca estáticas e pré-definidas. Elas não conseguem se adaptar dinamicamente ao contexto mutável da verificação (nível do frame, densidade de cláusulas, complexidade do CTI), o que limita a qualidade das cláusulas geradas e a performance global do verificador.

2. Metodologia: A-IC3

Os autores propõem o A-IC3, um framework leve baseado em aprendizado de máquina que trata a seleção de estratégias de generalização como um problema de Bandit Multibras Contextual (Contextual Multi-Armed Bandit - MAB).

Componentes Principais:

• Formulação como MAB Contextual:

  • Braços (Arms): O sistema possui um conjunto de estratégias de generalização pré-definidas, variando de conservadoras a agressivas. Cada estratégia é um "braço" com configurações diferentes de parâmetros (ex: profundidade de recursão, número de tentativas de CTG, orçamento de literal dropping).
  • Agente de Decisão: Utiliza o algoritmo LinUCB (Linear Upper Confidence Bound), adaptado para o contexto de prova, denominado PA-LinUCB (Proof-Aware LinUCB).

• Vetor de Contexto (Proof-Aware Context):
  Antes de cada generalização, o sistema extrai um vetor de características ($x_t$) que descreve o estado atual da prova no IC3. Este vetor combina:

  • Características Locais: Tamanho do cubo (CTI), profundidade da pilha de chamadas Block, pontuação de atividade do CTI e comprimento da fila de obrigações de prova (PO queue).
  • Características Globais: Nível do frame atual, nível do frame de fronteira, saturação do frame (número de cláusulas) e taxa de crescimento da fila de obrigações.
  • Essas métricas são normalizadas para permitir que o agente entenda a dificuldade local e o progresso global.

• Função de Recompensa:
  Após a generalização e a tentativa de propagação (push) da cláusula, o agente recebe uma recompensa ($r_t$) composta por:

  1. Redução de Tamanho ($R_s$): Medida de quão bem a cláusula foi simplificada.
  2. Qualidade de Propagação ($R_p$): Se a cláusula foi bem-sucedida ao ser movida para frames superiores.
  3. Bônus/Penalidades ($R_b$): Recompensas extras por eventos extremos (ex: alcançar a fronteira da prova) ou penalidades por generalização excessiva (cláusula forte mas não propagável).

• Aprendizado Online:
  O agente atualiza seus parâmetros em tempo real após cada passo de generalização, aprendendo quais estratégias funcionam melhor em quais contextos de prova, sem necessidade de treinamento offline ou grandes conjuntos de dados.

3. Contribuições Chave

1. Primeiro Controlador Adaptativo Baseado em Aprendizado para IC3: O A-IC3 é a primeira abordagem a modelar a seleção de estratégias de generalização no IC3 como um problema de decisão contextual, substituindo heurísticas estáticas por um controlador dinâmico.
2. Representação de Contexto e Recompensa Específicas para Prova: Desenvolvimento de um vetor de contexto que captura tanto a dificuldade local do CTI quanto o progresso global da prova, e uma função de recompensa que equilibra a força da cláusula com sua capacidade de propagação.
3. Integração Leve e Eficiente: A implementação utiliza o algoritmo LinUCB, que possui custo computacional baixo, permitindo que a decisão seja tomada milhões de vezes dentro do loop interno do IC3 sem sobrecarregar o verificador.
4. Desempenho Superior em Benchmarks Reais: Validação em uma suíte de 914 instâncias (HWMCC'20, '24, '25) integradas ao verificador de ponta rIC3.

4. Resultados Experimentais

Os experimentos foram realizados em 914 instâncias de benchmarks do HWMCC, comparando o A-IC3 com três baselines:

• rIC3-Standard (configuração padrão).
• rIC3-CtgDown (generalização baseada em CTG).
• rIC3-DynAMic (troca dinâmica baseada em regras fixas).

Principais Métricas:

• Instâncias Resolvidas: O A-IC3 resolveu 653 casos no total, superando o rIC3-Standard em 50 casos (+35 casos seguros e +15 casos inseguros).
• Pontuação PAR-2: O A-IC3 alcançou a melhor pontuação PAR-2 (média ponderada de tempo de execução), com uma melhoria de 194,72 a 389,29 pontos em relação às baselines.
• Eficiência em Casos Difíceis: Em instâncias que não foram resolvidas em 100 segundos (casos não triviais), o A-IC3 demonstrou ganhos significativos, resolvendo casos que as outras configurações não conseguiam dentro do limite de tempo (3600s).
• Nível de Terminação: O A-IC3 tende a convergir em níveis de frame mais baixos, indicando que as cláusulas geradas são mais eficazes para fechar o "gap" indutivo mais rapidamente.

5. Significado e Impacto

O trabalho demonstra que a integração de técnicas de aprendizado de máquina leves e online (como Bandits Contextuais) na verificação formal de hardware é viável e altamente benéfica.

• Superação de Limitações Estáticas: O A-IC3 prova que não existe uma única heurística de generalização ótima para todos os casos; a estratégia deve ser adaptada dinamicamente ao estado da prova.
• Baixo Custo de Overhead: Diferente de abordagens baseadas em Redes Neurais Profundas (que exigem treinamento pesado e têm alto custo de inferência), o A-IC3 opera com custo computacional mínimo, tornando-o prático para uso industrial.
• Nova Direção de Pesquisa: Abre caminho para o uso de agentes de decisão online para otimizar outras fases da verificação formal, movendo-se de métodos puramente heurísticos para métodos guiados por dados em tempo real.

Em resumo, o A-IC3 transforma a generalização indutiva de um processo estático em um processo adaptativo e inteligente, resultando em verificadores de modelo mais rápidos e capazes de resolver problemas de hardware mais complexos.