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.

翻译：用于表示和处理验证问题的格式，对于支撑工具、开发者和从业者的生态系统至关重要。优秀的格式既能表示多种类型的问题，又能配备强大的工具链以支持问题的操作与转换，并能随社区共同发展。在硬件验证领域，尤其是硬件模型检查竞赛（HWMCC）中，Btor2格式已成为主导性格式。该格式得到Btor2Tools、验证工具以及Yosys等Verilog设计工具的广泛支持。本文提出一种基于新兴MLIR框架的替代格式与工具链——Btor2MLIR。Btor2MLIR的优势在于复用成熟编译器基础设施中的现有组件，包括解析器、文本与二进制格式、多种中间表示的转换器，以及LLVM的可执行语义。我们期望该格式及配套工具能推动硬件验证领域验证工具及相关工具的快速原型开发。