Enabling UVM Support in Verilator Series — Constrained Randomization Support for All Types of Arrays

The DI-OSVISE project (De:sign Initiative – Open Source Verification of RISC-V Instruction Set Extensions), funded by the BMBF, aims to advance open-source tools for sustainable and reliable microelectronics in Germany and Europe. One of the goals of our participation in the project is to bridge the gap between open-source verification and industry standards by enhancing UVM support in Verilator.

1. Introduction

In our previous blog, we discussed PlanV’s contributions to Verilator by supporting basic randomization for aggregate data types. Building on that foundation, this blog delves into both the general principles of constrained randomization in Verilator and how PlanV has extended Verilator to support constrained randomization for all kinds of arrays. This essential feature plays a critical role in advanced verification scenarios, particularly in UVM-based testbenches.

Verilator’s previous limitation in supporting constrained randomization for arrays has been resolved through PlanV’s contributions, marking a significant enhancement in its capabilities. This blog outlines how PlanV contributed to solving this limitation, enabling support for all array types in Verilator.

2. Pre-Contribution State of Constrained Randomization in Verilator

To fully understand the progress made, it is important to first identify the gap in Verilator’s constrained randomization support prior to PlanV’s contributions. At that time, Verilator only supported constrained randomization for basic data types, such as int and bit, leaving more complex types, like arrays, unsupported.

So, let’s first take a closer look at how Verilator supports constrained randomization for basic data types, as this serves as the foundation for PlanV’s work. After that, we’ll dive into PlanV’s contributions.

This basic support is achieved through three key steps: AST processing, data structure storage, and solver interaction.

2.1 AST Processing (Verilate Phase)

As mentioned in the previous blog, Verilator’s workflow consists of two distinct phases: the verilate phase and the simulate phase. The process begins in the verilate phase, where Verilator parses SystemVerilog source code into an Abstract Syntax Tree (AST) and processes the AST to generate a series of C++ files for simulation.

Specifically, for randomization, this step identifies rand variables, marks them, and processes user-defined constraints. For example, consider the following SystemVerilog code:

rand int a;
constraint c { a inside {1, 2}; }

• The variable a is marked as a random variable (rand).
• The constraint specifies that a can only take values 1 or 2.

During the verilate phase, Verilator processes the AST to:

• Extract random variables using the write_var method.
• Extract SMT-LIB2 format constraints using the hard method.

SMT-LIB here is a widely adopted standard language, supported by many open-source solvers such as z3-solver and cvc5, making it highly versatile and compatible.

Once all AST processing is finished, C++ files will be generated, marking the completion of the verilate phase. These files set the foundation for the simulate phase, where actual randomization and solver interaction occur.

2.2 Store in m_vars and m_constraints(Simulate phase)

At the end of the verilate phase, Verilator generates C++ files based on the processed AST. These files, however, rely on “library functions” provided by Verilator (in the include folder) to complete simulation and produce the simulation results.

When it comes to randomization, one of the most critical components in this phase is the VlRandomizer class, defined in verilated_random.cpp/h. This class is designed to manage random variables and constraints efficiently.

To achieve this:

• The write_var method processes the random variables extracted in the verilate phase and stores them in the m_vars container.
• The hard method handles constraints in SMT-LIB2 format, storing them in the m_constraints container.

Fig. 1 shows an overview of the VlRandomizer class. The write_var and hard methods are responsible for populating m_vars and m_constraints. Other methods, such as randomConstraint(), parseSolution(), and next(), are used later for solver interaction and randomization logic.

Fig. 1 VlRandomizer class

By organizing variables and constraints into these two structures, Verilator lays the foundation for generating SMT-LIB2 descriptions and interacting with external solvers in the simulate phase.

2.3 Call External Solver

After storing variables in m_vars and constraints in m_constraints, VlRandomizer interacts with an external solver, such as z3-solver, which uses the SMT-LIB2 format, to evaluate and solve the constraints, as shown in Fig. 2.

Fig. 2 Solver Interaction

To understand how the solver processes these constraints and achieves the randomization, let’s take a closer look at its internal process, illustrated in Fig. 3. Once the solver is called and initiated, the following key steps occur:

1. Solver Initialization: The solver environment is initialized, and the logic type (e.g., QF_BV, quantifier-free bit-vectors), is defined. This establishes the rules and domain for the solver.
2. Define Helper Functions: Complex constraints may require auxiliary functions or macros, which are prepared during this step.
3. Variable Declarations: All random variables stored in m_vars are declared in the SMT-LIB2 format.
4. Constraints Assertion: The constraints from m_constraints are asserted, forming the basis of the solver’s satisfiability check.
5. Dynamic Constraint Generation: To ensure pseudo-randomness, the VlRandomizer dynamically generates additional constraints during the randomization process. These constraints often involve bit-level operations such as extract and concat. They modify the range or behavior of variables in a way that enhances diversity while maintaining constraint compliance.
6. Check Satisfiability: The solver evaluates the constraints to determine whether they can be satisfied. If so, it generates a valid solution.
7. Parse Solution: The solution is extracted from the solver’s output.
8. Assignment: The parsed solution is assigned back to the corresponding variables in the simulation environment.
9. Reset Solver State: After processing, the solver is reset, preparing for the next randomization.

