Support clocking event on a sequence declaration body (#7598) (#7793)

Fixes #7598.

src/V3AssertNfa.cpp

@@ -2162,6 +2162,43 @@ class AssertNfaVisitor final : public VNVisitor {
         VL_DO_DANGLING(pushDeletep(innerPropp), innerPropp);
     }
 
+    // Hoist a leading clocking event (IEEE 1800-2023 16.7):
+    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).
@@ -2337,6 +2374,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,23 @@ 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(false); }
+};
 class AstSConsRep final : public AstNodeExpr {
     // Consecutive repetition [*N], [*N:M], [+], [*] (IEEE 1800-2023 16.9.2)
     // op1 := exprp -- the repeated expression

src/V3EmitV.cpp

@@ -1142,6 +1142,13 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
         puts(") ");
         iterateConst(nodep->propp());
     }
+    void visit(AstSClocked* nodep) override {
+        puts("@(");
+        iterateConst(nodep->sensesp());
+        puts(") ");
+        iterateConst(nodep->exprp());
+        puts("\n");
+    }
     void visit(AstPropAlways* nodep) override {
         puts(nodep->isStrong() ? "s_always" : "always");
         if (!VN_IS(nodep->loBoundp(), Unbounded) || !VN_IS(nodep->hiBoundp(), Unbounded)) {

src/V3Width.cpp

@@ -1837,6 +1837,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

@@ -6673,6 +6673,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,53 @@
+// 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;
+  int cyc = 0;
+  int fails_single = 0;
+  int fails_multi = 0;
+
+  // verilog_format: off  // verible does not support clocking events inside sequence declarations
+  sequence s_single;
+    @(posedge clk) a
+  endsequence
+
+  sequence s_multi;
+    @(posedge clk) (a ##1 b);
+  endsequence
+
+  sequence s_unused;
+    @(posedge clk) b;
+  endsequence
+  // verilog_format: on
+
+  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; Questa: fails_single=17 fails_multi=17
+  final begin
+    `checkd(fails_single, 17);
+    `checkd(fails_multi, 17);
+    $write("*-* All Finished *-*\n");
+  end
+endmodule

test_regress/t/t_assert_seq_clocking_unsup.out

@@ -0,0 +1,30 @@
+%Error-UNSUPPORTED: t/t_assert_seq_clocking_unsup.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_unsup.v:19:5: Unsupported: clocking event inside sequence expression
+                                                        : ... note: In instance 't'
+   19 |     @(posedge clk) b;
+      |     ^
+%Error-UNSUPPORTED: t/t_assert_seq_clocking_unsup.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_unsup.v:27:5: Unsupported: non-edge clocking event on a sequence; use an edge such as @(posedge clk)
+                                                        : ... note: In instance 't'
+   27 |     @clk a
+      |     ^
+%Error-UNSUPPORTED: t/t_assert_seq_clocking_unsup.v:32:3: Unsupported: Unclocked assertion
+                                                        : ... note: In instance 't'
+   32 |   assert property (s_nest ##1 a);
+      |   ^~~~~~
+%Error-UNSUPPORTED: t/t_assert_seq_clocking_unsup.v:33:3: Unsupported: Unclocked assertion
+                                                        : ... note: In instance 't'
+   33 |   assert property (s_level);
+      |   ^~~~~~
+%Error-UNSUPPORTED: t/t_assert_seq_clocking_unsup.v:34:3: Unsupported: Unclocked assertion
+                                                        : ... note: In instance 't'
+   34 |   assert property (s_level2);
+      |   ^~~~~~
+%Error: Exiting due to

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

test_regress/t/t_assert_seq_clocking_unsup.v

@@ -0,0 +1,36 @@
+// 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,
+  input clk2
+);
+  logic a, b;
+
+  // verilog_format: off
+  sequence s_multi;
+    @(posedge clk) a;
+  endsequence
+
+  sequence s_nest;
+    @(posedge clk) b;
+  endsequence
+
+  sequence s_level;
+    @clk a;
+  endsequence
+
+  sequence s_level2;
+    @clk a
+  endsequence
+  // verilog_format: on
+
+  assert property (@(posedge clk2) s_multi);
+  assert property (s_nest ##1 a);
+  assert property (s_level);
+  assert property (s_level2);
+
+endmodule

test_regress/t/t_debug_emitv.out

@@ -364,6 +364,16 @@ module Vt_debug_emitv_t;
             release sum;
         end
     end
+    sequence s_clocked;
+    @(posedge clk) in
+    endsequence
+    begin : assert_seq_clocked
+        assert property ( s_clocked()
+        ) begin
+        end
+        else begin
+        end
+    end
     property p;
     @(posedge clk) ##1 sum[0]
     endproperty

test_regress/t/t_debug_emitv.v

@@ -286,6 +286,14 @@ module t (/*AUTOARG*/
     release sum;
   end
 
+  // verilog_format: off  // verible does not support clocking events inside sequence declarations
+  sequence s_clocked;
+    @(posedge clk) in
+  endsequence
+  // verilog_format: on
+
+  assert_seq_clocked: assert property (s_clocked);
+
   property p;
     @(posedge clk) ##1 sum[0]
   endproperty