K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909184136577024 |
|---|---|
| author | Zhao, Jianhong Kang, Jinhui Zhao, Yongwang |
| author_facet | Zhao, Jianhong Kang, Jinhui Zhao, Yongwang |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_18756 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs Zhao, Jianhong Kang, Jinhui Zhao, Yongwang Software Engineering Programming Languages 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. |
| title | K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs |
| topic | Software Engineering Programming Languages |
| url | https://arxiv.org/abs/2404.18756 |