Fig. 3 Detailed SMT-LIB2 Solver Workflow

3. The Challenge with Arrays

Previously, we detailed how Verilator supports constrained randomization for basic data types, such as int and bit. However, when it comes to complex data structures, like arrays, Verilator currently lacks native support.

In our earlier blog about basic randomization support, we introduced the concept of aggregate data types in SystemVerilog. Among these, arrays are particularly important and are divided into packed and unpacked types:

• Packed Arrays
  Packed arrays are treated as a long vector of contiguous bits. This straightforward representation allows them to be supported in Verilator by simply treating them as basic types. For example:

 rand logic [7:0][3:0] packed_arr;

In this example, the array consists of 4 elements, each 8 bits wide, resulting in a 32-bit vector. Verilator’s randomization process directly treats it as a basic type and generates SMT-LIB2 constraints accordingly, requiring no additional structural metadata.

• Unpacked Arrays
  Unpacked arrays present significant challenges due to their non-contiguous memory layout and dynamic sizing. Unlike packed arrays, they require additional metadata to describe their structure. To enable constrained randomization for unpacked arrays, several issues must be addressed:
  • Precise Element Access: Each element of an array needs to be represented and accessed accurately in the SMT-LIB2 format. This involves generating unique identifiers for each index and mapping them correctly in the solver.
  • Dimensionality: Multi-dimensional arrays add another layer of complexity. For example:

rand int unpacked_arr [4][3];

This declaration represents a 4x3 matrix, which requires handling cross-dimension indexing and maintaining consistency across dimensions during randomization.

• Variable-Sized Arrays: Unlike fixed-sized arrays, variable-sized arrays (e.g., dynamic, queue, associative) further complicate element representation and access. Although their sizes are determined at the beginning of the simulate phase, their lack of uniformity across dimensions presents unique challenges:
  • Dynamic Arrays and Queues: The size of these arrays can vary across dimensions, requiring flexible storage mechanisms that can efficiently handle their dynamic structure.
  • Associative Arrays: These arrays rely on key-based indexing. Keys can vary in type and include integers, strings, or even user-defined types like packed structs or packed arrays.

4. PlanV’s Contributions

To enable support for all kinds of arrays in constrained randomization, PlanV implemented several enhancements to Verilator’s framework. These contributions addressed the limitations discussed earlier by introducing:

• New SMT-LIB2 Array Logic for solver compatibility.
• Template-Based Iterative Processing for efficient metadata handling.
• Specialized Handling for Associative Arrays to support diverse index types.

4.1 SMT-LIB2 Array Construction

PlanV introduced a new logic, QF_ABV (Quantifier-Free Array and Bit-Vector), to build and manipulate arrays in SMT-LIB2 format. This logic enables Verilator to define, access, and modify arrays seamlessly within the solver. The core operations include:

• Declaration: Define arrays using declare-fun.
• Element Access: Use select to extract array elements.
• Element Modification: Use store to modify elements.

For example:

(declare-fun my_array () (Array Int Int))
(assert (= (select my_array 1) 42))  ; Accessing an element
(assert (= my_array (store my_array 1 84))) ; Modifying an element

These simple yet powerful operations provide the foundation for supporting all types of arrays in Verilator, enabling compatibility with external solvers.

4.2 Template-Based Iterative Array Processing

While SMT-LIB2 logic provides a solution for array declaration and element access, Verilator requires precise metadata to handle arrays effectively. This metadata includes indexed names, dimensions, and indexing information. Moreover, Verilator needs methods to transform metadata into SMT-LIB2 expressions for solver interaction. Recognizing the shared characteristics across various array types—such as packed, unpacked, dynamic, and associative arrays—PlanV adopted a template-based iterative method. This method enhances array handling, improves performance, and simplifies code maintenance. The approach comprises the following key steps:

4.2.1 Recording Array Information

Array metadata, including indexed names, dimensions, and indexing information, is extracted and stored in m_arr_vars as shown in Fig. 4. This structure complements m_vars:

• Complementary Storage: While high-level details like array names are recorded in m_vars, detailed metadata about each array is stored in m_arr_vars. This includes dimension sizes, type information, and element indexing.
• Efficient Metadata Lookup: Metadata is stored in a dictionary-like structure, where m_vars.name() serves as the key to access m_arr_vars. This eliminates the need to traverse and dissect array structures repeatedly during solver interaction, addressing performance bottlenecks in element access.

