Btor2MLIR: A Format and Toolchain for Hardware Verification

Imagina que eres un detective tratando de resolver un misterio, pero las pistas están escritas en un código secreto que solo unos pocos especialistas pueden leer. En el mundo de la informática, este "código secreto" es el lenguaje utilizado para describir cómo se supone que deben comportarse los chips de computadora (el hardware). Los ingenieros construyen estos chips para que ejecuten desde tu teléfono hasta los satélites en el espacio, pero si hay incluso un error minúsculo en el diseño, todo el sistema puede colapsar o actuar de forma extraña. Para prevenir esto, los investigadores utilizan "métodos formales" —herramientas matemáticas que actúan como superpotentes correctores ortográficos para demostrar que un diseño es perfecto antes de que sea construido.

Durante mucho tiempo, estos correctores ortográficos hablaban diferentes idiomas. Algunos hablaban "BTOR2", un formato popular en las competencias de hardware, mientras que otros hablaban "LLVM-IR", un lenguaje utilizado por los compiladores de software para verificar el código. Era como tener un traductor que solo sabía traducir de francés a inglés, y otro que hablaba de español a inglés. Si querías usar un traductor de francés para revisar un libro en español, no tenías suerte. Tenías que construir un traductor completamente nuevo desde cero cada vez. Este artículo presenta un nuevo traductor mágico llamado BTOR2MLIR. Se sitúa en el medio, actuando como un puente universal que permite que los diseños de hardware hablen con las herramientas de software sin necesidad de reinventar la rueda cada vez.

El Problema: Demasiados dialectos, no suficientes puentes

En el mundo de la verificación de hardware, el formato BTOR2 se ha convertido en la forma estándar de describir circuitos para competencias como la Hardware Model Checking Competition (HWMCC). Piensa en BTOR2 como un dialecto muy específico y eficiente para describir cómo un circuito digital cuenta, suma números o verifica errores. Herramientas como BTORMC están construidas específicamente para leer este dialecto y verificar si el circuito es seguro.

Sin embargo, el mundo de la verificación de software es enorme y poderoso. Herramientas como SEAHORN son expertas en verificar código de software escrito en el lenguaje LLVM-IR. Estas herramientas son increíblemente maduras, habiendo sido refinadas durante décadas por proyectos masivos como la infraestructura del compilador LLVM. Tienen funciones integradas para optimizar el código, encontrar errores y ejecutar simulaciones.

El problema es que estos dos mundos rara vez se comunican entre sí. Para usar una poderosa herramienta de software para verificar un diseño de hardware, los investigadores tenían que escribir traductores personalizados y únicos. Era como intentar encajar una pieza cuadrada en un agujero redondo cada vez. Estos traductores a menudo tenían que reimplementar funciones básicas (como el manejo de números o bucles) que ya existían en las herramientas de software, lo que llevaba a un esfuerzo desperdiciado y a posibles errores.

La Solución: El adaptador universal (BTOR2MLIR)

Los autores de este artículo, Joseph Tafese, Isabel Garcia-Contreras y Arie Gurfinkel de la Universidad de Waterloo, decidieron construir un puente mejor. Crearon BTOR2MLIR, un nuevo formato y cadena de herramientas basado en MLIR (Multi-Level Intermediate Representation).

Para entender MLIR, imagina un juego de Lego gigante y modular. En lugar de construir un castillo entero desde cero cada vez que quieres construir un tipo diferente de casa, MLIR te da un conjunto base de ladrillos (dialectos) que puedes ensamblar. Puedes definir un nuevo "lercillo de hardware" que se vea y actúe exactamente como BTOR2, pero que se conecte directamente a la estructura de Lego de "software" existente.

Así es como funciona su nueva herramienta:

