Formal Verification in the CIRCT Open-Source Hardware Design Stack

点击翻译按钮获取中文摘要

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.