[Bug] Solver failure when comparing rand_bit_t field against boolean expression using ==

[Balajimcr]

Environment
Python: 3.11
PyVSC: 0.9.4.22122858116

PyVSC fails with a solver error when a rand_bit_t field is compared against a boolean expression using equality (==).

The equivalent SystemVerilog constraint works correctly in SV simulators.

Interestingly, replacing == with != makes the constraint pass in PyVSC.

This appears related to boolean vs bitvector coercion/typing during SMT lowering.

PyVSC Passing Example (!= works)

import vsc


@vsc.randobj
class RgbpRandItem:

  def __init__(self):
    self.AB = vsc.rand_int_t(32)
    self.CD = vsc.rand_int_t(32)
    self.boolean_multi_10 = vsc.rand_bit_t(32)

  @vsc.constraint
  def parameter_range(self):
    self.AB.inside(vsc.rangelist(vsc.rng(-255, 255)))
    self.CD.inside(vsc.rangelist(vsc.rng(-255, 255)))
    self.boolean_multi_10.inside(vsc.rangelist(vsc.rng(0, 1)))

  @vsc.constraint
  def cr0(self):
    self.AB == self.CD
    self.AB != 0

  @vsc.constraint
  def cr1(self):
    self.CD != 0

  @vsc.constraint
  def cr2(self):
    self.boolean_multi_10 != (
        (self.AB >= 0) |
        (self.CD <= 90)
    )


obj = RgbpRandItem()

obj.randomize(solve_fail_debug=1)

print("Randomization PASSED")
print(f"AB                = {obj.AB}")
print(f"CD                = {obj.CD}")
print(f"boolean_multi_10  = {obj.boolean_multi_10}")

PyVSC Failing Example (== fails)

import vsc


@vsc.randobj
class RgbpRandItem:

  def __init__(self):
    self.AB = vsc.rand_int_t(32)
    self.CD = vsc.rand_int_t(32)
    self.boolean_multi_10 = vsc.rand_bit_t(32)

  @vsc.constraint
  def parameter_range(self):
    self.AB.inside(vsc.rangelist(vsc.rng(-255, 255)))
    self.CD.inside(vsc.rangelist(vsc.rng(-255, 255)))
    self.boolean_multi_10.inside(vsc.rangelist(vsc.rng(0, 1)))

  @vsc.constraint
  def cr0(self):
    self.AB == self.CD
    self.AB != 0

  @vsc.constraint
  def cr1(self):
    self.CD != 0

  @vsc.constraint
  def cr2(self):
    self.boolean_multi_10 == (
        (self.AB >= 0) |
        (self.CD <= 90)
    )


obj = RgbpRandItem()

obj.randomize(solve_fail_debug=1)

print("Randomization PASSED")
print(f"AB                = {obj.AB}")
print(f"CD                = {obj.CD}")
print(f"boolean_multi_10  = {obj.boolean_multi_10}")

Failure Output

Problem Set: 3 constraints
  <unknown>:
    (AB == CD);

  <unknown>:
    (boolean_multi_10 == ((AB >= 0) | (CD <= 90)));

  <unknown>:
    boolean_multi_10 in [0..1];

[DEBUG] SolveFailure captured during debug re-run.

solve failure

Observation

The following constraint PASSES successfully in PyVSC:

@vsc.constraint
def cr2(self):
    self.boolean_multi_10 != ((self.AB >= 0) | (self.CD <= 90))

Only the equality (==) version fails.

Why This Appears Valid

The RHS expression:

(self.AB >= 0) | (self.CD <= 90)

is logically boolean.

The LHS:

self.boolean_multi_10

is constrained to:

0 or 1

which mirrors standard SV boolean/integral coercion behaviour.

SystemVerilog handles this correctly.

[alwilson]

It looks like those comparisons (or relational operators) such as self.AB >= 0 are returning signed 1-bit scalars that then get sign-extended to 32 bits, which should be unsigned. I'm also noticing that AB and CD are always negative due to the swizzling range algorithm picking the wrong number of bits for negative ranges. I've got some changes that fix both that I'll submit later.

[Balajimcr]

Thank you, @alwilson, once again for your blazing-fast response and for tracking down the root cause so quickly. The explanation regarding the signed 1-bit comparison result getting sign-extended, along with the swizzling range issue for negative ranges, makes perfect sense.

I tested the latest changes on my side, and the issue is now working correctly. Really appreciate the quick turnaround and detailed investigation.