diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 8db3e7761..c5c36178d 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -177,6 +177,10 @@ struct BuildResult final { // Mid-window sources for range delays (pure boolean RHS): match-only (isUnbounded) std::vector 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}; } @@ -199,6 +203,10 @@ class SvaNfaBuilder final { // (IEEE 1800-2023 16.12.14 outer-wraps-inner). std::vector 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; @@ -406,6 +414,16 @@ 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(COVERIGN, + "Ignoring 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). @@ -428,13 +446,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 - = new AstLogNot{flp, sampledRefOrClone(hoistVarp, rhsExprp, flp)}; - guardedEdge(currentp, nextVtxp, notExprp, flp); + if (m_isCoverSeq) { + guardedEdge(currentp, nextVtxp, 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; } @@ -517,6 +543,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 consMidSources; + SvaStateVertex* currentp = entryVtxp; for (int i = 0; i < minN; ++i) { if (i > 0) { @@ -532,6 +562,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) { @@ -565,11 +599,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). @@ -608,6 +650,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(COVERIGN, + "Ignoring 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); @@ -662,6 +714,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(COVERIGN, + "Ignoring 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)), @@ -971,10 +1033,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() { @@ -1347,8 +1411,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. - void computeTerminalMatchAndReject(LowerCtx& c, AstNodeExpr* snapshotOkp, SignalSet& sigs) { + // wireMatchAndMidSources. When outPerMidSrcsp is non-null, also collect + // 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* outPerMidSrcsp = nullptr) { for (const SvaTransEdge* const tep : c.edges) { if (tep->toVtxp() != c.graph.m_matchVertexp) continue; const int fi = tep->fromVtxp()->color(); @@ -1360,6 +1427,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 @@ -1410,7 +1489,8 @@ class SvaNfaLowering final { } } - SignalSet computeSignals(LowerCtx& c, std::vector* outRequiredStepSrcsp) { + SignalSet computeSignals(LowerCtx& c, std::vector* outRequiredStepSrcsp, + std::vector* outPerMidSrcsp = nullptr) { SignalSet sigs; // Snapshot comparison expression for disable-iff counter. @@ -1422,7 +1502,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, @@ -1649,7 +1729,8 @@ public: AstNodeExpr* disableExprp = nullptr, bool negated = false, AstNodeExpr** outMatchpp = nullptr, AstVar* disableCntVarp = nullptr, AstVar* snapshotVarp = nullptr, - std::vector* outRequiredStepSrcsp = nullptr) { + std::vector* outRequiredStepSrcsp = nullptr, + std::vector* outPerMidSrcsp = nullptr) { const std::string baseName = m_names.get(""); // Number vertices with sequential colors for array indexing. @@ -1735,7 +1816,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, @@ -1766,7 +1847,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) { @@ -2235,9 +2319,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); @@ -2269,12 +2355,18 @@ class AssertNfaVisitor final : public VNVisitor { = !isCover && !parts.hasImplication && assertWithFailp && assertWithFailp->failsp(); std::vector 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 perMidSrcs; + AstNodeExpr* const alwaysTriggerp = new AstConst{flp, AstConst::BitTrue{}}; - AstNodeExpr* const outputExprp - = m_loweringp->lower(flp, graph, alwaysTriggerp, senTreep, result.finalCondp, isCover, - disableExprp ? disableExprp->cloneTreePure(false) : nullptr, - negated, needMatch ? &matchExprp : nullptr, disableCntVarp, - snapshotVarp, needPerSrcFail ? &requiredStepSrcs : nullptr); + AstNodeExpr* const outputExprp = m_loweringp->lower( + flp, graph, alwaysTriggerp, senTreep, result.finalCondp, isCover, + disableExprp ? disableExprp->cloneTreePure(false) : nullptr, negated, + needMatch ? &matchExprp : nullptr, disableCntVarp, snapshotVarp, + needPerSrcFail ? &requiredStepSrcs : nullptr, isCoverSeq ? &perMidSrcs : nullptr); AstSenTree* const perSrcSenTreep = (requiredStepSrcs.size() >= 2) ? senTreep->cloneTree(false) : nullptr; @@ -2287,9 +2379,38 @@ class AssertNfaVisitor final : public VNVisitor { attachMatchHandlers(flp, assertAssertp, assertWithFailp, needMatch ? matchExprp : nullptr, perSrcSenTreep, requiredStepSrcs); - AstNode* const innerPropp = propSpecp->propp(); - innerPropp->replaceWith(outputExprp); - VL_DO_DANGLING(pushDeletep(innerPropp), innerPropp); + if (isCoverSeq && perMidSrcs.size() > 1) { + // Clone AstCover (N-1) times, each gated by its own per-mid signal. + // 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 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); } diff --git a/src/V3AstNodeStmt.h b/src/V3AstNodeStmt.h index aed79ddc0..46c49b515 100644 --- a/src/V3AstNodeStmt.h +++ b/src/V3AstNodeStmt.h @@ -1607,12 +1607,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: diff --git a/src/V3AstNodes.cpp b/src/V3AstNodes.cpp index 0707c8d8f..453c45d21 100644 --- a/src/V3AstNodes.cpp +++ b/src/V3AstNodes.cpp @@ -2181,6 +2181,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]"; diff --git a/src/verilog.y b/src/verilog.y index d4392a5bc..847a5f828 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6497,14 +6497,34 @@ concurrent_assertion_statement: // ==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); } - // // IEEE: yCOVER ySEQUENCE '(' clocking_event sexpr ')' stmt - // // sexpr already includes "clocking_event sexpr" + { AstCover* const coverp = new AstCover{$1, + new AstPropSpec{$4->fileline(), nullptr, nullptr, $4}, + $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}; } diff --git a/test_regress/t/t_cover_sequence.py b/test_regress/t/t_cover_sequence.py new file mode 100755 index 000000000..23e13d99b --- /dev/null +++ b/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() diff --git a/test_regress/t/t_cover_sequence.v b/test_regress/t/t_cover_sequence.v new file mode 100644 index 000000000..719a3c1ba --- /dev/null +++ b/test_regress/t/t_cover_sequence.v @@ -0,0 +1,90 @@ +// 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 + cover sequence (a | b | c | d | e) hit_simple++; + + // Form 2: cover sequence ( clocking_event sexpr ) stmt + 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 + cover sequence (disable iff (!rst_n) a ##1 c) hit_default_disable++; + + // Form 5: consecutive repetition, counted per end-of-match + 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); + $finish; + end + end + + // Read the counters in 'final', not the clocked block: a same-cycle read of a + // cover counter races the cover's increment under --threads (vltmt). Verilator + // counts one more end-of-match than Questa 2022.3 on some forms at the + // simulation boundary; the Questa value is noted per check. + final begin +`ifdef TEST_VERBOSE + $write("simple=%0d clocked=%0d clk_dis=%0d def_dis=%0d range=%0d 2=%0d 3=%0d\n", hit_simple, + hit_clocked, hit_clocked_disable, hit_default_disable, hit_consrep_range, hit_consrep_2, + hit_consrep_3); +`endif + `checkd(hit_simple, 96); // Questa: 95 + `checkd(hit_clocked, 149); // Questa: 149 + `checkd(hit_clocked_disable, 28); // Questa: 27 + `checkd(hit_default_disable, 30); // Questa: 30 + `checkd(hit_consrep_2, 30); // Questa: 29 + `checkd(hit_consrep_3, 14); // Questa: 13 + // a[*2:3] == a[*2] or a[*3] (IEEE 1800-2023 16.9.2) + `checkd(hit_consrep_range, hit_consrep_2 + hit_consrep_3); // 44; Questa: 42 + $write("*-* All Finished *-*\n"); + end +endmodule diff --git a/test_regress/t/t_cover_sequence_unsup.out b/test_regress/t/t_cover_sequence_unsup.out new file mode 100644 index 000000000..47af703cb --- /dev/null +++ b/test_regress/t/t_cover_sequence_unsup.out @@ -0,0 +1,18 @@ +%Warning-COVERIGN: t/t_cover_sequence_unsup.v:21:33: Ignoring unsupported: cover sequence with a sequence operand of 'or' + 21 | cover sequence ((a ##[1:3] b) or 1'b0); + | ^~ + ... 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_cover_sequence_unsup.v:24:32: Ignoring unsupported: cover sequence with a sequence operand of 'or' + 24 | cover sequence ((a [* 1: 3]) or 1'b0); + | ^~ +%Warning-COVERIGN: t/t_cover_sequence_unsup.v:27:21: Ignoring unsupported: cover sequence with this ranged cycle delay + 27 | cover sequence (a ##[1:2] (b ##1 c)); + | ^~ +%Warning-COVERIGN: t/t_cover_sequence_unsup.v:30:21: Ignoring unsupported: cover sequence with this ranged cycle delay + 30 | cover sequence (a ##[1:300] b); + | ^~ +%Warning-COVERIGN: t/t_cover_sequence_unsup.v:33:21: Ignoring unsupported: cover sequence with a ranged goto repetition + 33 | cover sequence (a [-> 2: 3]); + | ^~~ +%Error: Exiting due to diff --git a/test_regress/t/t_cover_sequence_unsup.py b/test_regress/t/t_cover_sequence_unsup.py new file mode 100755 index 000000000..56c514bc5 --- /dev/null +++ b/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() diff --git a/test_regress/t/t_cover_sequence_unsup.v b/test_regress/t/t_cover_sequence_unsup.v new file mode 100644 index 000000000..b2770a2fa --- /dev/null +++ b/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 ignored (COVERIGN) 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 diff --git a/test_regress/t/t_debug_emitv.out b/test_regress/t/t_debug_emitv.out index b65ab991e..53f8ac53b 100644 --- a/test_regress/t/t_debug_emitv.out +++ b/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 diff --git a/test_regress/t/t_debug_emitv.v b/test_regress/t/t_debug_emitv.v index edc1ec87b..7d3805052 100644 --- a/test_regress/t/t_debug_emitv.v +++ b/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); diff --git a/test_regress/t/t_sequence_sexpr_unsup.out b/test_regress/t/t_sequence_sexpr_unsup.out index 975a06491..9bf5bf9ea 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.out +++ b/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