EPEX

Verifying processors has been and still is a major challenge. Therefore, intensive research has led to advanced verification solutions ranging from ISS-based reference models, (cross-level) simulation down to formal verification at the RTL. During the verification of the processor implementation at the Instruction Set Architecture (ISA) level, test stimuli, i.e. test programs are needed. They are either created manually or with the aid of sophisticated test program generators. However, significant effort is required to produce thorough test programs. In this paper, we devise a novel approach for processor verification by Equivalent Program EXecution (EPEX). Our approach is based on a new form of equivalence checking Instead of comparing the architectural states of two models which execute the same program P, we derive a second, but equivalent program P^ from P (wrt. to a formal ISA model), and check that executing P and P^ will produce equal architectural states on the same design. We show that EPEX can easily be used in a simulation-based verification environment and broadens existing tests automatically. In a RISC-V case study using different core configurations of the well-known VexRiscv core, we demonstrate the bug-finding capabilities of EPEX.