Support clocking event on a sequence declaration body

src/V3AssertNfa.cpp

@@ -2014,6 +2014,45 @@ class AssertNfaVisitor final : public VNVisitor {
         VL_DO_DANGLING(pushDeletep(innerPropp), innerPropp);
     }
 
+    // Hoist a leading clocking event (IEEE 1800-2023 16.7:
+    // sequence_expr ::= clocking_event sequence_expr) from the sequence body onto
+    // the enclosing assertion clock. Returns true if E_UNSUPPORTED was emitted.
+    bool hoistClockedSeq(AstPropSpec* specp) {
+        while (AstSClocked* const clockedp = VN_CAST(specp->propp(), SClocked)) {
+            if (specp->sensesp()) {
+                clockedp->v3warn(E_UNSUPPORTED, "Unsupported: multiclocked sequence or property");
+                replaceBodyOnBuildError(specp->fileline(), specp, true);
+                return true;
+            }
+            for (const AstSenItem* sp = clockedp->sensesp(); sp;
+                 sp = VN_CAST(sp->nextp(), SenItem)) {
+                if (!sp->edgeType().anEdge()) {
+                    clockedp->v3warn(E_UNSUPPORTED,
+                                     "Unsupported: non-edge clocking event on a sequence; "
+                                     "use an edge such as @(posedge clk)");
+                    replaceBodyOnBuildError(specp->fileline(), specp, true);
+                    return true;
+                }
+            }
+            specp->sensesp(clockedp->sensesp()->unlinkFrBackWithNext());
+            AstNodeExpr* const bodyp = clockedp->exprp()->unlinkFrBack();
+            clockedp->replaceWith(bodyp);
+            VL_DO_DANGLING(pushDeletep(clockedp), clockedp);
+        }
+        // A clocking event anywhere else in the sequence is not supported.
+        const AstSClocked* nestedp = nullptr;
+        specp->propp()->foreach([&](const AstSClocked* p) {
+            if (!nestedp) nestedp = p;
+        });
+        if (nestedp) {
+            nestedp->v3warn(E_UNSUPPORTED,
+                            "Unsupported: clocking event inside sequence expression");
+            replaceBodyOnBuildError(specp->fileline(), specp, true);
+            return true;
+        }
+        return false;
+    }
+
     // Build the NFA graph for a property body, handling both the antecedent
     // |-> consequent and simple sequence cases. Returns the consequent/body
     // BuildResult (invalid on parse/build failure).
@@ -2189,6 +2228,10 @@ class AssertNfaVisitor final : public VNVisitor {
 
         inlineAllSequenceRefs(assertp->propp());
 
+        if (AstPropSpec* const specp = VN_CAST(assertp->propp(), PropSpec)) {
+            if (hoistClockedSeq(specp)) return;
+        }
+
         AstNode* const propp = assertp->propp();
         if (!hasMultiCycleExpr(propp)) return;
         if (isBareTopLevelUntil(propp)) return;

src/V3AstNodeExpr.h

@@ -2225,6 +2225,25 @@ public:
     bool sameNode(const AstNode* /*samep*/) const override { return true; }
     bool isSystemFunc() const override { return true; }
 };
+class AstSClocked final : public AstNodeExpr {
+    // Sequence expression with an explicit leading clocking event
+    // IEEE 1800-2023 16.7: sequence_expr ::= clocking_event sequence_expr
+    // The clocking event is hoisted to the enclosing assertion clock by V3AssertNfa.
+    // @astgen op1 := sensesp : AstSenItem
+    // @astgen op2 := exprp : AstNodeExpr
+public:
+    AstSClocked(FileLine* fl, AstSenItem* sensesp, AstNodeExpr* exprp)
+        : ASTGEN_SUPER_SClocked(fl) {
+        this->sensesp(sensesp);
+        this->exprp(exprp);
+    }
+    ASTGEN_MEMBERS_AstSClocked;
+    string emitVerilog() override { V3ERROR_NA_RETURN(""); }
+    string emitC() override { V3ERROR_NA_RETURN(""); }
+    bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
+    int instrCount() const override { return widthInstrs(); }
+    bool isMultiCycleSva() const override { return false; }
+};
 class AstSConsRep final : public AstNodeExpr {
     // Consecutive repetition [*N], [*N:M], [+], [*] (IEEE 1800-2023 16.9.2)
     // op1 := exprp -- the repeated expression

src/V3Width.cpp

@@ -1838,6 +1838,22 @@ class WidthVisitor final : public VNVisitor {
             nodep->dtypeSetBit();
         }
     }
