Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The rIC3 Hardware Model Checker

Yuheng Su, Qiusong Yang, Yiwei Ci, Tianjun Bu, Ziyu Huang

TL;DR

Problem: scalable verification of hardware designs suffers from state-space explosion. Approach: rIC3 integrates IC3 with optimized GipSAT, dynamic generalization (DynAMic, CTG, EXCTG), internal-signal predicates (IC3INN), and localization abstraction, plus a 16-thread portfolio of IC3, BMC, and K-Induction. Contributions: concise IC3 core (~1700 LOC), modular Rust implementation, and state-of-the-art results on HWMCC’24 with a SymbiYosys backend. Findings: substantial speedups and scalability across bit-level and word-level tracks; ablation confirms the importance of GipSAT and dynamic generalization. Significance: provides an extensible academic platform for hardware verification and a practical backend for industrial RTL verification.

Abstract

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.

The rIC3 Hardware Model Checker

TL;DR

Problem: scalable verification of hardware designs suffers from state-space explosion. Approach: rIC3 integrates IC3 with optimized GipSAT, dynamic generalization (DynAMic, CTG, EXCTG), internal-signal predicates (IC3INN), and localization abstraction, plus a 16-thread portfolio of IC3, BMC, and K-Induction. Contributions: concise IC3 core (~1700 LOC), modular Rust implementation, and state-of-the-art results on HWMCC’24 with a SymbiYosys backend. Findings: substantial speedups and scalability across bit-level and word-level tracks; ablation confirms the importance of GipSAT and dynamic generalization. Significance: provides an extensible academic platform for hardware verification and a practical backend for industrial RTL verification.

Abstract

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.

Paper Structure

This paper contains 11 sections, 5 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Architecture
  3. Techniques
  4. Portfolio
  5. Implementation
  6. Related Work
  7. Evaluation
  8. Setup
  9. Results
  10. Strengths and Limitations
  11. Conclusion

Figures (5)

  • Figure 1: rIC3 Architecture and Verification Flow
  • Figure 2: The number of cases solved over time by various single-thread IC3 engines.
  • Figure 3: The solving times (in seconds) comparisons between various IC3 engines.
  • Figure 4: The number of cases solved over time by various portfolio engines.
  • Figure 5: The solving times (in seconds) comparisons between various portfolio engines.