diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp index 30d82d8ef..7a3c0b1ac 100644 --- a/src/V3Assert.cpp +++ b/src/V3Assert.cpp @@ -91,9 +91,7 @@ public: }; // Lower a sequence used as an event control ('@seq', IEEE 1800-2023 9.4.2.4) into a -// synthesized event plus an internal 'cover sequence' that fires the event on every -// end-of-match. Runs before V3AssertNfa so the sequence's automaton is built by the -// ordinary cover-sequence path; nothing sequence-event-specific reaches V3AssertNfa. +// synthesized event fired by an internal 'cover sequence' on each end-of-match class SeqEventLowerVisitor final : public VNVisitor { // STATE AstNodeModule* m_modp = nullptr; // Current module @@ -605,18 +603,19 @@ class AssertVisitor final : public VNVisitor { bool selfDestruct = false; bool passspGated = false; - if (const AstCover* const snodep = VN_CAST(nodep, Cover)) { + const AstCover* const coverp = VN_CAST(nodep, Cover); + // A sequence event control is not an assertion directive; no assertion control + const bool seqEvent = coverp && coverp->isSeqEvent(); + if (coverp) { ++m_statCover; - if (snodep->isSeqEvent()) { - // Synthesized driver for a sequence used as an event control; keep the - // action (the event fire) with no coverage bucket, independent of - // --coverage. + if (seqEvent) { + // Keep the event-fire action, with no coverage bucket } else if (!v3Global.opt.coverageUser()) { selfDestruct = true; } else { // V3Coverage assigned us a bucket to increment. - AstCoverInc* const covincp = VN_AS(snodep->coverincsp(), CoverInc); - UASSERT_OBJ(covincp, snodep, "Missing AstCoverInc under assertion"); + AstCoverInc* const covincp = VN_AS(coverp->coverincsp(), CoverInc); + UASSERT_OBJ(covincp, coverp, "Missing AstCoverInc under assertion"); covincp->unlinkFrBackWithNext(); // next() might have AstAssign for trace if (message != "") covincp->declp()->comment(message); if (passsp) { @@ -660,7 +659,8 @@ class AssertVisitor final : public VNVisitor { FileLine* const flp = nodep->fileline(); bool passspAlreadyGated = false; if (passsp && VN_IS(passsp, If)) passspAlreadyGated = VN_AS(passsp, If)->user1(); - if (passsp && !passspGated && !passspAlreadyGated && !VN_IS(propExprp, PExpr)) { + if (passsp && !passspGated && !passspAlreadyGated && !VN_IS(propExprp, PExpr) + && !seqEvent) { passsp = newIfAssertPassOn(passsp, nodep->directive(), nodep->userType(), /*vacuous=*/false); } @@ -670,7 +670,7 @@ class AssertVisitor final : public VNVisitor { AstNode* bodysp = assertBody(nodep, propExprp, passsp, failsp); if (disablep) bodysp = new AstIf{flp, new AstLogNot{flp, disablep}, bodysp}; // Add assertOn check last, for better combining - bodysp = newIfAssertOn(bodysp, nodep->directive(), nodep->userType()); + if (!seqEvent) bodysp = newIfAssertOn(bodysp, nodep->directive(), nodep->userType()); if (sentreep) bodysp = new AstAlways{flp, VAlwaysKwd::ALWAYS, sentreep, bodysp}; if (passsp && !passsp->backp()) VL_DO_DANGLING(pushDeletep(passsp), passsp); diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 6a35273a5..4c99c19f2 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -2876,11 +2876,17 @@ class AssertNfaVisitor final : public VNVisitor { bool senTreeOwned = false; // True if we created senTreep locally AstPropSpec* const propSpecp = VN_CAST(assertp->propp(), PropSpec); UASSERT_OBJ(propSpecp, assertp, "Concurrent assertion must have PropSpec"); + AstCover* const coverp = VN_CAST(assertp, Cover); + const bool isCover = coverp != nullptr; + const bool isCoverSeq = coverp && coverp->isCoverSeq(); + // A sequence event control is not an assertion directive; no default + // disable iff, no assertion control + const bool isSeqEvent = coverp && coverp->isSeqEvent(); // Inherit module defaults (IEEE 14.12, 16.15) when assertion has none. if (!propSpecp->sensesp() && m_defaultClockingp) { propSpecp->sensesp(m_defaultClockingp->sensesp()->cloneTree(true)); } - if (!propSpecp->disablep() && m_defaultDisablep) { + if (!propSpecp->disablep() && m_defaultDisablep && !isSeqEvent) { propSpecp->disablep(m_defaultDisablep->condp()->cloneTreePure(true)); } if (!senTreep && propSpecp->sensesp()) { @@ -2892,9 +2898,6 @@ class AssertNfaVisitor final : public VNVisitor { if (!senTreep) return; 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, isCoverSeq}; @@ -2939,13 +2942,16 @@ class AssertNfaVisitor final : public VNVisitor { std::vector perMidSrcs; AstNodeExpr* const alwaysTriggerp - = assertOnCond(flp, assertp->userType(), assertp->directive()); + = isSeqEvent ? new AstConst{flp, AstConst::BitTrue{}} + : assertOnCond(flp, assertp->userType(), assertp->directive()); 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, - assertp->userType(), assertp->directive()); + isSeqEvent ? VAssertType{VAssertType::INTERNAL} : assertp->userType(), + isSeqEvent ? VAssertDirectiveType{VAssertDirectiveType::INTERNAL} + : assertp->directive()); AstSenTree* const perSrcSenTreep = (requiredStepSrcs.size() >= 2) ? senTreep->cloneTree(false) : nullptr; diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index f45df83f3..d9332ff59 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -1466,7 +1466,9 @@ private: iterateAndNextNull(nodep->sensesp()); if (m_senip && m_senip != nodep->sensesp()) nodep->v3warn(E_UNSUPPORTED, "Unsupported: Only one PSL clock allowed per assertion"); - if (!nodep->disablep() && m_defaultDisablep) { + const AstCover* const coverp = VN_CAST(nodep->backp(), Cover); + const bool seqEvent = coverp && coverp->isSeqEvent(); + if (!nodep->disablep() && m_defaultDisablep && !seqEvent) { nodep->disablep(m_defaultDisablep->condp()->cloneTreePure(true)); } m_disablep = nodep->disablep(); diff --git a/src/V3AstNodeStmt.h b/src/V3AstNodeStmt.h index d99c22ddf..fbbceaec7 100644 --- a/src/V3AstNodeStmt.h +++ b/src/V3AstNodeStmt.h @@ -1612,9 +1612,8 @@ 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 - bool m_isSeqEvent = false; // Synthesized to implement a sequence used as an event - // control (IEEE 1800-2023 9.4.2.4); its action fires the - // event on every end-of-match, independent of --coverage + bool m_isSeqEvent = false; // Synthesized for a sequence used as an event control + // (IEEE 1800-2023 9.4.2.4) public: ASTGEN_MEMBERS_AstCover; AstCover(FileLine* fl, AstNode* propp, AstNode* stmtsp, VAssertType type, diff --git a/test_regress/t/t_assert_seq_event.v b/test_regress/t/t_assert_seq_event.v index 1e0311d07..d82078cff 100644 --- a/test_regress/t/t_assert_seq_event.v +++ b/test_regress/t/t_assert_seq_event.v @@ -33,8 +33,7 @@ module t ( endsequence // verilog_format: on - // seq_dc has no clocking event, so it inherits the default clocking and must - // behave identically to the explicitly-clocked seq above. + // seq_dc inherits the default clocking; counts must match seq default clocking @(posedge clk); endclocking @@ -42,13 +41,8 @@ module t ( a ##1 b ##1 c; endsequence - // A sequence used as an `@` event control resumes once per sequence end point - // (IEEE 1800-2023 9.4.2.4). seq_hits/seq_hits2 are two waiters on the same - // multi-cycle sequence; ref_hits is an independent shift-register oracle (end - // point at posedge N when a@N-2, b@N-1, c@N); one_hits is the single-cycle case. - // rng_hits waits on the ranged form: end points at posedge N when b@N and a@N-d - // for any d in 1..3; simultaneous end points resume a blocked waiter once, so - // rng_ref counts cycles with at least one end point. + // ref_hits and rng_ref are independent shift-register oracles; + // simultaneous end points resume a blocked waiter once initial forever begin @seq; seq_hits = seq_hits + 1; @@ -79,9 +73,7 @@ module t ( b1 <= b; end - // a/b/c are spaced to crc[0]/crc[4]/crc[8] -- past the ##2 window -- so the - // left-shift LFSR cannot correlate a@T, b@T+1, c@T+2 into one bit; otherwise - // the multi-cycle end-point machinery would collapse into a triviality. + // a/b/c bit spacing exceeds the ##2 window to decorrelate the LFSR taps always @(posedge clk) begin cyc <= cyc + 1; crc <= {crc[30:0], crc[31] ^ crc[21] ^ crc[1] ^ crc[0]}; diff --git a/test_regress/t/t_assert_seq_event_ctl.py b/test_regress/t/t_assert_seq_event_ctl.py new file mode 100755 index 000000000..e8cdbc78d --- /dev/null +++ b/test_regress/t/t_assert_seq_event_ctl.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.compile(verilator_flags2=['--timing']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_assert_seq_event_ctl.v b/test_regress/t/t_assert_seq_event_ctl.v new file mode 100644 index 000000000..d36f916ec --- /dev/null +++ b/test_regress/t/t_assert_seq_event_ctl.v @@ -0,0 +1,73 @@ +// 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 checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0); +// verilog_format: on + +module t ( + input clk +); + int unsigned crc = 32'h1; + bit a, b, rst; + bit a1; + int cyc; + int hits, ref_hits, one_hits, one_ref; + + // Neither the default disable iff nor $assertoff may suppress a sequence event control + default disable iff (rst); + + // verilog_format: off // verible does not support clocking events inside sequence declarations + sequence seq; + @(posedge clk) a ##1 b; + endsequence + + sequence seq_one; + @(posedge clk) 1; + endsequence + // verilog_format: on + + initial begin + $assertoff; + #300 $assertkill; + end + + initial forever begin + @seq; + hits = hits + 1; + end + initial forever begin + @seq_one; + one_hits = one_hits + 1; + end + + always @(posedge clk) begin + if (a1 && b) ref_hits = ref_hits + 1; + one_ref = one_ref + 1; + a1 <= a; + end + + always @(posedge clk) begin + cyc <= cyc + 1; + crc <= {crc[30:0], crc[31] ^ crc[21] ^ crc[1] ^ crc[0]}; + a <= crc[0]; + b <= crc[4]; + rst <= crc[2]; + end + + always @(negedge clk) begin + if (cyc == 60) $finish; + end + + final begin + `checkd(hits, ref_hits); + `checkd(one_hits, one_ref); + `checkd(hits, 19); // Other simulator: 19 + `checkd(one_hits, 60); // Other simulator: 60 + $write("*-* All Finished *-*\n"); + end +endmodule