Constrained Random Verification

Overview

Constrained Random Verification (CRV) is a constrained-random or constraint-based testcase-generation technique used in hardware design verification. In the evidence available, CRV is described as a stimulus generator that "samples uniformly over the subset of legal actions at each cycle, modeling typical constrained-random stimulus," and is used as one of several compared stimulus-generation methods in recent chip-verification studies. [crv-stimulusrl]

In the FuSS paper, CRV is grouped with "random and constrained-random verification" as part of "conventional verification approaches" that "struggle to achieve adequate coverage of the vast state space in modern SoCs," motivating coverage-guided and semi-formal alternatives. [crv-fuss]

In industry-oriented reporting on RISC-V verification, CRV is described as one of the methodologies needed to achieve complete RISC-V verification, exemplified through "coverage driven simulation based on UVM constrained random methods and compliant with the Universal Verification Methodology (UVM) standard," using the Google RISCV-DV open-source project as an example flow. [crv-riscv-uvm]

Description from evidence

The provided evidence characterizes CRV at a high level rather than specifying a single internal algorithm:

• Action space sampling: CRV is modeled as sampling actions uniformly from the subset of legal actions at each cycle, rather than uniformly over the entire action space. [crv-stimulusrl]
• Legality enforcement: CRV enforces protocol legality by construction (sampling only from legal actions), which means it does not explicitly target bins corresponding to illegal operations; in the StimulusRL evaluation, this is why CRV converges to fewer bins than Random on benchmarks such as FIFO8 where some bins encode illegal-operation attempts. [crv-stimulusrl]
• No coverage feedback or learned policy: In the compared taxonomy of stimulus generators, CRV uses legality constraints but neither coverage feedback nor a learned policy. [crv-stimulusrl]
• Runtime profile: CRV completes quickly relative to learning-based methods because it only samples actions and steps the design model; on the DMCache design, a 2000-step run takes 0.537 ± 0.004 s, compared with 0.378 ± 0.004 s for Random and 2.111 ± 0.005 s for StimulusRL. [crv-stimulusrl]
• Coverage limitations: CRV is described as struggling to achieve adequate coverage in modern SoCs; "even millions of random or constrained-random test vectors (input stimuli) fail to activate a majority of complex execution paths, leaving many potential corner cases untested." [crv-fuss]

Relationship to coverage-driven simulation

The SemiEngineering whitepaper on UVM functional coverage for RISC-V cores describes coverage driven simulation based on UVM constrained random methods that comply with the Universal Verification Methodology (UVM) standard, using Google RISCV-DV as the open-source test-generator. CRV supplies the stimulus-generation mechanism, while coverage-driven simulation supplies the feedback metric and closure methodology that guides test selection and randomization weights. [crv-riscv-uvm]

Python-based CRV environments

A 2024 study evaluates a Python-based verification environment for constrained random verification built on open-source frameworks such as PyUVM (a Python-based UVM 1.2 implementation) and PyVSC (which facilitates constrained randomization and functional coverage), and compares the resulting testbenches against established SystemVerilog-UVM methodology across multiple design IPs. [crv-pyuvm]

Formal distribution guarantees for CRV

A separate line of work addresses the fact that conventional CRV solutions provide no formal guarantees on the distribution of generated stimuli. The TraceSampler paper presents an algorithm based on Algebraic Decision Diagrams for sampling bounded traces (sequences of states) of a sequential circuit with provable uniformity (or bounded bias) guarantees while satisfying given constraints, and reports that TraceSampler outperforms alternative approaches offering similar uniformity guarantees. [crv-tracesampler]

The SAT-witness-generator literature situates CRV inside a broader taxonomy of sampling techniques for generating solutions of constraint problems, all of which trade off scalability against guarantees of uniformity:

• BDD-based sampling uses weighted binary decision diagrams to sample uniformly from SAT witnesses, but is known to suffer from scalability problems; adapted BDD-based techniques improve performance but achieve scalability at the cost of uniformity guarantees. [crv-sat-bdd]
• Random seeding of DPLL SAT solvers offers strong performance, but the resulting witness distributions can be highly skewed. [crv-sat-dpll]
• MCMC methods (simulated annealing, Metropolis–Hastings and related algorithms) guarantee eventual convergence to a target distribution under mild requirements, but convergence is often impractically slow. Adapted MCMC-based methods have been proposed specifically for constrained-random verification, but "most of these adaptations are heuristic in nature, and do not preserve theoretical guarantees of uniformity." [crv-sat-mcmc]
• Interval-propagation and belief-network samplers lend scalability to the techniques, but the generated distributions "can deviate significantly from the uniform distribution." [crv-sat-interval]
• Hashing-based sampling (pioneered by Sipser) partitions the witness space into roughly equal-sized cells using r-wise independent hash functions and randomly picks a solution from a randomly chosen cell. The Bellare–Goldreich–Petrank algorithm uses n-wise independent algebraic hash functions but scales poorly in practice; XORSample' uses 3-wise independent linear hash functions and scales to constraints involving a few thousand variables but requires difficult-to-estimate input parameters; UniWit, proposed by Chakraborty, Meel, and Vardi, uses 3-wise independent linear hash functions and represents a step toward marrying scalability with guarantees of uniformity. [crv-sat-hashing]

