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

DruckversionPer E-Mail sendenPDF-Version

Lucas Klemmer, Johannes Kepler University Linz, AT


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.


Lucas Klemmer, Johannes Kepler University Linz, ATLucas 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.