diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index a7f2a8c1b..e302be9eb 100644 --- a/src/V3AssertNfa.cpp +++ b/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; diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index 41d980697..f6e0d98f5 100644 --- a/src/V3AstNodeExpr.h +++ b/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 diff --git a/src/V3EmitV.cpp b/src/V3EmitV.cpp index 4201a0ad5..db0798e38 100644 --- a/src/V3EmitV.cpp +++ b/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)) { diff --git a/src/V3Width.cpp b/src/V3Width.cpp index e11285aa6..b323c0b92 100644 --- a/src/V3Width.cpp +++ b/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()) { diff --git a/src/verilog.y b/src/verilog.y index 847a5f828..6d6efea6b 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6673,6 +6673,12 @@ sequence_declarationBody: // 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: // IEEE: property_spec diff --git a/test_regress/t/t_assert_seq_clocking.py b/test_regress/t/t_assert_seq_clocking.py new file mode 100755 index 000000000..23f04b54c --- /dev/null +++ b/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() diff --git a/test_regress/t/t_assert_seq_clocking.v b/test_regress/t/t_assert_seq_clocking.v new file mode 100644 index 000000000..b835acb85 --- /dev/null +++ b/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 diff --git a/test_regress/t/t_assert_seq_clocking_unsup.out b/test_regress/t/t_assert_seq_clocking_unsup.out new file mode 100644 index 000000000..5ab9bb741 --- /dev/null +++ b/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 diff --git a/test_regress/t/t_assert_seq_clocking_unsup.py b/test_regress/t/t_assert_seq_clocking_unsup.py new file mode 100755 index 000000000..38cf36b43 --- /dev/null +++ b/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() diff --git a/test_regress/t/t_assert_seq_clocking_unsup.v b/test_regress/t/t_assert_seq_clocking_unsup.v new file mode 100644 index 000000000..785c67000 --- /dev/null +++ b/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 diff --git a/test_regress/t/t_debug_emitv.out b/test_regress/t/t_debug_emitv.out index 53f8ac53b..8c0ad2245 100644 --- a/test_regress/t/t_debug_emitv.out +++ b/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 diff --git a/test_regress/t/t_debug_emitv.v b/test_regress/t/t_debug_emitv.v index 7d3805052..813d02ea9 100644 --- a/test_regress/t/t_debug_emitv.v +++ b/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