“Gap-Free Processor Verification by S^2QED and Property Generation” by Keerthikumara Devarajegowda, Mohammad Rahmani Fadiheh, Eshan Singh, Clark Barrett, Subhasish Mitra, Wolfgang Ecker, Dominik Stoffel, and Wolfgang Kunz. In Proceedings of the 2020 Design, Automation and Test in Europe (DATE '20), Mar. 2020, pp. 526-531. Grenoble, France.
The required manual effort and verification expertise are among the main hurdles for adopting formal verification in processor design flows. Developing a set of properties that fully covers all instruction behaviors is a laborious and challenging task. This paper proposes a highly automated and “complete” processor verification approach which requires considerably less manual effort and expertise compared to the state of the art. The proposed approach extends the S^2QED approach to cover both single and multiple instruction bugs and ensures that a design is completely verified according to a well-defined criterion. This makes the approach robust against human errors. The properties are simple and can be automatically generated from an ISA model with small manual effort. Furthermore, unlike in conventional property checking, the verification engineer does not need to explicitly specify the processor's behavior in different special scenarios, such as stalling, exception, or speculation, since these are taken care of implicitly by the proposed computational model. The great promise of the approach is shown by an industrial case study with a 5-stage RISC-V processor
BibTeX entry:
@inproceedings{DFS+20,
author = {Keerthikumara Devarajegowda and Mohammad Rahmani Fadiheh and
Eshan Singh and Clark Barrett and Subhasish Mitra and Wolfgang
Ecker and Dominik Stoffel and Wolfgang Kunz},
title = {Gap-Free Processor Verification by {S}{\it ^2}{QED} and
Property Generation},
booktitle = {Proceedings of the 2020 Design, Automation and Test in
Europe (DATE '20)},
pages = {526--531},
publisher = {IEEE},
month = mar,
year = {2020},
doi = {10.23919/DATE48585.2020.9116515},
note = {Grenoble, France},
url = {http://theory.stanford.edu/~barrett/pubs/DFS+20.pdf}
}
(This webpage was created with bibtex2web.)