K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs
<|reference_start|>K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs: 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.<|reference_end|>
@article{zhao2024k-circt:,
    title={K-CIRCT: A Layered, Composable, and Executable Formal Semantics for
  CIRCT Hardware IRs},
    author={Jianhong Zhao, Jinhui Kang, Yongwang Zhao},
    journal={arXiv preprint arXiv:2404.18756},
    year={2024},
    archivePrefix={arXiv},
    eprint={2404.18756},
    primaryClass={cs.SE cs.PL}
}