The rIC3 Hardware Model Checker
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913849241763840 |
|---|---|
| author | Su, Yuheng Yang, Qiusong Ci, Yiwei Bu, Tianjun Huang, Ziyu |
| author_facet | Su, Yuheng Yang, Qiusong Ci, Yiwei Bu, Tianjun Huang, Ziyu |
| contents | In this paper, we present rIC3, an efficient bit-level hardware model checker primarily based on the IC3 algorithm. It boasts a highly efficient implementation and integrates several recently proposed optimizations, such as the specifically optimized SAT solver, dynamically adjustment of generalization strategies, and the use of predicates with internal signals, among others. As a first-time participant in the Hardware Model Checking Competition, rIC3 was independently evaluated as the best-performing tool, not only in the bit-level track but also in the word-level bit-vector track through bit-blasting. Our experiments further demonstrate significant advancements in both efficiency and scalability. rIC3 can also serve as a backend for verifying industrial RTL designs using SymbiYosys. Additionally, the source code of rIC3 is highly modular, with the IC3 algorithm module being particularly concise, making it an academic platform that is easy to modify and extend. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_13605 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The rIC3 Hardware Model Checker Su, Yuheng Yang, Qiusong Ci, Yiwei Bu, Tianjun Huang, Ziyu Formal Languages and Automata Theory In this paper, we present rIC3, an efficient bit-level hardware model checker primarily based on the IC3 algorithm. It boasts a highly efficient implementation and integrates several recently proposed optimizations, such as the specifically optimized SAT solver, dynamically adjustment of generalization strategies, and the use of predicates with internal signals, among others. As a first-time participant in the Hardware Model Checking Competition, rIC3 was independently evaluated as the best-performing tool, not only in the bit-level track but also in the word-level bit-vector track through bit-blasting. Our experiments further demonstrate significant advancements in both efficiency and scalability. rIC3 can also serve as a backend for verifying industrial RTL designs using SymbiYosys. Additionally, the source code of rIC3 is highly modular, with the IC3 algorithm module being particularly concise, making it an academic platform that is easy to modify and extend. |
| title | The rIC3 Hardware Model Checker |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2502.13605 |