Gap-free Processor Verification by S2QED and Property Generation
Keerthikumara Devarajegowda1,2, Mohammad Rahmani Fadiheh1, Eshan Singh3, Clark Barrett3, Subhasish Mitra3, Wolfgang Ecker1,4, Dominik Stoffel1 and Wolfgang Kunz1
1Technische Universität Kaiserslautern, Germany,
2Infineon Technologies AG, Germany
3Stanford University, USA,
4Technische Universität München, Germany
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.
