Extended CTG Generalization and Dynamic Adjustment of Generalization Strategies in IC3
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866913642415390720 |
|---|---|
| author | Su, Yuheng Yang, Qiusong Ci, Yiwei Huang, Ziyu |
| author_facet | Su, Yuheng Yang, Qiusong Ci, Yiwei Huang, Ziyu |
| contents | 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 unreachable states. The CTG approach enhances this by blocking counterexamples to generalization (CTG) when dropping literals fails. In this paper, we extend the CTG method (EXCTG) to put more effort into generalization. If blocking the CTG fails, EXCTG attempts to block its predecessors, aiming for better generalization. While CTG and EXCTG offer better generalization results, they also come with increased computational overhead. Finding an appropriate balance between generalization quality and computational overhead is challenging with a static strategy. We propose DynAMic, a method that dynamically adjusts generalization strategies according to the difficulty of blocking states, thereby improving scalability without compromising efficiency. A comprehensive evaluation demonstrates that EXCTG and DynAMic achieve significant scalability improvements, solving 8 and 25 more cases, respectively, compared to CTG generalization. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_02480 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Extended CTG Generalization and Dynamic Adjustment of Generalization Strategies in IC3 Su, Yuheng Yang, Qiusong Ci, Yiwei Huang, Ziyu Formal Languages and Automata Theory Logic in Computer Science 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 unreachable states. The CTG approach enhances this by blocking counterexamples to generalization (CTG) when dropping literals fails. In this paper, we extend the CTG method (EXCTG) to put more effort into generalization. If blocking the CTG fails, EXCTG attempts to block its predecessors, aiming for better generalization. While CTG and EXCTG offer better generalization results, they also come with increased computational overhead. Finding an appropriate balance between generalization quality and computational overhead is challenging with a static strategy. We propose DynAMic, a method that dynamically adjusts generalization strategies according to the difficulty of blocking states, thereby improving scalability without compromising efficiency. A comprehensive evaluation demonstrates that EXCTG and DynAMic achieve significant scalability improvements, solving 8 and 25 more cases, respectively, compared to CTG generalization. |
| title | Extended CTG Generalization and Dynamic Adjustment of Generalization Strategies in IC3 |
| topic | Formal Languages and Automata Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2501.02480 |