“Symbolic quick error detection using symbolic initial state for pre-silicon verification” by M. R. Fadiheh, J. Urdahl, S. S. Nuthakki, S. Mitra, C. Barrett, D. Stoffel, and W. Kunz. In Proceedings of the 2018 Design, Automation and Test in Europe (DATE '18), Mar. 2018, pp. 55-60. Dresden, Germany.
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 S^2QED method. As a first advantage, S^2QED 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 S^2QED using the Aquarius open-source processor example.
BibTeX entry:
@inproceedings{FUN+18,
author = {M. R. Fadiheh and J. Urdahl and S. S. Nuthakki and S. Mitra
and C. Barrett and D. Stoffel and W. Kunz},
title = {Symbolic quick error detection using symbolic initial state
for pre-silicon verification},
booktitle = {Proceedings of the 2018 Design, Automation and Test in
Europe (DATE '18)},
pages = {55--60},
publisher = {IEEE},
month = mar,
year = {2018},
isbn = {978-3-9819263-0-9},
doi = {10.23919/DATE.2018.8341979},
note = {Dresden, Germany},
url = {http://theory.stanford.edu/~barrett/pubs/FUN+18.pdf}
}
(This webpage was created with bibtex2web.)