MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering

Este artigo apresenta o MPBMC, uma abordagem híbrida que utiliza embeddings de redes neurais gráficas e estatísticas de tempo de execução para agrupar funcionalmente propriedades de hardware, acelerando significativamente a verificação formal por meio de Model Checking Limitado (BMC) em benchmarks do HWMCC.

O essencial

Imagine que você é um detetive encarregado de resolver 50 crimes diferentes em uma cidade gigante (que chamaremos de "Circuito Elétrico"). Cada crime tem suas próprias pistas, mas muitos deles acontecem nos mesmos bairros, usam os mesmos tipos de armas ou seguem padrões semelhantes.

Aqui está o que o artigo MPBMC propõe, explicado de forma simples:

O Problema: O Caos da Investigação Individual

Antes dessa nova ideia, os investigadores (os softwares de verificação) faziam uma de duas coisas:

1. Investigavam um crime de cada vez: Isso era lento e repetitivo. Eles gastavam tempo revisando as mesmas ruas e construindo o mesmo tipo de arquivo de evidências para cada caso, sem aproveitar o que aprenderam no caso anterior.
2. Investigavam todos os crimes juntos, ao mesmo tempo: Isso parecia eficiente, mas era um desastre. Se um caso fosse muito difícil, ele "atropelava" os outros, e o escritório de detetives ficava cheio de papéis confusos (chamados de "cláusulas de conflito"). O trabalho ficava mais lento do que se fizessem um por um.

O grande desafio: Como agrupar os crimes de forma inteligente? Você não quer juntar um roubo de banco com um caso de furto de bicicleta só porque ambos aconteceram na mesma rua. Você quer juntar crimes que são funcionalmente parecidos (mesmo modus operandi), para que as pistas de um ajudem a resolver o outro.

A Solução: O "Detetive com Cérebro de IA"

Os autores criaram um sistema chamado MPBMC. Pense nele como um Gerente de Detetives superinteligente que usa uma tecnologia chamada Redes Neurais Gráficas (GNN).

Aqui está como funciona, passo a passo, com analogias:

1. A Fase de Treinamento (O "Livro de Casos Antigos")

Antes de começar a investigar a cidade nova, o sistema olha para um arquivo gigante de casos antigos (bancos de dados de circuitos já verificados).

• Ele usa a IA para ler esses casos e criar um "mapa mental" (chamado de embedding) de como cada crime se parece.
• Ele não olha apenas para a localização (a estrutura), mas para a essência do crime (a função). É como se ele dissesse: "Este roubo de carro e aquele assalto a joalheria são muito parecidos na forma como foram planejados, mesmo que tenham ocorrido em lugares diferentes."
• O sistema aprende quais grupos de crimes, quando investigados juntos, ajudam uns aos outros a serem resolvidos mais rápido. Ele cria um "guia de melhores pares".

2. A Fase de Investigação (O "Novo Caso")

Agora, chega um novo circuito (uma nova cidade) com novos crimes (propriedades) para verificar.

• O Reconhecimento: O sistema olha para a nova cidade e diz: "Ei, essa cidade se parece muito com a 'Cidade X' dos nossos arquivos antigos."
• O Mapeamento: Ele pega os "melhores pares" que funcionaram na Cidade X e aplica na nova cidade. Ele diz: "Vamos investigar o Crime A e o Crime B juntos, porque na Cidade X eles se ajudaram mutuamente."
• A Investigação Conjunta: O detetive (o verificador) investiga esses grupos juntos. Como os crimes são parecidos, as pistas encontradas no Crime A ajudam a desvendar o Crime B instantaneamente.

O Resultado: Menos Papelada, Mais Rapidez

O artigo mostra que, ao fazer isso:

• Menos "Papelada Confusa": Em vez de gerar milhares de notas soltas e contraditórias (cláusulas de conflito), o grupo gera menos notas, mas mais úteis. É como se todos os detetives estivessem falando a mesma língua.
• Mais Profundidade: Eles conseguem investigar mais fundo (chegar a mais "quadros" ou frames) antes de ficar sem tempo. É como conseguir resolver um caso que levaria 10 horas em apenas 2 horas.
• Vitória sobre o Antigo: Nos testes com circuitos reais (os benchmarks do HWMCC), esse método foi muito mais rápido e eficiente do que os métodos antigos que apenas olhavam para a estrutura física dos circuitos ou tentavam adivinhar os grupos aleatoriamente.

Resumo em uma Frase

O MPBMC é como ter um detetive sábio que, antes de sair para investigar, lê a história de todos os casos passados para saber exatamente quem deve trabalhar com quem, garantindo que a equipe resolva os crimes mais difíceis juntos, aproveitando as descobertas de um para resolver o outro, economizando tempo e energia.

Resumo técnico

Resumo Técnico: MPBMC

1. O Problema

A verificação formal de designs de hardware com múltiplas propriedades (Multi-Property Verification - MPV) enfrenta um dilema clássico:

• Verificação Individual: Verificar propriedades uma a uma evita conflitos, mas perde a oportunidade de reutilizar informações e cláusulas aprendidas (conflict clauses), resultando em computação redundante.
• Verificação Conjunta (Tudo de uma vez): Verificar todas as propriedades simultaneamente pode levar a um desequilíbrio, onde propriedades difíceis de verificar "atrapalham" o progresso das mais fáceis, gerando um número excessivo de cláusulas de conflito e sobrecarregando o solver SAT.

