Fix parsing for sequence expressions (#6427)

Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>

src/verilog.y

@@ -6311,7 +6311,9 @@ property_port_itemDirE:
         ;
 
 property_declarationBody<nodep>:  // IEEE: part of property_declaration
-                assertion_variable_declarationList
+                assertion_variable_declarationList property_spec
+                        { $$ = nullptr; BBUNSUP($1->fileline(), "Unsupported: property variable declaration"); DEL($1); }
+        |       assertion_variable_declarationList property_spec ';'
                         { $$ = nullptr; BBUNSUP($1->fileline(), "Unsupported: property variable declaration"); DEL($1); }
         //                      // IEEE-2012: Incorrectly has yCOVER ySEQUENCE then property_spec here.
         //                      // Fixed in IEEE 1800-2017
@@ -6384,6 +6386,8 @@ property_spec<propSpecp>:               // IEEE: property_spec
                         { $$ = new AstPropSpec{$1, $3, $8, $10}; }
         |       '@' '(' senitem ')' pexpr
                         { $$ = new AstPropSpec{$1, $3, nullptr, $5}; }
+        |       '@' senitemVar pexpr
+                        { $$ = new AstPropSpec{$1, $2, nullptr, $3}; }
         //                      // Disable applied after the event occurs,
         //                      // so no existing AST can represent this
         |       yDISABLE yIFF '(' expr ')' '@' '(' senitemEdge ')' pexpr
@@ -6567,7 +6571,7 @@ sexpr<nodeExprp>:  // ==IEEE: sequence_expr  (The name sexpr is important as reg
         //                      // IEEE: "cycle_delay_range sequence_expr { cycle_delay_range sequence_expr }"
         //                      // IEEE: "sequence_expr cycle_delay_range sequence_expr { cycle_delay_range sequence_expr }"
         //                      // Both rules basically mean we can repeat sequences, so make it simpler:
-                cycle_delay_range sexpr  %prec yP_POUNDPOUND
+                cycle_delay_range ~p~sexpr  %prec yP_POUNDPOUND
                         { $$ = $2; BBUNSUP($2->fileline(), "Unsupported: ## (in sequence expression)"); }
         |       ~p~sexpr cycle_delay_range sexpr %prec prPOUNDPOUND_MULTI
                         { $$ = $1; BBUNSUP($2->fileline(), "Unsupported: ## (in sequence expression)"); }
@@ -6589,7 +6593,8 @@ sexpr<nodeExprp>:  // ==IEEE: sequence_expr  (The name sexpr is important as reg
         //                      // '(' sequence_expr {',' sequence_match_item } ')' [ boolean_abbrev ]
         //                      // "'(' sexpr ')' boolean_abbrev" matches "[sexpr:'(' expr ')'] boolean_abbrev" so we can drop it
         |       '(' ~p~sexpr ')'                        { $$ = $2; }
-        //UNSUP '(' ~p~sexpr ',' sequence_match_itemList ')'    { }
+        |       '(' ~p~sexpr ',' sequence_match_itemList ')'
+                        { $$ = $2; BBUNSUP($3, "Unsupported sequence match items"); }
         //
         //                      // AND/OR are between pexprs OR sexprs
         |       ~p~sexpr yAND ~p~sexpr

test_regress/t/t_property_pexpr.v

@@ -28,7 +28,7 @@ module t(/*AUTOARG*/
   // Test loop
   always @(posedge clk) begin
 `ifdef TEST_VERBOSE
-    $write("[%0t] cyc==%0d crc=%x result=%x\n", $time, cyc, crc);
+    $write("[%0t] cyc==%0d crc=%x\n", $time, cyc, crc);
 `endif
     cyc <= cyc + 1;
     crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
@@ -43,12 +43,17 @@ module t(/*AUTOARG*/
       `checkd(test.count_hits_iff, 48);
       `checkd(test.count_hits_implies, 24);
       `checkd(test.count_hits_not, 47);
+      `checkd(test.count_hits_event, 1);
 
       $write("*-* All Finished *-*\n");
       $finish;
     end
   end
 
+  always @(negedge clk) begin
+    if (cyc == 10) -> test.e;
+  end
+
 endmodule
 
 module Test(input clk,
@@ -59,6 +64,8 @@ module Test(input clk,
   int count_hits_iff;
   int count_hits_implies;
   int count_hits_not;
+  int count_hits_event;
+  event e;
 
   default disable iff cyc < 5;
 
@@ -73,4 +80,6 @@ module Test(input clk,
   assert property ( @(negedge clk) not a )
     else count_hits_not = count_hits_not + 1;
 
+  assert property ( @e not a )
+    else count_hits_event = count_hits_event + 1;
 endmodule

test_regress/t/t_property_sexpr_unsup.out

@@ -0,0 +1,122 @@
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:46:35: Unsupported: ## () cycle delay range expression
+   46 |   assert property (@(posedge clk) ##2 val)
+      |                                   ^~
+                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:46:39: Unsupported: ## (in sequence expression)
+   46 |   assert property (@(posedge clk) ##2 val)
+      |                                       ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:49:35: Unsupported: ## () cycle delay range expression
+   49 |   assert property (@(posedge clk) ##1 1 |=> 0)
+      |                                   ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:49:39: Unsupported: ## (in sequence expression)
+   49 |   assert property (@(posedge clk) ##1 1 |=> 0)
+      |                                       ^
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:52:35: Unsupported: ## () cycle delay range expression
+   52 |   assert property (@(posedge clk) ##1 1 |=> not (val))
+      |                                   ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:52:39: Unsupported: ## (in sequence expression)
+   52 |   assert property (@(posedge clk) ##1 1 |=> not (val))
+      |                                       ^
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:35: Unsupported: ## () cycle delay range expression
+   55 |   assert property (@(posedge clk) ##1 val)
+      |                                   ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:39: Unsupported: ## (in sequence expression)
+   55 |   assert property (@(posedge clk) ##1 val)
+      |                                       ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:58:35: Unsupported: ## () cycle delay range expression
+   58 |   assert property (@(posedge clk) ##1 (val))
+      |                                   ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:58:40: Unsupported: ## (in sequence expression)
+   58 |   assert property (@(posedge clk) ##1 (val))
+      |                                        ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:61:36: Unsupported: ## () cycle delay range expression
+   61 |   assert property (@(posedge clk) (##1 (val)))
+      |                                    ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:61:41: Unsupported: ## (in sequence expression)
+   61 |   assert property (@(posedge clk) (##1 (val)))
+      |                                         ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:64:36: Unsupported: ## () cycle delay range expression
+   64 |   assert property (@(posedge clk) (##1 (val)))
+      |                                    ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:64:41: Unsupported: ## (in sequence expression)
+   64 |   assert property (@(posedge clk) (##1 (val)))
+      |                                         ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:67:40: Unsupported: ## () cycle delay range expression
+   67 |   assert property (@(posedge clk) not (##1 val))
+      |                                        ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:67:44: Unsupported: ## (in sequence expression)
+   67 |   assert property (@(posedge clk) not (##1 val))
+      |                                            ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:70:35: Unsupported: ## () cycle delay range expression
+   70 |   assert property (@(posedge clk) ##1 1 |=> 1)
+      |                                   ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:70:39: Unsupported: ## (in sequence expression)
+   70 |   assert property (@(posedge clk) ##1 1 |=> 1)
+      |                                       ^
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:73:35: Unsupported: ## () cycle delay range expression
+   73 |   assert property (@(posedge clk) ##1 val |=> not val)
+      |                                   ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:73:39: Unsupported: ## (in sequence expression)
+   73 |   assert property (@(posedge clk) ##1 val |=> not val)
+      |                                       ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:76:35: Unsupported: ## () cycle delay range expression
+   76 |   assert property (@(posedge clk) ##1 (val) |=> not (val))
+      |                                   ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:76:40: Unsupported: ## (in sequence expression)
+   76 |   assert property (@(posedge clk) ##1 (val) |=> not (val))
+      |                                        ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:57: Unsupported: ## () cycle delay range expression
+   82 |   assert property (@(posedge clk) disable iff (cyc < 3) ##1 1 |=> cyc > 3)
+      |                                                         ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:61: Unsupported: ## (in sequence expression)
+   82 |   assert property (@(posedge clk) disable iff (cyc < 3) ##1 1 |=> cyc > 3)
+      |                                                             ^
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:85:36: Unsupported: ## () cycle delay range expression
+   85 |   assert property (@(posedge clk) (##1 val) |=> (##1 val))
+      |                                    ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:85:40: Unsupported: ## (in sequence expression)
+   85 |   assert property (@(posedge clk) (##1 val) |=> (##1 val))
+      |                                        ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:85:50: Unsupported: ## () cycle delay range expression
+   85 |   assert property (@(posedge clk) (##1 val) |=> (##1 val))
+      |                                                  ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:85:54: Unsupported: ## (in sequence expression)
+   85 |   assert property (@(posedge clk) (##1 val) |=> (##1 val))
+      |                                                      ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:103:14: Unsupported sequence match items
+  103 |     ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
+      |              ^
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:103:29: Unsupported: ## range cycle delay range expression
+  103 |     ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
+      |                             ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:103:39: Unsupported: ## (in sequence expression)
+  103 |     ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
+      |                                       ^
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:102:13: Unsupported: property variable declaration
+  102 |     integer l_b;
+      |             ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:120:16: Unsupported sequence match items
+  120 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
+      |                ^
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:120:35: Unsupported: ## () cycle delay range expression
+  120 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
+      |                                   ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:120:51: Unsupported: [-> boolean abbrev expression
+  120 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
+      |                                                   ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:120:54: Unsupported: boolean abbrev (in sequence expression)
+  120 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
+      |                                                      ^
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:120:37: Unsupported: ## (in sequence expression)
+  120 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
+      |                                     ^
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:118:14: Unsupported: property variable declaration
+  118 |     realtime l_t;
+      |              ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:124:31: Unsupported: ## () cycle delay range expression
+  124 |   assert property (@clk not a ##1 b);
+      |                               ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:124:33: Unsupported: ## (in sequence expression)
+  124 |   assert property (@clk not a ##1 b);
+      |                                 ^
+%Error: Exiting due to

test_regress/t/t_property_sexpr_unsup.py

@@ -0,0 +1,18 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# Copyright 2025 by Wilson Snyder. This program is free software; you
+# can redistribute it and/or modify it under the terms of either the GNU
+# Lesser General Public License Version 3 or the Perl Artistic License
+# Version 2.0.
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('vlt')
+
+test.lint(expect_filename=test.golden_filename,
+          verilator_flags2=['--assert', '--timing', '--error-limit 1000'],
+          fails=True)
+
+test.passes()

test_regress/t/t_property_sexpr_unsup.v

@@ -0,0 +1,125 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed into the Public Domain, for any use,
+// without warranty, 2025 by Antmicro.
+// SPDX-License-Identifier: CC0-1.0
+
+module t (  /*AUTOARG*/
+    // Inputs
+    clk
+);
+
+  input clk;
+  integer cyc = 1;
+  bit val = 0;
+
+  Test test (  /*AUTOINST*/
+      // Inputs
+      .clk(clk),
+      .val(val),
+      .cyc(cyc)
+  );
+
+  Ieee ieee();
+
+  always @(posedge clk) begin
+    if (cyc != 0) begin
+      cyc <= cyc + 1;
+      val = ~val;
+`ifdef TEST_VERBOSE
+      $display("cyc=%0d, val=%0d", cyc, val);
+`endif
+      if (cyc == 10) begin
+        $write("*-* All Finished *-*\n");
+        $finish;
+      end
+    end
+  end
+endmodule
+
+module Test (
+    input clk,
+    input bit val,
+    input integer cyc
+);
+
+  assert property (@(posedge clk) ##2 val)
+  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) ##1 1 |=> 0)
+  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) ##1 1 |=> not (val))
+  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) ##1 val)
+  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) ##1 (val))
+  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) (##1 (val)))
+  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) (##1 (val)))
+  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) not (##1 val))
+  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) ##1 1 |=> 1)
+  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) ##1 val |=> not val)
+  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) ##1 (val) |=> not (val))
+  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) ((val) |=> not (val)))
+  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) disable iff (cyc < 3) ##1 1 |=> cyc > 3)
+  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) (##1 val) |=> (##1 val))
+  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+endmodule
+
+// Test parsing only
+module Ieee;
+  // IEEE 1800-2023 16.6
+  bit a;
+  integer b;
+  byte q[$];
+  logic clk;
+
+  property p1;
+    $rose(a) |-> q[0];
+  endproperty
+
+  property p2;
+    integer l_b;
+    ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
+  endproperty
+
+  bit [2:0] count = 0;
+  realtime t;
+  always @(posedge clk) begin
+    if (count == 0) t = $realtime;
+    count++;
+  end
+  property p3;
+    @(posedge clk)
+    count == 7 |-> $realtime - t < 50.5;
+  endproperty
+
+  property p4;
+    realtime l_t;
+    @(posedge clk)
+    (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
+  endproperty
+
+  // IEEE 1800-2023 16.12.3
+  assert property (@clk not a ##1 b);
+endmodule

test_regress/t/t_property_var_unsup.out

@@ -1,11 +1,10 @@
+%Error-UNSUPPORTED: t/t_property_var_unsup.v:18:13: Unsupported sequence match items
+   18 |       (valid, prevcyc = cyc) |=> (cyc == prevcyc + 1);
+      |             ^
+                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
 %Error-UNSUPPORTED: t/t_property_var_unsup.v:17:11: Unsupported: property variable declaration
    17 |       int prevcyc;
       |           ^~~~~~~
-                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
-%Error: t/t_property_var_unsup.v:18:7: syntax error, unexpected '(', expecting endproperty
-   18 |       (valid, prevcyc = cyc) |=> (cyc == prevcyc + 1);
-      |       ^
-        ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
 %Error-UNSUPPORTED: t/t_property_var_unsup.v:24:31: Unsupported: property variable default value
    24 |    property with_def(int nine = 9);
       |                               ^