verilator Towards constrained randomization

We are looking into adding constrained randomization support to Verilator. Obviously that is a pretty big undertaking, so we would like to reuse some existing work for this. It appears there are only two solutions available for C/C++:

SCV from Accellera, seems to require SystemC which is pretty much a deal-breaker,
CRAVE from the University of Bremen, MIT license, looks to be well thought-out. It can use many solvers as backends, which is really cool. Unfortunately it doesn't work on a newer compiler without some tinkering, and isn't really active. So we would have to resurrect it and make it more compatible. It also has a bunch of dependencies, mostly Boost libs. However, looking at it closer, a lot of this Boost stuff could be replaced by C++11/14/17/20 equivalents, or reimplemented pretty quickly by hand. Their constraint DSL uses Boost.Proto, but we don't need that for Verilator, so we could remove it or put it behind some #ifdefs.

Of course, such a library would only be a dependency for those that actually use constrained random in their tests.

Would be great to hear your thoughts on this @wsnyder. Are you open to using something like this? Perhaps there's a different, better option?

Sep 02 '22 07:09 kbieganski

scv seems fairly small and uses CUDD under the covers. I'd suggest look more into that as a starting point for our own C++ library, versus a C++ library we can directly reuse without changes. The big benefit of scv is we know it has succeeded in solving the "same" problem, and is C++ based.

Sep 02 '22 12:09 wsnyder

Note scv is using cudd 2.3.0 which is old, if you looking into it use the latest (3.0.0?).

Sep 02 '22 12:09 wsnyder

So CRAVE is out of the question?

Sep 05 '22 08:09 kbieganski

I'm not ruling any options out at this point, it just seemed you had ruled out SCV and my point was the main library isn't SCV but cudd which is portable.

Though, FWIW I would consider requiring boost a major negative in the scorecarding of options.

Sep 05 '22 13:09 wsnyder

Oh I agree. That's why we're considering ripping it out. What I like about CRAVE is that it has multiple backends, including CUDD. If not CRAVE, perhaps we could use their solver wrapper library, metaSMT.

Sep 05 '22 15:09 kbieganski

Hi @wsnyder & @kbieganski, What is the current status for constraint randomization. Is this begin worked on?

Jan 08 '24 06:01 InputBlackBoxOutput

I've been doing some research on it, but it's not a priority. I wouldn't expect a usable implementation anytime soon. Contributions are welcome :)

Jan 08 '24 11:01 kbieganski