Fix sampled-value clocks in repeated assertions (#7944)

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<const AstProperty*> m_inliningProps;  // Recursion guard for inlineNamedProperty
 
+    template <typename T_Node>
+    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 {

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;