Gap-Free Processor Verification by S^2QED and Property Generation

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.

Abstract

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.)