Fig. 4 Recording Array Information in m_arr_vars

4.2.2 Iterative Processing via record_arr_table()

PlanV introduced the record_arr_table() method to iteratively process arrays:

• Dimension-Focused Processing: This method concentrates on the current dimension of an array without impacting other dimensions. This approach simplifies the handling of variable-sized arrays, such as dynamic arrays and queues, as it eliminates the need to resolve dimension sizes during every access.
• Single Pass Efficiency: A single traversal of the array processes all dimensions and elements, significantly improving the efficiency of multi-dimensional and cross-type array handling.
• Multi-Dimensional and Cross-Type Compatibility: The iterative, template-based processing seamlessly supports arrays of various types and dimensions, overcoming the challenges of nested arrays or arrays with mixed types. (See Fig. 5 for an illustration.)

Fig. 5 Diagram of record_arr_table()

4.2.3 Template-Based Unified Methods

To handle arrays effectively and maintain clean, concise code, PlanV implemented a template class for all array types:

• Shared Methods for All Arrays: The template class includes key methods like emitType(), emitSelect(), which are used to declare array types, access elements, and update values in SMT-LIB2 format, ensuring uniform handling across all array types.
• Unified Logic Across Types: Arrays of different types (e.g., packed, unpacked, associative) can access and utilize these template methods, minimizing redundancy and ensuring consistency in solver interaction.

By introducing m_arr_vars, iteratively processing arrays with record_arr_table(), and implementing a unified template class, PlanV addressed the complexities of array metadata management and element access. These enhancements ensure that Verilator can efficiently handle arrays of all types, enabling robust constrained randomization in simulation workflows.

4.3 Handling Associative Array Indices

Associative arrays require special handling due to their flexible indexing types. Unlike other arrays that use integers as indices, associative arrays can utilize more complex types, including:

• Integral Indices:
  • Standard 32-bit indices are directly supported.
  • For wider indices, a chunk-based approach is used. Indices are divided into chunks, and the size of each chunk is stored in a width vector. During retrieval, these chunks are reconstructed based on the width vector, ensuring compatibility with solver constraints, as shown in Fig. 6.

Fig. 6 Chunk-based Approach

• Non-Integral Types:
  • Associative arrays can use strings, packed structs, enums, and packed arrays as indices. Although constraints in IEEE 1800-2023 require expressions to evaluate to either integer or real types, these types are supported because they allow equality (==) operations, making them compatible with constraint expressions.
  • We implemented custom processing to ensure these index types are seamlessly translated into SMT-LIB2-compatible expressions.

By introducing chunk-based indexing for wide indices and supporting equality-comparable types in constraints, we extended Verilator’s capabilities to fully handle the diverse indexing requirements of associative arrays.

4.4 Final System Architecture

After these contributions, the updated Verilator framework seamlessly integrates array support into its existing Constrained Random Processing system. The overall architecture, illustrated in Fig. 7, demonstrates the complete workflow from AST processing to generating constrained random results.

The process begins with the AST, where the write_var and hard functions extract variables and constraints. These are then passed to the VlRandomizer class, which stores variables in m_vars and constraints in m_constraints. For arrays, record_arr_table iteratively processes and stores metadata in m_arr_vars for efficient access and manipulation of arrays.

Within the VlRandomizer class, methods help convert variables into SMT-LIB2 format and handle constraints during solver interaction. Data is sent to the external solver, which evaluates the constraints and generates valid random solutions.

Finally, the solver’s output is parsed and assigned back to the corresponding simulation variables, completing the constrained randomization cycle. This end-to-end system leverages Verilator’s efficiency while incorporating robust support for complex array types, enabling advanced verification scenarios with dynamic and multi-dimensional data structures.

Fig.7 Overall Framework of Randomization

5. Conclusion

It is our pleasure to invite everyone to explore the newly enhanced constrained randomization functionality in Verilator. As of the latest commit to Verilator’s master branch, constrained randomization for all array types has been fully supported. This represents PlanV’s recent key contribution to Verilator’s randomization capabilities and marks a significant milestone — Verilator now supports nearly all variable types for randomization. With this achievement, PlanV has reached a major phase goal in its randomization efforts and will now shift focus to new directions.

These contributions have also brought Verilator closer to full UVM support. PlanV’s work has made meaningful progress in addressing the items on Verilator’s `uvm_pkg_todo.svh` list, further solidifying its position as an advanced verification tool.

Looking ahead, PlanV will explore other areas of Verilator’s development, aiming to fill more gaps in SystemVerilog feature support. By doing so, we hope to expand Verilator’s capabilities and strengthen its role in modern verification workflows.

PlanV’s contributions have significantly enhanced Verilator’s constrained randomization capabilities. By enabling support for all array types, the framework now aligns with SystemVerilog’s aggregate data type requirements, paving the way for advanced UVM testbenches.