An Efficient Runtime Validation Framework based on the Theory of Refinement

TL;DR

This paper presents a refinement-based runtime validation framework that improves hardware and low-level software testing by enabling more complete, less error-prone, and design-agnostic correctness checks during simulation.

Contribution

It introduces a novel refinement-based methodology that compiles formal conjectures into runtime checks, addressing key limitations of existing industry testing practices.

Findings

Validated on a 5-stage RISCV microprocessor

Demonstrated improved testing completeness

Reduced oracle and property definition errors

Abstract

We introduce a new methodology based on refinement for testing the functional correctness of hardware and low-level software. Our methodology overcomes several major drawbacks of the de facto testing methodologies used in industry: (1) it is difficult to determine completeness of the properties and tests under consideration (2) defining oracles for tests is expensive and error-prone (3) properties are defined in terms of low-level designs. Our approach compiles a formal refinement conjecture into a runtime check that is performed during simulation. We describe our methodology, discuss algorithmic issues, and provide experimental validation using a 5-stage RISCV pipelined microprocessor and hypervisor.