[RFC] constrained randomization with popen and external solvers

[kozdra]

Verilator currently has support for basic randomization, but the constraints are ignored. Our previous approach involved an exteral library called CRAVE, which was versatile, but quite heavyweight for our limited needs, not yet packaged on any major distro and had a quite cumbersome build process (multiple nested dependencies). The high-level overview of the changes is that the constraints get expressed in SMT-LIB2 format (textual Lisp), written at runtime into a temporary file, and then solvers like z3, cvc4 or cvc5 are popen()ed and their output parsed.
The advantage of the approach over using the API of an external library are as follows:

• there are absolutely no build dependencies introduced to neither Verilator itself nor verilated code,
• the user does not need to have any new development headers installed,
• all three of the suggested solvers are packaged for Debian and many other major distros,
• the solver engines can be changed very easily both usage-wise and licensing-wise
  (this is effectively using a well-defined external batch processing interface),
• the problem description language looks fairly standard compared to C APIs of the solvers,
• the randomization can fail gracefully at runtime (here actual obj.randomize() warns and returns 0,
  doing no randomization, but it could equally easily randomize without looking at the constraints)
  instead of hindering the whole compilation process.
  Additionally, satisfiability modulo theories (SMT) solvers are typically faster than binary decision diagram (BDD) solvers, which could be considered as an alternative approach.

One nice example class that illustrates how the generated expression looks like:

class Cls;
   rand int x;
   int y;
   constraint UPPERBOUND { 3 * x < 2 * y; }
endclass

The class gets a method that could be expressed in a pseudo-SystemVerilog:

function UPPERBOUND_setup_constraint()
   this.constraint.hard($sformatf("(bvslt (mul #b0000000000000011 x) #b%b)", 2 * y));
endfunction

The main challenge was that the solvers are deterministic and do not typically have many possibilities to influence the results. The randomization is therefore achieved by adding an extra artificial constraint, choosing random bits of the variables being randomized, and forcing their xor to a random value, inspired by our understanding of CRAVE's randomization mechanisms. This forces an extra random narrowing of solution space, and hopefully introduces enough noise to the solver's internal state that the solutions start behaving more random.

Things done here:

• constraints involving simple expressions (basic arithmetic and logic)
• actual randomization (Verilator's PRNG has measurable effect)

Things still to consider:

• explicitly specifying a solver (very doable, not sure if useful)
• specifying probability distribution (should be considered separately)
• solve X before Y (does not change the solution space itself, only the probability distribution)
• the default probability distribution is likewise not very uniform
• switching constraints on and off (still ignored)
• contrary to the example code, constraints depending on state (doable in the future, but currently a warning is emitted)
• conditional constraints (still unsupported)
• randomizing complex variables, like arrays (still unsupported)
• soft constraints (simply treated as hard, no warning)
• obj.randomize() with {...} (still unsupported)

The changes are split into several commits for easier review.

Related issues: #2879 #3901

[wsnyder]

I believe we'll need to integrate a solver directly eventually because:

• It will be faster
• It'll consume less effort than supporting multiple solvers
• We'll find bugs in the solver we need to fix, and the fixes couple with Verilator

However I agree this decoupled approach is an acceptable way to make progress in the meantime.

It's not clear from the patch when the solver is needed. We should try to write internal code to remove whatever we can from the solver and continue to skip as needed - I think pretty much every variable that has "easy" constraints without coupling to other variables should be able to be done by Verilator without a solver. (And even after we have a real integrated solver to help runtime we should simplify what we can at compile time.)

As to the patch itself:

• The current patch is spawning a solver process for every solution. This is untenable from a performance standpoint. Please run it with --in, and feed commands to the "same" session as needed - perhaps you can also load up definitions at init time to make the interactive part faster. The pipe-filter option in Verilator is example code of how to do something similar.

• What that's currently in verilated_random can instead be moved to compile time? (In addition to what can be done at z3 startup per above)

• Need some internals.rst documentation on the sort of commands we send to/from the solver.

• Check for missing const's.