From 38533013670b950ff207fb192b3ea60ad8b0fa8a Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Fri, 26 Jun 2026 12:00:44 +0200 Subject: [PATCH] Fix disable iff ignored when its condition is held continuously true (#7841) --- src/V3AssertNfa.cpp | 12 +++- test_regress/t/t_cover_sequence.v | 2 +- test_regress/t/t_property_accept_reject_on.v | 20 +++--- test_regress/t/t_property_disable_iff_held.py | 18 +++++ test_regress/t/t_property_disable_iff_held.v | 65 +++++++++++++++++++ test_regress/t/t_sequence_within.v | 8 +-- 6 files changed, 109 insertions(+), 16 deletions(-) create mode 100755 test_regress/t/t_property_disable_iff_held.py create mode 100644 test_regress/t/t_property_disable_iff_held.v diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 7949f8563..6a35273a5 100644 --- a/src/V3AssertNfa.cpp +++ b/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)}; diff --git a/test_regress/t/t_cover_sequence.v b/test_regress/t/t_cover_sequence.v index 719a3c1ba..42f39949e 100644 --- a/test_regress/t/t_cover_sequence.v +++ b/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 diff --git a/test_regress/t/t_property_accept_reject_on.v b/test_regress/t/t_property_accept_reject_on.v index 020e754f2..1affe217c 100644 --- a/test_regress/t/t_property_accept_reject_on.v +++ b/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 diff --git a/test_regress/t/t_property_disable_iff_held.py b/test_regress/t/t_property_disable_iff_held.py new file mode 100755 index 000000000..8c5881f1b --- /dev/null +++ b/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() diff --git a/test_regress/t/t_property_disable_iff_held.v b/test_regress/t/t_property_disable_iff_held.v new file mode 100644 index 000000000..04530fc6e --- /dev/null +++ b/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 diff --git a/test_regress/t/t_sequence_within.v b/test_regress/t/t_sequence_within.v index 093b7afcb..dcffaae56 100644 --- a/test_regress/t/t_sequence_within.v +++ b/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