Fix disable iff ignored when its condition is held continuously true (#7841)

src/V3AssertNfa.cpp

@@ -1983,8 +1983,18 @@ class SvaNfaLowering final {
             AstNodeExpr*& sigp = c.vtx[i]->datap()->stateSigp;
             if (sigp) VL_DO_DANGLING(sigp->deleteTree(), sigp);
         }
-        // Disable iff gating on throughout/required-step rejects (IEEE 16.12).
+        // Disable iff gating (IEEE 1800-2023 16.12). The edge counter misses a
+        // continuously-true disable, so gate on the current level value too.
         if (c.disableExprp) {
+            // terminalActivep is always set, so gate it unconditionally.
+            AstNodeExpr* const notTermp
+                = new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)};
+            sigs.terminalActivep = new AstLogAnd{c.flp, sigs.terminalActivep, notTermp};
+            if (sigs.rejectBasep) {
+                AstNodeExpr* const notDisp
+                    = new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)};
+                sigs.rejectBasep = new AstLogAnd{c.flp, sigs.rejectBasep, notDisp};
+            }
             if (sigs.throughoutRejectp) {
                 AstNodeExpr* const notDisp
                     = new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)};

test_regress/t/t_cover_sequence.v

@@ -79,7 +79,7 @@ module t (
 `endif
     `checkd(hit_simple, 96);  // Questa: 95
     `checkd(hit_clocked, 149);  // Questa: 149
-    `checkd(hit_clocked_disable, 28);  // Questa: 27
+    `checkd(hit_clocked_disable, 27);  // Questa: 27
     `checkd(hit_default_disable, 30);  // Questa: 30
     `checkd(hit_consrep_2, 30);  // Questa: 29
     `checkd(hit_consrep_3, 14);  // Questa: 13

test_regress/t/t_property_accept_reject_on.v

@@ -94,16 +94,16 @@ module t (
     end
     else if (cyc == 99) begin
       `checkh(crc, 64'hc77bb9b3784ea091);
-      `checkd(count_fail1, 29);  // Questa: 14
-      `checkd(count_fail2, 65);  // Questa: 64
-      `checkd(count_fail3, 29);  // Questa: 14
-      `checkd(count_fail4, 65);  // Questa: 64
-      `checkd(count_fail5, 46);  // Questa: 31
-      `checkd(count_fail6, 65);  // Questa: 59
-      `checkd(count_fail7, 29);  // Questa: 14
-      `checkd(count_fail8, 14);  // Questa: 10
-      `checkd(count_fail9, 29);  // Questa: 14
-      `checkd(count_fail10, 29);  // Questa: 14
+      `checkd(count_fail1, 28);  // Questa: 14
+      `checkd(count_fail2, 64);  // Questa: 64
+      `checkd(count_fail3, 28);  // Questa: 14
+      `checkd(count_fail4, 64);  // Questa: 64
+      `checkd(count_fail5, 45);  // Questa: 31
+      `checkd(count_fail6, 64);  // Questa: 59
+      `checkd(count_fail7, 28);  // Questa: 14
+      `checkd(count_fail8, 13);  // Questa: 10
+      `checkd(count_fail9, 28);  // Questa: 14
+      `checkd(count_fail10, 28);  // Questa: 14
       $write("*-* All Finished *-*\n");
       $finish;
     end

test_regress/t/t_property_disable_iff_held.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 --coverage'])
+
+test.execute()
+
+test.passes()

test_regress/t/t_property_disable_iff_held.v

@@ -0,0 +1,65 @@
+// 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 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.12: a disable iff condition held continuously true must
+// disable every attempt of a multi-cycle property (verilator/verilator#7792).
+// en_held is a plain non-$sampled, non-constant signal held 1, so it exercises
+// the NFA disable-counter path. The held assert/cover must never fire; the
+// `disable iff (1'b0)` controls prove the same assert/cover do fire when enabled.
+
+module t (
+    input clk
+);
+  int cyc = 0;
+  reg [63:0] crc = 64'h5aef0c8d_d70a4497;
+  wire a = crc[0];
+  wire b = crc[4];
+
+  bit en_held = 1'b1;
+
+  int n_held_assert = 0;
+  int n_held_cover = 0;
+  int n_ctrl_assert = 0;
+  int n_ctrl_cover = 0;
+
+  // Held-true disable: assert + cover must be fully suppressed.
+  assert property (@(posedge clk) disable iff (en_held) (a ##1 b))
+    else n_held_assert <= n_held_assert + 1;
+  cover property (@(posedge clk) disable iff (en_held) (a ##1 b))
+    n_held_cover <= n_held_cover + 1;
+
+  // Enabled control (disable iff 1'b0): same assert + cover must fire.
+  assert property (@(posedge clk) disable iff (1'b0) (a ##1 b))
+    else n_ctrl_assert <= n_ctrl_assert + 1;
+  cover property (@(posedge clk) disable iff (1'b0) (a ##1 b))
+    n_ctrl_cover <= n_ctrl_cover + 1;
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
+    if (cyc == 99) begin
+      `checkd(n_held_assert, 0);  // Questa: 0
+      `checkd(n_held_cover, 0);  // Questa: 0
+      `checkd(n_ctrl_assert, 58);  // Questa: 58
+      `checkd(n_ctrl_cover, 26);  // Questa: 26
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+endmodule
+
+`ifndef VERILATOR
+module wrap;
+  logic clk = 0;
+  always #5 clk = ~clk;
+  t inst (.clk(clk));
+endmodule
+`endif

test_regress/t/t_sequence_within.v

@@ -107,14 +107,14 @@ module t (
       // engine-wide behavior, not within-specific.
       `checkd(count_p1, 23);  // Questa: 23
       `checkd(count_p2, 44);  // Questa: 44
-      `checkd(count_p3, 26);  // Questa: 20
-      `checkd(count_p4, 24);  // Questa: 22
+      `checkd(count_p3, 25);  // Questa: 20
+      `checkd(count_p4, 23);  // Questa: 22
       `checkd(count_p5, 26);  // Questa: 26
       `checkd(count_p6, 21);  // Questa: 16
       `checkd(count_p7, 15);  // Questa: 9
       `checkd(count_p8, 15);  // Questa: 4
-      `checkd(count_p9, 17);  // Questa: 10
-      `checkd(count_p10, 24);  // Questa: 15
+      `checkd(count_p9, 15);  // Questa: 10
+      `checkd(count_p10, 23);  // Questa: 15
       $write("*-* All Finished *-*\n");
       $finish;
     end