+    void visit(AstSClocked* nodep) override {
+        VL_RESTORER(m_underSExpr);
+        m_underSExpr = true;
+        m_hasSExpr = true;
+        assertAtExpr(nodep);
+        if (m_vup->prelim()) {
+            // Width each clock expression directly; the senitem chain is hoisted to
+            // the assertion clock by V3AssertNfa, where it is fully processed.
+            for (AstSenItem* senp = nodep->sensesp(); senp;
+                 senp = VN_CAST(senp->nextp(), SenItem)) {
+                userIterateAndNext(senp->sensp(), WidthVP{SELF, BOTH}.p());
+            }
+            iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH);
+            nodep->dtypeSetBit();
+        }
+    }
     void visit(AstURandomRange* nodep) override {
         assertAtExpr(nodep);
         if (m_vup->prelim()) {

src/verilog.y

@@ -6653,6 +6653,12 @@ sequence_declarationBody<nodep>:  // IEEE: part of sequence_declaration
         |       assertion_variable_declarationList sexpr ';'    { $$ = addNextNull($1, $2); }
         |       sexpr                                   { $$ = $1; }
         |       sexpr ';'                               { $$ = $1; }
+        //                      // IEEE: clocking_event sequence_expr (16.7)
+        //                      // A leading clocking event on a named sequence body.
+        |       '@' '(' event_expression ')' sexpr      { $$ = new AstSClocked{$1, $3, $5}; }
+        |       '@' '(' event_expression ')' sexpr ';'  { $$ = new AstSClocked{$1, $3, $5}; }
+        |       '@' senitemVar sexpr                    { $$ = new AstSClocked{$1, $2, $3}; }
+        |       '@' senitemVar sexpr ';'                { $$ = new AstSClocked{$1, $2, $3}; }
         ;
 
 property_spec<propSpecp>:               // IEEE: property_spec

test_regress/t/t_assert_seq_clocking.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=['--assert', '--timing'])
+
+test.execute()
+
+test.passes()

test_regress/t/t_assert_seq_clocking.v

@@ -0,0 +1,55 @@
+// 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
+module t (
+    input clk
+);
+  int unsigned crc = 32'h1;
+  bit a, b;
+  int cyc = 0;
+  int fails_single = 0;
+  int fails_multi = 0;
+
+  // Single-cycle clocked sequence body (IEEE 1800-2023 16.7).
+  sequence s_single;
+    @(posedge clk) a;
+  endsequence
+
+  // Multi-cycle clocked sequence body.
+  sequence s_multi;
+    @(posedge clk) (a ##1 b);
+  endsequence
+
+  // Declared but never referenced; must not reach codegen.
+  sequence s_unused;
+    @(posedge clk) b;
+  endsequence
+
+  ap_single: assert property (s_single) else fails_single = fails_single + 1;
+  ap_multi: assert property (s_multi) else fails_multi = fails_multi + 1;
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    crc <= {crc[30:0], crc[31] ^ crc[21] ^ crc[1] ^ crc[0]};
+    a <= crc[0];
+    b <= crc[1];
+    if (cyc == 40) $finish;
+  end
+
+  // Counts read in final (Postponed) to avoid same-timestep races.
+  // Concrete Verilator counts; cross-checked equal in Questa 2022.3
+  // on the self-clocked equivalent (same CRC stimulus).
+  // Questa: fails_single=17 fails_multi=17
+  final begin
+    if (fails_single == 17 && fails_multi == 17) begin
+      $write("*-* All Finished *-*\n");
+    end else begin
+      $write("FAILED fails_single=%0d fails_multi=%0d\n", fails_single, fails_multi);
+      $stop;
+    end
+  end
+endmodule

test_regress/t/t_assert_seq_clocking_bad.out

@@ -0,0 +1,22 @@
+%Error-UNSUPPORTED: t/t_assert_seq_clocking_bad.v:15:5: Unsupported: multiclocked sequence or property
+                                                      : ... note: In instance 't'
+   15 |     @(posedge clk) a;
+      |     ^
+                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
+%Error-UNSUPPORTED: t/t_assert_seq_clocking_bad.v:19:5: Unsupported: clocking event inside sequence expression
+                                                      : ... note: In instance 't'
+   19 |     @(posedge clk) b;
+      |     ^
+%Error-UNSUPPORTED: t/t_assert_seq_clocking_bad.v:23:5: Unsupported: non-edge clocking event on a sequence; use an edge such as @(posedge clk)
+                                                      : ... note: In instance 't'
+   23 |     @clk a;
+      |     ^
+%Error-UNSUPPORTED: t/t_assert_seq_clocking_bad.v:30:3: Unsupported: Unclocked assertion
+                                                      : ... note: In instance 't'
+   30 |   assert property (s_nest ##1 a);
+      |   ^~~~~~
+%Error-UNSUPPORTED: t/t_assert_seq_clocking_bad.v:33:3: Unsupported: Unclocked assertion
+                                                      : ... note: In instance 't'
+   33 |   assert property (s_level);
+      |   ^~~~~~
+%Error: Exiting due to

test_regress/t/t_assert_seq_clocking_bad.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('linter')
+
+test.lint(fails=True, expect_filename=test.golden_filename)
+
+test.passes()

test_regress/t/t_assert_seq_clocking_bad.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
+
+// verilog_format: off
+module t (
+    input clk,
+    input clk2
+);
+  logic a, b;
+
+  sequence s_multi;
+    @(posedge clk) a;
+  endsequence
+
+  sequence s_nest;
+    @(posedge clk) b;
+  endsequence
+
+  sequence s_level;
+    @clk a;
+  endsequence
+
+  // Multiclocked: explicit assertion clock differs from the sequence clock.
+  assert property (@(posedge clk2) s_multi);
+
+  // Clocking event nested inside a larger sequence expression.
+  assert property (s_nest ##1 a);
+
+  // Non-edge clocking event on a sequence.
+  assert property (s_level);
+
+endmodule