PSL: allow labels on psl directives (fix ticket26).

11 files changed, 48 insertions, 50 deletions

diff --git a/src/ghdldrv/ghdlprint.adb b/src/ghdldrv/ghdlprint.adb
index 45e70e1..1ab1cad 100644
--- a/src/ghdldrv/ghdlprint.adb
+++ b/src/ghdldrv/ghdlprint.adb
@@ -393,7 +393,6 @@ package body Ghdlprint is
               | Tok_Psl_Property
               | Tok_Psl_Sequence
               | Tok_Psl_Endpoint
-              | Tok_Psl_Assert
               | Tok_Psl_Cover
               | Tok_Psl_Boolean
               | Tok_Psl_Const
diff --git a/src/vhdl/disp_vhdl.adb b/src/vhdl/disp_vhdl.adb
index 73a8e42..3683ae5 100644
--- a/src/vhdl/disp_vhdl.adb
+++ b/src/vhdl/disp_vhdl.adb
@@ -2891,7 +2891,9 @@ package body Disp_Vhdl is
 
    procedure Disp_Psl_Assert_Statement (Stmt : Iir) is
    begin
-      Put ("--psl assert ");
+      Put ("--psl ");
+      Disp_Label (Stmt);
+      Put ("assert ");
       Disp_Psl_Expression (Get_Psl_Property (Stmt));
       Put_Line (";");
       Disp_PSL_NFA (Get_PSL_NFA (Stmt));
@@ -2899,7 +2901,9 @@ package body Disp_Vhdl is
 
    procedure Disp_Psl_Cover_Statement (Stmt : Iir) is
    begin
-      Put ("--psl cover ");
+      Put ("--psl ");
+      Disp_Label (Stmt);
+      Put ("cover ");
       Disp_Psl_Expression (Get_Psl_Property (Stmt));
       Put_Line (";");
       Disp_PSL_NFA (Get_PSL_NFA (Stmt));
diff --git a/src/vhdl/parse.adb b/src/vhdl/parse.adb
index 97ff876..0f3d9f5 100644
--- a/src/vhdl/parse.adb
+++ b/src/vhdl/parse.adb
@@ -6088,7 +6088,7 @@ package body Parse is
       Res : Iir;
    begin
       case Current_Token is
-         when Tok_Psl_Assert =>
+         when Tok_Assert =>
             Res := Create_Iir (Iir_Kind_Psl_Assert_Statement);
          when Tok_Psl_Cover =>
             Res := Create_Iir (Iir_Kind_Psl_Cover_Statement);
@@ -6096,9 +6096,6 @@ package body Parse is
             raise Internal_Error;
       end case;
 
-      --  Scan extended PSL tokens.
-      Scanner.Flag_Psl := True;
-
       --  Skip 'assert'
       Scan;
 
@@ -6143,6 +6140,14 @@ package body Parse is
             Postponed := False;
          end if;
       end Postponed_Not_Allowed;
+
+      procedure Label_Not_Allowed is
+      begin
+         if Label /= Null_Identifier then
+            Error_Msg_Parse ("'postponed' not allowed here");
+            Label := Null_Identifier;
+         end if;
+      end Label_Not_Allowed;
    begin
       -- begin was just parsed.
       Last_Stmt := Null_Iir;
@@ -6210,9 +6215,15 @@ package body Parse is
             when Tok_Process =>
                Stmt := Parse_Process_Statement (Label, Loc, Postponed);
             when Tok_Assert =>
-               Stmt := Create_Iir (Iir_Kind_Concurrent_Assertion_Statement);
-               Parse_Assertion (Stmt);
-               Expect (Tok_Semi_Colon);
+               if Vhdl_Std >= Vhdl_08
+                 or else (Flag_Psl_Comment and then Flag_Scan_In_Comment)
+               then
+                  Stmt := Parse_Psl_Assert_Statement;
+               else
+                  Stmt := Create_Iir (Iir_Kind_Concurrent_Assertion_Statement);
+                  Parse_Assertion (Stmt);
+                  Expect (Tok_Semi_Colon);
+               end if;
             when Tok_With =>
                Stmt := Parse_Selected_Signal_Assignment;
             when Tok_Block =>
@@ -6241,14 +6252,15 @@ package body Parse is
                end;
             when Tok_Psl_Default =>
                Postponed_Not_Allowed;
+               Label_Not_Allowed;
                Stmt := Parse_Psl_Default_Clock;
             when Tok_Psl_Property
               | Tok_Psl_Sequence
               | Tok_Psl_Endpoint =>
                Postponed_Not_Allowed;
+               Label_Not_Allowed;
                Stmt := Parse_Psl_Declaration;
-            when Tok_Psl_Assert
-              | Tok_Psl_Cover =>
+            when Tok_Psl_Cover =>
                Postponed_Not_Allowed;
                Stmt := Parse_Psl_Assert_Statement;
             when others =>
diff --git a/src/vhdl/scanner.adb b/src/vhdl/scanner.adb
index 260bd7c..7f68b32 100644
--- a/src/vhdl/scanner.adb
+++ b/src/vhdl/scanner.adb
@@ -702,6 +702,10 @@ package body Scanner is
                Current_Token := Tok_Psl_Sequence;
             when Std_Names.Name_Property =>
                Current_Token := Tok_Psl_Property;
+            when Std_Names.Name_Cover =>
+               Current_Token := Tok_Psl_Cover;
+            when Std_Names.Name_Default =>
+               Current_Token := Tok_Psl_Default;
             when Std_Names.Name_Inf =>
                Current_Token := Tok_Inf;
             when Std_Names.Name_Within =>
@@ -968,32 +972,16 @@ package body Scanner is
 
       case Id is
          when Name_Psl =>
