Formal Verification in the CIRCT Open-Source Hardware Design Stack

形式化方法在硬件验证领域已经使用了很多年。然而，现代正式的硬件验证框架通常是专有的、闭源的和昂贵的，而那些不是专有的——例如Yosys-SMTBMC——具有利基目标，并且严重依赖于Verilog（或基于Verilog的SystemVerilog），这是一种具有充分记录的问题和限制（例如不一致的模拟和合成语义）的语言。CIRCT （Circuit IR Compilers and Tools）是来自LLVM社区的开源设计成果，试图将LLVM和MLIR （Multi-Level Intermediate Representation）技术应用于硬件设计。该项目的动机声明认为，上面讨论的许多问题类似地存在于硬件编译领域，并提出许多这些问题可以通过基于LLVM和MLIR方法的公共硬件设计方法来解决。这是引入新的开源验证工具的理想环境，不仅允许广泛的社区访问和贡献，而且还允许与广泛的前端和后端进行交互。这里特别有趣的是MLIR的本质，它允许程序的表示（以及在CIRCT中，电路）在几个抽象级别上分开，这些不同级别之间有降低，或“方言”。这使得它成为形式化验证的一个特别有趣的目标，因为当使用更抽象的方言时，验证可能会大大减少计算密集型。对这些方言的语义所做的假设，然后可以使用较低级方言的更简单的语义来验证。该项目的当前方向是使用SMT求解器和BMC（有界模型检查），通过为IR操作定义适当的语义来验证电路设计上的给定属性，首先是在CIRCT中开发有界模型检查器，这已经在进行中。这作为CIRCT中正式验证框架的基础，最初关注表示基本逻辑范式（如组合逻辑和顺序逻辑）的核心方言。一旦建立了这样的框架，MLIR的本质就为潜在的新优化提供了充足的空间，例如跨多个抽象级别的验证和特定于领域的优化。辩证方法还可能提供有用的模块化方法来提供验证元数据，潜在地创建验证方言。结合起来，理想的结果将是一个公共的、开源的验证框架，它可以应用于广泛的前端和后端，以一种可访问的方式为设计提供强大的信心。

Formal methods have been used in the world of hardware verification for many years. However, modern formal hardware verification frameworks are typically proprietary, closed-source and expensive, and those that are not - Yosys-SMTBMC, for example - have niche targets, and are heavily reliant on Verilog (or SystemVerilog, which is based on Verilog), a language with well-documented issues and limitations (such as inconsistent simulation and synthesis semantics).CIRCT (Circuit IR Compilers and Tools) is an open-source design effort from the LLVM community, attempting to apply LLVM and MLIR (Multi-Level Intermediate Representation) technologies to hardware design. The project's motivation statement argues that many of the issues discussed above exist similarly in the space of hardware compilation and proposes that many of these issues can be tackled with a communal approach to hardware design based on LLVM and MLIR methodology. This is an ideal setting for the introduction of new, open-source verification tools, not only allowing widespread community access and contributions, but also permitting interaction with a wide-range of front- and back- ends. Particularly interesting here is the nature of MLIR, which allows representation of programs (and, within CIRCT, circuits) to be separated across several levels of abstraction, with lowerings between these different levels, or 'dialects'. This makes it a particularly interesting target for formal verification, as verification may prove to be substantially less computation-intensive when working with more abstract dialects. Assumptions made about the semantics of these dialects could then be verified using simpler semantics for lower-level dialects.The current direction of the project is to use SMT solvers and BMC (bounded model checking) to verify given properties on circuit designs by defining appropriate semantics for IR operations, beginning with the development of a bounded model checker within CIRCT, which is already underway. This acts as a foundation for a formal verification framework within CIRCT, initially focussing on core dialects that represent fundamental logical paradigms such as combinatorial and sequential logic. Once such a framework is established, the nature of MLIR provides abundant space for potential novel optimisations, such as verification across multiple levels of abstraction and domain-specific optimisations. The dialectic approach may also offer useful modular ways to provide verification metadata, potentially with the creation of a verification dialect. In combination, the ideal result would be a communal, open-source verification framework that can be applied over a wide range of front- and back-ends to provide strong confidence in designs in an accessible way.