Multiplication constraints use overflow to solve

Fun little bug here.

I created a simple constraint to generate an dest and src image sizes including src and width. I was going to get more complex, but saw this issue while testing what I had. This is a paired down version of my code which I tested and still saw the issue.

@vsc.randobj
class cmd():

  def __init__(self):
    self.DG_mem_map_src_size_rand = vsc.rand_bit_t(16)
    self.DG_mem_map_dst_size_rand = vsc.rand_bit_t(16)
    self.SrcDepth_rand = vsc.rand_bit_t(16)
    self.SrcWidth_rand = vsc.rand_bit_t(16)

  @vsc.constraint
  def tdf_size_c(self):
    #Basic constraint conditions
    #max size
    self.DG_mem_map_src_size_rand <= 1000
    self.DG_mem_map_src_size_rand >= 200
    self.DG_mem_map_dst_size_rand <= 1000

    self.DG_mem_map_src_size_rand == self.SrcDepth_rand * self.SrcWidth_rand
    self.DG_mem_map_dst_size_rand == self.SrcDepth_rand * self.SrcWidth_rand * 2

cmd = cmd()
for i in range(0,10):
    cmd.randomize()
    print("iter", i)
    print("src_size ", cmd.DG_mem_map_src_size_rand)
    print("dst_size ", cmd.DG_mem_map_dst_size_rand)
    print("SrcDepth ", cmd.SrcDepth_rand)
    print("SrcWidth ", cmd.SrcWidth_rand)

I frequently see results which take advantage of overflow to solve the constraint.

For example:

src_size  402
dst_size  804
SrcDepth  65095
SrcWidth  32990

65095 * 32990 = 2147484050 2147484050 -> 0x 8000 0192 This result is bigger than 1000, but truncating to 16 bits gives 0x192 0x192 == 402

So it solved the constraint technically, but is leveraging overflow to do so which isn't what I expected to see.

Admittedly, it's been a while since I've done SV constraints, so not sure if this behavior is seen there as well.

I can solve this issue by putting an upper bound on the src/width to be smaller than the result, but wanted to point out this behavior in case it should be fixed. If this is the expected behavior/solution, then please go ahead and close this issue.

fvutils / pyvsc

Multiplication constraints use overflow to solve #114