diff --git a/doc/Changelog.md b/doc/Changelog.md index 183e094..f314c94 100644 --- a/doc/Changelog.md +++ b/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 diff --git a/etc/ivpm.info b/etc/ivpm.info index 018f038..81f1459 100644 --- a/etc/ivpm.info +++ b/etc/ivpm.info @@ -1,4 +1,4 @@ name=pyvsc -version=0.7.6 +version=0.7.7 diff --git a/src/vsc/model/randomizer.py b/src/vsc/model/randomizer.py index 31a109e..990b993 100644 --- a/src/vsc/model/randomizer.py +++ b/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 diff --git a/src/vsc/model/solvegroup_swizzler_partsel.py b/src/vsc/model/solvegroup_swizzler_partsel.py index 547745f..b05d7c5 100644 --- a/src/vsc/model/solvegroup_swizzler_partsel.py +++ b/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: diff --git a/ve/unit/test_random_dist.py b/ve/unit/test_random_dist.py index abf7eeb..d8e80bd 100644 --- a/ve/unit/test_random_dist.py +++ b/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)) \ No newline at end of file