From 7f0785ce599a5af9a7db71dedf9ac075f9e36cf2 Mon Sep 17 00:00:00 2001 From: Ondrej Ille Date: Mon, 6 Oct 2025 22:31:13 +0200 Subject: [PATCH 1/3] psl dumping for built-in fcalls, union, and value sets. --- src/dump.c | 7 +++++ src/psl/psl-dump.c | 70 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 77 insertions(+) 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); From 37f6da0c44f1f437886deafbff8d6b48bede14a8 Mon Sep 17 00:00:00 2001 From: Ondrej Ille Date: Mon, 6 Oct 2025 22:33:39 +0200 Subject: [PATCH 2/3] implement partial support for PSL next_a property. --- NEWS.md | 1 + src/psl/psl-fsm.c | 49 +++++++++++++++++++++++++++++++------ test/regress/gold/psl23.txt | 5 ++++ test/regress/psl23.vhd | 3 +++ www/features.html.in | 2 +- 5 files changed, 52 insertions(+), 8 deletions(-) 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/psl/psl-fsm.c b/src/psl/psl-fsm.c index 492361036..9db610ba1 100644 --- a/src/psl/psl-fsm.c +++ b/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: 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 From 2b4943c60effe202b75c7ab3013958f51b5946ee Mon Sep 17 00:00:00 2001 From: Ondrej Ille Date: Wed, 8 Oct 2025 21:12:15 +0200 Subject: [PATCH 3/3] fix error from review. --- src/psl/psl-fsm.c | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/psl/psl-fsm.c b/src/psl/psl-fsm.c index 9db610ba1..08db1f423 100644 --- a/src/psl/psl-fsm.c +++ b/src/psl/psl-fsm.c @@ -113,12 +113,11 @@ 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) + 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) {