From 951404eac7eeb0b0cc4d8fd88378645ed1945ae2 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Fri, 3 Jul 2026 22:01:16 +0200 Subject: [PATCH] Lower sequence event controls via the cover sequence path --- src/V3Assert.cpp | 67 ++++++++++++++- src/V3Assert.h | 1 + src/V3AssertNfa.cpp | 91 --------------------- src/V3AstNodeStmt.h | 5 ++ src/V3AstNodes.cpp | 2 + src/Verilator.cpp | 1 + test_regress/t/t_assert_seq_event.v | 18 +++- test_regress/t/t_assert_seq_event_unsup.out | 17 ++-- test_regress/t/t_assert_seq_event_unsup.v | 16 ++-- test_regress/t/t_debug_emitv.out | 15 ++++ test_regress/t/t_debug_emitv.v | 11 +++ 11 files changed, 136 insertions(+), 108 deletions(-) diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp index 8d4bf5275..8e7b1bfc2 100644 --- a/src/V3Assert.cpp +++ b/src/V3Assert.cpp @@ -20,6 +20,7 @@ #include "V3AstUserAllocator.h" #include "V3Stats.h" +#include "V3UniqueNames.h" VL_DEFINE_DEBUG_FUNCTIONS; @@ -89,6 +90,61 @@ public: explicit DefaultDisablePropagateVisitor(AstNetlist* nodep) { iterate(nodep); } }; +// 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. +class SeqEventLowerVisitor final : public VNVisitor { + // STATE + AstNodeModule* m_modp = nullptr; // Current module + V3UniqueNames m_names{"__VseqEvent"}; // Synthesized event names + + // VISITORS + void visit(AstNodeModule* nodep) override { + VL_RESTORER(m_modp); + m_modp = nodep; + iterateChildren(nodep); + } + void visit(AstSenItem* nodep) override { + AstFuncRef* const funcrefp = VN_CAST(nodep->sensp(), FuncRef); + if (funcrefp && VN_IS(funcrefp->taskp(), Sequence)) { + FileLine* const flp = nodep->fileline(); + AstVar* const eventp = new AstVar{flp, VVarType::MODULETEMP, m_names.get(nodep), + m_modp->findBasicDType(VBasicDTypeKwd::EVENT)}; + eventp->lifetime(VLifetime::STATIC_EXPLICIT); + m_modp->addStmtsp(eventp); + v3Global.setHasEvents(); + funcrefp->unlinkFrBack(); + nodep->sensp(new AstVarRef{flp, eventp, VAccess::READ}); + // An automatic actual cannot be referenced from the module-level cover + const bool automaticActual = funcrefp->exists([](const AstNodeVarRef* refp) { + return refp->varp() && refp->varp()->lifetime().isAutomatic(); + }); + if (automaticActual) { + nodep->v3warn(E_UNSUPPORTED, "Unsupported: automatic variable as an argument" + " of a sequence used as an event control"); + VN_AS(funcrefp->taskp(), Sequence)->isReferenced(false); + VL_DO_DANGLING(pushDeletep(funcrefp), funcrefp); + return; + } + AstFireEvent* const firep + = new AstFireEvent{flp, new AstVarRef{flp, eventp, VAccess::WRITE}, false}; + AstCover* const coverp + = new AstCover{flp, new AstPropSpec{flp, nullptr, nullptr, funcrefp}, firep, + VAssertType::CONCURRENT}; + coverp->isCoverSeq(true); + coverp->isSeqEvent(true); + m_modp->addStmtsp(coverp); + return; + } + iterateChildren(nodep); + } + void visit(AstNode* nodep) override { iterateChildren(nodep); } + +public: + explicit SeqEventLowerVisitor(AstNetlist* nodep) { iterate(nodep); } +}; + } // namespace void V3AssertCommon::collectDefaultDisable(AstNetlist* nodep) { @@ -96,6 +152,11 @@ void V3AssertCommon::collectDefaultDisable(AstNetlist* nodep) { { DefaultDisablePropagateVisitor{nodep}; } } +void V3AssertCommon::lowerSequenceEvents(AstNetlist* nodep) { + { SeqEventLowerVisitor{nodep}; } + V3Global::dumpCheckGlobalTree("assertseqevent", 0, dumpTreeEitherLevel() >= 3); +} + //###################################################################### // AssertDeFutureVisitor // If any AstFuture, then move all non-future varrefs to be one cycle behind, @@ -546,7 +607,11 @@ class AssertVisitor final : public VNVisitor { bool passspGated = false; if (const AstCover* const snodep = VN_CAST(nodep, Cover)) { ++m_statCover; - if (!v3Global.opt.coverageUser()) { + 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. + } else if (!v3Global.opt.coverageUser()) { selfDestruct = true; } else { // V3Coverage assigned us a bucket to increment. diff --git a/src/V3Assert.h b/src/V3Assert.h index f144688b6..3bda2528e 100644 --- a/src/V3Assert.h +++ b/src/V3Assert.h @@ -27,6 +27,7 @@ class V3AssertCommon final { public: static void collectDefaultDisable(AstNetlist* nodep) VL_MT_DISABLED; + static void lowerSequenceEvents(AstNetlist* nodep) VL_MT_DISABLED; }; class V3Assert final { diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 2f404fed3..b6ec6964f 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -2071,7 +2071,6 @@ class AssertNfaVisitor final : public VNVisitor { V3UniqueNames m_propVarNames{"__Vpropvar"}; // Property-local variable names V3UniqueNames m_disableCntNames{"__VnfaDis"}; // Disable-iff counter names V3UniqueNames m_propTempNames{"__VnfaSampled"}; // Hoisted $sampled(propp) temps - V3UniqueNames m_seqEventNames{"__VseqEvent"}; // Synthesized `@seq` end-point events std::set m_inliningProps; // Recursion guard for inlineNamedProperty // Wire match vertex and mid-window sources for a successful NFA build. @@ -2734,87 +2733,6 @@ class AssertNfaVisitor final : public VNVisitor { UINFO(4, "NFA converted assertion at " << flp << endl); } - // IEEE 1800-2023 9.4.2.4: a sequence used as an event control (`@seq`) - // triggers each time the sequence reaches an end point. Lower it to a - // named-event wait: synthesize an `event`, re-point the sensitivity at it, - // and add a clocked monitor `always @(clk) if (end-of-match) -> event`. The - // match is the NFA terminal-active a `cover sequence` fires on, so the event - // fires on every end point, including overlapping ones. - void buildSeqEventMonitor(AstNodeModule* modp, AstSenItem* senitemp) { - FileLine* const flp = senitemp->fileline(); - AstVar* const eventp = new AstVar{flp, VVarType::MODULETEMP, m_seqEventNames.get(senitemp), - modp->findBasicDType(VBasicDTypeKwd::EVENT)}; - eventp->lifetime(VLifetime::STATIC_EXPLICIT); - modp->addStmtsp(eventp); - v3Global.setHasEvents(); - - AstFuncRef* const funcrefp = VN_AS(senitemp->sensp()->unlinkFrBack(), FuncRef); - senitemp->sensp(new AstVarRef{flp, eventp, VAccess::READ}); - - // Inline the referenced sequence, then any nested refs. Iterate the member - // specp->propp(), not the freshly-new'd specp, to dodge a gcc -Warray-bounds - // false positive. - AstSequence* const seqp = VN_AS(funcrefp->taskp(), Sequence); - AstPropSpec* const specp = new AstPropSpec{flp, nullptr, nullptr, funcrefp}; - inlineSequenceRef(funcrefp, seqp); - inlineAllSequenceRefs(specp->propp()); - if (hoistClockedSeq(specp)) { // Unsupported clocking form, already reported - VL_DO_DANGLING(pushDeletep(specp), specp); - return; - } - // Inherit the module default clocking (IEEE 14.12, 16.15) when the - // sequence has none of its own. - if (!specp->sensesp() && m_defaultClockingp) { - specp->sensesp(m_defaultClockingp->sensesp()->cloneTree(true)); - } - // A clockless sequence with no default clocking has no sampling edge. - if (!specp->sensesp()) { - specp->v3warn(E_UNSUPPORTED, - "Unsupported: '@' event control on a sequence without a clocking event"); - VL_DO_DANGLING(pushDeletep(specp), specp); - return; - } - AstNodeExpr* const bodyp = VN_CAST(specp->propp(), NodeExpr); - UASSERT_OBJ(bodyp, specp, "Sequence body must be an expression"); - AstSenTree* const senTreep = new AstSenTree{flp, specp->sensesp()->cloneTree(true)}; - - // End-of-match: sampled boolean for a single-cycle sequence, NFA - // terminal-active for a multi-cycle one. - AstNodeExpr* matchp = nullptr; - if (!hasMultiCycleExpr(bodyp)) { - matchp = sampled(bodyp->cloneTreePure(false)); - } else { - const PropertyParts parts = decomposeProperty(bodyp); - UASSERT_OBJ(parts.seqExprp, bodyp, "Sequence body must be an expression"); - SvaGraph graph; - SvaNfaBuilder builder{graph, modp, m_propTempNames, /*isCoverSeq=*/false}; - const BuildResult result - = buildAssertionGraph(builder, graph, parts.seqExprp, parts, flp); - if (!result.valid()) { - if (!result.errorEmitted) { - specp->v3warn( - E_UNSUPPORTED, - "Unsupported: this sequence form referenced by an '@' event control"); - } - VL_DO_DANGLING(pushDeletep(senTreep), senTreep); - VL_DO_DANGLING(pushDeletep(specp), specp); - return; - } - wireMatchAndMidSources(graph, result, flp); - AstNodeExpr* const triggerp = new AstConst{flp, AstConst::BitTrue{}}; - matchp = m_loweringp->lower(flp, graph, triggerp, senTreep, result.finalCondp, - /*isCover=*/true); - VL_DO_DANGLING(pushDeletep(triggerp), triggerp); - if (result.finalCondp && !result.finalCondp->backp()) pushDeletep(result.finalCondp); - } - - AstFireEvent* const firep - = new AstFireEvent{flp, new AstVarRef{flp, eventp, VAccess::WRITE}, false}; - modp->addStmtsp(new AstAlways{flp, VAlwaysKwd::ALWAYS, senTreep, - new AstIf{flp, matchp, firep, nullptr}}); - VL_DO_DANGLING(pushDeletep(specp), specp); - } - // VISITORS void visit(AstNodeModule* nodep) override { VL_RESTORER(m_modp); @@ -2832,15 +2750,6 @@ class AssertNfaVisitor final : public VNVisitor { if (nodep->isDefault() && !m_defaultClockingp) m_defaultClockingp = nodep; iterateChildren(nodep); } - void visit(AstSenItem* nodep) override { - if (const AstFuncRef* const funcrefp = VN_CAST(nodep->sensp(), FuncRef)) { - if (VN_IS(funcrefp->taskp(), Sequence)) { - buildSeqEventMonitor(m_modp, nodep); - return; - } - } - iterateChildren(nodep); - } void visit(AstGenBlock* nodep) override { VL_RESTORER(m_defaultDisablep); m_defaultDisablep = nodep->defaultDisablep(); diff --git a/src/V3AstNodeStmt.h b/src/V3AstNodeStmt.h index 25de3ad08..d99c22ddf 100644 --- a/src/V3AstNodeStmt.h +++ b/src/V3AstNodeStmt.h @@ -1612,6 +1612,9 @@ 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 public: ASTGEN_MEMBERS_AstCover; AstCover(FileLine* fl, AstNode* propp, AstNode* stmtsp, VAssertType type, @@ -1622,6 +1625,8 @@ public: void dumpJson(std::ostream& str) const override; bool isCoverSeq() const { return m_isCoverSeq; } void isCoverSeq(bool flag) { m_isCoverSeq = flag; } + bool isSeqEvent() const { return m_isSeqEvent; } + void isSeqEvent(bool flag) { m_isSeqEvent = flag; } }; class AstRestrict final : public AstNodeCoverOrAssert { public: diff --git a/src/V3AstNodes.cpp b/src/V3AstNodes.cpp index ec26f24a9..5f9041ffe 100644 --- a/src/V3AstNodes.cpp +++ b/src/V3AstNodes.cpp @@ -2226,9 +2226,11 @@ void AstNodeCoverOrAssert::dumpJson(std::ostream& str) const { void AstCover::dump(std::ostream& str) const { this->AstNodeCoverOrAssert::dump(str); if (isCoverSeq()) str << " [COVERSEQ]"; + if (isSeqEvent()) str << " [SEQEVENT]"; } void AstCover::dumpJson(std::ostream& str) const { dumpJsonBoolFuncIf(str, isCoverSeq); + dumpJsonBoolFuncIf(str, isSeqEvent); this->AstNodeCoverOrAssert::dumpJson(str); } void AstClocking::dump(std::ostream& str) const { diff --git a/src/Verilator.cpp b/src/Verilator.cpp index b1f0a9af0..b694691dd 100644 --- a/src/Verilator.cpp +++ b/src/Verilator.cpp @@ -261,6 +261,7 @@ static void process() { // Assertion insertion // After we've added block coverage, but before other nasty transforms V3AssertCommon::collectDefaultDisable(v3Global.rootp()); + V3AssertCommon::lowerSequenceEvents(v3Global.rootp()); V3AssertNfa::assertNfaAll(v3Global.rootp()); // V3AssertProp removed: NFA subsumes multi-cycle property lowering. // Unsupported constructs fall through to V3AssertPre. diff --git a/test_regress/t/t_assert_seq_event.v b/test_regress/t/t_assert_seq_event.v index c752f5758..d5aee4987 100644 --- a/test_regress/t/t_assert_seq_event.v +++ b/test_regress/t/t_assert_seq_event.v @@ -14,9 +14,10 @@ module t ( ); int unsigned crc = 32'h1; bit a, b, c; - bit a1, a2, b1; + bit a1, a2, a3, b1; int cyc = 0; int seq_hits = 0, seq_hits2 = 0, ref_hits = 0, one_hits = 0, dc_hits = 0; + int rng_hits = 0, rng_ref = 0; // verilog_format: off // verible does not support clocking events inside sequence declarations sequence seq; @@ -26,6 +27,10 @@ module t ( sequence seq_one; @(posedge clk) a; endsequence + + sequence seq_rng; + @(posedge clk) a ##[1:3] b; + endsequence // verilog_format: on // seq_dc has no clocking event, so it inherits the default clocking and must @@ -41,6 +46,9 @@ module t ( // (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. initial forever begin @seq; seq_hits = seq_hits + 1; @@ -57,9 +65,15 @@ module t ( @seq_dc; dc_hits = dc_hits + 1; end + initial forever begin + @seq_rng; + rng_hits = rng_hits + 1; + end always @(posedge clk) begin if (a2 && b1 && c) ref_hits = ref_hits + 1; + if (b && (a1 || a2 || a3)) rng_ref = rng_ref + 1; + a3 <= a2; a2 <= a1; a1 <= a; b1 <= b; @@ -84,6 +98,8 @@ module t ( `checkd(ref_hits, 14); `checkd(one_hits, 30); `checkd(dc_hits, 14); + `checkd(rng_hits, 26); + `checkd(rng_ref, 26); $write("*-* All Finished *-*\n"); end endmodule diff --git a/test_regress/t/t_assert_seq_event_unsup.out b/test_regress/t/t_assert_seq_event_unsup.out index 3dcb6e752..972eb571c 100644 --- a/test_regress/t/t_assert_seq_event_unsup.out +++ b/test_regress/t/t_assert_seq_event_unsup.out @@ -1,11 +1,14 @@ -%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:28:6: Unsupported: '@' event control on a sequence without a clocking event - 28 | @s_clockless; - | ^~~~~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:25:7: Unsupported: automatic variable as an argument of a sequence used as an event control + : ... note: In instance 't' + 25 | @(s_arg(x)); + | ^~~~~ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:19:5: Unsupported: non-edge clocking event on a sequence; use an edge such as @(posedge clk) - 19 | @(g) a ##1 b; +%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:15:5: Unsupported: non-edge clocking event on a sequence; use an edge such as @(posedge clk) + : ... note: In instance 't' + 15 | @(g) a ##1 b; | ^ -%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:30:6: Unsupported: this sequence form referenced by an '@' event control - 30 | @s_noncons; +%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:29:6: Unsupported: Unclocked assertion + : ... note: In instance 't' + 29 | @s_nonedge; | ^~~~~~~~~ %Error: Exiting due to diff --git a/test_regress/t/t_assert_seq_event_unsup.v b/test_regress/t/t_assert_seq_event_unsup.v index 886611d2e..5367f3c93 100644 --- a/test_regress/t/t_assert_seq_event_unsup.v +++ b/test_regress/t/t_assert_seq_event_unsup.v @@ -11,22 +11,22 @@ module t ( logic g = 0; // verilog_format: off - sequence s_clockless; - a ##1 b; - endsequence - sequence s_nonedge; @(g) a ##1 b; endsequence - sequence s_noncons; - @(posedge clk) a[=2]; + sequence s_arg(x); + @(posedge clk) x; endsequence // verilog_format: on + task automatic f; + bit x = 1; + @(s_arg(x)); + endtask + initial begin - @s_clockless; @s_nonedge; - @s_noncons; + f(); end endmodule diff --git a/test_regress/t/t_debug_emitv.out b/test_regress/t/t_debug_emitv.out index 8c0ad2245..5fcf5c7d7 100644 --- a/test_regress/t/t_debug_emitv.out +++ b/test_regress/t/t_debug_emitv.out @@ -1318,6 +1318,21 @@ module Vt_debug_emitv_sub; endfunction real r; endmodule +module Vt_debug_emitv_seq_event; + input logic clk; + bit a; + bit b; + bit c; + sequence sq; + @(posedge clk) a##1 b##1 c + endsequence + initial begin + begin + + ???? // EVENTCONTROL + @( sq())end + end +endmodule package Vt_debug_emitv_p; logic pkgvar; endpackage diff --git a/test_regress/t/t_debug_emitv.v b/test_regress/t/t_debug_emitv.v index 813d02ea9..7e474c305 100644 --- a/test_regress/t/t_debug_emitv.v +++ b/test_regress/t/t_debug_emitv.v @@ -138,6 +138,7 @@ module t (/*AUTOARG*/ endfunction sub sub(.*); + seq_event seq_event(.*); initial begin int other; @@ -443,6 +444,16 @@ module sub(input logic clk); real r; endmodule +module seq_event(input logic clk); + bit a, b, c; + sequence sq; + @(posedge clk) a ##1 b ##1 c; + endsequence + initial begin + @sq; + end +endmodule + package p; logic pkgvar; endpackage