Gap-free Processor Verification by S2QED and Property Generation

Keerthikumara Devarajegowda, Mohammad Rahmani Fadiheh, Eshan Singh, Clark Barrett, Subhasish Mitra, Wolfgang Ecker, Dominik Stoffel, Wolfgang Kunz

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

14 Scopus citations

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 S2QED 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 scenarios 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.

Original languageEnglish
Title of host publicationProceedings of the 2020 Design, Automation and Test in Europe Conference and Exhibition, DATE 2020
EditorsGiorgio Di Natale, Cristiana Bolchini, Elena-Ioana Vatajelu
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages526-531
Number of pages6
ISBN (Electronic)9783981926347
DOIs
StatePublished - Mar 2020
Externally publishedYes
Event2020 Design, Automation and Test in Europe Conference and Exhibition, DATE 2020 - Grenoble, France
Duration: 9 Mar 202013 Mar 2020

Publication series

NameProceedings of the 2020 Design, Automation and Test in Europe Conference and Exhibition, DATE 2020

Conference

Conference2020 Design, Automation and Test in Europe Conference and Exhibition, DATE 2020
Country/TerritoryFrance
CityGrenoble
Period9/03/2013/03/20

Fingerprint

Dive into the research topics of 'Gap-free Processor Verification by S2QED and Property Generation'. Together they form a unique fingerprint.

Cite this