Fix internal error on multi-cycle SVA under default clocking (#7472) (#7506)

src/V3AssertNfa.cpp

@@ -1467,6 +1467,8 @@ public:
 class AssertNfaVisitor final : public VNVisitor {
     // STATE
     AstNodeModule* m_modp = nullptr;  // Current module being processed
+    AstClocking* m_defaultClockingp = nullptr;  // Default clocking
+    AstDefaultDisable* m_defaultDisablep = nullptr;  // Default disable iff
     SvaNfaLowering* m_loweringp = nullptr;  // NFA-to-hardware lowering engine
     V3UniqueNames m_propVarNames{"__Vpropvar"};  // Property-local variable names
     V3UniqueNames m_disableCntNames{"__VnfaDis"};  // Disable-iff counter names
@@ -1815,6 +1817,13 @@ class AssertNfaVisitor final : public VNVisitor {
         bool senTreeOwned = false;  // True if we created senTreep locally
         AstPropSpec* const propSpecp = VN_CAST(assertp->propp(), PropSpec);
         UASSERT_OBJ(propSpecp, assertp, "Concurrent assertion must have PropSpec");
+        // Inherit module defaults (IEEE 14.12, 16.15) when assertion has none.
+        if (!propSpecp->sensesp() && m_defaultClockingp) {
+            propSpecp->sensesp(m_defaultClockingp->sensesp()->cloneTree(true));
+        }
+        if (!propSpecp->disablep() && m_defaultDisablep) {
+            propSpecp->disablep(m_defaultDisablep->condp()->cloneTreePure(true));
+        }
         if (!senTreep && propSpecp->sensesp()) {
             senTreep
                 = new AstSenTree{propSpecp->fileline(), propSpecp->sensesp()->cloneTree(true)};
@@ -1886,11 +1895,22 @@ class AssertNfaVisitor final : public VNVisitor {
     void visit(AstNodeModule* nodep) override {
         VL_RESTORER(m_modp);
         VL_RESTORER(m_loweringp);
+        VL_RESTORER(m_defaultClockingp);
+        VL_RESTORER(m_defaultDisablep);
         m_modp = nodep;
+        m_defaultClockingp = nullptr;
+        m_defaultDisablep = nullptr;
         SvaNfaLowering lowering{nodep};
         m_loweringp = &lowering;
         iterateChildren(nodep);
     }
+    void visit(AstClocking* nodep) override {
+        if (nodep->isDefault() && !m_defaultClockingp) m_defaultClockingp = nodep;
+        iterateChildren(nodep);
+    }
+    void visit(AstDefaultDisable* nodep) override {
+        if (!m_defaultDisablep) m_defaultDisablep = nodep;
+    }
     void visit(AstAssert* nodep) override { processAssertion(nodep); }
     void visit(AstCover* nodep) override { processAssertion(nodep); }
     void visit(AstRestrict* nodep) override {

src/V3AssertPre.cpp

@@ -240,6 +240,15 @@ private:
         VL_RESTORER(m_clockingp);
         m_clockingp = nodep;
         UINFO(8, "   CLOCKING" << nodep);
+        if (nodep->isDefault()) {
+            if (m_defaultClockingp) {
+                nodep->v3error("Only one default clocking block allowed per module"
+                               " (IEEE 1800-2023 14.12)");
+            } else {
+                m_defaultClockingp = nodep;
+                m_defaultClkEvtVarp = nodep->ensureEventp();
+            }
+        }
         iterateChildren(nodep);
         if (nodep->eventp()) nodep->addNextHere(nodep->eventp()->unlinkFrBack());
         VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
@@ -1182,7 +1191,12 @@ private:
     }
 
     void visit(AstDefaultDisable* nodep) override {
-        // Done with these
+        if (m_defaultDisablep) {
+            nodep->v3error("Only one 'default disable iff' allowed per module"
+                           " (IEEE 1800-2023 16.15)");
+        } else {
+            m_defaultDisablep = nodep;
+        }
         VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
     }
     void visit(AstInferredDisable* nodep) override {
@@ -1293,29 +1307,8 @@ private:
         VL_RESTORER(m_modp);
         m_defaultClockingp = nullptr;
         m_defaultClkEvtVarp = nullptr;
-        nodep->foreach([&](AstClocking* const clockingp) {
-            if (clockingp->isDefault()) {
-                if (m_defaultClockingp) {
-                    clockingp->v3error("Only one default clocking block allowed per module"
-                                       " (IEEE 1800-2023 14.12)");
-                }
-                m_defaultClockingp = clockingp;
-            }
-        });
         m_defaultDisablep = nullptr;
-        nodep->foreach([&](AstDefaultDisable* const disablep) {
-            if (m_defaultDisablep) {
-                disablep->v3error("Only one 'default disable iff' allowed per module"
-                                  " (IEEE 1800-2023 16.15)");
-            }
-            m_defaultDisablep = disablep;
-        });
         m_modp = nodep;
-        // Pre-create and cache the clocking event var before iterating children.
-        // visit(AstClocking) will unlink the event from the clocking node and place it
-        // in the module tree, then delete the clocking. After that, ensureEventp() would
-        // create an orphaned var. Caching here avoids this.
-        m_defaultClkEvtVarp = m_defaultClockingp ? m_defaultClockingp->ensureEventp() : nullptr;
         iterateChildren(nodep);
     }
     void visit(AstProperty* nodep) override {

test_regress/t/t_property_default_clocking_sexpr.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(timing_loop=True, verilator_flags2=['--assert', '--timing'])
+
+test.execute()
+
+test.passes()

test_regress/t/t_property_default_clocking_sexpr.v

@@ -0,0 +1,138 @@
+// 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='h%x exp='h%x\n", `__FILE__,`__LINE__, (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
+
+// Issue #7472 reproducer (default clocking + |=> + throughout).
+module wsn (
+  input clk,
+  input a, b, c, d
+);
+  default clocking @(posedge clk); endclocking
+  int fail = 0;
+  assert property (
+      a |=> b throughout (c ##1 d)
+  ) else fail <= fail + 1;
+endmodule
+
+// Explicit @(edge) must override default clocking.
+module clk_override (
+  input clk_default,
+  input clk_explicit,
+  input a, b, c, d
+);
+  default clocking @(posedge clk_default); endclocking
+  int default_fail = 0;
+  int explicit_fail = 0;
+  assert property (a |=> b throughout (c ##1 d))
+    else default_fail <= default_fail + 1;
+  assert property (@(posedge clk_explicit) a |=> b throughout (c ##1 d))
+    else explicit_fail <= explicit_fail + 1;
+endmodule
+
+// Explicit `disable iff` must override default disable.
+module dgate (
+  input clk,
+  input rst,
+  input a, b, c, d
+);
+  default clocking @(posedge clk); endclocking
+  default disable iff (rst);
+  int default_dis_fail = 0;
+  int explicit_dis_fail = 0;
+  assert property (a |=> b throughout (c ##1 d))
+    else default_dis_fail <= default_dis_fail + 1;
+  assert property (disable iff (1'b0) a |=> b throughout (c ##1 d))
+    else explicit_dis_fail <= explicit_dis_fail + 1;
+endmodule
+
+// No defaults, explicit clock -- fix must not alter this path.
+module nodef (
+  input clk,
+  input a, b, c, d
+);
+  int fail = 0;
+  assert property (@(posedge clk) a |=> b throughout (c ##1 d))
+    else fail <= fail + 1;
+endmodule
+
+module t (
+  input clk
+);
+  integer cyc = 0;
+  reg [63:0] crc = '0;
+
+  wire a = crc[0];
+  wire b = crc[4];
+  wire c = crc[8];
+  wire d = crc[12];
+
+  wire clk_alt = ~clk;
+  wire rst    = (cyc < 10);
+
+  default clocking @(posedge clk); endclocking
+  default disable iff (cyc < 10);
+
+  int count_fail1 = 0;
+  int count_fail2 = 0;
+  int count_fail3 = 0;
+  int count_fail4 = 0;
+
+  // Issue #7472 exact shape.
+  assert property (a |=> b throughout (c ##1 d))
+    else count_fail1 <= count_fail1 + 1;
+  assert property (a |-> b throughout (c ##1 d))
+    else count_fail2 <= count_fail2 + 1;
+  assert property (a |=> c ##1 d)
+    else count_fail3 <= count_fail3 + 1;
+  assert property (a |=> b throughout (c throughout (c ##1 d)))
+    else count_fail4 <= count_fail4 + 1;
+
+  cover property (a throughout (c ##[1:2] d));
+  cover property (a |=> b throughout (c ##1 d));
+
+  // Generate-scope: module foreach must reach inside generate blocks.
+  generate
+    if (1) begin : g
+      int gen_fail = 0;
+      assert property (a |=> b throughout (c ##1 d))
+        else gen_fail <= gen_fail + 1;
+    end
+  endgenerate
+
+  wsn          u_wsn      (.clk(clk), .a(a), .b(b), .c(c), .d(d));
+  clk_override u_override (.clk_default(clk), .clk_explicit(clk_alt),
+                           .a(a), .b(b), .c(c), .d(d));
+  dgate        u_dgate    (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .d(d));
+  nodef        u_nodef    (.clk(clk), .a(a), .b(b), .c(c), .d(d));
+
+  always_ff @(posedge clk) begin
+    cyc <= cyc + 1;
+    crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
+    if (cyc == 0) begin
+      crc <= 64'h5aef0c8d_d70a4497;
+    end else if (cyc == 99) begin
+      `checkh(crc, 64'hc77bb9b3784ea091);
+      `checkd(count_fail1, 35);
+      `checkd(count_fail2, 36);
+      `checkd(count_fail3, 29);
+      `checkd(count_fail4, 35);
+      `checkd(u_wsn.fail,                  39);
+      `checkd(u_override.default_fail,     39);
+      `checkd(u_override.explicit_fail,    39);
+      `checkd(u_dgate.default_dis_fail,    35);
+      `checkd(u_dgate.explicit_dis_fail,   39);
+      `checkd(u_nodef.fail,                39);
+      `checkd(g.gen_fail,                  35);
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+endmodule