Check PSL properties are in simple subset

nickg · Aug 27, 2024 · 82f2eae · 82f2eae
1 parent 3094b4b
commit 82f2eae
Show file tree

Hide file tree

Showing 4 changed files with 41 additions and 2 deletions.
diff --git a/src/parse.c b/src/parse.c
@@ -12037,7 +12037,7 @@ static psl_node_t p_psl_fl_property(void)
 
          consume(tRSQUARE);
 
-         (void)p_psl_fl_property();
+         psl_set_value(p, p_psl_fl_property());
       }
       break;
 

diff --git a/src/psl/psl-sem.c b/src/psl/psl-sem.c
@@ -181,6 +181,10 @@ static void psl_check_implication(psl_node_t p, nametab_t *tab)
 
    psl_node_t right = psl_operand(p, 1);
    psl_check(right, tab);
+
+   if (psl_kind(left) != P_HDL_EXPR || psl_type(left) != PSL_TYPE_BOOLEAN)
+      error_at(psl_loc(p), "property is not in the simple subset as the left "
+               "hand side of this implication is non-Boolean");
 }
 
 static void psl_check_next(psl_node_t p, nametab_t *tab)
@@ -191,6 +195,19 @@ static void psl_check_next(psl_node_t p, nametab_t *tab)
    psl_check(psl_value(p), tab);
 }
 
+static void psl_check_next_e(psl_node_t p, nametab_t *tab)
+{
+   if (psl_has_delay(p))
+      psl_check_number(psl_delay(p), tab);
+
+   psl_node_t value = psl_value(p);
+   psl_check(value, tab);
+
+   if (psl_kind(value) != P_HDL_EXPR)
+      error_at(psl_loc(p), "property is not in the simple subset as the "
+               "operand of this next_e operator is non-Boolean");
+}
+
 static void psl_check_until(psl_node_t p, nametab_t *tab)
 {
    assert(psl_operands(p) == 2);
@@ -200,6 +217,14 @@ static void psl_check_until(psl_node_t p, nametab_t *tab)
 
    psl_node_t right = psl_operand(p, 1);
    psl_check(right, tab);
+
+   const psl_flags_t flags = psl_flags(p);
+   if ((flags & PSL_F_INCLUSIVE) && psl_kind(right) != P_HDL_EXPR)
+      error_at(psl_loc(p), "property is not in the simple subset as the right "
+               "hand side of this overlapping until operator is non-Boolean");
+   else if (psl_kind(left) != P_HDL_EXPR)
+      error_at(psl_loc(p), "property is not in the simple subset as the left "
+               "hand side of this until operator is non-Boolean");
 }
 
 void psl_check(psl_node_t p, nametab_t *tab)
@@ -255,10 +280,12 @@ void psl_check(psl_node_t p, nametab_t *tab)
       break;
    case P_NEXT:
    case P_NEXT_A:
-   case P_NEXT_E:
    case P_NEXT_EVENT:
       psl_check_next(p, tab);
       break;
+   case P_NEXT_E:
+      psl_check_next_e(p, tab);
+      break;
    case P_UNTIL:
       psl_check_until(p, tab);
       break;

diff --git a/test/psl/sem1.vhd b/test/psl/sem1.vhd
@@ -17,5 +17,9 @@ begin
     -- psl assert x -> next[i] (y);           -- Error
     -- psl assert x -> next[c] (y);           -- OK
     -- psl assert x -> next i;                -- Error
+    -- psl assert (next x) -> not x;          -- Error
+    -- psl assert x until_ (next x);          -- Error
+    -- psl assert (next x) until y;           -- Error
+    -- psl assert always next_e [1 to 3] (y -> next x);   -- Error
 
 end architecture;
diff --git a/test/test_psl.c b/test/test_psl.c
@@ -105,6 +105,14 @@ START_TEST(test_sem1)
       { 16, "expression must be a PSL Number but have type BIT" },
       { 17, "expression must be static" },
       { 19, "expression must be a PSL Boolean but have type INTEGER" },
+      { 20, "property is not in the simple subset as the left hand side of "
+        "this implication is non-Boolean" },
+      { 21, "property is not in the simple subset as the right hand side of "
+        "this overlapping until operator is non-Boolean" },
+      { 22, "property is not in the simple subset as the left hand side of "
+        "this until operator is non-Boolean" },
+      { 23, "property is not in the simple subset as the operand of this "
+        "next_e operator is non-Boolean" },
       { -1, NULL }
    };
    expect_errors(expect);