[rfc] Constrained Random

[seldridge]

Placeholder issue for constrained random testing.

[sequencer]

I just pass by this issue for my CCC slide :) These comment copy and paste from my slide: constraint random is a easy Satisfiability Modulo Theory. We need an API for frontend, such as https://github.com/regb/scala-smtlib and https://github.com/dzufferey/scala-smtlib-interface (maybe these to need to be wrappered with simple API), and left rest to SMT solvers. Thus, I think these works are required:

1. an DSL to SMT representing constraint data, or parser to System Verilog constraint.
2. a compiler to emit standard SMTLIB file.
3. execute annotated solver to generate required random data, then consumed in Scala.

[ekiwi]

This can now be done using the formal backend. Biggest TODO is refining the user-facing API. Prototype: https://github.com/TsaiAnson/verif/blob/90b4d5f632d4f3e7cfa94623da63e3ec76c74c69/core/test/ConstrainedRandomTest.scala