EPEX: Processor Verification by Equivalent Program Execution

Description

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.

Period	22 Jun 2021
Event title	ACM Great Lakes Symposium on VLSI (GLSVLSI)
Event type	Conference
Location	AustriaShow on map