O desafio central é criar agrupamentos (clusters) de propriedades eficazes. O objetivo é agrupar propriedades que são funcionalmente similares (compartilhando partes significativas da lógica do design, conhecidas como Cone of Influence - COI) para que a aprendizagem de cláusulas de conflito em uma propriedade beneficie as outras no mesmo grupo, acelerando a verificação global. Métodos existentes baseados apenas em similaridade estrutural (COI) ou estatísticas de tempo de execução têm limitações na captura de similaridades funcionais semânticas.

2. Metodologia (MPBMC)

Os autores propõem uma abordagem híbrida que combina Redes Neurais de Grafos (GNN) para representação funcional de circuitos com estatísticas de tempo de execução. O framework, chamado MPBMC, opera em duas fases principais:

Fase 1: Preparação de Dados Offline (Treinamento e Análise)

• Base de Dados: Utiliza um conjunto de designs de referência (benchmarks) já verificados.
• Representação Funcional: Utiliza o modelo DeepGate2 (DG2), uma GNN especializada, para gerar embeddings (vetores de representação) dos COIs de cada propriedade. Isso captura a semântica funcional da lógica, indo além da simples estrutura.
• Construção de Clusters: Aplica algoritmos de clustering (K-means e K-medoids) sobre os embeddings funcionais para identificar grupos de propriedades similares.
• Identificação de "Clusters Influenciadores":
  • Executa BMC (Bounded Model Checking) em cada cluster gerado.
  • Calcula uma métrica de Ganho (Gain) para cada propriedade comparando o desempenho em execução isolada vs. execução em cluster.
  • Define um "Cluster Influenciador" para cada propriedade: o grupo onde ela obtém o maior benefício (ex: transição de UNDET para SAT, ou aumento da profundidade de desdobramento).
  • Nota Importante: As propriedades podem pertencer a múltiplos clusters, mas o sistema identifica qual cluster é o "ótimo" para cada uma.

Fase 2: Verificação Online (Aplicação)

• Entrada: Um design desconhecido ($\hat{U}$) com um conjunto de propriedades a verificar.
• Busca de Similaridade:
  1. Filtra designs da base de dados offline com número de propriedades similar ao de $\hat{U}$.
  2. Identifica o design de referência ($B$) mais similar a $\hat{U}$ comparando o tamanho dos COIs após o desdobramento (unfolding).
  3. Mapeia as propriedades de $\hat{U}$ para as propriedades mais similares em $B$.
• Aplicação de Clusters: Utiliza os "Clusters Influenciadores" aprendidos offline para o design $B$ e os aplica ao design $\hat{U}$ através do mapeamento de propriedades.
• Execução: O verificador BMC executa os grupos de propriedades conforme definido pelos clusters otimizados, aproveitando o tempo de execução compartilhado e a aprendizagem de cláusulas mútua.

3. Principais Contribuições

• Uso de GNN para Clustering Funcional: É a primeira proposta (segundo o contexto do artigo) a utilizar embeddings de GNN (especificamente DG2) para capturar similaridades funcionais semânticas entre propriedades de hardware, superando métodos puramente estruturais.
• Estratégia Híbrida Offline/Online: Combina a inteligência de dados históricos (offline) com estatísticas de tempo de execução (online) para guiar a verificação de novos designs.
• Clusters Não-Disjuntos: Diferente de abordagens tradicionais que forçam propriedades a grupos exclusivos, o método permite que uma propriedade pertença a múltiplos grupos, selecionando dinamicamente o grupo que oferece o maior ganho de desempenho.
• Métrica de Ganho Robusta: Define uma métrica de avaliação que considera transições de estado (ex: de UNDET para SAT, ou aumento da profundidade máxima de desdobramento) para determinar a eficácia de um cluster.

4. Resultados Experimentais

Os experimentos foram realizados em 30 benchmarks do HWMCC 2012-13, utilizando o verificador ABC com o motor bmc3g.

• Desempenho: O método MPBMC demonstrou ganhos significativos na profundidade de desdobramento (UNDET depth), que é a métrica principal para designs onde não se encontra contra-exemplo (CEX).
  • O ganho médio variou de 13,61% a 430,23%.
  • O ganho máximo atingido foi de 2647,76% em alguns casos.
• Comparação com o Estado da Arte: O MPBMC superou métodos de agrupamento estrutural recentes (referências [15], [16]) em 8 dos 10 casos de teste analisados.
• Eficiência de Cláusulas: A análise de Cláusulas de Conflito (Conflict Clauses - CC) mostrou que o MPBMC gera significativamente menos cláusulas de conflito por quadro (frame) em comparação com a verificação isolada, indicando uma aprendizagem de cláusulas mais eficiente e menos redundante.
• Casos de Sucesso: O método conseguiu formar clusters e obter resultados em designs complexos (como o 6s329 com ~1.7 milhão de portas AND) onde as técnicas concorrentes falharam em gerar qualquer cluster útil.

5. Significado e Impacto

O trabalho representa um avanço significativo na escalabilidade da verificação formal de hardware. Ao integrar técnicas de Aprendizado de Máquina (Deep Learning) com métodos formais tradicionais (BMC/SAT), os autores demonstram que:

1. A similaridade funcional (semântica) é um fator crítico para agrupar propriedades, muitas vezes mais importante que a similaridade estrutural bruta.
2. O uso de representações aprendidas por GNN permite automatizar a criação de estratégias de verificação complexas, reduzindo a necessidade de heurísticas manuais.
3. A abordagem oferece um caminho viável para lidar com designs de hardware cada vez mais complexos, onde a verificação de múltiplas propriedades simultaneamente se torna computacionalmente proibitiva sem uma estratégia de agrupamento inteligente.

Em suma, o MPBMC transforma a verificação multi-propriedade de um processo de "tentativa e erro" ou baseado em estrutura simples para um processo guiado por dados e inteligência artificial, resultando em economia de tempo computacional e recursos.