Support a sequence used as an event control

src/V3AssertNfa.cpp

@@ -2071,6 +2071,7 @@ 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<const AstProperty*> m_inliningProps;  // Recursion guard for inlineNamedProperty
 
     // Wire match vertex and mid-window sources for a successful NFA build.
@@ -2733,6 +2734,85 @@ class AssertNfaVisitor final : public VNVisitor {
         UINFO(4, "NFA converted assertion at " << flp << endl);
     }
 
+    // IEEE 1800-2023 9.4.2.4: a sequence instance used as an event control
+    // (`@seq`) triggers when the sequence reaches its 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 signal is the sequence's NFA terminal-active (the same per-cycle
+    // match a `cover sequence` fires on), so the event fires on every end point,
+    // including overlapping/consecutive attempts -- unlike a bare-sequence assert
+    // whose pass action is suppressed on cycles where a parallel attempt rejects.
+    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();
+
+        // Detach the sequence reference and re-point the wait at the new event.
+        AstFuncRef* const funcrefp = VN_AS(senitemp->sensp()->unlinkFrBack(), FuncRef);
+        senitemp->sensp(new AstVarRef{flp, eventp, VAccess::READ});
+
+        // Reuse the assertion machinery to inline the sequence body and hoist
+        // its clocking event; this also clears the sequence's isReferenced flag.
+        AstPropSpec* const specp = new AstPropSpec{flp, nullptr, nullptr, funcrefp};
+        inlineAllSequenceRefs(specp);
+        if (hoistClockedSeq(specp)) {  // Unsupported clocking form, already reported
+            VL_DO_DANGLING(pushDeletep(specp), specp);
+            return;
+        }
+        // A sequence used as an event must carry its own clocking event; a
+        // clockless sequence is illegal here even under a module default clocking
+        // (confirmed against Questa), unlike one embedded in an assert property.
+        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 signal: a single-cycle sequence matches on the sampled
+        // boolean at the clock; a multi-cycle sequence matches on the NFA
+        // terminal-active (the per-cycle end point a `cover sequence` fires on).
+        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);
@@ -2750,6 +2830,15 @@ 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();

test_regress/t/t_assert_seq_event.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()

test_regress/t/t_assert_seq_event.v

@@ -0,0 +1,80 @@
+// 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, c;
+  bit a1, a2, b1;
+  int cyc = 0;
+  int seq_hits = 0, seq_hits2 = 0, ref_hits = 0, one_hits = 0;
+
+  // verilog_format: off  // verible does not support clocking events inside sequence declarations
+  sequence seq;
+    @(posedge clk) a ##1 b ##1 c;
+  endsequence
+
+  sequence seq_one;
+    @(posedge clk) a;
+  endsequence
+  // verilog_format: on
+
+  // Feature under test: a sequence referenced outside an assertion via the `@`
+  // event control resumes once per sequence end point (IEEE 1800-2023 9.4.2.4).
+  initial forever begin
+    @seq;
+    seq_hits = seq_hits + 1;
+  end
+
+  // A second waiter on the SAME sequence must see exactly the same end points.
+  initial forever begin
+    @seq;
+    seq_hits2 = seq_hits2 + 1;
+  end
+
+  // Single-cycle sequence end point: resumes whenever `a` is sampled true.
+  initial forever begin
+    @seq_one;
+    one_hits = one_hits + 1;
+  end
+
+  // Independent oracle: an end point lands at posedge N when the sampled values
+  // give a at N-2, b at N-1, c at N.
+  always @(posedge clk) begin
+    if (a2 && b1 && c) ref_hits = ref_hits + 1;
+    a2 <= a1;
+    a1 <= a;
+    b1 <= b;
+  end
+
+  // Bits a/b/c are spaced past the ##2 window (crc[0]/crc[4]/crc[8]) so the
+  // left-shift LFSR does not correlate a@T, b@T+1, c@T+2 into one bit; the
+  // multi-cycle end-point machinery is then genuinely exercised.
+  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];
+    c <= crc[8];
+    if (cyc == 60) $finish;
+  end
+
+  // Counts read in final (Postponed) to avoid same-timestep races.
+  // Concrete Verilator counts; Questa: seq_hits=14 ref_hits=14 one_hits=30
+  final begin
+    `checkd(seq_hits, ref_hits);
+    `checkd(seq_hits2, seq_hits);
+    `checkd(seq_hits, 14);
+    `checkd(one_hits, 30);
+    $write("*-* All Finished *-*\n");
+  end
+endmodule

test_regress/t/t_assert_seq_event_unsup.out

@@ -0,0 +1,11 @@
+%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:33:6: Unsupported: '@' event control on a sequence without a clocking event
+   33 |     @s_unclocked;
+      |      ^~~~~~~~~~~
+                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
+%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:24:5: Unsupported: non-edge clocking event on a sequence; use an edge such as @(posedge clk)
+   24 |     @(g) a ##1 b;
+      |     ^
+%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:35:6: Unsupported: this sequence form referenced by an '@' event control
+   35 |     @s_noncons;
+      |      ^~~~~~~~~
+%Error: Exiting due to

test_regress/t/t_assert_seq_event_unsup.py

@@ -0,0 +1,16 @@
+#!/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=['--timing'], fails=True)
+
+test.passes()

test_regress/t/t_assert_seq_event_unsup.v

@@ -0,0 +1,37 @@
+// 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
+);
+  bit a, b;
+  logic g = 0;
+
+  // A module default clocking does NOT make a clockless sequence legal as an
+  // event (confirmed against Questa); s_unclocked below stays E_UNSUPPORTED.
+  default clocking @(posedge clk);
+  endclocking
+
+  // verilog_format: off
+  sequence s_unclocked;
+    a ##1 b;
+  endsequence
+
+  sequence s_nonedge;
+    @(g) a ##1 b;
+  endsequence
+
+  sequence s_noncons;
+    @(posedge clk) a[=2];
+  endsequence
+  // verilog_format: on
+
+  initial begin
+    @s_unclocked;
+    @s_nonedge;
+    @s_noncons;
+  end
+endmodule