dv-solve

dv-solve is a constraint solver for design verification. It finds values for bit-vector variables that satisfy a set of constraints, and when asked for many solutions it spreads them across the solution space. That suits it both to constrained-random stimulus generation and to answering yes/no questions from formal tools. Answers are sound: sat and unsat are definitive, and when dv-solve can't decide a problem it says unknown rather than guessing.

Documentation: https://dvkit.org/fvutils/dv-solve/

Ways to use it

Install

pip install dv-solve

The wheel holds the Python package, the native libraries, the C header, the SystemVerilog packages and the dv-solve-smt2 executable, which pip puts on PATH:

dv-solve-smt2 --version

To build everything from source instead:

cmake -S . -B build -DDVS_WITH_CADICAL=OFF
cmake --build build

See Installation for the details, including the optional CaDiCaL back end.

To develop in a checkout, set up the workspace with IVPM and build in place:

ivpm update -d dev
packages/python/bin/python setup.py build_ext --inplace

That fetches CaDiCaL and the Python environment into packages/, then builds the libraries into build/lib and dv-solve-smt2 into build/bin. The dv_solve package in src/ loads the library from build/lib.

Quick start

from dv_solve.builder import SolveProblemBuilder
from dv_solve.ctx import SolveCtx, SOLVE_OK
from dv_solve.problem import BIN_GT

b = SolveProblemBuilder()
X = 0
b.add_var(X, width=8, is_signed=False, lo=0, hi=255)
b.add_constraint(b.expr_binary(BIN_GT, b.expr_var(X), b.expr_const(100)))
problem, _ = b.finalize()

with SolveCtx(problem) as ctx:
    assert ctx.solve(seed=1, fair_pick=True) == SOLVE_OK
    print("x =", ctx.get_value(X))

Public API

Other modules are internal and may change. The C API is the one header dv_solve.h; other installed headers are internal. See the reference.

License

Apache-2.0.