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.

翻译：CIRCT是一个面向硬件描述语言的开源EDA框架，其地位类似于软件领域的LLVM。尽管作用关键，但CIRCT缺乏形式语义，这给必要的严谨硬件验证带来了挑战。为此，本文提出K-CIRCT——首个针对CIRCT核心子集在{\K}中定义的形式语义，该子集足以模拟RISC-V处理器。语义采用分层结构：（1）MLIR静态语义层，涵盖跨领域的MLIR基本概念；（2）CIRCT通用语义层，提供可捕获各方言关键硬件特征的通用硬件模型；（3）面向特定方言的可组合可扩展语义层，采用统一方法独立形式化建模。该方法已成功应用于CIRCT核心方言的形式化。我们通过全规则覆盖率测试验证了语义的完备性，并基于主流RISC-V硬件设计riscv-mini评估了其实用性。