SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program Execution

Symbolic quick error detection（SQED）已经极大地提高了芯片验证的效率。然而，由于其依赖于自洽性，它在检测单指令错误方面存在局限性。为了解决这个问题，我们提出了一种新的变体，称为基于语义等效程序执行的符号快速错误检测（SEPE-SQED），它利用程序合成技术找到与原始指令具有相同含义的序列。SEPE-SQED通过区分单指令错误对原始指令及其语义等效程序（指令序列）的影响，有效地检测单指令错误。为了管理与程序合成相关的搜索空间，我们引入了基于最高优先级优先算法的CEGIS。实验结果表明，与以前的方法相比，我们提出的CEGIS方法在时间上将所需的等效程序集生成速度提高了50%。与SQED相比，SEPE-SQED提供了更广泛的指令组合，并可以在某些情况下提供更短的跟踪以触发错误。

SEPE-SQED aims to improve the efficiency of formal chip verification by detecting single-instruction bugs, which is a limitation of the current SQED method.

SEPE-SQED uses program synthesis techniques to find semantically equivalent instruction sequences, effectively detecting single-instruction bugs by comparing their impact on the original instruction and its equivalent program.

SEPE-SQED introduces the CEGIS approach based on the highest priority first algorithm to manage the search space associated with program synthesis, which improves the speed of generating equivalent programs by 50% compared to previous methods. Experimental results show that SEPE-SQED offers a wider variety of instruction combinations and can provide a shorter trace for triggering bugs in certain scenarios.

Related work includes the current SQED method and other formal verification techniques for detecting bugs in chip design, such as bounded model checking and symbolic trajectory evaluation.