Support cover sequence statement

src/V3AssertNfa.cpp

@@ -176,6 +176,10 @@ struct BuildResult final {
     // Mid-window sources for range delays (pure boolean RHS): match-only (isUnbounded)
     std::vector<SvaStateVertex*> midSources;
     bool errorEmitted = false;  // Builder already emitted specific error; skip generic
+    // For cover_sequence: when true, midSources already enumerate every
+    // end-of-match, so wireMatchAndMidSources must NOT add the main
+    // termVtxp -> matchVertex Link (would double-count via the merge vertex).
+    bool termIsMidMerge = false;
     bool valid() const { return termVertexp != nullptr; }
     static BuildResult fail(bool errored = false) { return {nullptr, nullptr, {}, errored}; }
     static BuildResult failWithError() { return {nullptr, nullptr, {}, true}; }
@@ -198,6 +202,10 @@ class SvaNfaBuilder final {
     // (IEEE 1800-2023 16.12.14 outer-wraps-inner).
     std::vector<AstNodeExpr*> m_outerAbortStack;
     bool m_inUnboundedScope = false;  // Sticky: nodes created after inherit liveness
+    // IEEE 1800-2023 16.14.3 cover sequence: each end-of-match fires the action,
+    // not just the first. Builder builds parallel-branch (no first-match-wins)
+    // topology when true. Default false preserves cover_property semantics.
+    bool m_isCoverSeq = false;
 
     AstNodeExpr* throughoutCond(AstNodeExpr* baseCondp, FileLine* flp) {
         if (m_throughoutStack.empty()) return baseCondp;
@@ -405,6 +413,15 @@ class SvaNfaBuilder final {
         // count is O(1) in range regardless of user input; no adversarial N
         // blowup is possible.
         constexpr int kChainLimit = 256;
+        // IEEE 1800-2023 16.14.3: only a small bounded range before a plain
+        // boolean enumerates every end-of-match below. The counter FSM drops
+        // overlapping ends and the nested-sequence merge collapses them, so
+        // reject those for a cover sequence rather than under-count.
+        if (m_isCoverSeq && (range > kChainLimit || VN_IS(rhsExprp, SExpr))) {
+            flp->v3warn(E_UNSUPPORTED, "Unsupported: cover sequence with this ranged cycle delay");
+            outErrorEmitted = true;
+            return false;
+        }
         if (range > kChainLimit) {
             // Large range: counter FSM. Overlapping triggers during an active
             // count are dropped (non-overlapping semantics only).
@@ -427,13 +444,21 @@ 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);
+            // For cover_sequence (IEEE 1800-2023 16.14.3) the advance edge is
+            // unconditional so every (start, end) pair fires independently --
+            // dropping NOT(b) turns "first-match-wins" into "every end fires".
+            AstVar* const hoistVarp
+                = m_isCoverSeq ? nullptr : tryHoistSampled(rhsExprp, flp, range);
             midSources.push_back(currentp);
             for (int i = 0; i < range; ++i) {
                 SvaStateVertex* const nextVtxp = scopedCreateVertex();
-                AstNodeExpr* const notExprp
+                if (m_isCoverSeq) {
-                    = new AstLogNot{flp, sampledRefOrClone(hoistVarp, rhsExprp, flp)};
+                    guardedEdge(currentp, nextVtxp, flp);
-                guardedEdge(currentp, nextVtxp, notExprp, flp);
+                } else {
+                    AstNodeExpr* const notExprp
+                        = new AstLogNot{flp, sampledRefOrClone(hoistVarp, rhsExprp, flp)};
+                    guardedEdge(currentp, nextVtxp, notExprp, flp);
+                }
                 if (i < range - 1) midSources.push_back(nextVtxp);
                 currentp = nextVtxp;
             }
@@ -516,6 +541,10 @@ class SvaNfaBuilder final {
         if (exceedsAssertUnrollLimit(repp, totalSites)) return BuildResult::failWithError();
         AstVar* const hoistVarp = tryHoistSampled(exprp, flp, totalSites);
 
+        // Cover-sequence (IEEE 1800-2023 16.14.3): collect each end-of-match
+        // position so they all fire the action, not just the merged terminal.
+        std::vector<SvaStateVertex*> consMidSources;
+
         SvaStateVertex* currentp = entryVtxp;
         for (int i = 0; i < minN; ++i) {
             if (i > 0) {
@@ -531,6 +560,10 @@ class SvaNfaBuilder final {
             if (isTopLevelStep && (i == 0 || i == minN - 1)) { linkp->m_rejectOnFail = true; }
             currentp = condVtxp;
         }
+        // After minN: currentp is the first valid end-of-match position for [*m:n].
+        if (m_isCoverSeq && (repp->unbounded() || repp->maxCountp())) {
+            consMidSources.push_back(currentp);
+        }
 
         if (repp->unbounded()) {
             if (minN == 0) {
@@ -564,11 +597,19 @@ class SvaNfaBuilder final {
                 guardedLink(nextVtxp, checkVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp);
                 guardedLink(checkVtxp, mergeVtxp, flp);
                 currentp = checkVtxp;
+                if (m_isCoverSeq) consMidSources.push_back(checkVtxp);
             }
             currentp = mergeVtxp;
         }
         // finalCond = nullptr (already checked via Links)
-        return {currentp, nullptr, {}};
+        BuildResult res;
+        res.termVertexp = currentp;
+        res.finalCondp = nullptr;
+        res.midSources = std::move(consMidSources);
+        // mergeVtxp is the OR of all the end-positions we already pushed to
+        // midSources, so the main termVtxp -> matchVertex Link would duplicate.
+        res.termIsMidMerge = m_isCoverSeq && !res.midSources.empty();
+        return res;
     }
 
     // always[lo:hi] / s_always[lo:hi] (IEEE 1800-2023 16.12.11).
@@ -607,6 +648,16 @@ class SvaNfaBuilder final {
         UASSERT_OBJ(maxN >= minN, repp, "GotoRep range max < min (V3Width invariant)");
         if (exceedsAssertUnrollLimit(repp, maxN)) return BuildResult::failWithError();
 
+        // IEEE 1800-2023 16.14.3: a ranged goto repetition b[->M:N] ends at every
+        // M..N-th match, but only the shared merge vertex below reaches the
+        // terminal, so a cover sequence would under-count. Reject the ranged form
+        // (the single-count b[->N] has one end and is enumerated correctly).
+        if (m_isCoverSeq && hasMax && maxN > minN) {
+            flp->v3warn(E_UNSUPPORTED,
+                        "Unsupported: cover sequence with a ranged goto repetition");
+            return BuildResult::failWithError();
+        }
+
         // Wait + match per iter -> 2 sites per iteration; range form needs
         // sites for every iteration in [0..maxN). NOT($sampled(x)) matches
         // $sampled(NOT(x)) at the value level (IEEE 1800-2023 16.9.9);
@@ -661,6 +712,16 @@ class SvaNfaBuilder final {
         if (!lhs.valid() || !rhs.valid()) {  // LCOV_EXCL_START -- sub-build fail bail
             return BuildResult::fail(lhs.errorEmitted || rhs.errorEmitted);
         }  // LCOV_EXCL_STOP
+        // IEEE 1800-2023 16.14.3: a cover sequence counts every end-of-match. A
+        // sequence operand of 'or' can end more than once, but only its final
+        // end reaches the merge vertex below, so reject sequence operands rather
+        // than under-count. Plain boolean disjunction has one end per cycle and
+        // is handled by the OR-fold.
+        if (m_isCoverSeq && (lhs.termVertexp != entryVtxp || rhs.termVertexp != entryVtxp)) {
+            flp->v3warn(E_UNSUPPORTED,
+                        "Unsupported: cover sequence with a sequence operand of 'or'");
+            return BuildResult::failWithError();
+        }
         SvaStateVertex* const mergeVtxp = scopedCreateVertex();
         if (lhs.finalCondp) {
             guardedLink(lhs.termVertexp, mergeVtxp, sampled(lhs.finalCondp->cloneTreePure(false)),
@@ -970,10 +1031,12 @@ class SvaNfaBuilder final {
     }
 
 public:
-    SvaNfaBuilder(SvaGraph& graph, AstNodeModule* modp, V3UniqueNames& propTempNames)
+    SvaNfaBuilder(SvaGraph& graph, AstNodeModule* modp, V3UniqueNames& propTempNames,
+                  bool isCoverSeq = false)
         : m_graph{graph}
         , m_modp{modp}
-        , m_propTempNames{propTempNames} {}
+        , m_propTempNames{propTempNames}
+        , m_isCoverSeq{isCoverSeq} {}
 
     // Reset scope between antecedent and consequent: liveness must not leak.
     void resetScope() {
@@ -1346,8 +1409,11 @@ class SvaNfaLowering final {
     // throughout-drop reject; clean up intermediate state signals.
     // Phase 3: terminalActive and rejectBase from Links to matchVertex.
     // Builder only adds Links (non-clocked) to matchVertex via addLink in
-    // wireMatchAndMidSources.
+    // wireMatchAndMidSources. When outPerMidSrcsp is non-null, also collect
-    void computeTerminalMatchAndReject(LowerCtx& c, AstNodeExpr* snapshotOkp, SignalSet& sigs) {
+    // the per-edge match signal (IEEE 1800-2023 16.14.3 cover sequence: each
+    // end-of-match fires the action independently, no OR-fold).
+    void computeTerminalMatchAndReject(LowerCtx& c, AstNodeExpr* snapshotOkp, SignalSet& sigs,
+                                       std::vector<AstNodeExpr*>* outPerMidSrcsp = nullptr) {
         for (const SvaTransEdge* const tep : c.edges) {
             if (tep->toVtxp() != c.graph.m_matchVertexp) continue;
             const int fi = tep->fromVtxp()->color();
@@ -1359,6 +1425,18 @@ class SvaNfaLowering final {
             if (snapshotOkp) {
                 srcSigp = new AstLogAnd{c.flp, srcSigp, snapshotOkp->cloneTreePure(false)};
             }
+            if (outPerMidSrcsp) {
+                // Per-mid signal must also AND in matchCondp (the final boolean
+                // check, e.g. sampled(b) for `a ##[1:3] b`). assembleResult does
+                // this for the OR-collapsed terminalActivep; we replicate it
+                // per-edge here so each end-of-match is gated identically.
+                AstNodeExpr* perMidp = srcSigp->cloneTreePure(false);
+                if (c.matchCondp) {
+                    perMidp = new AstLogAnd{c.flp, perMidp,
+                                            sampled(c.matchCondp->cloneTreePure(false))};
+                }
+                outPerMidSrcsp->push_back(perMidp);
+            }
 
             if (tep->fromVtxp()->m_isCounter) {
                 sigs.terminalActivep
@@ -1409,7 +1487,8 @@ class SvaNfaLowering final {
         }
     }
 
-    SignalSet computeSignals(LowerCtx& c, std::vector<AstNodeExpr*>* outRequiredStepSrcsp) {
+    SignalSet computeSignals(LowerCtx& c, std::vector<AstNodeExpr*>* outRequiredStepSrcsp,
+                             std::vector<AstNodeExpr*>* outPerMidSrcsp = nullptr) {
         SignalSet sigs;
 
         // Snapshot comparison expression for disable-iff counter.
@@ -1421,7 +1500,7 @@ class SvaNfaLowering final {
                                     new AstVarRef{c.flp, c.disableCntVarp, VAccess::READ}};
         }
 
-        computeTerminalMatchAndReject(c, snapshotOkp, sigs);
+        computeTerminalMatchAndReject(c, snapshotOkp, sigs, outPerMidSrcsp);
 
         // Phase 3a: required-step rejection.
         // Builder only sets m_rejectOnFail on non-clocked Links with m_condp,
@@ -1648,7 +1727,8 @@ public:
                        AstNodeExpr* disableExprp = nullptr, bool negated = false,
                        AstNodeExpr** outMatchpp = nullptr, AstVar* disableCntVarp = nullptr,
                        AstVar* snapshotVarp = nullptr,
-                       std::vector<AstNodeExpr*>* outRequiredStepSrcsp = nullptr) {
+                       std::vector<AstNodeExpr*>* outRequiredStepSrcsp = nullptr,
+                       std::vector<AstNodeExpr*>* outPerMidSrcsp = nullptr) {
         const std::string baseName = m_names.get("");
 
         // Number vertices with sequential colors for array indexing.
@@ -1734,7 +1814,7 @@ public:
         emitAndCombinerDoneLatchNba(c);
 
         // Phase 3/3a/3b: Compute terminal match/reject signals (cleans up stateSig).
-        const SignalSet sigs = computeSignals(c, outRequiredStepSrcsp);
+        const SignalSet sigs = computeSignals(c, outRequiredStepSrcsp, outPerMidSrcsp);
 
         AstNodeExpr* const resultp = assembleResult(
             flp, isCover, negated, matchCondp, sigs.terminalActivep, sigs.rejectBasep,
@@ -1765,7 +1845,10 @@ class AssertNfaVisitor final : public VNVisitor {
     // Wire match vertex and mid-window sources for a successful NFA build.
     static void wireMatchAndMidSources(SvaGraph& graph, const BuildResult& result, FileLine* flp) {
         graph.createMatchVertex();
-        graph.addLink(result.termVertexp, graph.m_matchVertexp);
+        // Skip the main term Link when midSources already cover every
+        // end-of-match (cover_sequence path); otherwise the per-mid extraction
+        // double-counts via the merge vertex.
+        if (!result.termIsMidMerge) { graph.addLink(result.termVertexp, graph.m_matchVertexp); }
         for (SvaStateVertex* srcVtxp : result.midSources) {
             AstNodeExpr* condp = nullptr;
             for (AstNodeExpr* const tc : srcVtxp->m_throughoutConds) {
@@ -2234,9 +2317,11 @@ class AssertNfaVisitor final : public VNVisitor {
 
         FileLine* const flp = assertp->fileline();
         const bool isCover = VN_IS(assertp, Cover);
+        AstCover* const coverp = VN_CAST(assertp, Cover);
+        const bool isCoverSeq = coverp && coverp->isCoverSeq();
 
         SvaGraph graph;
-        SvaNfaBuilder builder{graph, m_modp, m_propTempNames};
+        SvaNfaBuilder builder{graph, m_modp, m_propTempNames, isCoverSeq};
 
         const BuildResult result = buildAssertionGraph(builder, graph, seqBodyp, parts, flp);
         if (result.valid()) wireMatchAndMidSources(graph, result, flp);
@@ -2268,12 +2353,18 @@ class AssertNfaVisitor final : public VNVisitor {
             = !isCover && !parts.hasImplication && assertWithFailp && assertWithFailp->failsp();
         std::vector<AstNodeExpr*> requiredStepSrcs;
 
+        // For `cover sequence` (IEEE 1800-2023 16.14.3) collect per-edge match
+        // signals so each end-of-match fires the action independently, rather
+        // than getting OR-folded into a single per-cycle terminalActive.
+        // coverp / isCoverSeq are computed earlier (passed to SvaNfaBuilder).
+        std::vector<AstNodeExpr*> perMidSrcs;
+
         AstNodeExpr* const alwaysTriggerp = new AstConst{flp, AstConst::BitTrue{}};
-        AstNodeExpr* const outputExprp
+        AstNodeExpr* const outputExprp = m_loweringp->lower(
-            = m_loweringp->lower(flp, graph, alwaysTriggerp, senTreep, result.finalCondp, isCover,
+            flp, graph, alwaysTriggerp, senTreep, result.finalCondp, isCover,
-                                 disableExprp ? disableExprp->cloneTreePure(false) : nullptr,
+            disableExprp ? disableExprp->cloneTreePure(false) : nullptr, negated,
-                                 negated, needMatch ? &matchExprp : nullptr, disableCntVarp,
+            needMatch ? &matchExprp : nullptr, disableCntVarp, snapshotVarp,
-                                 snapshotVarp, needPerSrcFail ? &requiredStepSrcs : nullptr);
+            needPerSrcFail ? &requiredStepSrcs : nullptr, isCoverSeq ? &perMidSrcs : nullptr);
 
         AstSenTree* const perSrcSenTreep
             = (requiredStepSrcs.size() >= 2) ? senTreep->cloneTree(false) : nullptr;
@@ -2286,9 +2377,38 @@ class AssertNfaVisitor final : public VNVisitor {
         attachMatchHandlers(flp, assertAssertp, assertWithFailp, needMatch ? matchExprp : nullptr,
                             perSrcSenTreep, requiredStepSrcs);
 
-        AstNode* const innerPropp = propSpecp->propp();
+        if (isCoverSeq && perMidSrcs.size() > 1) {
-        innerPropp->replaceWith(outputExprp);
+            // Clone AstCover (N-1) times, each gated by its own per-mid signal.
-        VL_DO_DANGLING(pushDeletep(innerPropp), innerPropp);
+            // V3Assert sees N independent covers and emits N `if (cond_i) {coverinc;
+            // userAction}` bodies; the shared AstCoverDecl bucket is incremented
+            // per fire, matching IEEE "executed each time the sequence matches."
+            // Clones reuse AstCover->propp's original SVA tree, but we overwrite
+            // each clone's inner propp with the corresponding per-mid signal
+            // BEFORE the next iterator step, so hasMultiCycleExpr() returns false
+            // and processAssertion skips them on revisit.
+            std::vector<AstCover*> coverList;
+            coverList.push_back(coverp);
+            for (size_t i = 1; i < perMidSrcs.size(); ++i) {
+                AstCover* const clonep = coverp->cloneTree(false);
+                coverp->addNextHere(clonep);
+                coverList.push_back(clonep);
+            }
+            for (size_t i = 0; i < perMidSrcs.size(); ++i) {
+                AstPropSpec* const clonePropSpecp = VN_CAST(coverList[i]->propp(), PropSpec);
+                AstNode* const innerp = clonePropSpecp->propp();
+                innerp->replaceWith(perMidSrcs[i]);
+                VL_DO_DANGLING(pushDeletep(innerp), innerp);
+            }
+            // Discard the OR-collapsed fallback signal -- cover_sequence path
+            // does not use it.
+            VL_DO_DANGLING(outputExprp->deleteTree(), outputExprp);
+        } else {
+            AstNode* const innerPropp = propSpecp->propp();
+            innerPropp->replaceWith(outputExprp);
+            VL_DO_DANGLING(pushDeletep(innerPropp), innerPropp);
+            // If we collected per-mid (N==1) but didn't clone, drop the spare.
+            for (AstNodeExpr* const sp : perMidSrcs) pushDeletep(sp);
+        }
 
         UINFO(4, "NFA converted assertion at " << flp << endl);
     }

src/V3AstNodeStmt.h

@@ -1606,12 +1606,18 @@ public:
 };
 class AstCover final : public AstNodeCoverOrAssert {
     // @astgen op3 := coverincsp: List[AstNode] // Coverage node
+    bool m_isCoverSeq = false;  // 'cover sequence' (IEEE 1800-2023 16.14.3): fires per
+                                // end-of-match, not per property success
 public:
     ASTGEN_MEMBERS_AstCover;
     AstCover(FileLine* fl, AstNode* propp, AstNode* stmtsp, VAssertType type,
              const string& name = "")
         : ASTGEN_SUPER_Cover(fl, propp, stmtsp, type, VAssertDirectiveType::COVER, name) {}
     string verilogKwd() const override { return "cover"; }
+    void dump(std::ostream& str) const override;
+    void dumpJson(std::ostream& str) const override;
+    bool isCoverSeq() const { return m_isCoverSeq; }
+    void isCoverSeq(bool flag) { m_isCoverSeq = flag; }
 };
 class AstRestrict final : public AstNodeCoverOrAssert {
 public:

src/V3AstNodes.cpp

@@ -2133,6 +2133,14 @@ void AstNodeCoverOrAssert::dumpJson(std::ostream& str) const {
     dumpJsonBoolFuncIf(str, immediate);
     dumpJsonBoolFuncIf(str, senFromAlways);
 }
+void AstCover::dump(std::ostream& str) const {
+    this->AstNodeCoverOrAssert::dump(str);
+    if (isCoverSeq()) str << " [COVERSEQ]";
+}
+void AstCover::dumpJson(std::ostream& str) const {
+    dumpJsonBoolFuncIf(str, isCoverSeq);
+    this->AstNodeCoverOrAssert::dumpJson(str);
+}
 void AstClocking::dump(std::ostream& str) const {
     this->AstNode::dump(str);
     if (isDefault()) str << " [DEFAULT]";

src/verilog.y

@@ -6497,14 +6497,34 @@ concurrent_assertion_statement<nodeStmtp>:  // ==IEEE: concurrent_assertion_stat
         |       yCOVER yPROPERTY '(' property_spec ')' stmt
                         { $$ = new AstCover{$1, $4, $6, VAssertType::CONCURRENT}; }
         //                      // IEEE: cover_sequence_statement
+        //                      // Reuses AstCover + AstPropSpec (same wrapper as
+        //                      // cover_property_statement above) and the isCoverSeq
+        //                      // flag drives V3AssertNfa to fire stmt per end-of-match
+        //                      // (IEEE 1800-2023 16.14.3), not per property success.
         |       yCOVER ySEQUENCE '(' sexpr ')' stmt
-                        { $$ = nullptr; BBCOVERIGN($2, "Ignoring unsupported: cover sequence"); DEL($4, $6); }
+                        { AstCover* const coverp = new AstCover{$1,
-        //                      // IEEE: yCOVER ySEQUENCE '(' clocking_event sexpr ')' stmt
+                              new AstPropSpec{$4->fileline(), nullptr, nullptr, $4},
-        //                      // sexpr already includes "clocking_event sexpr"
+                              $6, VAssertType::CONCURRENT};
+                          coverp->isCoverSeq(true);
+                          $$ = coverp; }
+        |       yCOVER ySEQUENCE '(' clocking_event sexpr ')' stmt
+                        { AstCover* const coverp = new AstCover{$1,
+                              new AstPropSpec{$4->fileline(), $4, nullptr, $5},
+                              $7, VAssertType::CONCURRENT};
+                          coverp->isCoverSeq(true);
+                          $$ = coverp; }
         |       yCOVER ySEQUENCE '(' clocking_event yDISABLE yIFF '(' expr/*expression_or_dist*/ ')' sexpr ')' stmt
-                        { $$ = nullptr; BBCOVERIGN($2, "Ignoring unsupported: cover sequence"); DEL($4, $8, $10, $12);}
+                        { AstCover* const coverp = new AstCover{$1,
+                              new AstPropSpec{$4->fileline(), $4, $8, $10},
+                              $12, VAssertType::CONCURRENT};
+                          coverp->isCoverSeq(true);
+                          $$ = coverp; }
         |       yCOVER ySEQUENCE '(' yDISABLE yIFF '(' expr/*expression_or_dist*/ ')' sexpr ')' stmt
-                        { $$ = nullptr; BBCOVERIGN($2, "Ignoring unsupported: cover sequence"); DEL($7, $9, $11); }
+                        { AstCover* const coverp = new AstCover{$1,
+                              new AstPropSpec{$7->fileline(), nullptr, $7, $9},
+                              $11, VAssertType::CONCURRENT};
+                          coverp->isCoverSeq(true);
+                          $$ = coverp; }
         //                      // IEEE: restrict_property_statement
         |       yRESTRICT yPROPERTY '(' property_spec ')' ';'
                         { $$ = new AstRestrict{$1, $4}; }

test_regress/t/t_cover_sequence.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('simulator')
+
+test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing', '--coverage-user'])
+
+test.execute()
+
+test.passes()

test_regress/t/t_cover_sequence.v

@@ -0,0 +1,87 @@
+// 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 checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0x exp=%0x (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0);
+`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
+);
+
+  logic [63:0] crc = 64'h5aef0c8dd70a4497;
+  logic rst_n = 1'b0;
+  logic a, b, c, d, e;
+  int cyc = 0;
+
+  int hit_simple = 0;
+  int hit_clocked = 0;
+  int hit_clocked_disable = 0;
+  int hit_default_disable = 0;
+  int hit_consrep_range = 0;
+  int hit_consrep_2 = 0;
+  int hit_consrep_3 = 0;
+
+  default clocking cb @(posedge clk);
+  endclocking
+
+  // Non-adjacent CRC bits to avoid LFSR shift correlation
+  assign a = crc[0];
+  assign b = crc[5];
+  assign c = crc[10];
+  assign d = crc[15];
+  assign e = crc[20];
+
+  // Form 1: cover sequence ( sexpr ) stmt  -- default clocking, no disable
+  cover sequence (a | b | c | d | e) hit_simple++;
+
+  // Form 2: cover sequence ( clocking_event sexpr ) stmt  -- explicit clock,
+  // bounded range delay (the case where IEEE "every end-of-match" diverges
+  // from cover_property's "one match per attempt" semantics)
+  cover sequence (@(posedge clk) (a | b | c | d | e) ##[1:3] b) hit_clocked++;
+
+  // Form 3: cover sequence ( clocking_event disable iff (expr) sexpr ) stmt
+  cover sequence (@(posedge clk) disable iff (!rst_n) a ##1 b) hit_clocked_disable++;
+
+  // Form 4: cover sequence ( disable iff (expr) sexpr ) stmt  -- default clock
+  cover sequence (disable iff (!rst_n) a ##1 c) hit_default_disable++;
+
+  // Form 5: consecutive repetition (per-end-of-match). A ranged repetition
+  // a[*2:3] ends every cycle a 2- or 3-run completes; by IEEE 1800-2023 16.9.2
+  // a[*2:3] == a[*2] or a[*3], so the range count equals the sum of the two
+  // fixed counts -- a Questa-free identity that validates the multiplicity.
+  cover sequence (a [* 2: 3]) hit_consrep_range++;
+  cover sequence (a [* 2]) hit_consrep_2++;
+  cover sequence (a [* 3]) hit_consrep_3++;
+
+  always @(posedge clk) begin
+`ifdef TEST_VERBOSE
+    $write("[%0t] cyc=%0d crc=%x a=%b b=%b c=%b d=%b e=%b\n", $time, cyc, crc, a, b, c, d, e);
+`endif
+    cyc <= cyc + 1;
+    crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[1] ^ crc[0]};
+    if (cyc == 2) rst_n <= 1'b1;
+    if (cyc == 99) begin
+      `checkh(crc, 64'h261a9f1371d7aadf);
+      `checkd(hit_simple, 96);  // Questa:  95 (single-sexpr sample-edge diff)
+      `checkd(hit_clocked, 149);  // IEEE 16.14.3: every end-of-match
+      `checkd(hit_clocked_disable, 28);  // Questa:  27 (sample-edge diff, ##1 single delay)
+      `checkd(hit_default_disable, 30);  // Questa:  30
+`ifdef TEST_VERBOSE
+      $write("consrep range=%0d  2=%0d  3=%0d  sum=%0d\n", hit_consrep_range, hit_consrep_2,
+             hit_consrep_3, hit_consrep_2 + hit_consrep_3);
+`endif
+      `checkd(hit_consrep_2, 30);
+      `checkd(hit_consrep_3, 14);
+      // IEEE 1800-2023 16.9.2: a[*2:3] == a[*2] or a[*3], so the per-end counts add.
+      `checkd(hit_consrep_range, hit_consrep_2 + hit_consrep_3);  // == 44
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+endmodule

test_regress/t/t_cover_sequence_unsup.out

@@ -0,0 +1,17 @@
+%Error-UNSUPPORTED: t/t_cover_sequence_unsup.v:21:33: Unsupported: cover sequence with a sequence operand of 'or'
+   21 |   cover sequence ((a ##[1:3] b) or 1'b0);
+      |                                 ^~
+                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
+%Error-UNSUPPORTED: t/t_cover_sequence_unsup.v:24:32: Unsupported: cover sequence with a sequence operand of 'or'
+   24 |   cover sequence ((a [* 1: 3]) or 1'b0);
+      |                                ^~
+%Error-UNSUPPORTED: t/t_cover_sequence_unsup.v:27:21: Unsupported: cover sequence with this ranged cycle delay
+   27 |   cover sequence (a ##[1:2] (b ##1 c));
+      |                     ^~
+%Error-UNSUPPORTED: t/t_cover_sequence_unsup.v:30:21: Unsupported: cover sequence with this ranged cycle delay
+   30 |   cover sequence (a ##[1:300] b);
+      |                     ^~
+%Error-UNSUPPORTED: t/t_cover_sequence_unsup.v:33:21: Unsupported: cover sequence with a ranged goto repetition
+   33 |   cover sequence (a [-> 2: 3]);
+      |                     ^~~
+%Error: Exiting due to

test_regress/t/t_cover_sequence_unsup.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(expect_filename=test.golden_filename,
+          verilator_flags2=['--assert --error-limit 1000'],
+          fails=True)
+
+test.passes()

test_regress/t/t_cover_sequence_unsup.v

@@ -0,0 +1,35 @@
+// 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
+
+module t (
+    input clk
+);
+
+  logic a, b, c;
+
+  default clocking cb @(posedge clk);
+  endclocking
+
+  // cover sequence (IEEE 1800-2023 16.14.3) counts every end-of-match. The
+  // following forms put a sub-sequence where only its final end is forwarded,
+  // so they are rejected rather than under-counted.
+
+  // Sequence operand of 'or' (ranged cycle delay).
+  cover sequence ((a ##[1:3] b) or 1'b0);
+
+  // Sequence operand of 'or' (consecutive repetition).
+  cover sequence ((a [* 1: 3]) or 1'b0);
+
+  // Ranged cycle delay before a multi-cycle sequence.
+  cover sequence (a ##[1:2] (b ##1 c));
+
+  // Ranged cycle delay wide enough to use the counter FSM.
+  cover sequence (a ##[1:300] b);
+
+  // Ranged goto repetition (every M..N-th match is a separate end).
+  cover sequence (a [-> 2: 3]);
+
+endmodule

test_regress/t/t_debug_emitv.out

@@ -651,6 +651,11 @@ module Vt_debug_emitv_t;
             $display("pass");
         end
     end
+    begin : cover_sequence_concurrent
+        cover property (@(posedge clk) in##1 in
+        ) begin
+        end
+    end
     begin : assert_prop_always
         assert property (@(posedge clk) always ['sh0:
                          'sh3] in

test_regress/t/t_debug_emitv.v

@@ -343,6 +343,8 @@ module t (/*AUTOARG*/
   cover_concurrent: cover property(prop);
   cover_concurrent_stmt: cover property(prop) $display("pass");
 
+  cover_sequence_concurrent: cover sequence (@(posedge clk) in ##1 in);
+
   assert_prop_always: assert property (@(posedge clk) always [0:3] in);
   assert_prop_s_always: assert property (@(posedge clk) s_always [1:2] in);
   assert_prop_overlap_impl: assert property (@(posedge clk) in |-> in);

test_regress/t/t_sequence_sexpr_unsup.out

@@ -8,15 +8,4 @@
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:99:5: Unsupported: first_match with sequence_match_items
    99 |     first_match (a, res0 = 1, res1 = 2);
       |     ^~~~~~~~~~~
-%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:102:9: Ignoring unsupported: cover sequence
-  102 |   cover sequence (s_a) $display("");
-      |         ^~~~~~~~
-                   ... For warning description see https://verilator.org/warn/COVERIGN?v=latest
-                   ... Use "/* verilator lint_off COVERIGN */" and lint_on around source to disable this message.
-%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:103:9: Ignoring unsupported: cover sequence
-  103 |   cover sequence (@(posedge a) disable iff (b) s_a) $display("");
-      |         ^~~~~~~~
-%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:104:9: Ignoring unsupported: cover sequence
-  104 |   cover sequence (disable iff (b) s_a) $display("");
-      |         ^~~~~~~~
 %Error: Exiting due to