1. El Traductor: Construyeron un "Dialecto BTOR" dentro de MLIR. Esta es una traducción directa y sin pérdida del formato BTOR2. Si tienes un archivo BTOR2, BTOR2MLIR puede convertirlo en este dialecto de MLIR instantáneamente.
2. El Puente: Debido a que MLIR está diseñado para ser extensible, crearon un "paso de conversión" que convierte su Dialecto BTOR en el Dialecto LLVM estándar. Este es el paso mágico. Toma la descripción del hardware y la convierte en un formato que las herramientas de software como SEAHORN pueden entender de forma nativa.
3. El Resultado: El producto es LLVM-IR, un lenguaje que los motores de verificación de software pueden absorber y analizar.

El Experimento: ¿Realmente funciona?

El equipo no solo construyó el puente; condujeron un camión a través de él para ver si resistía. Tomaron una colección de pruebas de rendimiento (benchmarks) de hardware del mundo real de la competencia HWMCC (específicamente los conjuntos de 2020 y 2019) y las pasaron por su nueva cadena de herramientas.

Primero, verificaron la corrección. Tomaron un archivo BTOR2, lo convirtieron a su formato MLIR y luego lo convirtieron de vuelta a BTOR2. Compararon el archivo original con el archivo tras el proceso de ida y vuelta (round-tripped). ¿El resultado? Eran idénticos. Las propiedades de seguridad (las reglas que el circuito debe seguir) se preservaron perfectamente. Incluso en casos complicados donde las herramientas originales agotaron el tiempo o la memoria, sus versiones procesadas a veces resolvieron el problema, lo que sugiere que la traducción no introdujo errores.

Después, probaron el rendimiento. Conectaron su herramienta a SEAHORN, un famoso verificador de modelos de software, y a BOOLECTOR, un solver rápido. Compararon este nuevo flujo de trabajo "híbrido" contra BTORMC, la herramienta estándar de oro que fue construida específicamente para BTOR2.

Los resultados fueron sorprendentes y alentadores:

• Velocidad: En muchos casos, el flujo de trabajo híbrido (BTOR2MLIR + SEACHORN + BOOLECTOR) fue competitivo y, a veces, más rápido que la herramienta dedicada BTORMC. Por ejemplo, en la categoría "19/mann" de los benchmarks, el enfoque híbrido resolvió 44 instancias en unos 3,190 segundos, mientras que BTORMC tardó más tiempo o se quedó sin tiempo en más instancias.
• Flexibilidad: La herramienta manejó con éxito operaciones complejas como la división y los vectores de bits, demostizando que los "ladrillos de Lego" de MLIR podían realizar el trabajo pesado de la lógica de hardware.
• Limitaciones: Los autores fueron honestos sobre lo que su herramienta aún no puede hacer. Actualmente soporta vectores de bits y arreglos, pero aún no maneja restricciones de "justicia" (fairness) y "justicia" (justice) (reglas sobre cómo se comporta un sistema a lo largo del tiempo infinito). Además, aunque funciona bien, no superó por completo a las herramientas dedicadas de hardware en cada categoría; fue un fuerte contendiente, no un reemplazo total.

Por qué esto es importante

El artículo no pretende haber resuelto toda la verificación de hardware. En cambio, sugiere una nueva forma de pensar. Al utilizar la infraestructura madura y robusta del compilador LLVM (que impulsa herramientas para todo, desde videojuegos hasta navegadores web), los investigadores de hardware pueden dejar de reinventar la rueda.

Los autores demuestran que puedes tomar un diseño de hardware, traducirlo a un lenguaje universal y luego usar potentes herramientas de software existentes para verificarlo. Esto abre la puerta al prototipado rápido. Si un investigador quiere probar una nueva técnica de verificación, no necesita construir un motor nuevo; solo necesita conectar su idea al marco de trabajo de MLIR.

En el futuro, el equipo planea conectar este puente a aún más herramientas, como KLEE (un motor de ejecución simbólica) y LIBFUZZER (una herramienta de fuzzing), que actualmente se usan para software pero podrían revolucionar la forma en que encontramos errores en el hardware. También planean generar otros formatos como AIGER y SMT-LIB.

En última instancia, BTOR2MLIR es una prueba de concepto de que los muros entre la verificación de hardware y software se están derrumbando. Sugiere que, al hablar un lenguaje común, podemos hacer que nuestro mundo digital sea más seguro, rápido y fácil de construir.