luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Internals: V3AssertNfa: hoist sampled(propp) into a per-property temp (#7502) (#7525) 

Fixes #7502.
This commit is contained in:
Yilou Wang 2026-05-02 18:13:58 +02:00 committed by GitHub
parent 659274e45d
commit 8011f9a796
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
3 changed files with 123 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

74
src/V3AssertNfa.cpp
View File

@ -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<AstNodeExpr*> 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<const AstProperty*> 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;

18
test_regress/t/t_prop_always_wide.py Executable file
View File

@ -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()

44
test_regress/t/t_prop_always_wide.v Normal file
View File

@ -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