An Efficient Runtime Validation Framework based on the Theory of Refinement
summary
A runtime refinement-based checker compares an executable ISA model (Spike) to a 5-stage pipelined RTL and validates each implementation step against the spec rather than hand-written properties. The system implements a refinement checker with a configurable commitment refinement map, injects decoder/control/ALU/forwarding mutations and detected all injected mutations. Measured overhead depends on the refinement map choice and falls to near-linear in these experiments, giving precise error locations at the point of divergence.
AI-written summary · about
chapters (4)
related talks
47mTutorial: Choosing Appropriate Verification Techniques for Desired RISC...
19mThe role of software in validating silicon IP
14mSVM: A Synthesizable Approach to Efficient RISC-V CPU Verification
12mRISC-V: Hardcore/Softcore Co-Simulation Environment with Cycle-Accurate Rollback
18mPreview: Verification (Correctness)
25mRISC-V System-level Certification from Verification Foundations
23mThe Continuum of RISC-V Compliance and Verification Testing
38mThe Verification of a Distributed System