diff --git a/doc/Changelog.md b/doc/Changelog.md index d286a81..39cf555 100644 --- a/doc/Changelog.md +++ b/doc/Changelog.md @@ -1,4 +1,7 @@ +## 0.9.0 +- (#219) - Add `unique_vec` constraint to support unique-vector constraints + ## 0.8.9 - (#205) - Ensure that recursive references between objects don't cause recursion diff --git a/etc/ivpm.info b/etc/ivpm.info index b988e33..904af44 100644 --- a/etc/ivpm.info +++ b/etc/ivpm.info @@ -1,4 +1,4 @@ name=pyvsc -version=0.8.9 +version=0.9.0 diff --git a/src/vsc/constraints.py b/src/vsc/constraints.py index 02ea9e5..af934e0 100644 --- a/src/vsc/constraints.py +++ b/src/vsc/constraints.py @@ -31,10 +31,12 @@ from vsc.model.constraint_soft_model import ConstraintSoftModel from vsc.model.constraint_solve_order_model import ConstraintSolveOrderModel from vsc.model.constraint_unique_model import ConstraintUniqueModel +from vsc.model.constraint_unique_vec_model import ConstraintUniqueVecModel from vsc.model.dist_weight_expr_model import DistWeightExprModel from vsc.model.expr_array_subscript_model import ExprArraySubscriptModel from vsc.model.expr_dynref_model import ExprDynRefModel from vsc.model.expr_fieldref_model import ExprFieldRefModel +from vsc.model.field_array_model import FieldArrayModel from vsc.model.expr_indexed_field_ref_model import ExprIndexedFieldRefModel from vsc.model.field_scalar_model import FieldScalarModel from vsc.types import to_expr, expr, type_base, rng @@ -271,6 +273,23 @@ def unique(*args): if in_srcinfo_mode(): c.srcinfo = SourceInfo.mk() push_constraint_stmt(c) + +def unique_vec(*args): + expr_l = [] + for i in range(-1, -(len(args)+1), -1): + to_expr(args[i]) + e = pop_expr() + if not isinstance(e, ExprFieldRefModel) or not isinstance(e.fm, FieldArrayModel): + raise Exception("All arguments to unique_vec must be lists") + expr_l.insert(0, e) + + if len(expr_l) < 2: + raise Exception("Must specify at least two vectors to uniquify") + + c = ConstraintUniqueVecModel(expr_l) + if in_srcinfo_mode(): + c.srcinfo = SourceInfo.mk() + push_constraint_stmt(c) class forall(object): diff --git a/src/vsc/model/constraint_unique_vec_model.py b/src/vsc/model/constraint_unique_vec_model.py new file mode 100644 index 0000000..5940fce --- /dev/null +++ b/src/vsc/model/constraint_unique_vec_model.py @@ -0,0 +1,82 @@ +# Licensed to the Apache Software Foundation (ASF) under one +# or more contributor license agreements. See the NOTICE file +# distributed with this work for additional information +# regarding copyright ownership. The ASF licenses this file +# to you under the Apache License, Version 2.0 (the +# "License"); you may not use this file except in compliance +# with the License. You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, +# software distributed under the License is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +# KIND, either express or implied. See the License for the +# specific language governing permissions and limitations +# under the License. + + +# Created on Jul 28, 2019 +# +# @author: ballance + +from vsc.model.constraint_model import ConstraintModel +from vsc.model.expr_bin_model import ExprBinModel +from vsc.model.bin_expr_type import BinExprType +from vsc.model.expr_fieldref_model import ExprFieldRefModel +from vsc.model.field_array_model import FieldArrayModel + +class ConstraintUniqueVecModel(ConstraintModel): + + def __init__(self, unique_l): + super().__init__() + self.unique_l = unique_l + self.expr = None + + def build(self, btor, soft=False): + ret = None + + # Elements in the unique list might be arrays + unique_l = [] + + sz = -1 + for i in self.unique_l: + if sz == -1: + sz = len(i.fm.field_l) + elif sz != len(i.fm.field_l): + raise Exception("All arguments to unique_vec must be of the same size") + + # Form ORs of inequalities across the vector pairs + and_e = None + for i in range(len(self.unique_l)): + for j in range(i+1, len(self.unique_l)): + v_ne = self._mkVecNotEq(btor, self.unique_l[i], self.unique_l[j]) + + if and_e is None: + and_e = v_ne + else: + and_e = btor.And(and_e, v_ne) + + return and_e + + def _mkVecNotEq(self, btor, v1, v2): + ret = None + for i in range(len(v1.fm.field_l)): + ne = ExprBinModel( + ExprFieldRefModel(v1.fm.field_l[i]), + BinExprType.Ne, + ExprFieldRefModel(v2.fm.field_l[i])) + if ret is None: + ret = ne.build(btor) + else: + ret = btor.Or(ne.build(btor), ret) + return ret + + def accept(self, visitor): + visitor.visit_constraint_unique_vec(self) + + def clone(self, deep=False)->'ConstraintModel': + ret = ConstraintUniqueVecModel(self.unique_l) + + return ret + \ No newline at end of file diff --git a/src/vsc/model/model_visitor.py b/src/vsc/model/model_visitor.py index 345be79..bee0a1d 100644 --- a/src/vsc/model/model_visitor.py +++ b/src/vsc/model/model_visitor.py @@ -30,6 +30,7 @@ from vsc.model.constraint_implies_model import ConstraintImpliesModel from vsc.model.constraint_scope_model import ConstraintScopeModel from vsc.model.constraint_unique_model import ConstraintUniqueModel +from vsc.model.constraint_unique_vec_model import ConstraintUniqueVecModel from vsc.model.expr_bin_model import ExprBinModel from vsc.model.expr_cond_model import ExprCondModel from vsc.model.covergroup_model import CovergroupModel @@ -158,6 +159,12 @@ def visit_constraint_unique(self, c : ConstraintUniqueModel): for e in c.unique_l: e.accept(self) self.visit_constraint_stmt_leave(c) + + def visit_constraint_unique_vec(self, c : ConstraintUniqueVecModel): + self.visit_constraint_stmt_enter(c) + for e in c.unique_l: + e.accept(self) + self.visit_constraint_stmt_leave(c) def visit_expr_array_product(self, s): self.visit_expr_dynamic(s) diff --git a/src/vsc/types.py b/src/vsc/types.py index d44e214..80ad028 100644 --- a/src/vsc/types.py +++ b/src/vsc/types.py @@ -983,6 +983,9 @@ def __init__(self, l): self.l = l self.model = l._int_field_info.model self.idx = 0 + + def __iter__(self): + return self def __next__(self): if self.idx >= int(self.model.size.get_val()): @@ -997,6 +1000,7 @@ def __next__(self): self.idx += 1 return int(v) + class list_object_it(object): def __init__(self, l): self.l = l diff --git a/src/vsc/visitors/variable_bound_visitor.py b/src/vsc/visitors/variable_bound_visitor.py index 5e3c96e..cb06846 100644 --- a/src/vsc/visitors/variable_bound_visitor.py +++ b/src/vsc/visitors/variable_bound_visitor.py @@ -14,6 +14,7 @@ from vsc.model.constraint_inline_scope_model import ConstraintInlineScopeModel from vsc.model.constraint_soft_model import ConstraintSoftModel from vsc.model.constraint_unique_model import ConstraintUniqueModel +from vsc.model.constraint_unique_vec_model import ConstraintUniqueVecModel from vsc.model.enum_field_model import EnumFieldModel from vsc.model.expr_array_subscript_model import ExprArraySubscriptModel from vsc.model.expr_bin_model import ExprBinModel @@ -134,6 +135,11 @@ def visit_constraint_unique(self, c:ConstraintUniqueModel): # Don't go into an unexpanded unique block. This # construct is a meta-constraint that will be expanded pass + + def visit_constraint_unique_vec(self, c:ConstraintUniqueModel): + # Don't go into an unexpanded unique block. This + # construct is a meta-constraint that will be expanded + pass def visit_expr_bin(self, e:ExprBinModel): # TODO: We'll need to deal with expressions that involve variables diff --git a/ve/unit/test_constraint_functions.py b/ve/unit/test_constraint_functions.py index dc5c1f1..7c85783 100644 --- a/ve/unit/test_constraint_functions.py +++ b/ve/unit/test_constraint_functions.py @@ -31,4 +31,5 @@ def clog2_c(self): for i in range(256): with c.randomize_with(): c.b == i - print("a=%d b=%d" % (c.a, c.b)) \ No newline at end of file + print("a=%d b=%d" % (c.a, c.b)) + diff --git a/ve/unit/test_unique.py b/ve/unit/test_unique.py index 14f9e7c..772aee8 100644 --- a/ve/unit/test_unique.py +++ b/ve/unit/test_unique.py @@ -200,5 +200,37 @@ def a_c(self): for j in range(len(total_l)): for k in range(j+1, len(total_l)): self.assertNotEqual(total_l[j], total_l[k]) + + def test_unique_vec_smoke(self): + @vsc.randobj + class my_c(object): + def __init__(self): + self.a = vsc.rand_list_t(vsc.rand_uint16_t(1), 2) + self.b = vsc.rand_list_t(vsc.rand_uint16_t(1), 2) + self.c = vsc.rand_list_t(vsc.rand_uint16_t(1), 2) + + @vsc.constraint + def index_1_constraint(self): + self.a[0] < 2 + self.b[0] < 2 + self.c[0] < 2 + self.a[1] < 2 + self.b[1] < 2 + self.c[1] < 2 + + @vsc.constraint + def unique_list_constraint(self): + vsc.unique_vec(self.a, self.b, self.c) + + it = my_c() + print("A:") + for i in range(len(it.a)): + print(" %d" % it.a[i]) + print("B:") + for i in range(len(it.b)): + print(" %d" % it.b[i]) + print("C:") + for i in range(len(it.c)): + print(" %d" % it.c[i])