Definition
Cross-Level Verification refers here to processor verification across abstraction levels: a register-transfer-level (RTL) core under test is co-simulated with a reference instruction-set simulator (ISS), and both execute the same generated instruction stream. Behavioral equality is checked during execution, with mismatches detected through register-value comparison. [cross-level-cosimulation-flow]
Method described in the evidence
The described approach combines cross-level co-simulation with coverage-guided fuzzing (CGF). A fuzzer generates bounded test vectors, which are used as processor instruction streams in a co-simulation consisting of the RTL core and the reference ISS. The flow has two main stages: a CGF-based fuzzing loop that generates test vectors, followed by a post-processing step that reduces or clusters generated tests that trigger mismatches. [cross-level-cosimulation-flow]
A central component is the Translation Buffer. It transforms a bounded fuzzer-generated test vector into a deterministic endless instruction stream through cyclic repetition. This is intended to decouple the co-simulation setup from micro-architecture-specific optimizations such as pipelining, and to make execution deterministic for the fuzzer. [translation-buffer]
The execution controller checks whether the RTL core and ISS behave equivalently while both execute the stream supplied by the Translation Buffer. The approach also uses a maximum instruction execution count in the ISS together with heuristic cycle-detection techniques to place an efficient runtime limit on each test-vector execution. [execution-control]
Motivation and design considerations
Earlier cross-level co-simulation approaches for RTL processor verification generated a single endless instruction stream that evolved dynamically at runtime. The evidence states that this can make a co-simulation setup complex when the ISS and RTL core have different fetch behavior, such as speculative prefetching caused by pipelining and branch prediction. In such cases, a deep pipeline understanding may be needed to feed the same instructions to both models and compare register values at appropriate time points. [prior-cross-level-limitations]
The described CGF-based approach instead generates test cases one after another. The evidence characterizes this as simplifying the co-simulation setup, making it easier to test different core configurations, and supporting arbitrary control flows, including self-loops, as well as load/store instructions. [testcase-based-approach]
Fuzzing support
The evidence identifies American Fuzzy Lop (AFL) as an out-of-process coverage-guided grey-box fuzzer. AFL resets the whole process between executions, uses edge coverage to detect new behaviors, and applies mutations such as bit flips, arithmetic mutations, and havoc mutations. [afl-background]
The processor-verification approach in the evidence relies on state-of-the-art fuzzing algorithms and adds lightweight domain-specific fuzzing extensions. It also describes custom mutation procedures tailored to generating common instruction patterns. [fuzzing-extensions]
Target domain
The evidence situates the approach in the RISC-V domain. RISC-V is described as a free and open ISA defined by the non-profit RISC-V International, with a modular design intended to make it suitable for many kinds of computing devices. [riscv-background]
As a case study, the paper reports verification of the open-source RISC-V-based VexRiscv processor, and states that the fuzzing-based approach was effective at finding numerous intricate bugs in VexRiscv. [riscv-vexriscv-case-study]