Introducing constrained randomization in Verilator

Large and complex SystemVerilog designs, such as CPUs, are difficult to test thoroughly, as there are many interesting signal combinations that influence a design’s behavior, including corner cases that are easy to overlook. Randomization is one strategy to increase testing coverage, however, not all randomly generated test values are interesting from a testing perspective. This is where constrained randomization comes into play – it helps ensure you use only relevant test values by limiting the possible randomization outputs, which also helps reduce the overall test case number. Constrained randomization is thus a crucial part of UVM testbenches which are standard in the SystemVerilog world, and it’s the backbone of verification suites in both closed and open silicon projects, such as OpenTitan, Open Se Cura or Caliptra (all of which we have been working with).

Within the CHIPS Alliance, together with customers like Google and Western Digital (and the broader community), Antmicro has been working towards enabling open source UVM support in Verilator, one of the most popular open source digital design tools for ASIC and FPGA development.

As active contributors, we have been providing commercial support to hyperscalers, silicon vendors and product companies involved in making their own chips to improve Verilator to enable a variety of production workloads, both in the context of local and cloud/CI usage. Today we are happy to present a recent development that closes an important gap towards open source UVM support by introducing constrained randomization into Verilator, opening the door to leverage infinite cloud scaling for ASIC verification.

Initial implementation with CRAVE

Verilator has had limited support for randomization before, but it’s the ability to introduce guided constraints that really make the feature useful for production-grade verification. Our first approach to implementing constrained randomization in Verilator involved using an external library, CRAVE. This allowed for very basic constrained randomization support, including value-based, soft and dynamic constraints.

CRAVE is a versatile tool, created with research and experimentation in mind, and as such, it turned out to be quite heavyweight for our specific needs. As described in a previous blog note, this initial PoC implementation was not optimal due to CRAVE’s complicated build process with multiple nested dependencies. It did, however, provide a good starting point for the current implementation – based on the experience of integrating CRAVE’s randomization mechanisms into Verilator, we knew what we had to do differently this time around to avoid challenges such as introducing new build time dependencies in Verilator.

Implementing constrained randomization in Verilator

With the new approach, Verilator parses constraints expressed in the SystemVerilog language as before, however, instead of generating API calls for CRAVE, it generates expressions in the smtlib2 language, which is used by many open source solvers. The result is a series of math equations that need to be solved by general purpose solvers, such as z3, cvc4 or cvc5. One issue with such constraint solvers is that they are deterministic and therefore they can only produce one solution for a given constraint set. Based on our experiences with the initial CRAVE integration, we introduced randomness by further narrowing the solution space with an extra artificial random constraint.

Verilator creates expressions and then executes the solvers in runtime. The language used for the solvers is fairly standard, as opposed to C APIs used by the solver libraries – usually each library has its own dedicated API, so switching from one to another could be troublesome. A common language means that switching to a different solver is fairly straightforward, and adding support for additional solvers is just a matter of preparing runtime command line arguments for them.

This new implementation introduces no new build time dependencies in Verilator, neither when building Verilator itself, nor when building the verilated code. Moving the dependency to runtime means it’s completely optional. Users will have a selection of solvers to choose from – many of those are widely available in most common distributions, so adding a solver would be a matter of running a single command like (on Debian-based distros) apt install z3 and using Verilator installed from the OS packages, as opposed to having to recompile Verilator with CRAVE.

Due to its novelty, constrained randomization support in Verilator is still being actively developed and improved – you can track its progress in this PR.

Complex SystemVerilog design verification with Antmicro

More details about constrained randomization in Verilator will be described soon in a separate blog note. The implementation introduced in this note was partially developed within the EU-funded TRISTAN project aiming at creating and improving more open and reusable tooling for RISC-V SoC development. An immediate goal is gradually adopting the new development in a variety of open source projects we participate in under the auspices of CHIPS, such as Google’s riscv-dv framework, the VeeR core used by Caliptra, etc.

If you’re interested in Antmicro’s help expanding constrained randomization and UVM support in Verilator to handle the verification of your complex ASIC projects, or require support in integrating Verilator into your workflow, don’t hesitate to contact us at contact@antmicro.com.