luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Support cover sequence statement (#7764)

This commit is contained in:
Yilou Wang 2026-06-15 14:36:21 +02:00 committed by GitHub
parent 969a775ae5
commit 077558a9b0
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
12 changed files with 369 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

167
src/V3AssertNfa.cpp
View File

@ -177,6 +177,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}; }
@ -199,6 +203,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;
@ -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<SvaStateVertex*> 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<AstNodeExpr*>* 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<AstNodeExpr*>* outRequiredStepSrcsp) {
SignalSet computeSignals(LowerCtx& c, std::vector<AstNodeExpr*>* outRequiredStepSrcsp,
std::vector<AstNodeExpr*>* 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<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.
@ -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<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
= 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<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);
}

6
src/V3AstNodeStmt.h
View File

@ -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:

8
src/V3AstNodes.cpp
View File

@ -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]";

30
src/verilog.y
View File

@ -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); }
// // 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}; }

18
test_regress/t/t_cover_sequence.py Executable file
View File

@ -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()

90
test_regress/t/t_cover_sequence.v Normal file
View File

@ -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

18
test_regress/t/t_cover_sequence_unsup.out Normal file
View File

@ -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

18
test_regress/t/t_cover_sequence_unsup.py Executable file
View File

@ -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()

35
test_regress/t/t_cover_sequence_unsup.v Normal file
View File

@ -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

5
test_regress/t/t_debug_emitv.out
View File

@ -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

2
test_regress/t/t_debug_emitv.v
View File

@ -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);

11
test_regress/t/t_sequence_sexpr_unsup.out
View File

@ -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