Fix mid-window disable iff (#7792) (#7869)

Fixes #7792

src/V3AssertNfa.cpp

@@ -1718,7 +1718,7 @@ class SvaNfaLowering final {
                 AstNodeExpr* srcSigp = c.vtx[fromIdx]->datap()->stateSigp->cloneTreePure(false);
                 srcSigp = andCond(c.flp, srcSigp, te.m_condp);
 
-                if (c.disableExprp && !c.snapshotVarp) {
+                if (c.disableExprp) {
                     AstNodeExpr* const notDisp
                         = new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)};
                     srcSigp = new AstLogAnd{c.flp, srcSigp, notDisp};
@@ -1770,7 +1770,7 @@ class SvaNfaLowering final {
                             "Delay-ring incoming source missing stateSig");
                 AstNodeExpr* contribp = c.vtx[fi]->datap()->stateSigp->cloneTreePure(false);
                 contribp = andCond(c.flp, contribp, tep->m_condp);
-                if (c.disableExprp && !c.snapshotVarp) {
+                if (c.disableExprp) {
                     AstNodeExpr* const notDisp
                         = new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)};
                     contribp = new AstLogAnd{c.flp, contribp, notDisp};
@@ -1805,7 +1805,7 @@ class SvaNfaLowering final {
             if (vtxp->m_delayRingClearCondp) {
                 clearCondp = sampled(vtxp->m_delayRingClearCondp->cloneTreePure(false));
             }
-            if (c.disableExprp && !c.snapshotVarp) {
+            if (c.disableExprp) {
                 clearCondp = orExprs(c.flp, clearCondp, c.disableExprp->cloneTreePure(false));
             }
             AstNodeExpr* guardp = nullptr;

test_regress/t/t_prop_always.v

@@ -88,7 +88,7 @@ module t (
       `checkd(rand_bounded_pass_q.size(), 0);
       `checkd(rand_bounded_fail_q.size(), 20);  // Other sims: 19, 11
       `checkd(disable_bounded_pass_q.size(), 0);
-      `checkd(disable_bounded_fail_q.size(), 13);  // Other sims: 5, 6
+      `checkd(disable_bounded_fail_q.size(), 8);  // Other sims: 5, 6
       $write("*-* All Finished *-*\n");
       $finish;
     end

test_regress/t/t_property_disable_iff_counter.py

@@ -0,0 +1,20 @@
+#!/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.sim_time = 16000
+
+test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing', '-Wno-UNOPTTHREADS'])
+
+test.execute()
+
+test.passes()

test_regress/t/t_property_disable_iff_counter.v

@@ -0,0 +1,69 @@
+// 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
+
+// disable iff mid-window on the counter-FSM path (##[1:N], N > 256 unroll limit).
+
+module t (
+    input clk
+);
+  localparam int N = 257;  // > 256 unroll limit -> counter FSM path
+  localparam int PERIOD = 260;  // > N -> attempts never overlap
+  localparam int NATT = 30;
+
+  int cyc = 0;
+  reg [63:0] crc = 64'h5aef0c8d_d70a4497;
+
+  int phase = 0;
+  int idx = 0;
+  wire in_run = (idx < NATT);
+  wire trig = in_run && (phase == 0);
+  wire value = 1'b0;
+
+  reg do_dis = 0;
+  int dis_at = 0;
+  wire dis = in_run && do_dis && (phase == dis_at);
+
+  int n_dis_fire = 0;
+  int n_ctrl_fire = 0;
+  int exp_dis_fire = 0;
+
+  assert property (@(posedge clk) disable iff (dis) trig |-> ##[1:N] value)
+  else n_dis_fire <= n_dis_fire + 1;
+
+  assert property (@(posedge clk) disable iff (1'b0) trig |-> ##[1:N] value)
+  else n_ctrl_fire <= n_ctrl_fire + 1;
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
+    if (phase == PERIOD - 1) begin
+      phase <= 0;
+      idx <= idx + 1;
+    end else begin
+      phase <= phase + 1;
+    end
+    if (phase == 0) begin
+      do_dis <= crc[3];
+      dis_at <= 1 + (int'(crc[20:12]) % (N - 1));
+    end
+    if (in_run && phase == N && !do_dis) exp_dis_fire <= exp_dis_fire + 1;
+    if (idx == NATT && phase == 4) begin
+`ifdef TEST_VERBOSE
+      $write("n_dis_fire=%0d exp=%0d n_ctrl_fire=%0d\n", n_dis_fire, exp_dis_fire, n_ctrl_fire);
+`endif
+      `checkd(n_dis_fire, exp_dis_fire);
+      `checkd(n_ctrl_fire, NATT);
+      if (n_dis_fire == 0 || n_dis_fire == NATT) $stop;  // guard a degenerate seed
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+endmodule

test_regress/t/t_property_disable_iff_held.v

@@ -9,47 +9,65 @@
 `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
+// A disable iff held true for the whole attempt window disables it.
-// 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
 );
+  localparam int N = 5;
+  localparam int PERIOD = 9;
+  localparam int NATT = 40;
+
   int cyc = 0;
   reg [63:0] crc = 64'h5aef0c8d_d70a4497;
-  wire a = crc[0];
-  wire b = crc[4];
 
-  bit en_held = 1'b1;
+  int phase = 0;
+  int idx = 0;
+  wire in_run = (idx < NATT);
+  wire trig = in_run && (phase == 0);
 
-  int n_held_assert = 0;
+  reg hold = 0;
-  int n_held_cover = 0;
+  reg fail_now = 0;
-  int n_ctrl_assert = 0;
+  wire value = !(in_run && (phase == N) && fail_now);
-  int n_ctrl_cover = 0;
+  wire dis = in_run && hold && (phase >= 1);
 
-  // Held-true disable: assert + cover must be fully suppressed.
+  int n_held_fire = 0;
-  assert property (@(posedge clk) disable iff (en_held) (a ##1 b))
+  int n_ctrl_fire = 0;
-    else n_held_assert <= n_held_assert + 1;
+  int exp_held_fire = 0;
-  cover property (@(posedge clk) disable iff (en_held) (a ##1 b))
+  int exp_ctrl_fire = 0;
-    n_held_cover <= n_held_cover + 1;
 
-  // Enabled control (disable iff 1'b0): same assert + cover must fire.
+  assert property (@(posedge clk) disable iff (dis) trig |-> ##N value)
-  assert property (@(posedge clk) disable iff (1'b0) (a ##1 b))
+  else n_held_fire <= n_held_fire + 1;
-    else n_ctrl_assert <= n_ctrl_assert + 1;
+
-  cover property (@(posedge clk) disable iff (1'b0) (a ##1 b))
+  assert property (@(posedge clk) disable iff (1'b0) trig |-> ##N value)
-    n_ctrl_cover <= n_ctrl_cover + 1;
+  else n_ctrl_fire <= n_ctrl_fire + 1;
 
   always @(posedge clk) begin
     cyc <= cyc + 1;
     crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
-    if (cyc == 99) begin
+    if (phase == PERIOD - 1) begin
-      `checkd(n_held_assert, 0);
+      phase <= 0;
-      `checkd(n_held_cover, 0);
+      idx <= idx + 1;
-      `checkd(n_ctrl_assert, 58);
+    end
-      `checkd(n_ctrl_cover, 26);  // Others: 26, One other: 0
+    else begin
+      phase <= phase + 1;
+    end
+    if (phase == 0) begin
+      hold <= crc[3];
+      fail_now <= crc[7];
+    end
+    if (in_run && phase == N) begin
+      exp_ctrl_fire <= exp_ctrl_fire + (fail_now ? 1 : 0);
+      if (!hold) exp_held_fire <= exp_held_fire + (fail_now ? 1 : 0);
+    end
+    if (idx == NATT && phase == 4) begin
+`ifdef TEST_VERBOSE
+      $write("n_held_fire=%0d exp=%0d n_ctrl_fire=%0d exp_ctrl=%0d\n", n_held_fire, exp_held_fire,
+             n_ctrl_fire, exp_ctrl_fire);
+`endif
+      `checkd(n_held_fire, exp_held_fire);
+      `checkd(n_ctrl_fire, exp_ctrl_fire);
+      if (n_held_fire == 0 || n_held_fire == NATT) $stop;
       $write("*-* All Finished *-*\n");
       $finish;
     end

test_regress/t/t_property_disable_iff_midpulse.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_disable_iff_midpulse.v

@@ -0,0 +1,77 @@
+// 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
+
+// Mid-window disable pulse on the packed ##N delay path (N < unroll limit).
+
+module t (
+    input clk
+);
+  localparam int N = 8;
+  localparam int PERIOD = 12;
+  localparam int NATT = 40;
+
+  int cyc = 0;
+  reg [63:0] crc = 64'h5aef0c8d_d70a4497;
+
+  int phase = 0;
+  int idx = 0;
+  wire in_run = (idx < NATT);
+  wire trig = in_run && (phase == 0);
+
+  reg do_dis = 0;
+  int dis_at = 0;
+  reg fail_now = 0;
+  wire value = !(in_run && (phase == N) && fail_now);
+  wire dis = in_run && do_dis && (phase == dis_at);
+
+  int n_dis_fire = 0;
+  int n_ctrl_fire = 0;
+  int exp_dis_fire = 0;
+  int exp_ctrl_fire = 0;
+
+  assert property (@(posedge clk) disable iff (dis) trig |-> ##N value)
+  else n_dis_fire <= n_dis_fire + 1;
+
+  assert property (@(posedge clk) disable iff (1'b0) trig |-> ##N value)
+  else n_ctrl_fire <= n_ctrl_fire + 1;
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
+    if (phase == PERIOD - 1) begin
+      phase <= 0;
+      idx <= idx + 1;
+    end
+    else begin
+      phase <= phase + 1;
+    end
+    if (phase == 0) begin
+      do_dis <= crc[3];
+      dis_at <= 1 + (int'(crc[20:12]) % (N - 1));
+      fail_now <= crc[7];
+    end
+    if (in_run && phase == N) begin
+      exp_ctrl_fire <= exp_ctrl_fire + (fail_now ? 1 : 0);
+      if (!do_dis) exp_dis_fire <= exp_dis_fire + (fail_now ? 1 : 0);
+    end
+    if (idx == NATT && phase == 4) begin
+`ifdef TEST_VERBOSE
+      $write("n_dis_fire=%0d exp=%0d n_ctrl_fire=%0d exp_ctrl=%0d\n", n_dis_fire, exp_dis_fire,
+             n_ctrl_fire, exp_ctrl_fire);
+`endif
+      `checkd(n_dis_fire, exp_dis_fire);
+      `checkd(n_ctrl_fire, exp_ctrl_fire);
+      if (n_dis_fire == 0 || n_dis_fire == NATT) $stop;
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+endmodule

test_regress/t/t_sequence_within.v

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