PyVSC internal solver error with satisfiable signed arithmetic constraint involving multiply/divide expressions

[Balajimcr]

Environment
Python: 3.11
PyVSC: 0.9.4.22122858116

Problem Summary

A satisfiable constraint set randomises successfully in SystemVerilog simulators (Cadence), but fails in PyVSC with:

Exception: internal error: system should solve

The issue appears related to:

signed arithmetic
multiplication
division
negative intermediate expressions
symbolic arithmetic normalisation

The constraint system is mathematically satisfiable.

This does NOT appear to be a true UNSAT condition.

Instead, it looks like an internal PyVSC arithmetic modelling or solver reconstruction issue.

Minimal PyVSC Code:

import vsc


@vsc.randobj
class RgbpRandItem:

  def __init__(self):
    self.AB = vsc.rand_int_t(32)
    self.CD = vsc.rand_int_t(32)
    self.div_3 = vsc.rand_int_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.div_3.inside(vsc.rangelist(vsc.rng(-65535, 65535)))

  @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.div_3 >= ((((self.AB * -1) * 2) * self.CD) / 1024)
    self.div_3 <= ((self.AB * self.CD) / 1024)


obj = RgbpRandItem()
obj.randomize(solve_fail_debug=1)

print(obj.AB)
print(obj.CD)
print(obj.div_3)

Full Error
Exception: internal error: system should solve

Stack trace:

Traceback (most recent call last):
  File "...", line ...
    obj.randomize(solve_fail_debug=1)

  File ".../vsc/model/randomizer.py", line 446, in create_diagnostics
    raise Exception("internal error: system should solve")

Exception: internal error: system should solve

Corresponding System Verilog Code:

class rgbp_rand_item extends uvm_sequence_item;

 rand bit signed [31:0] AB;
 rand bit signed [31:0] CD;
 rand bit signed [31:0] div_3;

`uvm_object_utils_begin(rgbp_rand_item)
 `uvm_field_int(AB, UVM_DEFAULT)
 `uvm_field_int(CD, UVM_DEFAULT)
 `uvm_field_int(div_3, UVM_DEFAULT)
`uvm_object_utils_end
   constraint CR_VAR_RANGE_AB
     {
       (AB >= -255 && AB <= 255);
     }

   constraint CR_VAR_RANGE_CD
     {
       (CD >= -255 && CD <= 255);
     }

   constraint CR_VAR_RANGE_div_3
     {
       (div_3 >= -65535 && div_3 <= 65535);
     }

   constraint cr0
     {
       AB == CD; AB != 0;
     }

   constraint cr1
     {
       CD != 0;
     }

   constraint cr2
     {
       div_3 >= (- AB * 2) * CD / 1024; div_3 <= AB * CD / 1024;
     }

endclass

Why This Constraint Is Valid

The constraints reduce to:

AB == CD
AB != 0
CD != 0

Therefore:

AB = CD = x
x ∈ [-255,255]
x != 0

Constraint:

div_3 >= (-AB * 2) * CD / 1024
div_3 <= AB * CD / 1024

becomes:

div_3 >= -2*x²/1024
div_3 <= x²/1024

This is clearly satisfiable.

Example valid solution:

AB = 255
CD = 255
div_3 = 0

The same constraint randomises successfully in Cadence SystemVerilog simulators.

This suggests the original SV semantics are valid, and the issue is specific to PyVSC arithmetic handling or solver integration. Please suggest how to fix this issue.

[alwilson]

I started getting the solver to pass when I moved the -1 in ((((self.AB * -1) * 2) * self.CD) / 1024) till after the division. I tried to use the PyBoolector dump command to see what the solver was doing (in btor and smt2 format), but it wasn't very readable to me. I saw the different division operators in the PyBoolector docs and that led me to finding out how pyvsc was mapping things. Hope this helps!

[Balajimcr]

Thank you @alwilson, for your quick reply and for identifying the root cause. I also confirmed that moving the -1 after the division allows the solver to pass on my side as well.

I appreciate the fix for signed division handling in the pyvsc library. The explanation regarding the different division operator mappings in PyBoolector was very helpful and gave much better insight into where the semantic mismatch was occurring.

[alwilson]

@Balajimcr You're welcome and thanks for isolating these test cases!