From b0d58bbcefd827c7459040931c1bbaeba61636ff Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Mon, 11 May 2026 13:07:51 +0200 Subject: [PATCH] Support SVA goto repetition with range `[->M:N]` (#7569) --- src/V3AssertNfa.cpp | 40 +++++++++--- src/V3AssertPre.cpp | 15 +++++ src/V3AstNodeExpr.h | 32 ++++++++-- src/V3Width.cpp | 36 +++++++++++ src/verilog.y | 12 ++-- test_regress/t/t_assert_goto_rep.v | 45 +++++++++---- test_regress/t/t_assert_rep_range_bad.out | 50 +++++++++++++++ test_regress/t/t_assert_rep_range_bad.py | 16 +++++ test_regress/t/t_assert_rep_range_bad.v | 63 +++++++++++++++++++ test_regress/t/t_assert_rep_range_unsup.out | 10 +++ test_regress/t/t_assert_rep_range_unsup.py | 16 +++++ test_regress/t/t_assert_rep_range_unsup.v | 23 +++++++ .../t/t_assert_rep_range_zero_min_unsup.out | 10 +++ .../t/t_assert_rep_range_zero_min_unsup.py | 16 +++++ .../t/t_assert_rep_range_zero_min_unsup.v | 28 +++++++++ test_regress/t/t_sequence_sexpr_unsup.out | 35 ++++------- test_regress/t/t_sequence_sexpr_unsup.v | 18 ------ 17 files changed, 397 insertions(+), 68 deletions(-) create mode 100644 test_regress/t/t_assert_rep_range_bad.out create mode 100755 test_regress/t/t_assert_rep_range_bad.py create mode 100644 test_regress/t/t_assert_rep_range_bad.v create mode 100644 test_regress/t/t_assert_rep_range_unsup.out create mode 100755 test_regress/t/t_assert_rep_range_unsup.py create mode 100644 test_regress/t/t_assert_rep_range_unsup.v create mode 100644 test_regress/t/t_assert_rep_range_zero_min_unsup.out create mode 100755 test_regress/t/t_assert_rep_range_zero_min_unsup.py create mode 100644 test_regress/t/t_assert_rep_range_zero_min_unsup.v diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 6c0a85ed4..cc27c2a37 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -593,15 +593,20 @@ class SvaNfaBuilder final { BuildResult buildGotoRep(AstSGotoRep* repp, SvaStateVertex* entryVtxp) { FileLine* const flp = repp->fileline(); AstNodeExpr* const exprp = repp->exprp(); - const int n = getConstInt(repp->countp()); - if (n <= 0) return BuildResult::fail(); + const int minN = getConstInt(repp->countp()); + if (minN <= 0) return BuildResult::fail(); + const bool hasMax = repp->maxCountp() != nullptr; + const int maxN = hasMax ? getConstInt(repp->maxCountp()) : minN; + UASSERT_OBJ(maxN >= minN, repp, "GotoRep range max < min (V3Width invariant)"); - // Wait + match per iter -> 2n sites. NOT($sampled(x)) matches + // Wait + match per iter -> 2 sites per iteration; range form needs + // sites for every iteration in [0..maxN). NOT($sampled(x)) matches // $sampled(NOT(x)) at the value level (IEEE 1800-2023 16.9.9); // purity is enforced uniformly via cloneTreePure inside sampledRefOrClone. - AstVar* const hoistVarp = tryHoistSampled(exprp, flp, 2 * n); + AstVar* const hoistVarp = tryHoistSampled(exprp, flp, 2 * maxN); SvaStateVertex* currentp = entryVtxp; - for (int i = 0; i < n; ++i) { + // Build minN match-wait chains to reach the first accept point. + for (int i = 0; i < minN; ++i) { SvaStateVertex* const waitVtxp = scopedCreateVertex(); // Edge (not Link) for all iterations: IEEE expansion ##1 before each // match. A Link at i==0 was wrong -- it allowed same-cycle matching @@ -614,9 +619,30 @@ class SvaNfaBuilder final { guardedLink(waitVtxp, matchVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp); currentp = matchVtxp; } - currentp->m_isUnbounded = true; // [->N] waits unboundedly + if (!hasMax) { + currentp->m_isUnbounded = true; // [->N] waits unboundedly + m_inUnboundedScope = true; + return {currentp, nullptr, {}}; + } + // [->M:N]: every match in [M..N] feeds a shared merge vertex so the + // property can accept at any count in that range. Mirrors + // buildConsRep's range fan-out. + SvaStateVertex* const mergeVtxp = scopedCreateVertex(); + guardedLink(currentp, mergeVtxp, flp); // accept at match_M + for (int i = minN; i < maxN; ++i) { + SvaStateVertex* const waitVtxp = scopedCreateVertex(); + guardedEdge(currentp, waitVtxp, flp); + AstNodeExpr* const waitCondp + = new AstNot{flp, sampledRefOrClone(hoistVarp, exprp, flp)}; + guardedEdge(waitVtxp, waitVtxp, waitCondp, flp); + SvaStateVertex* const matchVtxp = scopedCreateVertex(); + guardedLink(waitVtxp, matchVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp); + guardedLink(matchVtxp, mergeVtxp, flp); // accept at match_(i+1) + currentp = matchVtxp; + } + mergeVtxp->m_isUnbounded = true; // [->M:N] still has unbounded waits between matches m_inUnboundedScope = true; - return {currentp, nullptr, {}}; + return {mergeVtxp, nullptr, {}}; } // Build merge vertex for SOr / LogOr: both branches feed into one vertex. diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 4b4ff8424..de2b4ae3a 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -1082,6 +1082,19 @@ private: return new AstPExpr{flp, beginp, exprp->findBitDType()}; } + // Reject [=M:N] nonconsecutive range that reached V3AssertPre. + // [->M:N] is fully handled upstream (NFA path); only [=M:N] still lands + // here because AstSNonConsRep lowering is not yet implemented there. + // Replaces the node with BitFalse so lowering continues after the warning. + bool rejectNonconsecRange(AstNode* nodep, AstNodeExpr* maxCountp) { + if (!maxCountp) return false; + nodep->v3warn(E_UNSUPPORTED, "Unsupported: [=M:N] nonconsecutive range repetition" + " (IEEE 1800-2023 16.9.2)"); + nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}}); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + return true; + } + void visit(AstSGotoRep* nodep) override { // Standalone goto rep (not inside implication antecedent) iterateChildren(nodep); @@ -1097,6 +1110,7 @@ private: void visit(AstSNonConsRep* nodep) override { // Standalone nonconsecutive rep (not inside implication antecedent) iterateChildren(nodep); + if (rejectNonconsecRange(nodep, nodep->maxCountp())) return; FileLine* const flp = nodep->fileline(); AstNodeExpr* countp = nodep->countp()->unlinkFrBack(); if (!validateRepCount(nodep, countp)) return; @@ -1154,6 +1168,7 @@ private: if (AstSNonConsRep* const ncrp = VN_CAST(nodep->lhsp(), SNonConsRep)) { iterateChildren(ncrp); iterateAndNextNull(nodep->rhsp()); + if (rejectNonconsecRange(nodep, ncrp->maxCountp())) return; FileLine* const flp = nodep->fileline(); AstNodeExpr* countp = ncrp->countp()->unlinkFrBack(); if (!validateRepCount(nodep, countp)) return; diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index a447b707a..ea75a24b9 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -2380,16 +2380,28 @@ public: bool isSystemFunc() const override { return true; } }; class AstSGotoRep final : public AstNodeExpr { - // Goto repetition: expr [-> count] + // Goto repetition: expr [-> count] or [-> count : maxCount] // IEEE 1800-2023 16.9.2 + // op1 := exprp -- the repeated expression + // op2 := countp -- min repetition count (M); positive constant after V3Width + // op3 := maxCountp -- max repetition count (N); nullptr for exact [->N] // @astgen op1 := exprp : AstNodeExpr // @astgen op2 := countp : AstNodeExpr + // @astgen op3 := maxCountp : Optional[AstNodeExpr] public: - explicit AstSGotoRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp) + // Exact [->N] + AstSGotoRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp) : ASTGEN_SUPER_SGotoRep(fl) { this->exprp(exprp); this->countp(countp); } + // Range [->M:N] + AstSGotoRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp, AstNodeExpr* maxCountp) + : ASTGEN_SUPER_SGotoRep(fl) { + this->exprp(exprp); + this->countp(countp); + this->maxCountp(maxCountp); + } ASTGEN_MEMBERS_AstSGotoRep; string emitVerilog() override { V3ERROR_NA_RETURN(""); } string emitC() override { V3ERROR_NA_RETURN(""); } @@ -2397,16 +2409,28 @@ public: bool isMultiCycleSva() const override { return true; } }; class AstSNonConsRep final : public AstNodeExpr { - // Nonconsecutive repetition: expr [= count] + // Nonconsecutive repetition: expr [= count] or [= count : maxCount] // IEEE 1800-2023 16.9.2 + // op1 := exprp -- the repeated expression + // op2 := countp -- min repetition count (M); positive constant after V3Width + // op3 := maxCountp -- max repetition count (N); nullptr for exact [=N] // @astgen op1 := exprp : AstNodeExpr // @astgen op2 := countp : AstNodeExpr + // @astgen op3 := maxCountp : Optional[AstNodeExpr] public: - explicit AstSNonConsRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp) + // Exact [=N] + AstSNonConsRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp) : ASTGEN_SUPER_SNonConsRep(fl) { this->exprp(exprp); this->countp(countp); } + // Range [=M:N] + AstSNonConsRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp, AstNodeExpr* maxCountp) + : ASTGEN_SUPER_SNonConsRep(fl) { + this->exprp(exprp); + this->countp(countp); + this->maxCountp(maxCountp); + } ASTGEN_MEMBERS_AstSNonConsRep; string emitVerilog() override { V3ERROR_NA_RETURN(""); } string emitC() override { V3ERROR_NA_RETURN(""); } diff --git a/src/V3Width.cpp b/src/V3Width.cpp index d82ca6717..036a95ae6 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -1745,6 +1745,7 @@ class WidthVisitor final : public VNVisitor { if (m_vup->prelim()) { iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH); userIterateAndNext(nodep->countp(), WidthVP{SELF, BOTH}.p()); + if (nodep->maxCountp()) widthCheckGotoRepRange(nodep, "Goto"); nodep->dtypeSetBit(); } } @@ -1753,9 +1754,44 @@ class WidthVisitor final : public VNVisitor { if (m_vup->prelim()) { iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH); userIterateAndNext(nodep->countp(), WidthVP{SELF, BOTH}.p()); + if (nodep->maxCountp()) widthCheckGotoRepRange(nodep, "Nonconsecutive"); nodep->dtypeSetBit(); } } + // IEEE 1800-2023 16.9.2 range-form bound validation for goto/nonconsec. + // Parent accessors are re-fetched after constifyParamsEdit because that + // call can replace the node in-tree (Lesson: AstSConsRep visitor pattern). + // Templated to cover AstSGotoRep and AstSNonConsRep uniformly. + template + void widthCheckGotoRepRange(T_Rep* nodep, const char* kind) { + userIterateAndNext(nodep->maxCountp(), WidthVP{SELF, BOTH}.p()); + V3Const::constifyParamsEdit(nodep->countp()); + V3Const::constifyParamsEdit(nodep->maxCountp()); + const AstConst* const minConstp = VN_CAST(nodep->countp(), Const); + const AstConst* const maxConstp = VN_CAST(nodep->maxCountp(), Const); + if (!minConstp || !maxConstp) { + nodep->v3error(std::string{kind} + + " repetition range bounds must be constant expressions" + " (IEEE 1800-2023 16.9.2)"); + return; + } + if (minConstp->toSInt() < 0) { + nodep->v3error(std::string{kind} + + " repetition range min count must be non-negative" + " (IEEE 1800-2023 16.9.2)"); + return; + } + if (maxConstp->toSInt() < minConstp->toSInt()) { + nodep->v3error(std::string{kind} + + " repetition range max count must be >= min count" + " (IEEE 1800-2023 16.9.2)"); + return; + } + if (minConstp->isZero()) { + nodep->v3warn(E_UNSUPPORTED, std::string{"Unsupported: zero min count in "} + kind + + " repetition range (IEEE 1800-2023 16.9.2)"); + } + } void visit(AstSThroughout* nodep) override { m_hasSExpr = true; assertAtExpr(nodep); diff --git a/src/verilog.y b/src/verilog.y index f8013b962..627e457e9 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6860,15 +6860,15 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg // // IEEE: goto_repetition (single count form) | ~p~sexpr/*sexpression_or_dist*/ yP_BRAMINUSGT constExpr ']' { $$ = new AstSGotoRep{$2, $1, $3}; } - // // IEEE: goto_repetition (range form -- unsupported) + // // IEEE: goto_repetition (range form) | ~p~sexpr/*sexpression_or_dist*/ yP_BRAMINUSGT constExpr ':' constExpr ']' - { $$ = $1; BBUNSUP($2, "Unsupported: [-> range goto repetition"); DEL($3); DEL($5); } + { $$ = new AstSGotoRep{$2, $1, $3, $5}; } // // IEEE: nonconsecutive_repetition (single count form) | ~p~sexpr/*sexpression_or_dist*/ yP_BRAEQ constExpr ']' { $$ = new AstSNonConsRep{$2, $1, $3}; } - // // IEEE: nonconsecutive_repetition (range form -- unsupported) + // // IEEE: nonconsecutive_repetition (range form) | ~p~sexpr/*sexpression_or_dist*/ yP_BRAEQ constExpr ':' constExpr ']' - { $$ = $1; BBUNSUP($2, "Unsupported: [= range nonconsecutive repetition"); DEL($3); DEL($5); } + { $$ = new AstSNonConsRep{$2, $1, $3, $5}; } // // All boolean_abbrev forms are now handled above: // // [*N], [*N:M], [+], [*] via AstSConsRep // // [->N], [->M:N] via AstSGotoRep @@ -6956,8 +6956,8 @@ sequence_match_item: // ==IEEE: sequence_match_item // boolean_abbrev -- all forms now handled directly in sexpr rule: // // IEEE: consecutive_repetition -- [*N], [*N:M], [+], [*] via AstSConsRep -// // IEEE: goto_repetition -- [->N] via AstSGotoRep, [->M:N] unsupported -// // IEEE: nonconsecutive_repetition -- [=N] via AstSNonConsRep, [=M:N] unsupported +// // IEEE: goto_repetition -- [->N], [->M:N] via AstSGotoRep +// // IEEE: nonconsecutive_repetition -- [=N], [=M:N] via AstSNonConsRep //************************************************ // Covergroup diff --git a/test_regress/t/t_assert_goto_rep.v b/test_regress/t/t_assert_goto_rep.v index 74d4ab6a1..f926a3b5b 100644 --- a/test_regress/t/t_assert_goto_rep.v +++ b/test_regress/t/t_assert_goto_rep.v @@ -27,27 +27,46 @@ module t ( int count_fail2 = 0; int count_fail3 = 0; int count_fail4 = 0; + int count_fail5 = 0; + int count_fail6 = 0; + int count_fail7 = 0; + int count_fail8 = 0; // Test 1: a[->2] |-> b (overlapping implication, 2 non-consecutive occurrences) - assert property (@(posedge clk) a[->2] |-> b) - else count_fail1 <= count_fail1 + 1; + assert property (@(posedge clk) a [-> 2] |-> b) + else count_fail1 <= count_fail1 + 1; // Test 2: a[->1] |-> c (single occurrence, overlapping) - assert property (@(posedge clk) a[->1] |-> c) - else count_fail2 <= count_fail2 + 1; + assert property (@(posedge clk) a [-> 1] |-> c) + else count_fail2 <= count_fail2 + 1; // Test 3: a[->3] |=> d (3 occurrences, non-overlapping implication) - assert property (@(posedge clk) a[->3] |=> d) - else count_fail3 <= count_fail3 + 1; + assert property (@(posedge clk) a [-> 3] |=> d) + else count_fail3 <= count_fail3 + 1; // Test 4: standalone goto rep (no implication) -- exercises standalone visitor - assert property (@(posedge clk) b[->2]) - else count_fail4 <= count_fail4 + 1; + assert property (@(posedge clk) b [-> 2]) + else count_fail4 <= count_fail4 + 1; + + // Test 5: a[->1:2] |-> b -- basic range, NFA merge fan-out (M=1, N=2). + assert property (@(posedge clk) a [-> 1: 2] |-> b) + else count_fail5 <= count_fail5 + 1; + + // Test 6: a[->1:3] |-> c -- wider range. + assert property (@(posedge clk) a [-> 1: 3] |-> c) + else count_fail6 <= count_fail6 + 1; + + // Test 7: a[->2:5] |=> d -- non-overlapping implication, min > 1. + assert property (@(posedge clk) a [-> 2: 5] |=> d) + else count_fail7 <= count_fail7 + 1; + + // Test 8: a[->1:4] |-> b -- wider overlapping range. + assert property (@(posedge clk) a [-> 1: 4] |-> b) + else count_fail8 <= count_fail8 + 1; always @(posedge clk) begin `ifdef TEST_VERBOSE - $write("[%0t] cyc==%0d crc=%x a=%b b=%b c=%b d=%b\n", - $time, cyc, crc, a, b, c, d); + $write("[%0t] cyc==%0d crc=%x a=%b b=%b c=%b d=%b\n", $time, cyc, crc, a, b, c, d); `endif cyc <= cyc + 1; crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; @@ -59,7 +78,11 @@ module t ( `checkd(count_fail1, 20); // Questa: 20 `checkd(count_fail2, 25); // Questa: 25 `checkd(count_fail3, 19); // Questa: 19 - `checkd(count_fail4, 0); // Questa: 0 + `checkd(count_fail4, 0); // Questa: 0 + `checkd(count_fail5, 20); // Questa: 20 + `checkd(count_fail6, 25); // Questa: 25 + `checkd(count_fail7, 20); // Questa: 20 + `checkd(count_fail8, 20); // Questa: 20 $write("*-* All Finished *-*\n"); $finish; end diff --git a/test_regress/t/t_assert_rep_range_bad.out b/test_regress/t/t_assert_rep_range_bad.out new file mode 100644 index 000000000..6190821f0 --- /dev/null +++ b/test_regress/t/t_assert_rep_range_bad.out @@ -0,0 +1,50 @@ +%Error: t/t_assert_rep_range_bad.v:15:35: Expecting expression to be constant, but variable isn't const: 'n' + : ... note: In instance 't' + 15 | @(posedge clk) a |-> b [-> 1: n]; + | ^ + ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. +%Error: t/t_assert_rep_range_bad.v:15:28: Goto repetition range bounds must be constant expressions (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 15 | @(posedge clk) a |-> b [-> 1: n]; + | ^~~ +%Error: t/t_assert_rep_range_bad.v:19:34: Expecting expression to be constant, but variable isn't const: 'n' + : ... note: In instance 't' + 19 | @(posedge clk) a |-> b [= 1: n]; + | ^ +%Error: t/t_assert_rep_range_bad.v:19:28: Nonconsecutive repetition range bounds must be constant expressions (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 19 | @(posedge clk) a |-> b [= 1: n]; + | ^~ +%Error: t/t_assert_rep_range_bad.v:23:32: Expecting expression to be constant, but variable isn't const: 'n' + : ... note: In instance 't' + 23 | @(posedge clk) a |-> b [-> n: 2]; + | ^ +%Error: t/t_assert_rep_range_bad.v:23:28: Goto repetition range bounds must be constant expressions (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 23 | @(posedge clk) a |-> b [-> n: 2]; + | ^~~ +%Error: t/t_assert_rep_range_bad.v:27:31: Expecting expression to be constant, but variable isn't const: 'n' + : ... note: In instance 't' + 27 | @(posedge clk) a |-> b [= n: 2]; + | ^ +%Error: t/t_assert_rep_range_bad.v:27:28: Nonconsecutive repetition range bounds must be constant expressions (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 27 | @(posedge clk) a |-> b [= n: 2]; + | ^~ +%Error: t/t_assert_rep_range_bad.v:31:28: Goto repetition range max count must be >= min count (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 31 | @(posedge clk) a |-> b [-> 3: 1]; + | ^~~ +%Error: t/t_assert_rep_range_bad.v:35:28: Nonconsecutive repetition range max count must be >= min count (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 35 | @(posedge clk) a |-> b [= 3: 1]; + | ^~ +%Error: t/t_assert_rep_range_bad.v:39:28: Goto repetition range min count must be non-negative (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 39 | @(posedge clk) a |-> b [-> -1: 2]; + | ^~~ +%Error: t/t_assert_rep_range_bad.v:43:28: Nonconsecutive repetition range min count must be non-negative (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 43 | @(posedge clk) a |-> b [= -1: 2]; + | ^~ +%Error: Exiting due to diff --git a/test_regress/t/t_assert_rep_range_bad.py b/test_regress/t/t_assert_rep_range_bad.py new file mode 100755 index 000000000..38cf36b43 --- /dev/null +++ b/test_regress/t/t_assert_rep_range_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() diff --git a/test_regress/t/t_assert_rep_range_bad.v b/test_regress/t/t_assert_rep_range_bad.v new file mode 100644 index 000000000..b9a73f748 --- /dev/null +++ b/test_regress/t/t_assert_rep_range_bad.v @@ -0,0 +1,63 @@ +// 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; + bit clk; + bit a; + bit b; + int n; + + // Goto non-constant max bound. + property p_goto_nonconst; + @(posedge clk) a |-> b [-> 1: n]; + endproperty + // Nonconsecutive non-constant max bound. + property p_nc_nonconst; + @(posedge clk) a |-> b [= 1: n]; + endproperty + // Goto non-constant min bound. + property p_goto_min_nonconst; + @(posedge clk) a |-> b [-> n: 2]; + endproperty + // Nonconsecutive non-constant min bound. + property p_nc_min_nonconst; + @(posedge clk) a |-> b [= n: 2]; + endproperty + // Goto max < min. + property p_goto_bad_order; + @(posedge clk) a |-> b [-> 3: 1]; + endproperty + // Nonconsecutive max < min. + property p_nc_bad_order; + @(posedge clk) a |-> b [= 3: 1]; + endproperty + // Goto min < 0 is a hard error. + property p_goto_neg_min; + @(posedge clk) a |-> b [-> -1: 2]; + endproperty + // Nonconsecutive min < 0 is a hard error. + property p_nc_neg_min; + @(posedge clk) a |-> b [= -1: 2]; + endproperty + + a1 : + assert property (p_goto_nonconst); + a2 : + assert property (p_nc_nonconst); + a3 : + assert property (p_goto_min_nonconst); + a4 : + assert property (p_nc_min_nonconst); + a5 : + assert property (p_goto_bad_order); + a6 : + assert property (p_nc_bad_order); + a7 : + assert property (p_goto_neg_min); + a8 : + assert property (p_nc_neg_min); + +endmodule diff --git a/test_regress/t/t_assert_rep_range_unsup.out b/test_regress/t/t_assert_rep_range_unsup.out new file mode 100644 index 000000000..303ac5f73 --- /dev/null +++ b/test_regress/t/t_assert_rep_range_unsup.out @@ -0,0 +1,10 @@ +%Error-UNSUPPORTED: t/t_assert_rep_range_unsup.v:13:28: Unsupported: [=M:N] nonconsecutive range repetition (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 13 | @(posedge clk) a |-> b [= 1: 2]; + | ^~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error-UNSUPPORTED: t/t_assert_rep_range_unsup.v:16:31: Unsupported: [=M:N] nonconsecutive range repetition (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 16 | @(posedge clk) a [= 1: 2] |-> b; + | ^~~ +%Error: Exiting due to diff --git a/test_regress/t/t_assert_rep_range_unsup.py b/test_regress/t/t_assert_rep_range_unsup.py new file mode 100755 index 000000000..74c8e2367 --- /dev/null +++ b/test_regress/t/t_assert_rep_range_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(expect_filename=test.golden_filename, verilator_flags2=['--assert'], fails=True) + +test.passes() diff --git a/test_regress/t/t_assert_rep_range_unsup.v b/test_regress/t/t_assert_rep_range_unsup.v new file mode 100644 index 000000000..550982cf2 --- /dev/null +++ b/test_regress/t/t_assert_rep_range_unsup.v @@ -0,0 +1,23 @@ +// 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; + bit clk; + bit a; + bit b; + + property p_nc_range; + @(posedge clk) a |-> b [= 1: 2]; + endproperty + property p_nc_lhs_range; + @(posedge clk) a [= 1: 2] |-> b; + endproperty + + a_nc_range : + assert property (p_nc_range); + a_nc_lhs_range : + assert property (p_nc_lhs_range); +endmodule diff --git a/test_regress/t/t_assert_rep_range_zero_min_unsup.out b/test_regress/t/t_assert_rep_range_zero_min_unsup.out new file mode 100644 index 000000000..c1fa0968b --- /dev/null +++ b/test_regress/t/t_assert_rep_range_zero_min_unsup.out @@ -0,0 +1,10 @@ +%Error-UNSUPPORTED: t/t_assert_rep_range_zero_min_unsup.v:18:28: Unsupported: zero min count in Goto repetition range (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 18 | @(posedge clk) a |-> b [-> 0: 2]; + | ^~~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error-UNSUPPORTED: t/t_assert_rep_range_zero_min_unsup.v:21:28: Unsupported: zero min count in Nonconsecutive repetition range (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 21 | @(posedge clk) a |-> b [= 0: 2]; + | ^~ +%Error: Exiting due to diff --git a/test_regress/t/t_assert_rep_range_zero_min_unsup.py b/test_regress/t/t_assert_rep_range_zero_min_unsup.py new file mode 100755 index 000000000..eb780c46e --- /dev/null +++ b/test_regress/t/t_assert_rep_range_zero_min_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(expect_filename=test.golden_filename, fails=True) + +test.passes() diff --git a/test_regress/t/t_assert_rep_range_zero_min_unsup.v b/test_regress/t/t_assert_rep_range_zero_min_unsup.v new file mode 100644 index 000000000..825b8646f --- /dev/null +++ b/test_regress/t/t_assert_rep_range_zero_min_unsup.v @@ -0,0 +1,28 @@ +// 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 + +// Zero min count in a repetition range is IEEE-legal (16.9.2 / 16.9.2.1 +// define an empty match for [*0]; the same applies to [->] and [=]) but +// V3AssertNfa cannot represent a 0-iteration goto/nonconsec match today, +// so V3Width emits E_UNSUPPORTED. + +module t; + bit clk; + bit a; + bit b; + + property p_goto_zero_min; + @(posedge clk) a |-> b [-> 0: 2]; + endproperty + property p_nc_zero_min; + @(posedge clk) a |-> b [= 0: 2]; + endproperty + + a_goto_zero_min : + assert property (p_goto_zero_min); + a_nc_zero_min : + assert property (p_nc_zero_min); +endmodule diff --git a/test_regress/t/t_sequence_sexpr_unsup.out b/test_regress/t/t_sequence_sexpr_unsup.out index c84289009..975a06491 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.out +++ b/test_regress/t/t_sequence_sexpr_unsup.out @@ -1,31 +1,22 @@ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:94:7: Unsupported: [= range nonconsecutive repetition - 94 | a [= 1:2]; - | ^~ - ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:7: Unsupported: [= range nonconsecutive repetition - 97 | a [= 1:$]; - | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:103:7: Unsupported: [-> range goto repetition - 103 | a [-> 1:2]; - | ^~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:106:26: Unsupported: sequence argument data type - 106 | sequence p_arg_seqence(sequence inseq); +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:88:26: Unsupported: sequence argument data type + 88 | sequence p_arg_seqence(sequence inseq); | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:114:5: Unsupported: first_match with sequence_match_items - 114 | first_match (a, res0 = 1); + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:96:5: Unsupported: first_match with sequence_match_items + 96 | first_match (a, res0 = 1); | ^~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:117:5: Unsupported: first_match with sequence_match_items - 117 | first_match (a, res0 = 1, res1 = 2); +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:99:5: Unsupported: first_match with sequence_match_items + 99 | first_match (a, res0 = 1, res1 = 2); | ^~~~~~~~~~~ -%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:120:9: Ignoring unsupported: cover sequence - 120 | cover sequence (s_a) $display(""); +%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:102:9: Ignoring unsupported: cover sequence + 102 | cover sequence (s_a) $display(""); | ^~~~~~~~ ... For warning description see https://verilator.org/warn/COVERIGN?v=latest ... Use "/* verilator lint_off COVERIGN */" and lint_on around source to disable this message. -%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:121:9: Ignoring unsupported: cover sequence - 121 | cover sequence (@(posedge a) disable iff (b) s_a) $display(""); +%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:103:9: Ignoring unsupported: cover sequence + 103 | cover sequence (@(posedge a) disable iff (b) s_a) $display(""); | ^~~~~~~~ -%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:122:9: Ignoring unsupported: cover sequence - 122 | cover sequence (disable iff (b) s_a) $display(""); +%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:104:9: Ignoring unsupported: cover sequence + 104 | cover sequence (disable iff (b) s_a) $display(""); | ^~~~~~~~ %Error: Exiting due to diff --git a/test_regress/t/t_sequence_sexpr_unsup.v b/test_regress/t/t_sequence_sexpr_unsup.v index 807062e1a..73f6b5147 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.v +++ b/test_regress/t/t_sequence_sexpr_unsup.v @@ -78,27 +78,9 @@ module t ( a ## [+] b; endsequence - sequence s_booleanabbrev_brastar_int; - a [* 1 ]; - endsequence - sequence s_booleanabbrev_brastar; - a [*]; - endsequence - sequence s_booleanabbrev_plus; - a [+]; - endsequence - sequence s_booleanabbrev_eq; - a [= 1]; // Now supported (AstSNonConsRep) - endsequence sequence s_booleanabbrev_eq_range; a [= 1:2]; endsequence - sequence s_booleanabbrev_eq_unbounded; - a [= 1:$]; - endsequence - sequence s_booleanabbrev_minusgt; - a [-> 1]; - endsequence sequence s_booleanabbrev_minusgt_range; a [-> 1:2]; endsequence