From ec124a0905efb96f4c599c3cde61fd26715f0a42 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Sun, 12 Jul 2026 02:44:56 +0200 Subject: [PATCH] Fix mid-window disable iff (#7792) (#7869) Fixes #7792 --- src/V3AssertNfa.cpp | 6 +- test_regress/t/t_prop_always.v | 2 +- .../t/t_property_disable_iff_counter.py | 20 +++++ .../t/t_property_disable_iff_counter.v | 69 +++++++++++++++++ test_regress/t/t_property_disable_iff_held.v | 72 ++++++++++------- .../t/t_property_disable_iff_midpulse.py | 18 +++++ .../t/t_property_disable_iff_midpulse.v | 77 +++++++++++++++++++ test_regress/t/t_sequence_within.v | 4 +- 8 files changed, 235 insertions(+), 33 deletions(-) create mode 100755 test_regress/t/t_property_disable_iff_counter.py create mode 100644 test_regress/t/t_property_disable_iff_counter.v create mode 100755 test_regress/t/t_property_disable_iff_midpulse.py create mode 100644 test_regress/t/t_property_disable_iff_midpulse.v diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 552eabd48..680213f18 100644 --- a/src/V3AssertNfa.cpp +++ b/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; diff --git a/test_regress/t/t_prop_always.v b/test_regress/t/t_prop_always.v index f389a3a8c..69ccda1c9 100644 --- a/test_regress/t/t_prop_always.v +++ b/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 diff --git a/test_regress/t/t_property_disable_iff_counter.py b/test_regress/t/t_property_disable_iff_counter.py new file mode 100755 index 000000000..941ecc46f --- /dev/null +++ b/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() diff --git a/test_regress/t/t_property_disable_iff_counter.v b/test_regress/t/t_property_disable_iff_counter.v new file mode 100644 index 000000000..a25a67be5 --- /dev/null +++ b/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 diff --git a/test_regress/t/t_property_disable_iff_held.v b/test_regress/t/t_property_disable_iff_held.v index 37fa06461..e1ef13a13 100644 --- a/test_regress/t/t_property_disable_iff_held.v +++ b/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 -// 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. +// A disable iff held true for the whole attempt window disables it. 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; - int n_held_cover = 0; - int n_ctrl_assert = 0; - int n_ctrl_cover = 0; + reg hold = 0; + reg fail_now = 0; + wire value = !(in_run && (phase == N) && fail_now); + wire dis = in_run && hold && (phase >= 1); - // 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; + int n_held_fire = 0; + int n_ctrl_fire = 0; + int exp_held_fire = 0; + int exp_ctrl_fire = 0; - // 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; + assert property (@(posedge clk) disable iff (dis) trig |-> ##N value) + else n_held_fire <= n_held_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 (cyc == 99) begin - `checkd(n_held_assert, 0); - `checkd(n_held_cover, 0); - `checkd(n_ctrl_assert, 58); - `checkd(n_ctrl_cover, 26); // Others: 26, One other: 0 + if (phase == PERIOD - 1) begin + phase <= 0; + idx <= idx + 1; + end + 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 diff --git a/test_regress/t/t_property_disable_iff_midpulse.py b/test_regress/t/t_property_disable_iff_midpulse.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/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() diff --git a/test_regress/t/t_property_disable_iff_midpulse.v b/test_regress/t/t_property_disable_iff_midpulse.v new file mode 100644 index 000000000..9106ab850 --- /dev/null +++ b/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 diff --git a/test_regress/t/t_sequence_within.v b/test_regress/t/t_sequence_within.v index e8d73ad61..a7cc3c5ed 100644 --- a/test_regress/t/t_sequence_within.v +++ b/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