Improving constrained randomization in Verilator with near-uniform result distribution

When working with SystemVerilog designs of hardware components, one of the most important steps is the design verification process that ensures everything works as intended. When building a suitable test environment and throughout its execution, data randomization becomes crucial - it ensures that the tests are thorough by including variables and combinations that might have otherwise been omitted if the stimuli were written by hand. However, purely random stimuli are oftentimes invalid - containing incorrect addresses or combinations which are outright impossible.

To avoid the issues that come with true randomization, testing of designs utilizes constrained randomization, which still returns random results, but unlike true randomization, ones that fit certain specified conditions. Some time ago, in order to further aid in more comprehensive design testing, Antmicro introduced constrained randomization into Verilator, an open source digital tool for developing ASIC and FPGA designs that is steadily becoming the industry standard for modern digital design.

Continuing our work, we’ve recently improved the constrained randomization feature in Verilator by implementing the UniGen2 algorithm, an advanced, hashing-based SAT witness sampler designed to provide a more uniform distribution of results. In this article, we present the algorithm and its approach to constrained randomization to illustrate how it provides a more efficient randomization solution when testing designs in Verilator.

How UniGen2 provides near-uniform solutions

The UniGen2 algorithm is split into the following steps: problem measurement, subset creation, and drawing solutions. The uniformity can be attributed to the process of subset creation. It uses a randomized hash function, which splits the whole solution space into smaller subsets (also called cells), and only one subset satisfies that hash function. Because the hash function is random, so is the way the space gets split and the cell that comes out of it. Since we then pick solutions at random from that one cell, the samples returned by constrained randomization are likewise random, and every solution has a near-equal chance of being picked. To learn more about UniGen2, refer to the research paper which introduces it; our implementation of it into Verilator is based on calculations from this paper.

As a demonstration of UniGen2’s functionality, we will consider the following example - randomizing a point inside a 50 x 40 rectangle 300 times:

module t;
  class Point;
    rand bit [7:0] x;
    rand bit [7:0] y;
    constraint box { x < 50; y < 40; }
  endclass
  initial begin
    automatic Point p = new;
    for (int i = 0; i < 300; ++i) begin
      void'(p.randomize());
      $display("%0d %0d", p.x, p.y);
    end
    $finish;
  end
endmodule

This particular example has 2000 possible solutions (50 x 40 points inside the rectangle) - the 300 calls we wish to make should be spread as evenly as possible across that. Z3, the SMT solver that Verilator uses for constrained randomization, is deterministic by design - given the same call, it would return the same solution every single time. As such, the randomization has to come from Verilator itself, rather than the solver.

And so, instead of handing the solver the same space of the 2000 example solutions, we create subsets - small, randomly chosen chunks taken from the entire solution space. As the subset is randomly picked and different each time, we force the solver to return a solution from a different part of the space.

Subset creation is handled by an XOR hash function, which is asserted over the bits of the variables being randomized; the selection of specific bits to be included in the equation is done randomly, and the result is also randomly fixed to 0 or 1. About half of the possible solutions satisfy such an equation; as such, one XOR discards half of the solutions, while a second one halves what is left, and so on. The remaining chunk is the desired cell, and its size is roughly 1/2^N of the original solution space, where N is the number of XOR equations applied.

To illustrate that, we can show the full effect on eight values, with b0 XOR b2 = 0 as the first equation and b1 XOR b2 = 1 as the second:

After initially starting with 8 values, we see that 4 pass the first equation, and out of those, 2 pass the second one. The 2 of the 4 that pass the second XOR equation depend on which bits each equation covers, and what target value it is fixed to.

Every time the sampler requires more solutions, the XOR equations are drawn anew - each round results in a different cell. This forces the solver to pick answers from a different chunk of the solution space. And once a cell is small enough to be listed completely, the solver stops choosing altogether: Verilator enumerates the whole cell and picks from it at random itself.

Determining the number of needed XOR equations

