diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 680213f18..ccbd6f74d 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -16,6 +16,7 @@ // V3AssertNfa's Transformations: // // - Convert multi-cycle SVA sequences/properties into NFA graphs. +// - Attach inherited assertion clocks before moving sampled-value functions. // - Emit module-level state registers driven by AstAlways blocks. // - Replace converted assertions with combinational match/reject checks // so V3AssertPre sees no multi-cycle SExpr (unsupported ones fall through). @@ -2411,11 +2412,20 @@ class AssertNfaVisitor final : public VNVisitor { AstClocking* m_defaultClockingp = nullptr; // Default clocking AstDefaultDisable* m_defaultDisablep = nullptr; // Default disable iff SvaNfaLowering* m_loweringp = nullptr; // NFA-to-hardware lowering engine + AstSenTree* m_sampledValueClockp = nullptr; // Inherited clock during scoped attachment 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 + template + void visitSampledValue(T_Node* const nodep) { + if (m_sampledValueClockp && !nodep->sentreep()) { + nodep->sentreep(m_sampledValueClockp->cloneTree(true)); + } + iterateChildren(nodep); + } + // Wire match vertex and mid-window sources for a successful NFA build. static void wireMatchAndMidSources(SvaGraph& graph, const BuildResult& result, FileLine* flp) { graph.createMatchVertex(); @@ -2972,6 +2982,15 @@ class AssertNfaVisitor final : public VNVisitor { AstNodeExpr* disableExprp = propSpecp->disablep(); if (!senTreep) return; + // NFA lowering clones repeated operands and may hoist them into an + // always_comb block. Resolve implicit sampled-value clocks first, while + // the enclosing assertion clock is still available. + { + VL_RESTORER(m_sampledValueClockp); + m_sampledValueClockp = senTreep; + iterate(propSpecp->propp()); + } + FileLine* const flp = assertp->fileline(); SvaGraph graph; @@ -3107,6 +3126,10 @@ class AssertNfaVisitor final : public VNVisitor { iterateChildren(nodep); } void visit(AstDefaultDisable* nodep) override {} + void visit(AstFell* nodep) override { visitSampledValue(nodep); } + void visit(AstPast* nodep) override { visitSampledValue(nodep); } + void visit(AstRose* nodep) override { visitSampledValue(nodep); } + void visit(AstStable* nodep) override { visitSampledValue(nodep); } void visit(AstAssert* nodep) override { processAssertion(nodep); } void visit(AstCover* nodep) override { processAssertion(nodep); } void visit(AstRestrict* nodep) override { diff --git a/test_regress/t/t_assert_consec_rep.v b/test_regress/t/t_assert_consec_rep.v index d5461b5e5..2daee40e8 100644 --- a/test_regress/t/t_assert_consec_rep.v +++ b/test_regress/t/t_assert_consec_rep.v @@ -91,6 +91,15 @@ module t ( assert property (@(posedge clk) a [*] ##1 b) else count_fail11 <= count_fail11 + 1; + // Parenthesized sampled-value functions followed by consecutive repetition + assert property (@(posedge clk) ($stable(1'b0)) [+]); + assert property (@(posedge clk) ($stable(a)) [+] |-> 1'b1); + assert property (@(posedge clk) ($stable(a, clk)) [+] |-> 1'b1); + assert property (@(posedge clk) ($fell(a)) [+] |-> 1'b1); + assert property (@(posedge clk) ($past(a)) [+] |-> 1'b1); + assert property (@(posedge clk) ($rose(a)) [+] |-> 1'b1); + assert property (@(posedge clk) ($changed(a)) [+] |-> 1'b1); + // Tests 12-13: explicit unbounded aliases assert property (@(posedge clk) a [*0:$] ##1 b) else count_fail12 <= count_fail12 + 1;