3 papers
cs.FL2025
The rIC3 Hardware Model Checker
Yuheng Su, Qiusong Yang, Yiwei Ci +2
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 sever…
cs.LO2025
Deeply Optimizing the SAT Solver for the IC3 Algorithm
Yuheng Su, Qiusong Yang, Yiwei Ci +3
The IC3 algorithm, also known as PDR, is a SAT-based model checking algorithm that has significantly influenced the field in recent years due to its efficiency, scalability, and co…
cs.FL2025
Extended CTG Generalization and Dynamic Adjustment of Generalization Strategies in IC3
Yuheng Su, Qiusong Yang, Yiwei Ci +1
The IC3 algorithm is widely used in hardware formal verification, with generalization as a crucial step. Standard generalization expands a cube by dropping literals to include more…