Handle external names in PSL assertions. Fixes #952

NEWS.md

@@ -8,6 +8,8 @@
   or larger (#949).
 - Fixed a crash when a constant array with unconstrained element type is
   initialised with an aggregate (#954).
+- External names in concurrent assertion statements and PSL assertions
+  are now parsed correctly (#952).
 
 ## Version 1.13.2 - 2024-08-11
 - Fixed an incorrect bounds check error when a constant declaration has

src/dump.c

@@ -1110,15 +1110,10 @@ static void dump_instance(tree_t t, int indent)
 
 static void dump_stmt(tree_t t, int indent)
 {
-   switch (tree_kind(t)) {
-   case T_PSL:
-      dump_psl(t, indent);
-      return;
-   case T_VERILOG:
+   const tree_kind_t kind = tree_kind(t);
+   if (kind == T_VERILOG) {
       vlog_dump(tree_vlog(t), indent);
       return;
-   default:
-      break;
    }
 
    tab(indent);
@@ -1437,6 +1432,10 @@ static void dump_stmt(tree_t t, int indent)
       print_syntax("\n");
       return;
 
+   case T_PSL:
+      dump_psl(t, indent);
+      break;
+
    default:
       cannot_dump(t, "stmt");
    }

src/lexer.l

@@ -312,7 +312,6 @@ UNION         ?i:union
 {END}                    { TOKEN(tEND); }
 {GENERIC}                { TOKEN(tGENERIC); }
 {PORT}                   { TOKEN(tPORT); }
-{CONSTANT}               { TOKEN(tCONSTANT); }
 {COMPONENT}              { TOKEN(tCOMPONENT); }
 {CONFIGURATION}          { TOKEN(tCONFIGURATION); }
 {ARCHITECTURE}           { TOKEN(tARCHITECTURE); }
@@ -324,13 +323,11 @@ UNION         ?i:union
 {BUS}                    { TOKEN(tBUS); }
 {REGISTER}               { TOKEN(tREGISTER); }
 {UNAFFECTED}             { TOKEN(tUNAFFECTED); }
-{SIGNAL}                 { TOKEN(tSIGNAL); }
 {PROCESS}                { TOKEN(tPROCESS); }
 {WAIT}                   { TOKEN(tWAIT); }
 {REPORT}                 { TOKEN(tREPORT); }
 {INOUT}                  { TOKEN(tINOUT); }
 {LINKAGE}                { TOKEN(tLINKAGE); }
-{VARIABLE}               { TOKEN(tVARIABLE); }
 {FOR}                    { TOKEN(tFOR); }
 {TYPE}                   { TOKEN(tTYPE); }
 {SUBTYPE}                { TOKEN(tSUBTYPE); }
@@ -422,6 +419,9 @@ UNION         ?i:union
 <INITIAL,PSL>{TO}        { TOKEN(tTO); }
 <INITIAL,PSL>{DOWNTO}    { TOKEN(tDOWNTO); }
 <INITIAL,PSL>{UNTIL}     { TOKEN(tUNTIL); }
+<INITIAL,PSL>{CONSTANT}  { TOKEN(tCONSTANT); }
+<INITIAL,PSL>{SIGNAL}    { TOKEN(tSIGNAL); }
+<INITIAL,PSL>{VARIABLE}  { TOKEN(tVARIABLE); }
 
 <*>"("                   { TOKEN(tLPAREN); }
 <*>")"                   { TOKEN(tRPAREN); }

src/names.c

@@ -4961,73 +4961,80 @@ type_t solve_target(nametab_t *tab, tree_t target, tree_t value)
    return solve_types(tab, target, value_type);
 }
 
-type_t solve_condition(nametab_t *tab, tree_t *expr, type_t constraint)
+type_t solve_condition(nametab_t *tab, tree_t *expr)
 {
+   type_t boolean = std_type(NULL, STD_BOOLEAN);
+
+   if (standard() < STD_08)
+      return solve_types(tab, *expr, boolean);
+
+   // Apply the rules for condition conversion from LRM 08 section 9.2.9
+
    type_set_push(tab);
-   type_set_add(tab, constraint, NULL);
+   type_set_add(tab, boolean, NULL);
 
    type_t type;
-   if (standard() >= STD_08) {
-      if (is_unambiguous(*expr))
-         type = _solve_types(tab, *expr);
-      else
-         type = try_solve_type(tab, *expr);
-
-      type_t boolean = std_type(NULL, STD_BOOLEAN);
-      if (type == NULL || !type_eq(type, boolean)) {
-         ident_t cconv = well_known(W_OP_CCONV);
-         const symbol_t *sym = symbol_for(tab->top_scope, cconv);
-         if (sym != NULL) {
-            for (int i = 0; i < sym->ndecls; i++) {
-               const decl_t *dd = get_decl(sym, i);
-
-               tree_t sub = dd->tree;
-               if (dd->kind == T_ALIAS && !(sub = get_aliased_subprogram(sub)))
-                  continue;
-
-               if ((dd->mask & N_FUNC) && tree_ports(sub) == 1) {
-                  type_t p0_type = tree_type(tree_port(sub, 0));
-                  type_set_add(tab, p0_type, dd->tree);
-               }
+   if (is_unambiguous(*expr))
+      type = _solve_types(tab, *expr);
+   else
+      type = try_solve_type(tab, *expr);
+
+   if (type == NULL || !type_eq(type, boolean)) {
+      ident_t cconv = well_known(W_OP_CCONV);
+      const symbol_t *sym = symbol_for(tab->top_scope, cconv);
+      if (sym != NULL) {
+         for (int i = 0; i < sym->ndecls; i++) {
+            const decl_t *dd = get_decl(sym, i);
+
+            tree_t sub = dd->tree;
+            if (dd->kind == T_ALIAS && !(sub = get_aliased_subprogram(sub)))
+               continue;
+
+            if ((dd->mask & N_FUNC) && tree_ports(sub) == 1) {
+               type_t p0_type = tree_type(tree_port(sub, 0));
+               type_set_add(tab, p0_type, dd->tree);
             }
          }
+      }
 
-         if (type == NULL)
-            type = _solve_types(tab, *expr);
+      if (type == NULL)
+         type = _solve_types(tab, *expr);
 
-         const bool do_conversion =
-            !type_eq(type, boolean) &&
-            tab->top_type_set->members.count > 0
-            && type_set_contains(tab, type);
+      const bool do_conversion =
+         !type_eq(type, boolean) &&
+         tab->top_type_set->members.count > 0
+         && type_set_contains(tab, type);
 
-         if (do_conversion) {
-            tree_t fcall = tree_new(T_FCALL);
-            tree_set_loc(fcall, tree_loc(*expr));
-            tree_set_ident(fcall, cconv);
-            add_param(fcall, *expr, P_POS, NULL);
+      if (do_conversion) {
+         tree_t fcall = tree_new(T_FCALL);
+         tree_set_loc(fcall, tree_loc(*expr));
+         tree_set_ident(fcall, cconv);
+         add_param(fcall, *expr, P_POS, NULL);
 
-            type = solve_fcall(tab, fcall);
-            *expr = fcall;
-         }
+         type = solve_fcall(tab, fcall);
+         *expr = fcall;
       }
    }
-   else
-      type = _solve_types(tab, *expr);
 
    type_set_pop(tab);
    return type;
 }
 
-type_t solve_psl_condition(nametab_t *tab, tree_t expr)
+type_t solve_psl_condition(nametab_t *tab, tree_t *expr)
 {
-   type_set_push(tab);
+   if (standard() >= STD_08)
+      return solve_condition(tab, expr);
+   else {
+      // Allow BIT and STD_LOGIC in PSL conditions for VHDL-93
+      type_set_push(tab);
 
-   type_set_add(tab, std_type(NULL, STD_BOOLEAN), NULL);
-   type_set_add(tab, std_type(NULL, STD_BIT), NULL);
-   type_set_add(tab, ieee_type(IEEE_STD_ULOGIC), NULL);
+      type_set_add(tab, std_type(NULL, STD_BOOLEAN), NULL);
+      type_set_add(tab, std_type(NULL, STD_BIT), NULL);
+      type_set_add(tab, ieee_type(IEEE_STD_ULOGIC), NULL);
 
-   type_t type = _solve_types(tab, expr);
+      type_t type = _solve_types(tab, *expr);
 
-   type_set_pop(tab);
-   return type;
+      type_set_pop(tab);
+      return type;
+   }
 }

src/names.h

@@ -119,7 +119,7 @@ void walk_predefs(nametab_t *tab, ident_t name, predef_cb_t fn, void *context);
 type_t solve_types(nametab_t *tab, tree_t expr, type_t constraint);
 type_t solve_known_subtype(nametab_t *tab, tree_t expr, type_t constraint);
 type_t solve_target(nametab_t *tab, tree_t target, tree_t value);
-type_t solve_condition(nametab_t *tab, tree_t *expr, type_t constraint);
-type_t solve_psl_condition(nametab_t *tab, tree_t expr);
+type_t solve_condition(nametab_t *tab, tree_t *expr);
+type_t solve_psl_condition(nametab_t *tab, tree_t *expr);
 
 #endif // _NAMES_H

src/parse.c

@@ -6809,7 +6809,7 @@ static tree_t p_psl_condition(void)
    BEGIN("condition");
 
    tree_t value = p_expression();
-   solve_psl_condition(nametab, value);
+   solve_psl_condition(nametab, &value);
 
    return value;
 }
@@ -6818,10 +6818,8 @@ static tree_t p_condition(void)
 {
    BEGIN("condition");
 
-   type_t boolean = std_type(NULL, STD_BOOLEAN);
-
    tree_t value = p_expression();
-   solve_condition(nametab, &value, boolean);
+   solve_condition(nametab, &value);
 
    return value;
 }
@@ -6866,7 +6864,6 @@ static tree_t p_concurrent_assertion_statement(ident_t label)
       tree_set_flag(conc, TREE_F_POSTPONED);
 
    tree_t s = p_assertion();
-   tree_set_ident(s, get_implicit_label(s, nametab));
    tree_add_stmt(conc, s);
 
    consume(tSEMI);
@@ -10861,7 +10858,7 @@ static tree_t p_block_statement(ident_t label)
       consume(tLPAREN);
 
       tree_t expr = p_expression();
-      solve_condition(nametab, &expr, std_type(NULL, STD_BOOLEAN));
+      solve_condition(nametab, &expr);
 
       make_implicit_guard_signal(b, expr);
 
@@ -12060,6 +12057,7 @@ static psl_node_t p_psl_fl_property(void)
             // where we cannot determine ahead-of-time whether (x or y)
             // is a VHDL expression or PSL property
             tree_t expr = p_expression_with_head(psl_tree(p));
+            solve_psl_condition(nametab, &expr);
             psl_set_tree(p, expr);
          }
       }
@@ -12233,7 +12231,7 @@ static psl_node_t p_psl_fairness(void)
    psl_set_flag(a, flags);
 
    tree_t e1 = p_expression();
-   solve_psl_condition(nametab, e1);
+   solve_psl_condition(nametab, &e1);
 
    psl_node_t p1 = psl_new(P_HDL_EXPR);
    psl_set_tree(p1, e1);
@@ -12244,7 +12242,7 @@ static psl_node_t p_psl_fairness(void)
       consume(tCOMMA);
 
       tree_t e2 = p_expression();
-      solve_psl_condition(nametab, e2);
+      solve_psl_condition(nametab, &e2);
 
       psl_node_t p2 = psl_new(P_HDL_EXPR);
       psl_set_tree(p2, e2);
@@ -12472,36 +12470,67 @@ static tree_t p_psl_or_concurrent_assert(ident_t label)
    //  assert condition [ report expression ] [ severity expression ] ;
    //   | assert Property [ report String ] ;
 
+   BEGIN("PSL or concurrent assertion statement");
+
+   if (peek() == tPOSTPONED)
+      return p_concurrent_assertion_statement(label);   // Cannot be PSL
+
+   consume(tASSERT);
+
    scan_as_psl();
 
-   const look_params_t lookp = {
-      .look     = { tIFIMPL, tALWAYS, tNEVER },
-      .stop     = { tREPORT, tSEVERITY },
-      .abort    = tSEMI,
-      .nest_in  = tLPAREN,
-      .nest_out = tRPAREN,
-   };
+   psl_node_t p = p_psl_property();
 
-   if (look_for(&lookp)) {
-      psl_node_t a = p_psl_assert_directive();
+   scan_as_vhdl();
+
+   tree_t conc;
+   if (psl_kind(p) == P_HDL_EXPR) {
+      tree_t s = tree_new(T_ASSERT);
+      tree_set_value(s, psl_tree(p));
+
+      if (optional(tREPORT)) {
+         tree_t message = p_expression();
+         solve_types(nametab, message, std_type(NULL, STD_STRING));
+         tree_set_message(s, message);
+      }
 
-      tree_t s = tree_new(T_PSL);
-      tree_set_psl(s, a);
-      tree_set_ident(s, label);
+      if (optional(tSEVERITY)) {
+         tree_t severity = p_expression();
+         solve_types(nametab, severity, std_type(NULL, STD_SEVERITY_LEVEL));
+         tree_set_severity(s, severity);
+      }
 
-      scan_as_vhdl();
+      consume(tSEMI);
 
       tree_set_loc(s, CURRENT_LOC);
-      ensure_labelled(s, label);
 
-      insert_name(nametab, s, NULL);
-      sem_check(s, nametab);
-      return s;
+      conc = tree_new(T_CONCURRENT);
+      tree_add_stmt(conc, s);
    }
    else {
-      scan_as_vhdl();
-      return p_concurrent_assertion_statement(label);
+      if (!psl_has_clock(p))
+         psl_set_clock(p, find_default_clock(nametab));
+
+      psl_node_t a = psl_new(P_ASSERT);
+      psl_set_value(a, p);
+
+      if (peek() == tREPORT)
+         p_psl_report(a);
+
+      consume(tSEMI);
+
+      psl_set_loc(a, CURRENT_LOC);
+
+      conc = tree_new(T_PSL);
+      tree_set_psl(conc, a);
    }
+
+   tree_set_loc(conc, CURRENT_LOC);
+   ensure_labelled(conc, label);
+
+   if (label) insert_name(nametab, conc, NULL);
+   sem_check(conc, nametab);
+   return conc;
 }
 
 static tree_t p_concurrent_statement(void)

test/dump/vhdl6.vhd

@@ -0,0 +1,9 @@
+entity vhdl6 is
+end entity;
+
+architecture test of vhdl6 is
+    signal x : integer;
+begin
+    assert << constant ^.foo : integer >> = 2;  -- VHDL
+    assert (x = 1 -> x = 2);            -- PSL
+end architecture;

test/parse/issue952.vhd

@@ -0,0 +1,11 @@
+entity issue952 is
+end entity;
+
+architecture test of issue952 is
+    signal x : integer;
+begin
+    assert << constant ^.foo : integer >> = 2;  -- VHDL
+    assert (x = 1 -> x = 2);            -- PSL
+    assert x = 1 -> next x = 2;         -- PSL
+    assert (<< signal issue952.x : integer >> = 4 -> next x =2);  -- PSL
+end architecture;