The number of XOR equations required for the cell to be the right size cannot be fixed. In accordance with the paper that the algorithm is based on, the threshold for the subset size is between 11 and 61 solutions. These are the defaults given in the paper, which were verified to provide satisfying results. Depending on the size of the entire solution space, the number of equations needed to split into correctly-sized cells will differ every time.

As such, UniGen2 measures the number of equations needed first - it sequentially adds on equations until the number of solutions within a cell is small enough to be fully enumerated. This process is illustrated in the graphic seen below.

Measuring how many XOR equations are needed runs only once, as that number depends on the size of the solution space and thus on the given constraints. As long as the constraints stay the same, the algorithm keeps reusing it: the equations themselves are drawn anew each round, so every round lands on a different cell, but the number of equations does not change.

A cell is then enumerated by repeatedly asking Z3 for a solution and adding a blocking clause for each one, which makes it impossible for the same solution to come back, until the cell is exhausted. Keeping the cell size small improves the speed of the process - drawing and blocking solutions from a large subset would significantly increase the enumeration time.

Each round enumerates a new cell and keeps 11 of its solutions, chosen at random; 1 of them is returned to the caller and the remaining 10 are cached, so the following 10 randomize() calls do not need to call the solver at all, further speeding up the process.

Better performance than the previous sampler

To ensure the proper functionality of UniGen2 within Verilator, and to give insight into its performance when compared to the previous sampler, we prepared several benchmarks. We ran both samplers at three different sampling budgets: 1x, 5x, and 25x of the solution-space size, while the largest test cases were measured at 3x.

For a complete list of all benchmark results at all budgets, see this report file.

The presented graphs are solution frequency plots showing a representative case of a large array, consisting of 15625 solutions, sampled at the x25 budget, with the left representing the results from the previous master’s sampler, and the right from UniGen2.

Below is the same graph of UniGen2 solutions zoomed in, showcasing exactly how close to uniform the results are.

When presented with these benchmarks, as well as looking at the complete report, we see that UniGen2 gives better results than the previous sampler in almost every benchmark test, at every budget, and on every given metric. The only exceptions are three near-ties on coverage and divergence, where the two samplers land within about a percentage point of each other. That performance gap becomes greater as the constraints become less trivial.

However, it’s worth noting that UniGen2, by the very nature of how it works, does not take over every randomization. It’s designed for plain rand variables: scalars, arrays, queues and associative arrays alike; it steps aside for randc, solve ... before ordering, rand_mode(0)-frozen variables, soft constraints, and the first call for any given set of constraints (at which it waits for the second call with the same set, so the up-front measuring can pay for itself). In such cases, Verilator falls back to the sampler it used before with no change of behavior.

Future improvements for large solution spaces

Currently, our implementation of UniGen2 limits the number of XOR equations to 10 in order to keep solver time reasonable, as Z3 is not efficient when given a large number of XOR equations. For very large solution spaces, this limitation may leave cells bigger than the desired size.

In the future, we plan to continue our work on constrained randomization in Verilator by implementing an algorithm designed specifically for very large solution spaces.

Efficient SystemVerilog design testing using Verilator

The implementation of UniGen2 into Verilator opens a new door for more thorough verification of SystemVerilog designs, allowing for randomization of variables while maintaining a high percentage of coverage and uniformity. Antmicro is a frequent contributor to Verilator with years of experience developing solutions for helping with SystemVerilog design testing for various customers, the results of which are converging within the CHIPS Alliance’s SV Tools Project. Earlier this year, we implemented an initial version of four-state logic into Verilator, which is a significant stepping stone towards full four-state logic - a major milestone we are actively striving towards as part of our work on improving Verilator. We’ve also recently released the Verilator Playground, which we introduced at ORConf 2026, allowing you to use Verilator in the browser; with it, you can edit, compile and run SystemVerilog code, see coverage results, and much more!

With our experience and expertise, we can aid your ASIC and FPGA projects by providing commercial support for Verilator, designing custom tooling for design aggregation, developer productivity, fault injection, verification and test planning, and so much more. If you’d like us to assist you on your next project, reach out to us at contact@antmicro.com.