diff --git a/NEWS.md b/NEWS.md index 30de9dd11..f099e5795 100644 --- a/NEWS.md +++ b/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). diff --git a/src/dump.c b/src/dump.c index 195985d39..77b59f905 100644 --- a/src/dump.c +++ b/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: diff --git a/src/psl/psl-dump.c b/src/psl/psl-dump.c index ade419ca6..f70b51e91 100644 --- a/src/psl/psl-dump.c +++ b/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); diff --git a/src/psl/psl-fsm.c b/src/psl/psl-fsm.c index 492361036..08db1f423 100644 --- a/src/psl/psl-fsm.c +++ b/src/psl/psl-fsm.c @@ -108,6 +108,16 @@ 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 +541,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 +687,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: diff --git a/test/regress/gold/psl23.txt b/test/regress/gold/psl23.txt index 9e8ae6c73..dfd78383d 100644 --- a/test/regress/gold/psl23.txt +++ b/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 diff --git a/test/regress/psl23.vhd b/test/regress/psl23.vhd index 51dd71c47..7f6228a69 100644 --- a/test/regress/psl23.vhd +++ b/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; diff --git a/www/features.html.in b/www/features.html.in index b305da487..f227d8fed 100644 --- a/www/features.html.in +++ b/www/features.html.in @@ -687,7 +687,7 @@ table below. 6.2.1.4.1 next_a - + master 6.2.1.4.2