Overview
Directed-random test sequence generation is a model-based random testing technique used in processor verification. Instead of formally proving equivalence between a model and an implementation, the technique generates test sequences and looks for behavioral divergence; when a mismatch is found, the test provides a counterexample to equivalence.
In the RISC-V context, directed-random test-sequence generation has been used to debug pipeline and memory bugs and to uncover unexpected divergences in implementation behavior. Generated tests are commonly run on both a golden model and a processor under development so that execution traces or other observable behavior can be compared.
Role in RISC-V verification
RISC-V has multiple random or directed-random test generators. The cited TestRIG paper identifies RISCV-DV as the most advanced RISC-V sequence generator among the examples discussed. RISCV-DV generates assembly programs that can be converted into in-memory images for execution. Its generators cover RV32IMAFDC and RV64IMAFDC and include support for page-table interactions, privileged CSR use, and traps or interrupts.
Instruction-sequence workflow
The core output of the technique is an instruction or assembly sequence. In a traditional workflow, a generated assembly program is converted into an executable memory image, then run on a reference model and an implementation under test. The verification framework detects divergences by comparing behavior, particularly when detailed traces are available.
In TestRIG-style direct-instruction-injection workflows, the instruction stream can be supplied directly to instrumented models or implementations. The cited paper states that Direct Instruction Injection decouples the instruction stream from control flow and directly specifies the expected instruction sequence in the output trace, which simplifies sequence generation and shrinking because the program counter does not affect the instruction stream.
Generation, comparison, and shrinking
QCVEngine is an example of a tool that applies this style using Haskell QuickCheck. It generates arbitrary instruction sequences, sends the same instruction list over two Direct Instruction Injection sockets, collects RVFI traces, checks that the traces match, and returns a pass/fail result to QuickCheck. Because QuickCheck searches for failing inputs and supports shrinking, QCVEngine can generate, compare, and shrink instruction sequences.
The cited paper also describes targeted generators for subsets of the instruction set and template-based generators intended to reach deeper states such as virtual-memory mappings and cache conflicts. It notes that templates are a common technique in random test generators for reaching desired deep states.
Limitations
Directed-random test sequence generation is a refutation-oriented testing approach: it can expose divergences from a model with concrete counterexamples, but it does not prove full equivalence between a formal model and an implementation.