Skip to content

Commit 7250e7c

Browse files
committed
0.4.4
- (#92) Corrected an issue where soft constraints were dropped while combining solve sets - (#91) Corrected the field-access overloading to properly handle re-assignment to VSC fields - (#88) Correct how the width of unary expressions is propagated - (#87) Correct handling of enum-type fields by increasing common implementation with scalar/int-type fields - (#86) Properly handle part-select on array-element references - (#85) Correct an issue with complex-reference resolution and dist constraints - (#84) Correct an issue with expanding complex references inside foreach constraints Signed-off-by: Matthew Ballance <matt.ballance@gmail.com>
1 parent 8d4a567 commit 7250e7c

27 files changed

+1222
-214
lines changed

doc/Changelog.md

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,18 @@
11

2+
## 0.4.4
3+
- (#92) Corrected an issue where soft constraints were dropped while
4+
combining solve sets
5+
- (#91) Corrected the field-access overloading to properly handle
6+
re-assignment to VSC fields
7+
- (#88) Correct how the width of unary expressions is propagated
8+
- (#87) Correct handling of enum-type fields by increasing common
9+
implementation with scalar/int-type fields
10+
- (#86) Properly handle part-select on array-element references
11+
- (#85) Correct an issue with complex-reference resolution and
12+
dist constraints
13+
- (#84) Correct an issue with expanding complex references inside
14+
foreach constraints
15+
216
## 0.4.3
317
- (#81,#82) Correctly propagate context-dependent expression widths
418
down the evaluation tree

etc/ivpm.info

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11

22
name=pyvsc
3-
version=0.4.3
3+
version=0.4.4
44

src/vsc/coverage.py

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -127,18 +127,18 @@ def sample(self, *args, **kwargs):
127127
if isinstance(ex_f, FieldCompositeModel):
128128
# TODO: probably need to do something a bit more than this?
129129
model.set_field(i, args[i].get_model())
130-
elif isinstance(ex_f, FieldScalarModel):
131-
if isinstance(args[i], type_base):
132-
ex_f.set_val(args[i].get_val())
133-
else:
134-
ex_f.set_val(int(args[i]))
135130
elif isinstance(ex_f, EnumFieldModel):
136131
ei = us_f.enum_i
137132
if isinstance(args[i], type_enum):
138133
ex_f.set_val(args[i].get_val())
139134
else:
140135
# Use the enum map to convert to an int
141136
ex_f.set_val(ei.e2v(args[i]))
137+
elif isinstance(ex_f, FieldScalarModel):
138+
if isinstance(args[i], type_base):
139+
ex_f.set_val(args[i].get_val())
140+
else:
141+
ex_f.set_val(int(args[i]))
142142
else:
143143
raise Exception("unhandled sample case")
144144

src/vsc/impl/enum_info.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ def e2v(self, ev)->int:
3636
return self.e2v_m[ev]
3737

3838
def v2e(self, v):
39-
return self.v2e_m[v]
39+
return self.v2e_m[int(v)]
4040

4141
def e2e(self, ev):
4242
v = self.e2v_m[ev]

src/vsc/model/enum_field_model.py

Lines changed: 15 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -8,41 +8,32 @@
88

99
from vsc.model.field_model import FieldModel
1010
from vsc.model.rand_gen_data import RandGenData
11+
from vsc.model.value_enum import ValueEnum
12+
from vsc.model.field_scalar_model import FieldScalarModel
1113

1214

13-
class EnumFieldModel(FieldModel):
15+
class EnumFieldModel(FieldScalarModel):
1416

1517
def __init__(self,
1618
name : str,
1719
enums : List[int],
1820
is_rand : bool):
19-
super().__init__(name)
21+
super().__init__(
22+
name,
23+
32,
24+
True,
25+
is_rand,
26+
None)
2027
self.enums = enums
21-
self.is_declared_rand = is_rand
22-
self.is_used_rand = is_rand
23-
self.var = None
24-
self.val = enums[0]
25-
self.rand_if = None
26-
27-
# TODO: a bit simplistic
28-
self.width = 32
29-
self.is_signed = True
30-
31-
32-
def set_used_rand(self, is_rand, level=0):
33-
self.is_used_rand = (is_rand and (self.is_declared_rand or level==0))
34-
35-
def dispose(self):
36-
self.var = None
28+
self.val = ValueEnum(enums[0])
3729

3830
def accept(self, v):
3931
v.visit_enum_field(self)
4032

4133
def build(self, btor):
34+
super().build(btor)
35+
4236
if self.is_used_rand:
43-
sort = btor.BitVecSort(self.width)
44-
self.var = btor.Var(sort)
45-
4637
c = None
4738
for e in self.enums:
4839
if c is None:
@@ -56,32 +47,8 @@ def build(self, btor):
5647
self.var,
5748
btor.Const(e, self.width)))
5849
btor.Assert(c)
59-
else:
60-
self.var = btor.Const(self.val, self.width)
50+
6151
return self.var
6252

63-
def get_constraints(self, constraint_l):
64-
pass
65-
66-
def pre_randomize(self):
67-
if self.rand_if is not None:
68-
self.rand_if.do_pre_randomize()
69-
70-
def set_val(self, val):
71-
self.val = val
72-
73-
def get_val(self):
74-
return self.val
75-
76-
def post_randomize(self):
77-
if self.var is not None:
78-
val = 0
79-
for b in self.var.assignment:
80-
val <<= 1
81-
if b == '1':
82-
val |= 1
83-
self.set_val(val)
84-
85-
if self.rand_if is not None:
86-
self.rand_if.do_post_randomize()
87-
53+
# def set_val(self, val):
54+
# self.val.v = val

src/vsc/model/expr_partselect_model.py

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
from vsc.model.expr_literal_model import ExprLiteralModel
2-
31
# Licensed to the Apache Software Foundation (ASF) under one
42
# or more contributor license agreements. See the NOTICE file
53
# distributed with this work for additional information
@@ -23,6 +21,7 @@
2321
#
2422
# @author: ballance
2523

24+
from vsc.model.expr_literal_model import ExprLiteralModel
2625
from vsc.model.expr_model import ExprModel
2726

2827
class ExprPartselectModel(ExprModel):
@@ -37,8 +36,8 @@ def build(self, btor, ctx_width=-1):
3736
lower = self.lower if self.lower is not None else self.upper
3837
return btor.Slice(
3938
self.lhs.build(btor),
40-
lower.val(),
41-
upper.val())
39+
upper.val(),
40+
lower.val())
4241

4342
def width(self):
4443
upper = self.upper

src/vsc/model/expr_unary_model.py

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,11 @@ def build(self, btor : Boolector, ctx_width=-1):
2626
ret = btor.Not(self.expr.build(btor, ctx_width))
2727

2828
return ret
29+
30+
def width(self):
31+
# Currently-supported unary expressions have the
32+
# same width as the base expression
33+
return self.expr.width()
2934

3035
def accept(self, v):
3136
v.visit_expr_unary(self)

src/vsc/model/rand_info_builder.py

Lines changed: 57 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -44,10 +44,13 @@
4444
from vsc.model.rand_set import RandSet
4545
from vsc.model.constraint_dist_scope_model import ConstraintDistScopeModel
4646
from vsc.visitors.expand_solve_order_visitor import ExpandSolveOrderVisitor
47+
from vsc.visitors.expr2field_visitor import Expr2FieldVisitor
4748

4849

4950
class RandInfoBuilder(ModelVisitor,RandIF):
5051

52+
EN_DEBUG = 0
53+
5154
def __init__(self, rng):
5255
# TODO: need access to the random state
5356
super().__init__()
@@ -69,9 +72,9 @@ def __init__(self, rng):
6972
self.active_cp = None
7073
self._rng = rng
7174
self._order_l = []
72-
self._order_s = set()
7375

7476
self._order_m = {}
77+
self._expr2fm = Expr2FieldVisitor()
7578

7679
@staticmethod
7780
def build(
@@ -167,30 +170,6 @@ def visit_constraint_solve_order(self, c : ConstraintSolveOrderModel):
167170
for b in c.before_l:
168171
for a in c.after_l:
169172
ExpandSolveOrderVisitor(self._order_m).expand(a, b)
170-
171-
# b_i = -1
172-
# a_i = -1
173-
# if b in self._order_s:
174-
# b_i = self._order_l.index(b)
175-
# if a in self._order_s:
176-
# a_i = self._order_l.index(a)
177-
#
178-
# if b_i == -1 and a_i == -1:
179-
# # Just add the elements to the list
180-
# self._order_l.append(b)
181-
# self._order_l.append(a)
182-
# self._order_s.add(a)
183-
# self._order_s.add(b)
184-
# elif b_i != -1:
185-
# self._order_l.insert(b_i+1, a)
186-
# self._order_s.add(a)
187-
# elif a_i != -1:
188-
# self._order_l.insert(a_i, b)
189-
# self._order_s.add(b)
190-
# else:
191-
# # Found both in the list already.
192-
# # They might be in the list for good reasons or bad
193-
# pass
194173

195174
def visit_constraint_stmt_enter(self, c):
196175
if self._pass == 1 and len(self._constraint_s) == 1:
@@ -219,27 +198,39 @@ def visit_constraint_dynref(self, c):
219198
c_stmt.accept(self)
220199

221200
def visit_constraint_expr(self, c):
201+
if RandInfoBuilder.EN_DEBUG:
202+
print("--> RandInfoBuilder::visit_constraint_expr")
203+
222204
super().visit_constraint_expr(c)
223205

206+
if RandInfoBuilder.EN_DEBUG:
207+
print("<-- RandInfoBuilder::visit_constraint_expr")
208+
224209
def visit_constraint_dist_scope(self, s : ConstraintDistScopeModel):
225210
super().visit_constraint_dist_scope(s)
226211

227212
# Save information on dist constraints to the
228213
# appropriate randset
229214
if self._active_randset is not None:
230-
f = s.dist_c.lhs.fm
215+
f = self._expr2fm.field(s.dist_c.lhs)
231216
if f in self._active_randset.dist_field_m.keys():
232217
self._active_randset.dist_field_m[f].append(s)
233218
else:
234219
self._active_randset.dist_field_m[f] = [s]
235220

236221
def visit_constraint_soft(self, c:ConstraintSoftModel):
222+
if RandInfoBuilder.EN_DEBUG:
223+
print("--> RandInfoBuilder::visit_constraint_soft")
224+
237225
# Update the priority of this constraint
238226
c.priority += self._soft_priority
239227
self._soft_priority += 1
240228

241229
super().visit_constraint_soft(c)
242230

231+
if RandInfoBuilder.EN_DEBUG:
232+
print("<-- RandInfoBuilder::visit_constraint_soft")
233+
243234
def visit_expr_array_subscript(self, s : ExprArraySubscriptModel):
244235
fm = s.getFieldModel()
245236
if self._pass == 1:
@@ -281,53 +272,64 @@ def visit_expr_array_subscript(self, s : ExprArraySubscriptModel):
281272
self._field_s.remove(fm)
282273

283274
def visit_expr_fieldref(self, e):
284-
if self._pass == 1:
275+
# If the field is already referenced by an existing randset
276+
# that is not this one, we need to merge the sets
277+
fm = self._expr2fm.field(e)
278+
279+
if self._pass == 0:
280+
fm.accept(self)
281+
elif self._pass == 1:
285282
# During pass 1, build out randsets based on constraint
286283
# relationships
287284

288-
# If the field is already referenced by an existing randset
289-
# that is not this one, we need to merge the sets
290-
if isinstance(e.fm, FieldArrayModel):
285+
286+
if isinstance(fm, FieldArrayModel):
287+
# Note: this is important for unique constraints on an
288+
# entire (possibly variable-size) scalar array
291289
for f in e.fm.field_l:
292290
self.process_fieldref(f)
293291
else:
294-
self.process_fieldref(e.fm)
292+
self.process_fieldref(fm)
295293

296-
297-
super().visit_expr_fieldref(e)
294+
# super().visit_expr_fieldref(e)
298295

299296
def visit_expr_indexed_fieldref(self, e):
300297
self.process_fieldref(e.get_target())
301298

302299
def process_fieldref(self, fm):
300+
if RandInfoBuilder.EN_DEBUG > 0:
301+
print("--> RandInfoBuilder::process_fieldref %s" % fm.fullname)
303302
if fm in self._randset_field_m.keys():
304303
# There's an existing randset that holds this field
305304
ex_randset = self._randset_field_m[fm]
306305
if self._active_randset is None:
307306
self._active_randset = ex_randset
308307
elif ex_randset is not self._active_randset:
309-
if fm in self._order_s:
310-
# This field is part of the ordering constraint set.
311-
if self._active_randset.order != -1 and self._active_randset.order < ex_randset.order:
312-
# If the active randset is also ordered, and comes before
313-
# the one containing this field as primary, then we must
314-
# save the constraints
315-
self._active_order_randset_s.add(ex_randset)
316-
self._active_randset.add_nontarget(fm)
317-
else:
318-
# This field isn't being ordered, so go ahead and
319-
for f in self._active_randset.fields():
320-
# Relink to the new consolidated randset
321-
self._randset_field_m[f] = ex_randset
322-
ex_randset.add_field(f)
308+
if RandInfoBuilder.EN_DEBUG > 0:
309+
print("RandInfoBuilder: combine two randsets")
310+
311+
# This field isn't being ordered, so go ahead and
312+
for f in self._active_randset.fields():
313+
# Relink to the new consolidated randset
314+
self._randset_field_m[f] = ex_randset
315+
ex_randset.add_field(f)
323316

324-
for c in self._active_randset.constraints():
325-
ex_randset.add_constraint(c)
317+
for c in self._active_randset.constraints():
318+
ex_randset.add_constraint(c)
319+
320+
for c in self._active_randset.soft_constraints():
321+
ex_randset.add_constraint(c)
326322

327-
# Remove the previous randset
328-
self._randset_s.remove(self._active_randset)
329-
self._active_randset = ex_randset
323+
# Remove the previous randset
324+
self._randset_s.remove(self._active_randset)
325+
self._active_randset = ex_randset
326+
else:
327+
# Field is handled by a randset that is the active one
328+
pass
330329
else:
330+
if RandInfoBuilder.EN_DEBUG > 0:
331+
print("RandInfoBuilder: create new randset")
332+
331333
# No existing randset holds this field
332334
if self._active_randset is None:
333335
self._active_randset = RandSet()
@@ -339,6 +341,9 @@ def process_fieldref(self, fm):
339341

340342
if fm in self._field_s:
341343
self._field_s.remove(fm)
344+
345+
if RandInfoBuilder.EN_DEBUG > 0:
346+
print("<-- RandInfoBuilder::process_fieldref %s" % fm.fullname)
342347

343348

344349
def visit_composite_field(self, f):

src/vsc/model/rand_set_node_builder.py

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,4 +51,5 @@ def visit_expr_fieldref(self, e):
5151
if self.phase == 0:
5252
e.fm.accept(self)
5353
super().visit_expr_fieldref(e)
54+
5455

0 commit comments

Comments
 (0)