Btor2MLIR: A Format and Toolchain for Hardware Verification

Imagine que você é um detetive tentando resolver um mistério, mas as pistas estão escritas em um código secreto que apenas alguns especialistas conseguem ler. No mundo da ciência da computação, esse "código secreto" é a linguagem usada para descrever como os chips de computador (hardware) devem se comportar. Engenheiros constroem esses chips para executar tudo, desde o seu telefone até os satélites no espaço, mas se houver mesmo um erro minúsculo no design, todo o sistema pode travar ou agir de forma estranha. Para evitar isso, pesquisadores usam "métodos formais" — ferramentas matemáticas que atuam como corretores ortográficos superpotentes para provar que um design é perfeito antes mesmo de ser construído.

Por muito tempo, esses corretores ortográficos falavam idiomas diferentes. Alguns falavam "BTOR2", um formato popular em competições de hardware, enquanto outros falavam "LLVM-IR", uma linguagem usada por compiladores de software para verificar código. Era como ter um tradutor que só sabia traduzir de francês para inglês, e outro que só sabia de espanhol para inglês. Se você quisesse usar um tradutor de francês para verificar um livro em espanhol, estava sem sorte. Você tinha que construir um novo tradutor do zero toda vez. Este artigo apresenta um novo, mágico tradutor chamado BTOR2MLIR. Ele se posiciona no meio, atuando como uma ponte universal que permite que designs de hardware falem com ferramentas de software sem a necessidade de reinventar a roda toda vez.

O Problema: Muitos Dialetos, Poucas Pontes

No mundo da verificação de hardware, o formato BTOR2 tornou-se a maneira padrão de descrever circuitos para competições como a Hardware Model Checking Competition (HWMCC). Pense no BTOR2 como um dialeto muito específico e eficiente para descrever como um circuito digital conta, soma números ou verifica erros. Ferramentas como o BTORMC são construídas especificamente para ler este dialeto e verificar se o circuito é seguro.

No entanto, o mundo da verificação de software é enorme e poderoso. Ferramentas como o SEAHORN são especialistas em verificar códigos de software escritos na linguagem LLVM-IR. Essas ferramentas são incrivelmente maduras, tendo sido refinadas ao longo de décadas por projetos massivos como a infraestrutura de compilador LLVM. Elas possuem recursos integrados para otimizar código, encontrar bugs e executar simulações.

O problema é que esses dois mundos raramente conversam entre si. Para usar uma poderosa ferramenta de software para verificar um design de hardware, os pesquisadores tinham que escrever tradutores personalizados e únicos. Era como tentar encaixar um pino quadrado em um buraco redondo todas as vezes. Esses tradutores frequentemente tinham que reimplementar recursos básicos (como lidar com números ou loops) que já existiam nas ferramentas de software, levando a um esforio desperdiçado e potenciais erros.

A Solução: O Adaptador Universal (BTOR2MLIR)

Os autores deste artigo, Joseph Tafese, Isabel Garcia-Contreras e Arie Gurfinkel, da Universidade de Waterloo, decidiram construir uma ponte melhor. Eles criaram o BTOR2MLIR, um novo formato e toolchain baseado em MLIR (Multi-Level Intermediate Representation).

Para entender o MLIR, imagine um conjunto de Lego gigante e modular. Em vez de construir um castelo inteiro do zero toda vez que você quiser construir um tipo diferente de casa, o MLIR oferece um conjunto de base de peças (dialetos) que você pode encaixar. Você pode definir uma nova peça de "hardware" que se pareça e aja exatamente como o BTOR2, mas que se encaixe diretamente na estrutura de "software" existente.

Aqui está como a nova ferramenta deles funciona:

1. O Tradutor: Eles construíram um "Dialeto BTOR" dentro do MLIR. Este é uma tradução direta e sem perdas do formato BTOR2. Se você tiver um arquivo BTOR2, o BTOR2MLIR pode transformá-lo neste dialeto MLIR instantaneamente.
2. A Ponte: Como o MLIR é projetado para ser extensível, eles criaram uma "passagem de conversão" que transforma o seu Dialeto BTOR no Dialeto LLVM padrão. Este é o passo mágico. Ele pega a descrição do hardware e a transforma em um formato que ferramentas de software como o SEAHORN podem entender nativamente.
3. O Resultado: O resultado é o LLVM-IR, uma linguagem que motores de verificação de software podem consumir e analisar.

