K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs

TL;DR

K-CIRCT introduces the first formal, executable semantics for CIRCT implemented in the $\mathbb{K}$ framework, enabling rigorous reasoning and simulation of hardware IRs. It adopts a layered approach with MLIR static semantics, CIRCT common semantics, and unified dialect semantics to achieve composability and extensibility across hardware dialects (hw, comb, seq, sv). A generic hardware model within CIRCT common semantics and effectful interfaces enable cross-dialect interaction, while a dialect-focused formalization yields executable semantics and a simulator, Kimulator, validated via full-rule coverage and riscv-mini. This work paves the way for formal verification, symbolic execution, and equivalence checking in CIRCT-based designs, with potential for translation validation and hardware verification tooling.

Abstract

CIRCT, an open-source EDA framework akin to LLVM for software, is a foundation for various hardware description languages. Despite its crucial role, CIRCT's lack of formal semantics challenges necessary rigorous hardware verification. Thus, this paper introduces K-CIRCT, the first formal semantics in {\K} for a substantial CIRCT subset adequate for simulating a RISC-V processor. Our semantics are structured into multiple layers: (1) MLIR static semantics, which covers fundamental MLIR concepts across domains; (2) CIRCT common semantics, featuring a generic hardware model that captures key hardware features across dialects; and (3) composable and extensible semantics for specific dialects, formalized individually using a unified approach. This approach has been applied to formalize CIRCT core dialects. We validated our semantics through full-rule coverage tests and assessed its practicality using the popular RISC-V hardware design, riscv-mini.

Figures (11)

• Figure 1: An example of CIRCT/MLIR program.
• Figure 2: The structure of K-CIRCT.
• Figure 3: Syntax for generic MLIR. Note that this figure omits some syntax definitions due to the limited space. Indeed, our formalization consists of the complete syntax. Appendix \ref{['app:generic-mlir-syntax']} provides a more detailed version.
• Figure 4: The structure of MLIR state.
• Figure 5: The structure of CIRCT common state.