Symbolic Quick Error Detection Using Symbolic Initial State for Pre-Silicon Verification
Mohammad Rahmani Fadiheh1, Joakim Urdahl1, Srinivas Shashank Nuthakki2, Subhasish Mitra2, Clark Barrett2, Dominik Stoffel1 and Wolfgang Kunz1
1Technische Universität Kaiserslautern, Germany
2Stanford University, Stanford, CA, USA
ABSTRACT
Driven by the demand for highly customizable processor cores for IoT and related applications, there is a renewed interest in effective but low‐cost techniques for verifying systems on‐ chip (SoCs). This paper revisits the problem of processor verification and presents a radically different approach when compared to the state of the art. The proposed approach is highly automated and leverages recent progress in the field of post‐silicon validation by the method of Quick Error Detection (QED) and Symbolic Quick Error Detection (SQED). In this paper, we modify SQED by incorporating a symbolic initial state in its BMC‐based analysis and generalize the approach into the S2QED method. As a first advantage, S2QED can separate logic bugs from electrical bugs in QED‐based postsilicon validation. Secondly, it also makes a strong contribution to pre‐silicon verification by proving that the execution of each instruction is independent of its context in the program. The manual efforts for the proposed approach are orders of magnitude smaller than for conventional property checking. Our experimental results demonstrate the potential of S2QED using the Aquarius open‐source processor example.
