Skip to content

swizzler: add dist constraint retry and fallback #245

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mballance merged 1 commit into from
Nov 8, 2025
Merged

swizzler: add dist constraint retry and fallback #245

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
99 changes: 61 additions & 38 deletions src/vsc/model/solvegroup_swizzler_partsel.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ def swizzle_field_l(self, field_l, rs : RandSet, bound_m, btor):
if len(field_l) > 0:
field_idx = self.randstate.randint(0, len(field_l)-1)
f = field_l.pop(field_idx)
e_l = self.swizzle_field(f, rs, bound_m)
e_l = self.swizzle_field(f, rs, bound_m, btor)
if e_l is not None:
for e in e_l:
swizzle_node_l.append(e.build(btor))
Expand Down Expand Up @@ -104,52 +104,75 @@ def swizzle_field_l(self, field_l, rs : RandSet, bound_m, btor):
def swizzle_field(self,
f : FieldScalarModel,
rs : RandSet,
bound_m : VariableBoundModel)->ExprModel:
bound_m : VariableBoundModel,
btor
) -> list[ExprModel]:
ret = None

if self.debug > 0:
print("Swizzling field %s" % f.name)

if f in rs.dist_field_m.keys():
max_dist_samples = 4
for _ in range(max_dist_samples):
e = self.sample_dist_weights(f, rs)
n = e.build(btor)
btor.Assume(n)
if self.solve_info is not None:
self.solve_info.n_sat_calls += 1
if btor.Sat() == btor.SAT:
if self.debug > 0: print(" Dist constraint SAT")
btor.Assert(n)
return ret
else:
if self.debug > 0: print(" Dist constraint UNSAT")
if self.debug > 0: print(" max_dist_samples exceeded, falling back to rand domain")

if f in bound_m.keys():
f_bound = bound_m[f]
if not f_bound.isEmpty():
ret = self.create_rand_domain_constraint(f, f_bound)

return ret

def sample_dist_weights(self,
f : FieldScalarModel,
rs : RandSet,
) -> ExprModel:
if self.debug > 0:
print("Note: field %s is in dist map" % f.name)
for d in rs.dist_field_m[f]:
print(" Weight list %s" % d.weight_list)

if len(rs.dist_field_m[f]) > 1:
target_d = self.randstate.randint(0, len(rs.dist_field_m[f])-1)
dist_scope_c = rs.dist_field_m[f][target_d]
else:
dist_scope_c = rs.dist_field_m[f][0]

target_range = dist_scope_c.next_target_range(self.randstate)
target_w = dist_scope_c.dist_c.weights[target_range]
if target_w.rng_rhs is not None:
# Dual-bound range
val_l = target_w.rng_lhs.val()
val_r = target_w.rng_rhs.val()
val = self.randstate.randint(val_l, val_r)
if self.debug > 0:
print("Note: field %s is in dist map" % f.name)
for d in rs.dist_field_m[f]:
print(" Weight list %s" % d.weight_list)
if len(rs.dist_field_m[f]) > 1:
target_d = self.randstate.randint(0, len(rs.dist_field_m[f])-1)
dist_scope_c = rs.dist_field_m[f][target_d]
else:
dist_scope_c = rs.dist_field_m[f][0]

target_range = dist_scope_c.next_target_range(self.randstate)
target_w = dist_scope_c.dist_c.weights[target_range]
if target_w.rng_rhs is not None:
# Dual-bound range
val_l = target_w.rng_lhs.val()
val_r = target_w.rng_rhs.val()
val = self.randstate.randint(val_l, val_r)
if self.debug > 0:
print("Select dist-weight range: %d..%d ; specific value %d" % (
int(val_l), int(val_r), int(val)))
ret = [ExprBinModel(
print("Select dist-weight range: %d..%d ; specific value %d" % (
int(val_l), int(val_r), int(val)))
ret = ExprBinModel(
ExprFieldRefModel(f),
BinExprType.Eq,
ExprLiteralModel(val, f.is_signed, f.width))]
else:
# Single value
val = target_w.rng_lhs.val()
if self.debug > 0:
print("Select dist-weight value %d" % (int(val)))
ret = [ExprBinModel(
ExprLiteralModel(val, f.is_signed, f.width))
else:
# Single value
val = target_w.rng_lhs.val()
if self.debug > 0:
print("Select dist-weight value %d" % (int(val)))
ret = ExprBinModel(
ExprFieldRefModel(f),
BinExprType.Eq,
ExprLiteralModel(int(val), f.is_signed, f.width))]
else:
if f in bound_m.keys():
f_bound = bound_m[f]
if not f_bound.isEmpty():
ret = self.create_rand_domain_constraint(f, f_bound)

ExprLiteralModel(int(val), f.is_signed, f.width))
return ret

def create_rand_domain_constraint(self,
Expand Down