The overarching pattern is that prior work has either paid for scalability by sacrificing uniformity guarantees, or paid for uniformity by sacrificing scalability, and that bridging the two extremes is an open research direction. [crv-sat-tradeoff]

Relationship to RISC-V verification

A reference list in a RISC-V test-sequence generation paper cites Constrained random verification for RISC-V: Overview, evaluation and discussion by Ahmadi-Pour, Herdt, and Drechsler (MBMV 2021; 24th Workshop, 2021: 1–8), placing CRV directly within the RISC-V verification literature. [crv-riscv-overview]

The Scale4Edge project publication list at the University of Bremen likewise records this paper as one of its relevant publications, anchoring the same MBMV 2021 reference within a broader RISC-V verification research agenda. [crv-riscv-scl]

A 2022 RISC-V Summit tutorial on RISC-V processor verification techniques (Moore and Sutton, Imperas Software) lists Constrained Random testing alongside other RISC-V design verification building blocks such as ISS-based trace compare, UVM functional coverage, interrupts, signatures, RVVI, and instruction stream generators (ISG) such as the open-source riscv-dv (CHIPS Alliance) and the commercial Valtrix STING. The tutorial states that RISC-V processor verification has historically used "proprietary techniques" and lacked "industry-standard best practices or verification IP," and that techniques inherited from ASIC/SoC verification (the broader category in which CRV is the dominant stimulus-generation approach) are insufficient on their own, motivating new methods that combine and adapt ASIC/SoC techniques for RISC-V. [crv-riscvsummit]

Relationship to coverage-guided fuzzing

The strongest direct evidence connecting CRV-adjacent testcase generation to coverage-guided fuzzing comes from the paper Verifying Instruction Set Simulators using Coverage-guided Fuzzing. That paper proposes using coverage-guided fuzzing (CGF) for ISS verification, implemented on top of LLVM libFuzzer with a functional coverage metric that complements code coverage and a mutation procedure tailored to ISS verification. [cgf-method]

The paper reports a case study on three publicly available RISC-V ISSs. It states that the fuzzer was effective at maximizing most coverage metrics and found new errors in every considered ISS, including an error in the official RISC-V reference simulator Spike. [cgf-results]

For CRV, the relevant comparison point is complementarity: the paper states that fuzzing is useful for triggering and checking corner cases and error cases and "can complement other testcase generation techniques." Its references include constraint-based and constrained-random verification work, indicating that CRV belongs to the broader testcase-generation landscape against which CGF is positioned. [cgf-complementarity]

Practical interpretation from the evidence

Within the limits of the provided evidence, CRV should be treated as a constrained-random stimulus-generation technique that samples from the legal action subspace, commonly used as a baseline in chip-design verification studies. Coverage-driven simulation wraps CRV with UVM-compliant feedback and closure methodology, coverage-guided fuzzing and reinforcement-learning-based stimulus agents (such as StimulusRL) are presented as related but distinct techniques that can complement CRV (particularly for ISS corner-case and error-case discovery and for addressing CRV's coverage limitations on complex SoC designs), and formal approaches such as TraceSampler address CRV's lack of distribution guarantees by providing provably uniform sampling under given constraints. A broader line of SAT-based witness-generation research places CRV within a wider taxonomy of samplers — including BDD-, DPLL-, MCMC-, interval-propagation-, and hashing-based methods — where scalability and uniformity guarantees are typically traded off against one another. PyUVM/PyVSC-based Python verification environments target constrained randomization and functional coverage outside of the SystemVerilog-UVM ecosystem. [crv-fuss][crv-stimulusrl][crv-riscv-uvm][crv-tracesampler][crv-sat-tradeoff][crv-sat-bdd][crv-sat-dpll][crv-sat-mcmc][crv-sat-interval][crv-sat-hashing][crv-pyuvm][cgf-complementarity]