From 021c8be67c184c1a9c30ffdbd793604759199d82 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Fri, 3 Jul 2026 22:09:47 +0200 Subject: [PATCH] Complete mid-window disable across counter-FSM and and-combiner, pack b[*N] and chunk over-64-bit shift chains --- src/V3AssertNfa.cpp | 261 ++++++++++-------- .../t/t_property_disable_iff_counter.py | 18 ++ .../t/t_property_disable_iff_counter.v | 48 ++++ test_regress/t/t_property_shift_chunk.py | 18 ++ test_regress/t/t_property_shift_chunk.v | 39 +++ 5 files changed, 265 insertions(+), 119 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_shift_chunk.py create mode 100644 test_regress/t/t_property_shift_chunk.v diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index c0019ea34..610d28a90 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -1656,6 +1656,131 @@ class SvaNfaLowering final { AstNodeExpr* throughoutRejectp = nullptr; // Reject when a throughout guard drops }; + // Pack ##N delay and uniform b[*N] repetition sub-chains into packed shift + // vectors: a maximal simple path of registered vertices whose state is the + // previous vertex shifted one position (optionally gated by a shared per-step + // condition) lowers to one vector shifted once per clock instead of L separate + // 1-bit registers with L shift assignments (igorosky, verilator/verilator#7792). + // Sets shiftVecp/shiftBit/shiftStepCondp on each packed vertex; uniform + // disable/kill gating is applied later by masking the whole vector. + void detectShiftChains(const std::vector& vtx, int N, int startIdx, + const std::string& baseName, FileLine* flp) { + 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; + }; + // Chain predecessor of a registered vertex, plus the per-step condition on + // the transition into it (null = unconditional). Two lowered shapes count + // as a shift step: a direct clocked edge (##N delay), and a clocked edge + // fed through one pass-through condition Link vertex -- the shape of + // consecutive repetition `b[*N]`, whose ##1 edge is unconditional and + // whose boolean sits on a combinational Link. The Link boolean becomes the + // step condition, folded into the shift mask. + const auto chainPred = [&](int ci, AstNodeExpr*& condpr) -> int { + condpr = nullptr; + const SvaTransEdge* const e = singleClockedInEdge(vtx[ci]); + if (!e || e->m_rejectOnFail || e->m_condVtxp) return -1; + const int mi = e->fromVtxp()->color(); + if (shiftable(mi)) { // direct clocked step + condpr = e->m_condp; + return mi; + } + if (e->m_condp) return -1; // pass-through requires an unconditional ##1 edge + SvaStateVertex* const m = vtx[mi]; + const SvaTransEdge* linkp = nullptr; + for (const V3GraphEdge& er : m->inEdges()) { + if (linkp) return -1; // more than one input -> not a clean pass-through + linkp = static_cast(&er); + } + if (!linkp || linkp->m_consumesCycle || linkp->m_rejectOnFail || linkp->m_condVtxp) + return -1; + const int pi = linkp->fromVtxp()->color(); + if (!shiftable(pi)) return -1; + condpr = linkp->m_condp; + return pi; + }; + const auto sameCond = [](const AstNodeExpr* a, const AstNodeExpr* b) -> bool { + if (!a && !b) return true; + if (!a || !b) return false; + return a->sameTree(b); + }; + // Bond each vertex to its chain predecessor; a predecessor feeding more + // than one chain vertex branches and cannot shift unambiguously. + struct Bond final { + int pred = -1; + AstNodeExpr* stepCondp = nullptr; // borrowed step condition into this vertex + }; + std::vector bond(N); + std::vector childCount(N, 0); + for (int i = 0; i < N; ++i) { + if (!shiftable(i)) continue; + AstNodeExpr* cp = nullptr; + const int p = chainPred(i, cp); + if (p < 0) continue; + bond[i] = {p, cp}; + ++childCount[p]; + } + std::vector nextInChain(N, -1); + std::vector hasPrevInChain(N, false); + for (int i = 0; i < N; ++i) { + const int p = bond[i].pred; + if (p < 0 || childCount[p] != 1) continue; + nextInChain[p] = i; + hasPrevInChain[i] = true; + } + // Walk each chain head, splitting into maximal segments whose interior + // steps share one condition (`##N` = all null, `b[*N]` = all `b`); each + // segment of >= 2 vertices collapses to one packed vector. Segments are + // also capped at 64 bits: V3AssertNfa runs after V3Width, and emitting a + // wider (VlWide) shift here trips V3Subst ("Non AstNodeExpr under + // AstNodeExpr"), which expects wide ops to have been word-split earlier -- + // an upstream limitation this cap works around. A capped chain simply + // continues in the next vector, whose bit 0 injects the previous + // segment's top bit through the shared clocked predecessor. + constexpr int kMaxShiftVec = 64; + for (int h = 0; h < N; ++h) { + if (hasPrevInChain[h] || nextInChain[h] == -1) continue; + std::vector chain; + for (int j = h; j != -1; j = nextInChain[j]) chain.push_back(j); + int a = 0; + while (a + 1 < static_cast(chain.size())) { + AstNodeExpr* const segCondp = bond[chain[a + 1]].stepCondp; + int b = a + 1; + while (b + 1 < static_cast(chain.size()) + && sameCond(bond[chain[b + 1]].stepCondp, segCondp) + && (b - a + 1) < kMaxShiftVec) + ++b; + AstVar* const vecp = new AstVar{ + flp, VVarType::MODULETEMP, baseName + "__v" + std::to_string(chain[a]), + m_modp->findBitDType(b - a + 1, b - a + 1, VSigning::UNSIGNED)}; + vecp->lifetime(VLifetime::STATIC_EXPLICIT); + m_modp->addStmtsp(vecp); + for (int k = a; k <= b; ++k) { + vtx[chain[k]]->datap()->shiftVecp = vecp; + vtx[chain[k]]->datap()->shiftBit = k - a; + } + vtx[chain[a]]->datap()->shiftStepCondp = segCondp; // borrowed + a = b + 1; // next segment starts at the condition-change vertex + } + } + } + // Phase 2/2b/2c: Emit NBA state-update always blocks for registered vertices, // counter FSMs, and SAnd combiner done-latches. // Phase 2: State register NBA always block. Each clocked-edge target @@ -1719,6 +1844,7 @@ class SvaNfaLowering final { const int fromIdx = te.fromVtxp()->color(); UASSERT_OBJ(c.vtx[fromIdx]->datap()->stateSigp, te.fromVtxp(), "Shift-chain head feeder missing stateSig"); + UASSERT_OBJ(!injectp, c.vtx[i], "Shift-chain head has >1 clocked feeder"); injectp = andCond(c.flp, c.vtx[fromIdx]->datap()->stateSigp->cloneTreePure(false), te.m_condp); } @@ -1727,6 +1853,7 @@ class SvaNfaLowering final { = new AstShiftL{c.flp, new AstVarRef{c.flp, vecp, VAccess::READ}, new AstConst{c.flp, AstConst::WidthedValue{}, 32, 1u}, width}; if (AstNodeExpr* const stepp = c.vtx[i]->datap()->shiftStepCondp) { + UASSERT_OBJ(stepp->width() == 1, c.vtx[i], "Shift step condition must be 1-bit"); shiftedp = new AstAnd{c.flp, shiftedp, new AstReplicate{c.flp, stepp->cloneTreePure(false), static_cast(width)}}; @@ -1808,8 +1935,13 @@ class SvaNfaLowering final { = new AstEq{c.flp, new AstVarRef{c.flp, cntp, VAccess::READ}, new AstConst{c.flp, AstConst::WidthedValue{}, 32, counterMax}}; - AstNodeExpr* const donep = new AstLogOr{ - c.flp, killActive(c), new AstLogOr{c.flp, matchedNowp, counterAtEndp}}; + AstNodeExpr* donep = new AstLogOr{c.flp, killActive(c), + new AstLogOr{c.flp, matchedNowp, counterAtEndp}}; + // A mid-window disable aborts the in-flight count, as the state + // register and shift vector already zero their state (IEEE 1800-2023 + // 16.12, level-based); the expiry reject is separately disable-gated. + if (c.disableExprp) + donep = new AstLogOr{c.flp, donep, c.disableExprp->cloneTreePure(false)}; AstAssignDly* const clearActivep = new AstAssignDly{c.flp, new AstVarRef{c.flp, activep, VAccess::WRITE}, @@ -1889,8 +2021,14 @@ class SvaNfaLowering final { AstIf* const setRIfp = new AstIf{c.flp, gateRp, setRp, nullptr}; setLIfp->addNext(setRIfp); - AstNodeExpr* const clearCondp = new AstLogOr{ + AstNodeExpr* clearCondp = new AstLogOr{ c.flp, killActive(c), c.vtx[ai]->datap()->stateSigp->cloneTreePure(false)}; + // A mid-window disable clears a half-latched and-combiner side so a + // disabled attempt's progress cannot pair with a later attempt's + // completion, keeping the latches consistent with the state-register + // and shift-vector zeroing (IEEE 1800-2023 16.12). + if (c.disableExprp) + clearCondp = new AstLogOr{c.flp, clearCondp, c.disableExprp->cloneTreePure(false)}; AstIf* const topp = new AstIf{c.flp, clearCondp, clearLp, setLIfp}; m_modp->addStmtsp( new AstAlways{c.flp, VAlwaysKwd::ALWAYS, c.senTreep->cloneTree(false), topp}); @@ -2289,122 +2427,7 @@ 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; - }; - // Chain predecessor of a registered vertex, plus the per-step condition on - // the transition into it (null = unconditional). Two lowered shapes count - // as a shift step: a direct clocked edge (##N delay), and a clocked edge - // fed through one pass-through condition Link vertex -- the shape of - // consecutive repetition `b[*N]`, whose ##1 edge is unconditional and - // whose boolean sits on a combinational Link. The Link boolean becomes the - // step condition, folded into the shift mask. - const auto chainPred = [&](int ci, AstNodeExpr*& condpr) -> int { - condpr = nullptr; - const SvaTransEdge* const e = singleClockedInEdge(vtx[ci]); - if (!e || e->m_rejectOnFail || e->m_condVtxp) return -1; - const int mi = e->fromVtxp()->color(); - if (shiftable(mi)) { // direct clocked step - condpr = e->m_condp; - return mi; - } - if (e->m_condp) return -1; // pass-through requires an unconditional ##1 edge - SvaStateVertex* const m = vtx[mi]; - const SvaTransEdge* linkp = nullptr; - for (const V3GraphEdge& er : m->inEdges()) { - if (linkp) return -1; // more than one input -> not a clean pass-through - linkp = static_cast(&er); - } - if (!linkp || linkp->m_consumesCycle || linkp->m_rejectOnFail || linkp->m_condVtxp) - return -1; - const int pi = linkp->fromVtxp()->color(); - if (!shiftable(pi)) return -1; - condpr = linkp->m_condp; - return pi; - }; - const auto sameCond = [](const AstNodeExpr* a, const AstNodeExpr* b) -> bool { - if (!a && !b) return true; - if (!a || !b) return false; - return a->sameTree(b); - }; - // Bond each vertex to its chain predecessor; a predecessor feeding more - // than one chain vertex branches and cannot shift unambiguously. - std::vector predOf(N, -1); - std::vector stepCondp(N, nullptr); // borrowed; step into vtx[i] - std::vector childCount(N, 0); - for (int i = 0; i < N; ++i) { - if (!shiftable(i)) continue; - AstNodeExpr* cp = nullptr; - const int p = chainPred(i, cp); - if (p < 0) continue; - predOf[i] = p; - stepCondp[i] = cp; - ++childCount[p]; - } - std::vector nextInChain(N, -1); - std::vector hasPrevInChain(N, false); - for (int i = 0; i < N; ++i) { - const int p = predOf[i]; - if (p < 0 || childCount[p] != 1) continue; - nextInChain[p] = i; - hasPrevInChain[i] = true; - } - // Walk each chain head, splitting into maximal segments whose interior - // steps share one condition (`##N` = all null, `b[*N]` = all `b`); each - // segment of >= 2 vertices collapses to one packed vector. Segments are - // also capped at 64 bits: V3AssertNfa runs after V3Width, and wider - // (VlWide) arithmetic emitted this late is not lowered by later passes. - // A capped chain simply continues in the next vector, whose bit 0 injects - // the previous segment's top bit through the shared clocked predecessor. - constexpr int kMaxShiftVec = 64; - for (int h = 0; h < N; ++h) { - if (hasPrevInChain[h] || nextInChain[h] == -1) continue; - std::vector chain; - for (int j = h; j != -1; j = nextInChain[j]) chain.push_back(j); - int a = 0; - while (a + 1 < static_cast(chain.size())) { - AstNodeExpr* const segCondp = stepCondp[chain[a + 1]]; - int b = a + 1; - while (b + 1 < static_cast(chain.size()) - && sameCond(stepCondp[chain[b + 1]], segCondp) - && (b - a + 1) < kMaxShiftVec) - ++b; - AstVar* const vecp = new AstVar{ - flp, VVarType::MODULETEMP, baseName + "__v" + std::to_string(chain[a]), - m_modp->findBitDType(b - a + 1, b - a + 1, VSigning::UNSIGNED)}; - vecp->lifetime(VLifetime::STATIC_EXPLICIT); - m_modp->addStmtsp(vecp); - for (int k = a; k <= b; ++k) { - vtx[chain[k]]->datap()->shiftVecp = vecp; - vtx[chain[k]]->datap()->shiftBit = k - a; - } - vtx[chain[a]]->datap()->shiftStepCondp = segCondp; // borrowed - a = b + 1; // next segment starts at the condition-change vertex - } - } + detectShiftChains(vtx, N, startIdx, baseName, flp); AstNodeDType* const u32DTypep = m_modp->findBasicDType(VBasicDTypeKwd::UINT32); AstVar* const killVarp 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..35e44000c --- /dev/null +++ b/test_regress/t/t_property_disable_iff_counter.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_counter.v b/test_regress/t/t_property_disable_iff_counter.v new file mode 100644 index 000000000..230f4b226 --- /dev/null +++ b/test_regress/t/t_property_disable_iff_counter.v @@ -0,0 +1,48 @@ +// 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 true at ANY point of a multi-cycle +// attempt window disables it. A range delay ##[1:N] with N over the 256 unroll +// limit lowers to a counter-FSM backend (not a state-register chain), which had +// the same mid-window-disable hole as the register path +// (verilator/verilator#7792 follow-up). value never matches, so a live attempt +// fails at window end; skip pulses once mid-window and must abort the in-flight +// counter so the disabled assert does not fire. + +module t ( + input clk +); + int cyc = 0; + wire trig = (cyc == 5); + wire value = 1'b0; // never matches -> attempt would fail at window end + wire skip = (cyc == 50); // single mid-window pulse + + int n_dis_fire = 0; + int n_ctrl_fire = 0; + + // Range > 256 -> counter FSM. The cyc-5 attempt is hit by the skip pulse. + assert property (@(posedge clk) disable iff (skip) trig |-> ##[1:300] value) + else n_dis_fire <= n_dis_fire + 1; + + // Control: same property never disabled -> the cyc-5 attempt fails once. + assert property (@(posedge clk) disable iff (1'b0) trig |-> ##[1:300] value) + else n_ctrl_fire <= n_ctrl_fire + 1; + + always @(posedge clk) begin + cyc <= cyc + 1; + if (cyc == 320) 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_property_shift_chunk.py b/test_regress/t/t_property_shift_chunk.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/test_regress/t/t_property_shift_chunk.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_shift_chunk.v b/test_regress/t/t_property_shift_chunk.v new file mode 100644 index 000000000..6a90526c1 --- /dev/null +++ b/test_regress/t/t_property_shift_chunk.v @@ -0,0 +1,39 @@ +// 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 + +// A ##130 delay is a 129-vertex shift chain packed across three <=64-bit +// vectors (verilator/verilator#7792 optimization). This exercises the +// cross-chunk carry: each next vector's bit 0 injects the previous vector's top +// bit through the shared clocked predecessor. res is high only exactly 130 +// cycles after the single antecedent match, so an off-by-one or dropped carry +// makes the consequent miss and the assert fire. + +module t ( + input clk +); + int cyc = 0; + wire trig = (cyc == 5); + wire res = (cyc == 5 + 130); + + int n_fire = 0; + + assert property (@(posedge clk) trig |-> ##130 res) + else n_fire <= n_fire + 1; + + always @(posedge clk) begin + cyc <= cyc + 1; + if (cyc == 160) begin + `checkd(n_fire, 0); + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule