SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program Execution
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910400090472448 |
|---|---|
| author | Li, Yufeng Yang, Qiusong Ci, Yiwei Tian, Enyuan |
| author_facet | Li, Yufeng Yang, Qiusong Ci, Yiwei Tian, Enyuan |
| contents | Symbolic quick error detection (SQED) has greatly improved efficiency in formal chip verification. However, it has a limitation in detecting single-instruction bugs due to its reliance on the self-consistency property. To address this, we propose a new variant called symbolic quick error detection by semantically equivalent program execution (SEPE-SQED), which utilizes program synthesis techniques to find sequences with equivalent meanings to original instructions. SEPE-SQED effectively detects single-instruction bugs by differentiating their impact on the original instruction and its semantically equivalent program (instruction sequence). To manage the search space associated with program synthesis, we introduce the CEGIS based on the highest priority first algorithm. The experimental results show that our proposed CEGIS approach improves the speed of generating the desired set of equivalent programs by 50% in time compared to previous methods. Compared to SQED, SEPE-SQED offers a wider variety of instruction combinations and can provide a shorter trace for triggering bugs in certain scenarios. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_03172 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program Execution Li, Yufeng Yang, Qiusong Ci, Yiwei Tian, Enyuan Software Engineering Hardware Architecture Systems and Control Symbolic quick error detection (SQED) has greatly improved efficiency in formal chip verification. However, it has a limitation in detecting single-instruction bugs due to its reliance on the self-consistency property. To address this, we propose a new variant called symbolic quick error detection by semantically equivalent program execution (SEPE-SQED), which utilizes program synthesis techniques to find sequences with equivalent meanings to original instructions. SEPE-SQED effectively detects single-instruction bugs by differentiating their impact on the original instruction and its semantically equivalent program (instruction sequence). To manage the search space associated with program synthesis, we introduce the CEGIS based on the highest priority first algorithm. The experimental results show that our proposed CEGIS approach improves the speed of generating the desired set of equivalent programs by 50% in time compared to previous methods. Compared to SQED, SEPE-SQED offers a wider variety of instruction combinations and can provide a shorter trace for triggering bugs in certain scenarios. |
| title | SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program Execution |
| topic | Software Engineering Hardware Architecture Systems and Control |
| url | https://arxiv.org/abs/2404.03172 |