[BUG] PyVSC Solver Failure with Mixed Signed/Unsigned Arithmetic

[Balajimcr]

Environment
Python: 3.11
PyVSC: 0.9.4.22122858116

PyVSC reports a solve failure for a satisfiable constraint set involving:

two unsigned 32-bit variables (rand_bit_t(32))
one signed 32-bit variable (rand_int_t(32))
multiplication by a negative constant (-2)
a bounded signed result variable

The equivalent SystemVerilog constraint randomises successfully in commercial simulators.

The issue appears to be related to arithmetic type promotion and/or signedness handling when evaluating:

self.C >= ((-2 * self.A * self.B) / 1024)

PyVSC Failing Example (Failing)

import vsc

@vsc.randobj
class Item:

    def __init__(self):
        self.A = vsc.rand_bit_t(32)
        self.B = vsc.rand_bit_t(32)
        self.C = vsc.rand_int_t(32)

    @vsc.constraint
    def c(self):
        self.A.inside(vsc.rangelist(vsc.rng(32, 12288)))
        self.B.inside(vsc.rangelist(vsc.rng(1, 32767)))
        self.C.inside(vsc.rangelist(vsc.rng(-32767, 32767)))

        vsc.solve_order(self.A, self.C)
        vsc.solve_order(self.B, self.C)

       self.C >= ((-2 * self.A * self.B) / 1024)
       self.C <= ((self.A * self.B) / 1024)


obj = Item()
obj.randomize()

print(f"A={obj.A} B={obj.B} C={obj.C}")

PyVSC reports:

Problem Set: 4 constraints

(C >= (((A * B) * -2) / 1024));
(C <= ((A * B) / 1024));
A in [32..12288];
B in [1..32767];

solve failure

Randomisation fails consistently.

Additional Observation: Equivalent Mathematical Expression Solves Successfully

self.C >= -1 * ((2 * self.A * self.B) / 1024)

PyVSC Failing Example (Working)

import vsc

@vsc.randobj
class Item:

    def __init__(self):
        self.A = vsc.rand_bit_t(32)
        self.B = vsc.rand_bit_t(32)
        self.C = vsc.rand_int_t(32)

    @vsc.constraint
    def c(self):
        self.A.inside(vsc.rangelist(vsc.rng(32, 12288)))
        self.B.inside(vsc.rangelist(vsc.rng(1, 32767)))
        self.C.inside(vsc.rangelist(vsc.rng(-32767, 32767)))

        vsc.solve_order(self.A, self.C)
        vsc.solve_order(self.B, self.C)

        self.C >= -1 * ((2 * self.A * self.B) / 1024)
        self.C <= ((self.A * self.B) / 1024)


obj = Item()
obj.randomize()

print(f"A={obj.A} B={obj.B} C={obj.C}")

[alwilson]

I peeked at how we handle signed and unsigned with multiplication and I think pyvsc is doing the right thing. I also converted the failing testcase to SystemVerilog (attached below) and it fails with an inconsistent constraint error. Does that match your SV testcase?

class basic;
  rand bit [31:0] A;
  rand bit [31:0] B;
  rand int        C;

  constraint c_abc {
    A inside {[32 : 12288]};
    B inside {[1 : 32767]};
    C inside {[-32767 : 32767]};

    solve A before C;
    solve B before C;

    C >= ((-2 * A * B) / 1024);
    C <= (A * B) / 1024;
  }
endclass

program p_basic;
    basic obj;

    initial begin
        obj = new;
        obj.randomize();
        $display("%p", obj);
        for (int i = 0; i < 5; i++) begin
            obj.randomize();
            $display("%p", obj);
        end
    end
endprogram

Also, in the expression self.C >= ((-2 * self.A * self.B) / 1024) the -2 * self.A combines a signed and an unsigned operand, which results in an unsigned value. Is that what you intend to happen in this constraint?

[Balajimcr]

Yes, you are correct. It is failing in System Verilog code as well. But how to handle this scenario in the code?

[alwilson]

I think the most info you'll get right now is usingsolve_fail_debug=1. I believe SMT solvers refer to this as the unsat core. I'm not sure if boolector has that feature and pyvsc narrows down the failure to constraints that are failing. In this case it appears the only extra information it add is that this constraint isn't contributing to the problem:

self.C.inside(vsc.rangelist(vsc.rng(-32767, 32767)))

Example output using the failure debug flag:

obj.randomize(solve_fail_debug=1)
...
Problem Set: 4 constraints
  <unknown>:
    B in [1..32767];
  <unknown>:
    A in [32..12288];
  <unknown>:
    (C >= (((-2 * A) * B) / 1024));
  <unknown>:
    (C <= ((A * B) / 1024));
...
vsc.model.solve_failure.SolveFailure: solve failure

[alwilson]

I plugged the failing python snippet and the unsat core into Gemini 3.1 Pro and it gave me a nice analysis. The expression -2 * A * B using the smallest values for A and B is -2 * 32 * 1 => -64 (signed) => 4,294,967,232 (unsigned) means C, after the 1024 division, has to be C >= 4,194,303.

I know z3 and other SMT solvers have more options for unsat core minimization and analysis. I found an interesting z3 script implementing an algorithm for enumerating all maximal satisfiable subsets (MSSes) or minimal unsatisfiable subsets (MUSes). I converted this problem into a z3py expression and had it enumerate them all. Still a bit confusing with the signed-as-unsigned output, but it's interesting to see what combinations of constraints work and don't work.

MUS:
	And(UGE(A, 32), ULE(A, 12288))
	And(UGE(B, 1), ULE(B, 32767))
	C >= UDiv(4294967294*A*B, 1024)
	C <= UDiv(A*B, 1024)
MUS:
	And(UGE(A, 32), ULE(A, 12288))
	And(UGE(B, 1), ULE(B, 32767))
	And(C >= 4294934529, C <= 32767)
	C >= UDiv(4294967294*A*B, 1024)
MSS:
	And(UGE(B, 1), ULE(B, 32767))
	And(C >= 4294934529, C <= 32767)
	C >= UDiv(4294967294*A*B, 1024)
	C <= UDiv(A*B, 1024)
MSS:
	And(UGE(A, 32), ULE(A, 12288))
	And(C >= 4294934529, C <= 32767)
	C >= UDiv(4294967294*A*B, 1024)
	C <= UDiv(A*B, 1024)
MSS:
	And(UGE(A, 32), ULE(A, 12288))
	And(UGE(B, 1), ULE(B, 32767))
	And(C >= 4294934529, C <= 32767)
	C <= UDiv(A*B, 1024)
MSS:
	And(UGE(A, 32), ULE(A, 12288))
	And(UGE(B, 1), ULE(B, 32767))
	C >= UDiv(4294967294*A*B, 1024)