O Experimento: Isso Realmente Funciona?

A equipe não apenas construiu a ponte; eles dirigiram um caminhão através dela para ver se ela aguentava. Eles pegaram uma coleção de benchmarks de hardware do mundo real da competição HWMCC (especificamente os conjuntos de 2019 e 2020) e os passaram pelo novo toolchain.

Primeiro, eles verificaram a corretude. Eles pegaram um arquivo BTOR2, o converteram para o formato MLIR deles e depois converteram de volta para BTOR2. Eles compararam o arquivo original e o arquivo após o processo de ida e volta (round-tripped). O resultado? Eles eram idênticos. As propriedades de segurança (as regras que o circuito deve seguir) foram preservadas perfeitamente. Mesmo em casos complicados onde as ferramentas originais sofreram timeout ou ficaram sem memória, as versões processadas por eles às vezes resolveram o problema, sugerindo que a tradução não introduziu erros.

Em seguida, eles testaram o desempenho. Eles conectaram sua ferramenta ao SEAHORN, um famoso model checker de software, e ao BOOLECTOR, um solver rápido. Eles compararam este novo pipeline "híbrido" contra o BTORMC, a ferramenta padrão ouro que foi construída especificamente para o BTOR2.

Os resultados foram surpreendentes e encorajadores:

• Velocidade: Em muitos casos, o pipeline híbrido (BTOR2MLIR + SEACHORN + BOOLECTOR) foi competitivo e, às vezes, mais rápido que a ferramenta dedicada BTORMC. Por exemplo, na categoria "19/mann" de benchmarks, a abordagem híbrida resolveu 44 instâncias em cerca de 3.190 segundos, enquanto o BTORMC levou mais tempo ou sofreu timeout em mais instâncias.
• Flexibilidade: A ferramenta lidou com sucesso com operações complexas como divisão e vetores de bits, provando que as "peças de Lego" do MLIR podem realizar o trabalho pesado da lógica de hardware.
• Limitações: Os autores foram honestos sobre o que sua ferramenta ainda não consegue fazer. Atualmente, ela suporta vetores de bits e arrays, mas ainda não lida com restrições de "fairness" (equidade) e "justice" (justiça) — regras sobre como um sistema se comporta ao longo do tempo infinito. Além disso, embora funcione bem, não esmagou completamente as ferramentas dedicadas de hardware em todas as categorias; foi um forte concorrente, não um substituto total.

Por Que Isso Importa

O artigo não afirma ter resolvido toda a verificação de hardware. Em vez disso, sugere uma nova forma de pensar. Ao usar a infraestrutura madura e robusta do compilador LLVM (que alimenta ferramentas para tudo, desde videogames até navegadores web), pesquisadores de hardware podem parar de reinventar a roda.

Os autores mostram que você pode pegar um design de hardware, traduzi-lo para uma linguagem universal e, então, usar ferramentas de software poderosas e existentes para verificá-lo. Isso abre as portas para a prototipagem rápida. Se um pesquisador quiser testar uma nova técnica de verificação, ele não precisa construir um motor inteiro novo; ele só precisa conectar sua ideia à estrutura do MLIR.

No futuro, a equipe planeja conectar esta ponte a ainda mais ferramentas, como o KLEE (um motor de execução simbólica) e o LIBFUZZER (uma ferramenta de fuzzing), que são atualmente usados para software, mas poderiam revolucionar a forma como encontramos bugs em hardware. Eles também planejam gerar outros formatos como AIGER e SMT-LIB.

Em última análise, o BTOR2MLIR é uma prova de conceito de que os muros entre a verificação de hardware e software estão caindo. Sugere que, ao falar uma linguagem comum, podemos tornar nosso mundo digital mais seguro, rápido e fácil de construir.