Constrained Randomization

Overview

Constrained randomization is a stimulus-generation methodology used in functional verification of digital designs. Instead of applying purely unconstrained random values to a design under test (DUT), the verification engineer declares a set of variables as random (rand in SystemVerilog) and writes constraints that restrict the legal values those variables may take. Calling randomize() then produces values that satisfy every constraint, giving the testbench random but valid stimuli ^[1]. The technique concentrates simulation effort on inputs considered useful and interesting, allowing verification regressions to converge faster than naive random testing ^[1].

Role in SystemVerilog and UVM

In SystemVerilog, constrained randomization is expressed through class objects containing rand fields and constraint blocks. A typical pattern declares several rand bit-vector variables and groups the legal-value restrictions into named constraints. When randomize() is invoked, the simulator solves the conjunction of all active constraints and returns a satisfying assignment ^[1]. This mechanism is the foundation of UVM-style testbenches, which drive sequence items, register models, and protocol transactions through the same randomization engine ^[1].

Open-source Implementation in Verilator

Verilator historically lacked constrained-randomization support, which limited its use for UVM-style verification. Antmicro introduced constrained randomization into Verilator by translating SystemVerilog constraint expressions into the SMT-LIB2 problem-description language and delegating solving to SMT solvers such as Z3 and cvc5 ^[1].

Expression-to-SMT translation

Each SystemVerilog constraint is compiled into a separate runtime function that emits an SMT-LIB2 representation of the expression. Sub-expressions are formatted via the $sformatf system function (for example LHS && RHS becomes $sformatf("(and %s %s)", LHS, RHS)); constant folding in Verilator collapses the nested formatting calls into a single $sformatf whose missing arguments are filled at randomize-time ^[1]. The resulting bit-vector problem is encoded in the QF_BV logic.

Signedness and operator mapping

SMT-LIB2 has no signed/unsigned bit-vector types — signedness is a property of the operation. Verilator therefore maps signed comparisons to bvslt, bvsle, etc., and unsigned comparisons to bvult, bvule, etc. ^[2].

Achieving randomness with deterministic solvers

SMT solvers are deterministic, which is normally desirable but conflicts with randomization. To obtain truly random solutions — even in narrow solution spaces — Verilator forces a random hash of the output variables to a random value: a randomly chosen subset of output bits is XORed together and an extra assert is issued so the solver picks a different solution, introducing entropy into its internal state ^[2].

Current limitations and ongoing work

The initial Verilator implementation does not yet cover arrays (each array element must become a separate SMT variable), state-dependent/conditional constraints, or the distinction between 1-bit vectors and SMT booleans. A practical workaround for the boolean/1-bit issue is to append == 1'b1 to force a boolean conversion ^[2].

Research Directions

Coverage-aware constraint tuning

The NOVA framework observes that traditional constrained-random stimuli generation depends on manually crafted distributions that are difficult to design and often ineffective; it coordinates coverage-aware test selection with Bayes-optimized constrained randomization, modifying the constraint solver to expose parameterized decision strategies whose settings are tuned via Bayesian optimization to maximize coverage growth, achieving up to a 2.82× coverage convergence speedup across multiple RTL designs [arxiv:2512.00688].

Python-based constrained-random verification

Alternative verification environments can also offer constrained randomization. A Python-based flow using cocotb and cocotb-coverage can interface with available simulators and facilitate constrained randomization, lowering the cost of building a testbench compared to SystemVerilog [arxiv:2407.10312].