Paper on RISC-V ISA Conformance Model Checking Accepted at JSA'26

We are proud that our paper "χRVFormal: Formal Verification of RISC-V Processor Chisel Designs", has been accepted at Journal of Systems Architecture (JSA) 2026.

χRVFormal presents the first end-to-end approach for formally verifying RISC-V processor designs entirely at the Chisel high-level. By constructing a modular, parameterized reference model in Chisel and devising a novel synchronization mechanism, it reduces verification to a model-checking problem applicable to both in-order and out-of-order processors. Evaluated on riscv-mini, NutShell, and BOOM, our tool significantly outperforms state-of-the-art methods, discovering 7 real-world unknown bugs and achieving three orders of magnitude higher efficiency.

@article{JSA26Shen,
  title = {χRVFormal: Formal Verification of RISC-V Processor Chisel Designs},
  journal = {Journal of Systems Architecture},
  pages = {103761},
  year = {2026},
  issn = {1383-7621},
  doi = {https://doi.org/10.1016/j.sysarc.2026.103761},
  url = {https://www.sciencedirect.com/science/article/pii/S1383762126000792},
  author = {Shidong Shen and Shijie Chen and Yicheng Liu and Lijun Zhang and Fu Song and Zhilin Wu}
}