SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program Execution
Yufeng Li, Qiusong Yang, Yiwei Ci, Enyuan Tian
TL;DR
SEPE-SQED addresses the limitation of SQED in detecting single-instruction bugs by comparing an original instruction against semantically equivalent program executions generated via program synthesis. It introduces HPF-CEGIS to efficiently discover these equivalent sequences and defines EDSEP-V for validation within a pre-silicon verification flow. Experimental results show HPF-CEGIS reduces synthesis time by approximately 50% on average and that SEPE-SQED can detect both single-instruction and multiple-instruction bugs, sometimes producing shorter bug traces than SQED. The approach broadens the practical reach of QED-based verification and improves pre-silicon reliability for processors.
Abstract
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.