0.7.7

- (#161) Adjust swizzling algorithm to improve multi-variable distribution

Signed-off-by: Matthew Ballance <[email protected]>

doc/Changelog.md

@@ -1,4 +1,7 @@
 
+## 0.7.7
+- (#161) Adjust swizzling algorithm to improve multi-variable distribution
+
 ## 0.7.6
 - (#160) Cache a coverpoint's target value to improve efficiency when 
   computing the target value is time consuming 

etc/ivpm.info

@@ -1,4 +1,4 @@
 
 name=pyvsc
-version=0.7.6
+version=0.7.7
 

src/vsc/model/randomizer.py

@@ -82,7 +82,7 @@ def __init__(self, randstate, debug=0, lint=0, solve_fail_debug=0, solve_info=No
             self.solve_fail_debug = glbl_solvefail_debug
 
 #        self.swizzler = SolveGroupSwizzlerRange(solve_info)
-        self.swizzler = SolveGroupSwizzlerPartsel(randstate, solve_info)
+        self.swizzler = SolveGroupSwizzlerPartsel(randstate, solve_info, debug=self.debug)
 
     _state_p = [0,1]
     _rng = None

src/vsc/model/solvegroup_swizzler_partsel.py

@@ -16,8 +16,8 @@
 
 class SolveGroupSwizzlerPartsel(object):
 
-    def __init__(self, randstate, solve_info):
-        self.debug = 0
+    def __init__(self, randstate, solve_info, debug=0):
+        self.debug = debug
         self.randstate = randstate
         self.solve_info = solve_info
 
@@ -59,7 +59,6 @@ def swizzle_field_l(self, field_l, rs, bound_m, btor):
             field_l = field_l.copy()
 
             swizzle_node_l = []
-            swizzle_expr_l = []
             max_swizzle = 4
 
             # Select up to `max_swizzle` fields to swizzle            
@@ -69,38 +68,26 @@ def swizzle_field_l(self, field_l, rs, bound_m, btor):
                     f = field_l.pop(field_idx)
                     e_l = self.swizzle_field(f, rs, bound_m)
                     if e_l is not None:
-                        swizzle_expr_l.append(e_l)
-                        n_l = []
                         for e in e_l:
-                            n_l.append(e.build(btor))
-                        swizzle_node_l.append(n_l)
+                            swizzle_node_l.append(e.build(btor))
                 else:
                     break
 
             # Each entry in the nodelist corresponds to a field
-            for field_nl in swizzle_node_l:
-                # Start by assuming all
-                for n in field_nl:
-                    btor.Assume(n)
-
+            while (len(swizzle_node_l) > 0):
+                idx = self.randstate.randint(0, len(swizzle_node_l)-1)
+                n = swizzle_node_l.pop(idx)
+                btor.Assume(n)
                 if self.solve_info is not None:
                     self.solve_info.n_sat_calls += 1
-                if btor.Sat() != btor.SAT:
-                    # Add one at a time, preserving those that are SAT
-
-                    for n in field_nl:
-                        btor.Assume(n)
-                        if btor.Sat() == btor.SAT:
-                            btor.Assert(n)
-
-#                    if self.debug > 0:
-#                        print("Randomization constraint failed. Removing last: %s" %
-#                              self.pretty_printer.print(e))
+                if btor.Sat() == btor.SAT:
+                    if self.debug > 0:
+                        print("  Constraint SAT")
+                    btor.Assert(n)
                 else:
-                    # Randomization constraints succeeded. Go ahead and assert
-                    for n in field_nl:
-                        btor.Assert(n)
-
+                    if self.debug > 0:
+                        print("  Constraint UNSAT")
+
             if self.solve_info is not None:
                 self.solve_info.n_sat_calls += 1
             if btor.Sat() != btor.SAT:

ve/unit/test_random_dist.py

@@ -779,5 +779,26 @@ def a_c(self):
 
         for i,b in enumerate(bins):
             self.assertNotEqual(b, 0)
+
+    def test_two_var_1(self):
+
+        @vsc.randobj
+        class my_cls(object):
+            def __init__(self):
+                self.a = vsc.rand_bit_t(32)
+                self.b = vsc.rand_bit_t(32)
+
+            @vsc.constraint
+            def ab_c(self):
+                self.a >= 0
+                self.b >= 0
+                self.a <= 50
+                self.b <= 50
+                self.a + self.b <= 60
+
+        c = my_cls()
+        for i in range(100):
+            c.randomize(debug=False)
+            print("[%d] a=%d b=%d" % (i, c.a, c.b))