Partial support of PSL next_a

NEWS.md

@@ -5,6 +5,7 @@
   `vhpiIntTypeDeclK` base type instead of another `vhpiSubtypeDeclK`.
 - PSL `next_e` and `next_e!` operators are now supported.
 - PSL `nondet` built-in function is now supported.
+- PSL `next_a` is now supported with simple expressions.
 - Fixed a crash when `release` is used with a record signal (#1313).
 - Several other minor bugs were resolved (#1308).
 

src/dump.c

@@ -429,6 +429,11 @@ static void dump_expr(tree_t t)
       dump_expr(tree_value(t));
       break;
 
+   case T_PSL_FCALL:
+   case T_PSL_UNION:
+      psl_dump(tree_psl(t));
+      break;
+
    default:
       cannot_dump(t, "expr");
    }
@@ -1726,6 +1731,8 @@ void vhdl_dump(tree_t t, int indent)
    case T_STRING:
    case T_PACKAGE_MAP:
    case T_TYPE_REF:
+   case T_PSL_FCALL:
+   case T_PSL_UNION:
       dump_expr(t);
       break;
    case T_INSTANCE:

src/psl/psl-dump.c

@@ -243,6 +243,67 @@ static void psl_dump_clocked(psl_node_t p)
    }
 }
 
