Core Concepts
SEPE-SQED utilizes program synthesis techniques to find semantically equivalent instruction sequences to the original instructions, enabling the detection of both single-instruction and multiple-instruction bugs in processor designs.
Abstract
The paper presents SEPE-SQED, a novel variant of the symbolic quick error detection (SQED) approach for formal verification of processor designs. SQED has limitations in detecting single-instruction bugs due to its reliance on the self-consistency property. To address this, SEPE-SQED incorporates program synthesis techniques to find sequences of instructions that are semantically equivalent to the original instructions.
The key highlights of the paper are:
- SEPE-SQED can effectively detect both single-instruction and multiple-instruction bugs by comparing the execution of the original instruction and its semantically equivalent program.
- The authors introduce the HPF-CEGIS algorithm, which improves the speed of generating the desired set of equivalent programs by 50% compared to previous CEGIS-based methods.
- Experimental results on a real open-source high-performance processor demonstrate that SEPE-SQED can detect a wider variety of bugs and, in certain scenarios, generate shorter bug traces compared to SQED.
The paper first provides background on SQED and program synthesis techniques. It then presents the overview of the SEPE-SQED approach, including the formal semantic model of instructions and the HPF-CEGIS algorithm for program synthesis. The integration of the EDSEP-V module into the design under verification (DUV) is also described. Finally, the evaluation section compares the performance of HPF-CEGIS with previous CEGIS approaches and assesses the bug detection capabilities of SEPE-SQED on a real processor design.
Stats
SEPE-SQED can detect single-instruction bugs in 12 different instruction types, including ADD, SUB, XOR, OR, AND, SLT, SLTU, SRA, MULH, XORI, SLLI, and SRAI.
SEPE-SQED exhibits an average reduction of 50% in synthesis time compared to the iterative CEGIS approach, with up to 90% reduction in certain cases.
Quotes
"SEPE-SQED effectively detects single-instruction bugs by differentiating their impact on the original instruction and its semantically equivalent program (instruction sequence)."
"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."