4 papers · 1 filter
AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction
Enyuan Tian, Yiwei Ci, Qiusong Yang +2
Assertion-Based Verification (ABV) is critical for ensuring functional correctness in modern hardware systems. However, manually writing high-quality SVAs remains labor-intensive a…
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…
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…
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…