0.9.0

- (#219) - Add `unique_vec` constraint to support unique-vector constraints

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

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
 

etc/ivpm.info

@@ -1,4 +1,4 @@
 
 name=pyvsc
-version=0.8.9
+version=0.9.0
 

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):
 

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
+

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)

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

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

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))
+            print("a=%d b=%d" % (c.a, c.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])