diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index b4bb45263..6f937a68d 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -185,6 +185,8 @@ struct BuildResult final { class SvaNfaBuilder final { SvaGraph& m_graph; // NFA graph being built + AstNodeModule* const m_modp; // Module to receive hoisted sampled-prop temps + V3UniqueNames& m_propTempNames; // Module-shared temp-var name source std::vector m_throughoutStack; // Active throughout guards (IEEE 16.9.9) bool m_inUnboundedScope = false; // Sticky: nodes created after inherit liveness @@ -284,6 +286,29 @@ class SvaNfaBuilder final { return sp; } + // Cuts AST size from O(N * sizeof(exprp)) to O(N) + O(sizeof(exprp)) by + // sharing a single `VarRef` across N check edges. Hoist also matches the + // IEEE 1800-2023 16.9.9 "single preponed-region snapshot" semantic for + // any exprp -- even an impure one would now evaluate exactly once per + // clock instead of N times. Orphan temps from failed builds are unused + // MODULETEMPs and are removed by V3Dead. + AstVar* tryHoistSampled(AstNodeExpr* exprp, FileLine* flp, int cloneCount) { + constexpr int kHoistThreshold = 2; + if (cloneCount < kHoistThreshold) return nullptr; + AstVar* const tempVarp = new AstVar{flp, VVarType::MODULETEMP, m_propTempNames.get(exprp), + m_modp->findBitDType()}; + m_modp->addStmtsp(tempVarp); + AstAssign* const assignp = new AstAssign{flp, new AstVarRef{flp, tempVarp, VAccess::WRITE}, + sampled(exprp->cloneTreePure(false))}; + m_modp->addStmtsp(new AstAlways{flp, VAlwaysKwd::ALWAYS_COMB, nullptr, assignp}); + return tempVarp; + } + + static AstNodeExpr* sampledRefOrClone(AstVar* hoistVarp, AstNodeExpr* exprp, FileLine* flp) { + if (hoistVarp) return new AstVarRef{flp, hoistVarp, VAccess::READ}; + return sampled(exprp->cloneTreePure(false)); + } + // Create vertex and inherit throughout guards from current scope (IEEE 16.9.9). SvaStateVertex* scopedCreateVertex() { SvaStateVertex* const vtxp = m_graph.createStateVertex(); @@ -388,11 +413,12 @@ class SvaNfaBuilder final { } else { // Pure boolean RHS: register chain. Each mid-position links to // match (match-only); last position is the reject source. + AstVar* const hoistVarp = tryHoistSampled(rhsExprp, flp, range); midSources.push_back(currentp); for (int i = 0; i < range; ++i) { SvaStateVertex* const nextVtxp = scopedCreateVertex(); AstNodeExpr* const notExprp - = new AstNot{flp, sampled(rhsExprp->cloneTreePure(false))}; + = new AstNot{flp, sampledRefOrClone(hoistVarp, rhsExprp, flp)}; guardedEdge(currentp, nextVtxp, notExprp, flp); if (i < range - 1) midSources.push_back(nextVtxp); currentp = nextVtxp; @@ -474,6 +500,16 @@ class SvaNfaBuilder final { } // LCOV_EXCL_STOP + // Sum sites across prefix + unbounded/range tail so one hoist covers + // every check edge of this repetition. + int totalSites = minN; + if (repp->unbounded()) { + totalSites += 1; + } else if (repp->maxCountp()) { + totalSites += getConstInt(repp->maxCountp()) - minN; + } + AstVar* const hoistVarp = tryHoistSampled(exprp, flp, totalSites); + SvaStateVertex* currentp = entryVtxp; for (int i = 0; i < minN; ++i) { if (i > 0) { @@ -485,7 +521,7 @@ class SvaNfaBuilder final { // reject on standalone ConsRep. SvaStateVertex* const condVtxp = scopedCreateVertex(); SvaTransEdge* const linkp - = guardedLink(currentp, condVtxp, sampled(exprp->cloneTreePure(false)), flp); + = guardedLink(currentp, condVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp); if (isTopLevelStep && (i == 0 || i == minN - 1)) { linkp->m_rejectOnFail = true; } currentp = condVtxp; } @@ -495,7 +531,7 @@ class SvaNfaBuilder final { SvaStateVertex* const waitVtxp = scopedCreateVertex(); guardedEdge(currentp, waitVtxp, flp); SvaStateVertex* const checkVtxp = scopedCreateVertex(); - guardedLink(waitVtxp, checkVtxp, sampled(exprp->cloneTreePure(false)), flp); + guardedLink(waitVtxp, checkVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp); guardedEdge(checkVtxp, waitVtxp, flp); guardedLink(currentp, checkVtxp, flp); currentp = checkVtxp; @@ -503,7 +539,8 @@ class SvaNfaBuilder final { SvaStateVertex* const loopBackVtxp = scopedCreateVertex(); guardedEdge(currentp, loopBackVtxp, flp); SvaStateVertex* const reCheckVtxp = scopedCreateVertex(); - guardedLink(loopBackVtxp, reCheckVtxp, sampled(exprp->cloneTreePure(false)), flp); + guardedLink(loopBackVtxp, reCheckVtxp, sampledRefOrClone(hoistVarp, exprp, flp), + flp); guardedEdge(reCheckVtxp, loopBackVtxp, flp); guardedLink(reCheckVtxp, currentp, flp); } @@ -518,7 +555,7 @@ class SvaNfaBuilder final { SvaStateVertex* const nextVtxp = scopedCreateVertex(); guardedEdge(currentp, nextVtxp, flp); SvaStateVertex* const checkVtxp = scopedCreateVertex(); - guardedLink(nextVtxp, checkVtxp, sampled(exprp->cloneTreePure(false)), flp); + guardedLink(nextVtxp, checkVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp); guardedLink(checkVtxp, mergeVtxp, flp); currentp = checkVtxp; } @@ -536,6 +573,7 @@ class SvaNfaBuilder final { const int lo = getConstInt(nodep->loBoundp()); const int hi = getConstInt(nodep->hiBoundp()); UASSERT_OBJ(lo >= 0 && hi >= lo, nodep, "PropAlways bounds invariant (V3Width)"); + AstVar* const hoistVarp = tryHoistSampled(propp, flp, hi - lo + 1); SvaStateVertex* currentp = addDelayChain(entryVtxp, lo, flp); for (int k = 0; k <= hi - lo; ++k) { if (k > 0) { @@ -545,7 +583,7 @@ class SvaNfaBuilder final { } SvaStateVertex* const checkp = scopedCreateVertex(); SvaTransEdge* const linkp - = guardedLink(currentp, checkp, sampled(propp->cloneTreePure(false)), flp); + = guardedLink(currentp, checkp, sampledRefOrClone(hoistVarp, propp, flp), flp); if (isTopLevelStep && !m_inUnboundedScope) linkp->m_rejectOnFail = true; currentp = checkp; } @@ -558,6 +596,10 @@ class SvaNfaBuilder final { const int n = getConstInt(repp->countp()); if (n <= 0) return BuildResult::fail(); + // Wait + match per iter -> 2n sites. NOT($sampled(x)) matches + // $sampled(NOT(x)) at the value level (IEEE 1800-2023 16.9.9); + // purity is enforced uniformly via cloneTreePure inside sampledRefOrClone. + AstVar* const hoistVarp = tryHoistSampled(exprp, flp, 2 * n); SvaStateVertex* currentp = entryVtxp; for (int i = 0; i < n; ++i) { SvaStateVertex* const waitVtxp = scopedCreateVertex(); @@ -565,10 +607,11 @@ class SvaNfaBuilder final { // match. A Link at i==0 was wrong -- it allowed same-cycle matching // and was discarded by Phase 2 (waitNode has a self-loop Edge). guardedEdge(currentp, waitVtxp, flp); - AstNodeExpr* const notExprp = new AstNot{flp, exprp->cloneTreePure(false)}; - guardedEdge(waitVtxp, waitVtxp, sampled(notExprp), flp); + AstNodeExpr* const waitCondp + = new AstNot{flp, sampledRefOrClone(hoistVarp, exprp, flp)}; + guardedEdge(waitVtxp, waitVtxp, waitCondp, flp); SvaStateVertex* const matchVtxp = scopedCreateVertex(); - guardedLink(waitVtxp, matchVtxp, sampled(exprp->cloneTreePure(false)), flp); + guardedLink(waitVtxp, matchVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp); currentp = matchVtxp; } currentp->m_isUnbounded = true; // [->N] waits unboundedly @@ -741,8 +784,10 @@ class SvaNfaBuilder final { } public: - explicit SvaNfaBuilder(SvaGraph& graph) - : m_graph{graph} {} + SvaNfaBuilder(SvaGraph& graph, AstNodeModule* modp, V3UniqueNames& propTempNames) + : m_graph{graph} + , m_modp{modp} + , m_propTempNames{propTempNames} {} // Reset scope between antecedent and consequent: liveness must not leak. void resetScope() { @@ -1472,6 +1517,7 @@ class AssertNfaVisitor final : public VNVisitor { SvaNfaLowering* m_loweringp = nullptr; // NFA-to-hardware lowering engine V3UniqueNames m_propVarNames{"__Vpropvar"}; // Property-local variable names V3UniqueNames m_disableCntNames{"__VnfaDis"}; // Disable-iff counter names + V3UniqueNames m_propTempNames{"__VnfaSampled"}; // Hoisted $sampled(propp) temps std::set m_inliningProps; // Recursion guard for inlineNamedProperty // Wire match vertex and mid-window sources for a successful NFA build. @@ -1836,13 +1882,15 @@ class AssertNfaVisitor final : public VNVisitor { const bool isCover = VN_IS(assertp, Cover); SvaGraph graph; - SvaNfaBuilder builder{graph}; + SvaNfaBuilder builder{graph, m_modp, m_propTempNames}; const BuildResult result = buildAssertionGraph(builder, graph, seqBodyp, parts, flp); if (result.valid()) wireMatchAndMidSources(graph, result, flp); if (!result.valid()) { // Fall through to V3AssertPre for unsupported constructs; only - // replace the body on real semantic errors. + // replace the body on real semantic errors. Any hoisted temps + // from this attempt become orphan MODULETEMPs; V3Dead removes + // them along with the dead always_comb driver. replaceBodyOnBuildError(flp, propSpecp, result.errorEmitted); if (senTreeOwned) VL_DO_DANGLING(pushDeletep(senTreep), senTreep); return; diff --git a/test_regress/t/t_prop_always_wide.py b/test_regress/t/t_prop_always_wide.py new file mode 100755 index 000000000..2351d6963 --- /dev/null +++ b/test_regress/t/t_prop_always_wide.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('vlt') + +test.compile() + +test.execute() + +test.passes() diff --git a/test_regress/t/t_prop_always_wide.v b/test_regress/t/t_prop_always_wide.v new file mode 100644 index 000000000..a0e297293 --- /dev/null +++ b/test_regress/t/t_prop_always_wide.v @@ -0,0 +1,44 @@ +// 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 + +module t ( + input clk +); + + int cyc = 0; + logic a_high = 1'b1, b_high = 1'b1, c_high = 1'b1; + int wide_pass_q[$], wide_strong_pass_q[$]; + + // Wide range with multi-operand pure propp -- exercises the shared + // $sampled(propp) hoist path; pre-fix would clone propp 33 times. + assert property (@(posedge clk) always[1: 33] (a_high && b_high && c_high)) + wide_pass_q.push_back(cyc); + + // Wide strong s_always over the same expression (in-window matches weak). + assert property (@(posedge clk) s_always[1: 33] (a_high && b_high && c_high)) + wide_strong_pass_q.push_back(cyc); + + always @(posedge clk) begin + cyc <= cyc + 1; + if (cyc == 49) begin + // Constant-true [1:33]: K=0..16 succeed at cyc K+33 = 33..49. + `checkd(wide_pass_q.size(), 17); + `checkd(wide_pass_q[0], 33); + `checkd(wide_pass_q[$], 49); + `checkd(wide_strong_pass_q.size(), 17); + `checkd(wide_strong_pass_q[0], 33); + `checkd(wide_strong_pass_q[$], 49); + $write("*-* All Finished *-*\n"); + $finish; + end + end + +endmodule