Support weak until / until_with property operators (#7290) (#7548) (#7685)

Fixes #7290. Fixes #7685.

src/V3AssertNfa.cpp

@@ -818,6 +818,91 @@ class SvaNfaBuilder final {
         return result;
     }
 
+    // until / until_with (weak forms only) per IEEE 1800-2023 16.12.12.
+    // Topology: combinational wait vertex with self-feeding state register.
+    //   entry  --link[T]--> waitC
+    //   waitR  --link[T]--> waitC                          (back-loop)
+    //   waitC  --edge[##1, sampled(p) && !sampled(q)]--> waitR  (continue)
+    //   waitC  --link[REQUIRE, rejectOnFail]--> sink            (per-cycle fail)
+    //   waitC  --link[T]--> match  (added by wireMatchAndMidSources;
+    //                               accept condition rides via finalCondp)
+    // waitC is m_isUnbounded so the terminal-match link contributes only to
+    // terminalActive, not to rejectBase (which would otherwise spuriously fire
+    // every cycle q is false). Per-cycle reject comes from the explicit
+    // rejectOnFail link to the sink vertex.
+    //
+    // Weak non-overlapping (p until q):
+    //   REQUIRE = sampled(p) || sampled(q)   accept = sampled(q)
+    // Weak overlapping (p until_with q):
+    //   REQUIRE = sampled(p)                 accept = sampled(p) && sampled(q)
+    BuildResult buildUntil(AstUntil* nodep, SvaStateVertex* entryVtxp, bool isTopLevelStep) {
+        FileLine* const flp = nodep->fileline();
+        if (!isTopLevelStep) {
+            nodep->v3warn(E_UNSUPPORTED, "Unsupported: 'until' in complex property expression");
+            return BuildResult::failWithError();
+        }
+        if (nodep->isStrong()) {
+            nodep->v3warn(E_UNSUPPORTED, "Unsupported: s_until"
+                                             << (nodep->isOverlapping() ? "_with" : "")
+                                             << " (in property expresion)");
+            return BuildResult::failWithError();
+        }
+        AstNodeExpr* const lhsp = nodep->lhsp();
+        AstNodeExpr* const rhsp = nodep->rhsp();
+        const auto hasSeq = [](const AstNodeExpr* ep) {
+            return ep->exists([](const AstNodeExpr* np) { return np->isMultiCycleSva(); });
+        };
+        if (hasSeq(lhsp) || hasSeq(rhsp)) {
+            nodep->v3warn(E_UNSUPPORTED, "Unsupported: 'until' in complex property expression");
+            return BuildResult::failWithError();
+        }
+
+        const bool ov = nodep->isOverlapping();
+        AstNodeExpr* const lhsBitp = nodep->lhsp();
+        AstNodeExpr* const rhsBitp = nodep->rhsp();
+        // p hoist count: continue, require (ov: 1 use; nov: 1 use). At least 2 uses.
+        AstVar* const pHoistp = tryHoistSampled(lhsBitp, flp, 2);
+        // q hoist count: continue (1) + require nov (1) = 2; ov: continue only (1).
+        AstVar* const qHoistp = ov ? nullptr : tryHoistSampled(rhsBitp, flp, 2);
+
+        SvaStateVertex* const waitCp = scopedCreateVertex();
+        SvaStateVertex* const waitRp = scopedCreateVertex();
+        waitCp->m_isUnbounded = true;
+
+        // Entry and back-loop Links carry no condition; throughout-folding still applies.
+        guardedLink(entryVtxp, waitCp, flp);
+        guardedLink(waitRp, waitCp, flp);
+
+        // Continue clocked edge: p && !q advances to next-cycle wait.
+        AstNodeExpr* const contCondp
+            = new AstLogAnd{flp, sampledRefOrClone(pHoistp, lhsBitp, flp),
+                            new AstLogNot{flp, sampledRefOrClone(qHoistp, rhsBitp, flp)}};
+        guardedEdge(waitCp, waitRp, contCondp, flp);
+
+        // Reject sink: fires when require-condition is false.
+        SvaStateVertex* const sinkVtxp = m_graph.createStateVertex();
+        sinkVtxp->m_isRejectSink = true;
+        AstNodeExpr* requireCondp;
+        if (ov) {
+            requireCondp = sampledRefOrClone(pHoistp, lhsBitp, flp);
+        } else {
+            requireCondp = new AstLogOr{flp, sampledRefOrClone(pHoistp, lhsBitp, flp),
+                                        sampledRefOrClone(qHoistp, rhsBitp, flp)};
+        }
+        SvaTransEdge* const rejEdgep = m_graph.addLink(waitCp, sinkVtxp, requireCondp);
+        rejEdgep->m_rejectOnFail = true;
+
+        // Accept condition rides via finalCondp; assembleResult $sampled-wraps it.
+        AstNodeExpr* acceptCondp;
+        if (ov) {
+            acceptCondp
+                = new AstLogAnd{flp, lhsBitp->cloneTreePure(false), rhsBitp->cloneTreePure(false)};
+        } else {
+            acceptCondp = rhsBitp->cloneTreePure(false);
+        }
+        return {waitCp, acceptCondp, {}};
+    }
+
     // IEEE 1800-2023 16.12.14 property abort operators. Sync and async share
     // the same NFA encoding: AstSampled already gives matured values at every
     // maturing clocking event, and async firing "between clocks" is not
@@ -948,6 +1033,9 @@ public:
                                          implp->isOverlapped(), implp->isFollowedBy(),
                                          implp->lhsp(), implp->fileline());
         }
+        if (AstUntil* const untilp = VN_CAST(nodep, Until)) {
+            return buildUntil(untilp, entryVtxp, isTopLevelStep);
+        }
         // Boolean leaf (including LogAnd): return as finalCond
         return {entryVtxp, nodep, {}};
     }
@@ -1836,6 +1924,25 @@ class AssertNfaVisitor final : public VNVisitor {
         });
     }
 
+    // Bare `assert property (p until q)` with boolean operands stays on
+    // V3AssertPre's AstLoop lowering, which preserves per-attempt action-block
+    // firings that this NFA's single-bit aggregated state cannot. NFA still
+    // owns strong forms, sequence operands, and any embedding inside a
+    // multi-cycle context (implication consequent, or/and operands, etc.).
+    static bool isBareTopLevelUntil(AstNode* propp) {
+        AstNode* p = propp;
+        if (AstPropSpec* const specp = VN_CAST(p, PropSpec)) p = specp->propp();
+        while (AstLogNot* const notp = VN_CAST(p, LogNot)) p = notp->lhsp();
+        AstUntil* const untilp = VN_CAST(p, Until);
+        if (!untilp) return false;
+        if (untilp->isStrong()) return false;
+        const auto hasSeq = [](const AstNodeExpr* ep) {
+            return ep->exists([](const AstNodeExpr* np) { return np->isMultiCycleSva(); });
+        };
+        if (hasSeq(untilp->lhsp()) || hasSeq(untilp->rhsp())) return false;
+        return true;
+    }
+
     struct PropertyParts final {
         AstNodeExpr* triggerExprp = nullptr;
         AstNodeExpr* seqExprp = nullptr;
@@ -2083,6 +2190,7 @@ class AssertNfaVisitor final : public VNVisitor {
 
         AstNode* const propp = assertp->propp();
         if (!hasMultiCycleExpr(propp)) return;
+        if (isBareTopLevelUntil(propp)) return;
 
         PropertyParts parts = decomposeProperty(propp);
         UASSERT_OBJ(parts.seqExprp, propp, "Property body must be an expression");