diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 6a35273a5..ee6569873 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -54,6 +54,10 @@ struct SvaVertexData final { AstVar* doneRVarp = nullptr; // SAnd RHS done-latch AstNodeExpr* stateSigp = nullptr; // Combinational state signal (owned during lowering) bool needsReg = false; // True if vertex has incoming clocked edge + // Pure ##N delay chains collapse to one packed vector shifted once per clock + // instead of one 1-bit register per position (verilator/verilator#7792). + AstVar* shiftVecp = nullptr; // Shared packed shift vector, or null for a standalone reg + int shiftBit = -1; // Bit index within shiftVecp (0 = chain entry) }; // NFA state vertex -- one per NFA position in the sequence evaluation @@ -1669,7 +1673,10 @@ 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) { + // Zero in-flight state on an active disable in both modes; the + // edge counter misses a held or mid-window disable (IEEE + // 1800-2023 16.12, level-based). + if (c.disableExprp) { AstNodeExpr* const notDisp = new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)}; srcSigp = new AstLogAnd{c.flp, srcSigp, notDisp}; @@ -1691,6 +1698,47 @@ class SvaNfaLowering final { } } + // Pure ##N delay chains: one masked shift per vector. + // vec <= ((vec << 1) | inject) & {W{!disable & !kill}} + // bit 0 injects the head's feeder contribution; interior bits shift up. + // The per-bit mask reproduces the same disable/kill gating the standalone + // registers get, so mid-window disable zeroing is preserved. + for (int i = 0; i < c.N; ++i) { + if (!c.vtx[i]->datap()->shiftVecp || c.vtx[i]->datap()->shiftBit != 0) continue; + AstVar* const vecp = c.vtx[i]->datap()->shiftVecp; + const int width = vecp->width(); + AstNodeExpr* injectp = nullptr; + for (const V3GraphEdge& er : c.vtx[i]->inEdges()) { + const SvaTransEdge& te = static_cast(er); + if (!te.m_consumesCycle) continue; + const int fromIdx = te.fromVtxp()->color(); + UASSERT_OBJ(c.vtx[fromIdx]->datap()->stateSigp, te.fromVtxp(), + "Shift-chain head feeder missing stateSig"); + injectp = andCond(c.flp, c.vtx[fromIdx]->datap()->stateSigp->cloneTreePure(false), + te.m_condp); + } + UASSERT_OBJ(injectp, c.vtx[i], "Shift-chain head has no clocked feeder"); + AstNodeExpr* const shiftedp + = new AstShiftL{c.flp, new AstVarRef{c.flp, vecp, VAccess::READ}, + new AstConst{c.flp, AstConst::WidthedValue{}, 32, 1u}, width}; + AstNodeExpr* const nextp + = new AstOr{c.flp, shiftedp, new AstExtend{c.flp, injectp, width}}; + AstNodeExpr* gatep = notKillActive(c); + if (c.disableExprp) { + gatep = new AstLogAnd{ + c.flp, new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)}, gatep}; + } + AstNodeExpr* const maskedp = new AstAnd{ + c.flp, nextp, new AstReplicate{c.flp, gatep, static_cast(width)}}; + AstAssignDly* const assignp + = new AstAssignDly{c.flp, new AstVarRef{c.flp, vecp, VAccess::WRITE}, maskedp}; + if (!bodyp) { + bodyp = assignp; + } else { + bodyp->addNext(assignp); + } + } + if (!bodyp) return; // Capture disableCnt in Phase-2 NBA before any reactive re-evaluation. // snapshotVarp and disableCntVarp are allocated together. @@ -2024,7 +2072,11 @@ class SvaNfaLowering final { // datap() was freshly allocated in lower() -- all stateSigp start null. c.vtx[c.startIdx]->datap()->stateSigp = triggerExprp->cloneTreePure(false); for (int i = 0; i < c.N; ++i) { - if (c.vtx[i]->datap()->stateVarp) { + if (c.vtx[i]->datap()->shiftVecp) { + c.vtx[i]->datap()->stateSigp = new AstSel{ + c.flp, new AstVarRef{c.flp, c.vtx[i]->datap()->shiftVecp, VAccess::READ}, + c.vtx[i]->datap()->shiftBit, 1}; + } else if (c.vtx[i]->datap()->stateVarp) { c.vtx[i]->datap()->stateSigp = new AstVarRef{c.flp, c.vtx[i]->datap()->stateVarp, VAccess::READ}; } else if (c.vtx[i]->datap()->counterActiveVarp) { @@ -2227,6 +2279,67 @@ public: } } + // Pure ##N delay sub-chains: a maximal simple path of registered vertices + // whose state is a plain 1-cycle copy of a single predecessor. Each such + // chain lowers to one packed vector shifted once per clock instead of L + // separate 1-bit registers with L shift assignments (igorosky, + // verilator/verilator#7792). Uniform disable/kill gating is preserved by + // masking the whole vector, so the mid-window disable fix is unaffected. + const auto singleClockedInEdge = [](SvaStateVertex* v) -> const SvaTransEdge* { + const SvaTransEdge* inp = nullptr; + for (const V3GraphEdge& er : v->inEdges()) { + const SvaTransEdge& te = static_cast(er); + if (!te.m_consumesCycle) return nullptr; // an incoming Link disqualifies + if (inp) return nullptr; // more than one clocked source -> OR-merge + inp = &te; + } + return inp; + }; + const auto shiftable = [&](int i) -> bool { + SvaStateVertex* const v = vtx[i]; + if (!v->datap()->needsReg) return false; + if (i == startIdx || v->m_isMatch) return false; + if (v->m_isCounter || v->m_isAndCombiner || v->m_isRejectSink) return false; + if (v->m_isUnbounded) return false; // self-loop accumulator, not a pure shift + if (v->m_strongPending) return false; // final-block liveness reads its own reg + if (!v->m_throughoutConds.empty()) return false; + return singleClockedInEdge(v) != nullptr; + }; + const auto outClockedCount = [](SvaStateVertex* v) -> int { + int n = 0; + for (const V3GraphEdge& er : v->outEdges()) + if (static_cast(er).m_consumesCycle) ++n; + return n; + }; + std::vector nextInChain(N, -1); + std::vector hasPrevInChain(N, false); + for (int i = 0; i < N; ++i) { + if (!shiftable(i)) continue; + const SvaTransEdge* const inp = singleClockedInEdge(vtx[i]); + // A conditional/reject in-edge keeps its own inject; such a vertex can + // still be a chain head, never a shifted interior bit. + if (inp->m_condp || inp->m_rejectOnFail || inp->m_condVtxp) continue; + const int p = inp->fromVtxp()->color(); + if (!shiftable(p) || outClockedCount(vtx[p]) != 1) continue; // p branches + nextInChain[p] = i; + hasPrevInChain[i] = true; + } + for (int i = 0; i < N; ++i) { + if (hasPrevInChain[i] || nextInChain[i] == -1) continue; // head of a >=2 chain only + int len = 0; + for (int j = i; j != -1; j = nextInChain[j]) ++len; + AstVar* const vecp + = new AstVar{flp, VVarType::MODULETEMP, baseName + "__v" + std::to_string(i), + m_modp->findBitDType(len, len, VSigning::UNSIGNED)}; + vecp->lifetime(VLifetime::STATIC_EXPLICIT); + m_modp->addStmtsp(vecp); + int bit = 0; + for (int j = i; j != -1; j = nextInChain[j], ++bit) { + vtx[j]->datap()->shiftVecp = vecp; + vtx[j]->datap()->shiftBit = bit; + } + } + AstNodeDType* const u32DTypep = m_modp->findBasicDType(VBasicDTypeKwd::UINT32); AstVar* const killVarp = new AstVar{flp, VVarType::MODULETEMP, baseName + "__kill", u32DTypep}; @@ -2263,6 +2376,7 @@ public: } if (!vtx[i]->datap()->needsReg) continue; if (i == startIdx || vtx[i]->m_isMatch) continue; + if (vtx[i]->datap()->shiftVecp) continue; // lives in a packed shift vector const std::string varName = baseName + "__s" + std::to_string(i); AstVar* const varp = new AstVar{flp, VVarType::MODULETEMP, varName, m_modp->findBitDType()}; diff --git a/test_regress/t/t_prop_always.v b/test_regress/t/t_prop_always.v index 52cfea02c..e36927455 100644 --- a/test_regress/t/t_prop_always.v +++ b/test_regress/t/t_prop_always.v @@ -90,7 +90,11 @@ module t ( `checkd(rand_bounded_pass_q.size(), 0); `checkd(rand_bounded_fail_q.size(), 20); `checkd(disable_bounded_pass_q.size(), 0); - `checkd(disable_bounded_fail_q.size(), 13); + // Level-based disable now suppresses attempts whose [0:3] window touches + // rst_rand (not only the start cyc), dropping 13 -> 8 toward Questa. The + // residual 8 vs 6 is a disable that goes true AFTER an in-window failure + // already fired: a streaming NFA cannot retroactively un-fire it. + `checkd(disable_bounded_fail_q.size(), 8); // Questa: 6 $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..66f2bf73c --- /dev/null +++ b/test_regress/t/t_property_disable_iff_midpulse.v @@ -0,0 +1,49 @@ +// 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 true at ANY point of a +// multi-cycle attempt window disables that attempt, not only when held +// continuously (verilator/verilator#7792 follow-up to #7841). skip is a plain +// non-$sampled, non-constant signal pulsed true for a single cycle in the +// MIDDLE of the ##10 window. value is low only at the attempt's match cycle, so +// exactly one attempt would fail; the mid-window skip pulse must disable it. +// Pre-fix the in-flight NFA states were not zeroed on a mid-window pulse, so the +// disabled assert fired; the control proves the same attempt fails when enabled. + +module t ( + input clk +); + int cyc = 0; + wire value = (cyc != 10); // low only at the cyc-0 attempt's match cycle + wire skip = (cyc == 5); // single-cycle pulse, mid-window of [0..10] + + int n_dis_fire = 0; + int n_ctrl_fire = 0; + + // Mid-window-pulse disable: the cyc-0 attempt (matches at cyc 10, where value + // is low -> would fail) must be disabled by the skip pulse at cyc 5. + assert property (@(posedge clk) disable iff (skip) (##10 value)) + else n_dis_fire <= n_dis_fire + 1; + + // Control: same property always enabled -> the cyc-0 attempt fails once. + assert property (@(posedge clk) disable iff (1'b0) (##10 value)) + else n_ctrl_fire <= n_ctrl_fire + 1; + + always @(posedge clk) begin + cyc <= cyc + 1; + if (cyc == 20) begin + `checkd(n_dis_fire, 0); + `checkd(n_ctrl_fire, 1); + $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 dcffaae56..778bf6f3a 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, 25); // Questa: 20 + `checkd(count_p3, 24); // 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, 15); // Questa: 10 - `checkd(count_p10, 23); // Questa: 15 + `checkd(count_p10, 21); // Questa: 15 $write("*-* All Finished *-*\n"); $finish; end