Support negated properties (#3572)

docs/CONTRIBUTORS

@@ -5,6 +5,7 @@ Please see the Verilator manual for 200+ additional contributors. Thanks to all.
 
 Adrien Le Masle
 Ahmed El-Mahmoudy
+Aleksander Kiryk
 Alex Chadwick
 Àlex Torregrosa
 Aliaksei Chapyzhenka

src/verilog.y

@@ -5529,9 +5529,23 @@ property_spec<nodep>:                   // IEEE: property_spec
 pexpr<nodep>:  // IEEE: property_expr  (The name pexpr is important as regexps just add an "p" to expr.)
         //UNSUP: This rule has been super-specialized to what is supported now
         //UNSUP remove below
+        //
+        // This rule is divided between expr and complex_pexpr to avoid an ambiguity in SystemVerilog grammar.
+        // Both pexpr and expr can consist of parentheses, and so a pexpr "((expr))" can be reduced in two ways:
+        // 1. ((expr)) -> (pexpr) -> pexpr
+        // 2. ((expr)) -> (expr)  -> pexpr
+        // The division below forces YACC to always assume the parentheses reduce to expr, unless they enclose
+        // operators that can only appear in a pexpr.
+        //
+                complex_pexpr                           { $$ = $1; }
+        |       expr                                    { $$ = $1; }
+        ;
+
+complex_pexpr<nodep>:  // IEEE: part of property_expr, see comments there
                 expr yP_ORMINUSGT pexpr                 { $$ = new AstLogOr($2, new AstLogNot($2, $1), $3); }
         |       expr yP_OREQGT pexpr                    { $$ = new AstImplication($2, $1, $3); }
-        |       expr                                    { $$ = $1; }
+        |       yNOT pexpr %prec prNEGATION             { $$ = new AstLogNot{$1, $2}; }
+        |       '(' complex_pexpr ')'                   { $$ = $2; }
         //UNSUP remove above, use below:
         //
         //                      // IEEE: sequence_expr

test_regress/t/t_negated_property.pl

@@ -0,0 +1,22 @@
+#!/usr/bin/env perl
+if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; }
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# Copyright 2022 by Antmicro Ltd. 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
+
+scenarios(simulator => 1);
+
+compile(
+    verilator_flags2 => ['--assert'],
+    );
+
+execute(
+    check_finished => 1,
+    );
+
+ok(1);
+1;

test_regress/t/t_negated_property.v

@@ -0,0 +1,50 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain, for
+// any use, without warranty, 2022 by Antmicro Ltd.
+// SPDX-License-Identifier: CC0-1.0
+
+`define MAX 10
+
+module t (/*AUTOARG*/
+      clk
+   );
+
+   input clk;
+   int cyc = 0;
+   logic [`MAX:0] val = {`MAX+1{1'b0}};
+
+   initial val[0] = 1;
+
+   Test1 t1(clk, cyc, val);
+
+   always @(posedge clk) begin
+      cyc <= cyc + 1;
+
+      $display("val = %20b", val);
+
+      if (cyc < `MAX) begin
+         val[cyc] <= 0;
+         val[cyc+1] <= 1;
+      end else begin
+         $write("*-* All Finished *-*\n");
+         $finish;
+      end
+   end
+
+endmodule
+
+module Test1 (
+      clk,
+      cyc,
+      val
+   );
+
+   input clk;
+   input [`MAX:0] val;
+   input integer cyc;
+
+   assert property(@(posedge clk) not (&val));
+
+   assert property(@(posedge clk) (not ~|val));
+endmodule