-            --  Scan first identifier after '-- psl'.
-            if not Scan_Comment_Identifier then
-               return False;
+            --  Accept tokens after '-- psl'.
+            if Flag_Psl_Comment then
+               Flag_Psl := True;
+               Flag_Scan_In_Comment := True;
+               return True;
             end if;
-            Id := Name_Table.Get_Identifier;
-            case Id is
-               when Name_Property =>
-                  Current_Token := Tok_Psl_Property;
-               when Name_Sequence =>
-                  Current_Token := Tok_Psl_Sequence;
-               when Name_Endpoint =>
-                  Current_Token := Tok_Psl_Endpoint;
-               when Name_Assert =>
-                  Current_Token := Tok_Psl_Assert;
-               when Name_Cover =>
-                  Current_Token := Tok_Psl_Cover;
-               when Name_Default =>
-                  Current_Token := Tok_Psl_Default;
-               when others =>
-                  return False;
-            end case;
-            Flag_Scan_In_Comment := True;
-            return True;
          when others =>
-            return False;
+            null;
       end case;
+      return False;
    end Scan_Comment;
 
    function Scan_Exclam_Mark return Boolean is
@@ -1118,10 +1106,8 @@ package body Scanner is
                end if;
 
                --  Handle keywords in comment (PSL).
-               if Flag_Comment_Keyword
-                 and then Scan_Comment
-               then
-                  return;
+               if Flag_Comment_Keyword and then Scan_Comment then
+                  goto Again;
                end if;
 
                --  LRM93 13.2
diff --git a/src/vhdl/tokens.adb b/src/vhdl/tokens.adb
index 5d27be8..f741127 100644
--- a/src/vhdl/tokens.adb
+++ b/src/vhdl/tokens.adb
@@ -405,8 +405,6 @@ package body Tokens is
             return "sequence";
          when Tok_Psl_Endpoint =>
             return "endpoint";
-         when Tok_Psl_Assert =>
-            return "assert";
          when Tok_Psl_Cover =>
             return "cover";
          when Tok_Psl_Const =>
diff --git a/src/vhdl/tokens.ads b/src/vhdl/tokens.ads
index c728731..bd313e2 100644
--- a/src/vhdl/tokens.ads
+++ b/src/vhdl/tokens.ads
@@ -240,7 +240,6 @@ package Tokens is
        Tok_Psl_Property,
        Tok_Psl_Sequence,
        Tok_Psl_Endpoint,
-       Tok_Psl_Assert,
        Tok_Psl_Cover,
 
        Tok_Psl_Const,
diff --git a/testsuite/gna/ticket18/psl_test_error.vhd b/testsuite/gna/ticket18/psl_test_error.vhd
index aff4362..07a96d5 100644
--- a/testsuite/gna/ticket18/psl_test_error.vhd
+++ b/testsuite/gna/ticket18/psl_test_error.vhd
@@ -42,7 +42,7 @@ begin
 
 
 
-  -- psl statements
+  -- -psl statements
 
   -- psl default clock is rising_edge(s_clk);
 
@@ -50,4 +50,4 @@ begin
   -- psl assert always (s_write -> not(s_read)) report "ERROR: s_write and s_read active @ same time!";
 
 
-end architecture test;
\ No newline at end of file
+end architecture test;
diff --git a/testsuite/gna/ticket18/psl_test_working.vhd b/testsuite/gna/ticket18/psl_test_working.vhd
index acb8aae..7939cff 100644
--- a/testsuite/gna/ticket18/psl_test_working.vhd
+++ b/testsuite/gna/ticket18/psl_test_working.vhd
@@ -42,7 +42,7 @@ begin
 
 
 
-  -- psl statements
+  -- -psl statements
 
   -- psl default clock is rising_edge(s_clk);
 
@@ -50,4 +50,4 @@ begin
   -- psl assert always (s_write -> not(s_read));
 
 
-end architecture test;
\ No newline at end of file
+end architecture test;
diff --git a/testsuite/gna/ticket19/psl_test_cover.vhd b/testsuite/gna/ticket19/psl_test_cover.vhd
index 4f3666f..9fa73ec 100644
--- a/testsuite/gna/ticket19/psl_test_cover.vhd
+++ b/testsuite/gna/ticket19/psl_test_cover.vhd
@@ -42,7 +42,7 @@ begin
 
 
 
-  -- psl statements
+  -- -psl statements
 
   -- psl default clock is rising_edge(s_clk);
 
@@ -50,4 +50,4 @@ begin
   -- psl cover always (s_write -> not(s_read));
 
 
-end architecture test;
\ No newline at end of file
+end architecture test;
diff --git a/testsuite/gna/ticket19/psl_test_cover2.vhd b/testsuite/gna/ticket19/psl_test_cover2.vhd
index 16d6ac8..000657d 100644
--- a/testsuite/gna/ticket19/psl_test_cover2.vhd
+++ b/testsuite/gna/ticket19/psl_test_cover2.vhd
@@ -49,7 +49,7 @@ begin
 
 
 
-  -- psl statements
+  -- -psl statements
 
   -- psl default clock is rising_edge(s_clk);
 
diff --git a/testsuite/gna/ticket19/psl_test_cover3.vhd b/testsuite/gna/ticket19/psl_test_cover3.vhd
index 0ef5d6e..260a479 100644
--- a/testsuite/gna/ticket19/psl_test_cover3.vhd
+++ b/testsuite/gna/ticket19/psl_test_cover3.vhd
@@ -42,7 +42,7 @@ begin
 
 
 
-  -- psl statements
+  --- psl statements
 
   -- psl default clock is rising_edge(s_clk);