diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index f235e56b8..05375f41e 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -33,6 +33,7 @@ #include "V3Assert.h" #include "V3Const.h" #include "V3Graph.h" +#include "V3Stats.h" #include "V3Task.h" #include "V3UniqueNames.h" @@ -1706,6 +1707,7 @@ class SvaNfaLowering final { AstNodeModule* const m_modp; // Module to add state vars and always blocks to AstNodeDType* const m_u32DTypep; // Shared unsigned counter dtype V3UniqueNames m_names{"__Vnfa"}; + size_t m_statDelayRingEdgeVisits = 0; // Delay-ring incoming edges visited // Per-lowering shared context (passed to phase sub-functions) // Per-vertex lowering state is stored in SvaVertexData and accessed via @@ -1883,15 +1885,16 @@ class SvaNfaLowering final { const uint32_t size = static_cast(vtxp->m_delayRingSize); AstNodeExpr* incomingp = nullptr; - for (const SvaTransEdge* const tedgep : c.edges) { - if (static_cast(tedgep->toVtxp()->color()) != ri) continue; - UASSERT_OBJ(tedgep->m_consumesCycle == vtxp->m_isFixedDelayRing, vtxp, + for (const V3GraphEdge& edger : vtxp->inEdges()) { + ++m_statDelayRingEdgeVisits; + const SvaTransEdge& tedger = static_cast(edger); + UASSERT_OBJ(tedger.m_consumesCycle == vtxp->m_isFixedDelayRing, vtxp, "Delay-ring incoming edge kind mismatch"); - const int fi = tedgep->fromVtxp()->color(); + const int fi = tedger.fromVtxp()->color(); UASSERT_OBJ(c.vtx[fi]->datap()->stateSigp, c.vtx[fi], "Delay-ring incoming source missing stateSig"); AstNodeExpr* contribp = c.vtx[fi]->datap()->stateSigp->cloneTreePure(false); - contribp = andCond(c.flp, contribp, tedgep->m_condp); + contribp = andCond(c.flp, contribp, tedger.m_condp); if (c.disableExprp) { AstNodeExpr* const notDisp = new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)}; @@ -2409,6 +2412,9 @@ public: explicit SvaNfaLowering(AstNodeModule* modp) : m_modp{modp} , m_u32DTypep{modp->findBasicDType(VBasicDTypeKwd::UINT32)} {} + ~SvaNfaLowering() { + V3Stats::addStatSum("Assertions, NFA delay ring edge visits", m_statDelayRingEdgeVisits); + } // Lower NFA graph to synthesizable AstAlways blocks and raw result signals. // Links are combinational; Edges are registered (NBA). diff --git a/test_regress/t/t_property_nfa_edge_perf.py b/test_regress/t/t_property_nfa_edge_perf.py new file mode 100755 index 000000000..4387d6b04 --- /dev/null +++ b/test_regress/t/t_property_nfa_edge_perf.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.lint(verilator_flags2=['--stats']) + +test.file_grep(test.stats, r'Assertions, NFA delay ring edge visits\s+(\d+)', 15) + +test.passes() diff --git a/test_regress/t/t_property_nfa_edge_perf.v b/test_regress/t/t_property_nfa_edge_perf.v new file mode 100644 index 000000000..e17d8c433 --- /dev/null +++ b/test_regress/t/t_property_nfa_edge_perf.v @@ -0,0 +1,18 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 Antmicro +// SPDX-License-Identifier: CC0-1.0 + +`define S0 a +`define S1 (`S0 ##2 `S0) +`define S2 (`S1 ##2 `S1) +`define S3 (`S2 ##2 `S2) +`define S4 (`S3 ##2 `S3) + +module t ( + input clk, + input a +); + assert property (@(posedge clk) `S4); +endmodule