Formal Verification in the CIRCT Open-Source Hardware Design Stack

CIRCT 开源硬件设计堆栈中的形式验证

• 批准号: 2737542
• 金额: --
• 依托单位: University of Edinburgh
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2022
• 资助国家: 英国
• 起止时间: 2022 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2737542
• 关键词: Formal; Verification; CIRCT; Open; Source

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.

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