Support procedural concurrent assertions with inferred clock (#7581)

src/V3Assert.cpp

@@ -415,24 +415,22 @@ class AssertVisitor final : public VNVisitor {
             nodep->v3fatalSrc("Unhandled assert type");
         }
         iterateAndNextNull(nodep->passsp());
-        AstSenTree* const sentreep = nodep->sentreep();
+        AstSenTree* sentreep = nodep->sentreep();
         if (nodep->immediate()) {
             UASSERT_OBJ(!sentreep, nodep, "Immediate assertions don't have sensitivity");
         } else {
             UASSERT_OBJ(sentreep, nodep, "Concurrent assertions must have sensitivity");
-            if (m_procedurep) {
-                if (!nodep->senFromAlways()) {
-                    // To support this need queue of asserts to activate
-                    nodep->v3warn(E_UNSUPPORTED,
-                                  "Unsupported: Procedural concurrent assertion with"
-                                  " clocking event inside always (IEEE 1800-2023 16.14.6)");
-                }
-                // Change type to concurrent and relink after process
-                nodep->immediate(false);
+            // Explicit inline clock differs from the enclosing always: hoist
+            // and warn. To support this need queue of asserts to activate.
+            if (m_procedurep && !nodep->senFromAlways()) {
+                nodep->v3warn(E_UNSUPPORTED,
+                              "Unsupported: Procedural concurrent assertion with"
+                              " clocking event inside always (IEEE 1800-2023 16.14.6)");
                 static_cast<AstNode*>(m_procedurep)->addNext(nodep->unlinkFrBack());
                 return;  // Later iterate will pick up
             }
             sentreep->unlinkFrBack();
+            if (m_procedurep) { VL_DO_DANGLING(pushDeletep(sentreep), sentreep); }
         }
         //
         const string& message = nodep->name();

test_regress/t/t_assert_procedural_gated.py

@@ -0,0 +1,18 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# 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-FileCopyrightText: 2026 Wilson Snyder
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('simulator')
+
+test.compile()
+
+test.execute()
+
+test.passes()

test_regress/t/t_assert_procedural_gated.v

@@ -0,0 +1,68 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 PlanV GmbH
+// SPDX-License-Identifier: CC0-1.0
+
+// verilog_format: off
+`define stop $stop
+`define checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0x exp=%0x (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0);
+`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
+// verilog_format: on
+
+// IEEE 1800-2023 16.14.6: if-gated procedural concurrent assertion vs
+// module-scope reference; counts must diverge to prove the gate is preserved.
+
+module t (
+    input clk
+);
+
+  int cyc;
+  reg [63:0] crc;
+  reg rst_l;
+
+  // Derive property operands from non-adjacent CRC bits.
+  wire [1:0] req = {crc[6], crc[0]};
+  wire gnt = crc[12];
+
+  int count_gated = 0;
+  int count_ref = 0;
+
+  // Procedural concurrent assertion with inferred clock, guarded by
+  // `if (cyc[0])`. The assertion attempt only starts on odd cycles.
+  always @(negedge clk) begin
+    if (cyc[0])
+      assert property (disable iff (!rst_l) ((&req) |-> gnt))
+      else count_gated <= count_gated + 1;
+  end
+
+  // Module-scope reference assertion with identical disable iff / property
+  // but no procedural gating.
+  assert property (@(negedge clk) disable iff (!rst_l) ((&req) |-> gnt))
+  else count_ref <= count_ref + 1;
+
+  always @(posedge clk) begin
+`ifdef TEST_VERBOSE
+    $write("[%0t] cyc==%0d crc=%x rst_l=%b req=%b gnt=%b gated=%0d ref=%0d\n", $time, cyc, crc,
+           rst_l, req, gnt, count_gated, count_ref);
+`endif
+    cyc <= cyc + 1;
+    crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
+    if (cyc == 0) begin
+      crc <= 64'h5aef0c8d_d70a4497;
+      rst_l <= 1'b0;
+    end
+    else if (cyc == 3) begin
+      rst_l <= 1'b1;
+    end
+    else if (cyc == 99) begin
+      `checkh(crc, 64'hc77bb9b3784ea091);
+      // Questa 2022.3 golden: count_gated=5, count_ref=12.
+      `checkd(count_gated, 5);
+      `checkd(count_ref, 12);
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+
+endmodule