Btor2MLIR: A Format and Toolchain for Hardware Verification

TL;DR

Btor2MLIR introduces a new hardware verification format and toolchain based on MLIR, aiming to enhance interoperability, reuse, and rapid development of verification tools in hardware design.

Contribution

It presents an alternative to the Btor2 format using MLIR, leveraging existing compiler infrastructure for improved hardware verification tooling.

Findings

Supports multiple verification problem types

Enables reuse of compiler components

Facilitates rapid prototyping of verification tools

Abstract

Formats for representing and manipulating verification problems are extremely important for supporting the ecosystem of tools, developers, and practitioners. A good format allows representing many different types of problems, has a strong toolchain for manipulating and translating problems, and can grow with the community. In the world of hardware verification, and, specifically, the Hardware Model Checking Competition (HWMCC), the Btor2 format has emerged as the dominating format. It is supported by Btor2Tools, verification tools, and Verilog design tools like Yosys. In this paper, we present an alternative format and toolchain, called Btor2MLIR, based on the recent MLIR framework. The advantage of Btor2MLIR is in reusing existing components from a mature compiler infrastructure, including parsers, text and binary formats, converters to a variety of intermediate representations, and executable semantics of LLVM. We hope that the format and our tooling will lead to rapid prototyping of verification and related tools for hardware verification.