+static void psl_dump_value_set(psl_node_t p)
+{
+   print_syntax("{");
+
+   for (int i = 0; i < psl_operands(p); i++) {
+      psl_dump(psl_operand(p, i));
+      print_syntax(",");
+   }
+
+   print_syntax("}");
+}
+
+static void psl_dump_union(psl_node_t p)
+{
+   psl_dump(psl_operand(p, 0));
+
+   print_syntax(" union ");
+
+   psl_dump(psl_operand(p, 1));
+}
+
+static void psl_dump_builtin_fcall(psl_node_t p)
+{
+   switch (psl_subkind(p)) {
+   case PSL_BUILTIN_NEXT:
+      print_syntax("next");
+      break;
+   case PSL_BUILTIN_PREV:
+      print_syntax("prev");
+      break;
+   case PSL_BUILTIN_STABLE:
+      print_syntax("stable");
+      break;
+   case PSL_BUILTIN_ROSE:
+      print_syntax("rose");
+      break;
+   case PSL_BUILTIN_FELL:
+      print_syntax("fell");
+      break;
+   case PSL_BUILTIN_ENDED:
+      print_syntax("ended");
+      break;
+   case PSL_BUILTIN_NONDET:
+      print_syntax("nondet");
+      break;
+   case PSL_BUILTIN_NONDET_VECTOR:
+      print_syntax("nondet_vector");
+      break;
+   }
+
+   print_syntax("(");
+
+   for (int i = 0; i < psl_operands(p); i++) {
+      psl_dump(psl_operand(p, i));
+      print_syntax(",");
+   }
+
+   print_syntax(")");
+}
+
+
 void psl_dump(psl_node_t p)
 {
    switch (psl_kind(p)) {
@@ -309,6 +370,15 @@ void psl_dump(psl_node_t p)
    case P_CLOCKED:
       psl_dump_clocked(p);
       break;
+   case P_BUILTIN_FCALL:
+      psl_dump_builtin_fcall(p);
+      break;
+   case P_VALUE_SET:
+      psl_dump_value_set(p);
+      break;
+   case P_UNION:
+      psl_dump_union(p);
+      break;
    default:
       print_syntax("\n");
       fflush(stdout);

src/psl/psl-fsm.c

@@ -108,6 +108,17 @@ static int64_t get_number(tree_t t)
    return result;
 }
 
+static void get_range(psl_node_t range, int64_t *lo, int64_t *hi)
+{
+   *lo = get_number(psl_tree(psl_left(range)));
+   *hi = get_number(psl_tree(psl_right(range)));
+
+   if (lo > hi)
+      fatal_at(psl_loc(range), "left bound of PSL range (%"PRIi64") must be "
+               "lower than right bound (%"PRIi64")", *lo, *hi);
+}
+
+
 static psl_guard_t make_binop_guard(psl_fsm_t *fsm, binop_kind_t kind,
                                     psl_guard_t left, psl_guard_t right)
 {
@@ -531,21 +542,43 @@ static fsm_state_t *build_next(psl_fsm_t *fsm, fsm_state_t *state, psl_node_t p)
    return build_node(fsm, state, psl_value(p));
 }
 
-static fsm_state_t *build_next_e(psl_fsm_t *fsm, fsm_state_t *state, psl_node_t p)
+static fsm_state_t *build_next_a(psl_fsm_t *fsm, fsm_state_t *state, psl_node_t p)
 {
+   psl_node_t guard = psl_value(p);
+   if (psl_kind(guard) != P_HDL_EXPR)
+      fatal_at(psl_loc(p), "sorry, PSL next_a is supported only with expression");
+
+   bool strong = (psl_flags(p) & PSL_F_STRONG) ? true : false;
+   fsm_state_t *curr = state;
+
+   int64_t lo,hi = 0;
    psl_node_t range = psl_delay(p);
+   get_range(range, &lo, &hi);
+
+   for (int i = 0; i < hi; i++) {
+      fsm_state_t *new = add_state(fsm, p);
+      new->strong = strong;
+      if (i < lo - 1)
+         add_edge(fsm, curr, new, EDGE_NEXT, NULL);
+      else
+         add_edge(fsm, curr, new, EDGE_NEXT, guard);
+      curr = new;
+   }
+
+   return curr;
+}
+
+static fsm_state_t *build_next_e(psl_fsm_t *fsm, fsm_state_t *state, psl_node_t p)
+{
    psl_node_t guard = psl_value(p);
    bool strong = (psl_flags(p) & PSL_F_STRONG) ? true : false;
 
    psl_guard_t guard_n = not_guard(guard);
    fsm_state_t *curr = state;
 
-   const int lo = get_number(psl_tree(psl_left(range)));
-   const int hi = get_number(psl_tree(psl_right(range)));
-
-   if (lo > hi)
-      fatal_at(psl_loc(p), "left bound of PSL range (%d) must be "
-               "lower than right bound (%d)", lo, hi);
+   int64_t lo,hi = 0;
+   psl_node_t range = psl_delay(p);
+   get_range(range, &lo, &hi);
 
    for (int i = 0; i < lo - 1; i++) {
       fsm_state_t *new = add_state(fsm, p);
@@ -655,6 +688,8 @@ static fsm_state_t *build_node(psl_fsm_t *fsm, fsm_state_t *state, psl_node_t p)
       return build_next(fsm, state, p);
    case P_NEXT_E:
       return build_next_e(fsm, state, p);
+   case P_NEXT_A:
+      return build_next_a(fsm, state, p);
    case P_SERE:
       return build_sere(fsm, state, p);
    case P_REPEAT:

test/regress/gold/psl23.txt

@@ -1,8 +1,13 @@
 2500ps+1: two
+7500ps+1: four
+7500ps+1: four
+8500ps+1: four
 9500ps+1: one
 9500ps+1: two
 9500ps+1: three
+9500ps+1: four
 10500ps+1: one
 10500ps+1: two
 10500ps+1: three
+10500ps+1: four
 11500ps+0: three

test/regress/psl23.vhd

@@ -41,4 +41,7 @@ begin
     -- non-finished assertions.
     -- psl three: assert always (a -> next_e![2 to 4] (b='1')) report "three";
 
+    -- Shall
+    -- psl four: assert always (a -> next_a[7 to 9] (b='1')) report "four";
+
 end architecture;

www/features.html.in

@@ -687,7 +687,7 @@ table below.
   <tr>
     <td>6.2.1.4.1</td>
     <td>next_a</td>
-    <td class="feature-missing"></td>
+    <td class="feature-partial">master</td>
   </tr>
   <tr>
     <td>6.2.1.4.2</td>