Applying the Four-Eyes Principle to RISC-V Processor Verification by Equivalent Program Execution

Lucas Klemmer, Johannes Kepler University Linz, AT

Abstract

We present a new verification approach for RISC-V processors which allows broadening existing test programs automatically. For a given test program our approach derives a second program that is different from the original one but proven to be equivalent. By definition, executing both programs on the same processor has to produce equal architectural states even though the executed instructions are completely different. We demonstrate the bug-finding capabilities of our approach on the well-known VexRiscv processor. Broadening a few tests already resulted in the detection of more bugs and increased test quality.

Biography

Lucas Klemmer is a PhD student at the Institute for Complex Systems (ICS) at the Johannes Kepler University in Linz, Austria. He received his Master’s degree in computer science from the University of Bremen in Germany. Currently, his research interest includes RISC-V, verification at the HW/SW interface, and new EDA approaches.