diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 13287998f..cd8868632 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -60,6 +60,7 @@ private: AstIf* m_disableSeqIfp = nullptr; // Used for handling disable iff in sequences // Other: V3UniqueNames m_cycleDlyNames{"__VcycleDly"}; // Cycle delay counter name generator + V3UniqueNames m_gotoRepNames{"__VgotoRep"}; // Goto repetition counter name generator V3UniqueNames m_disableCntNames{"__VdisableCnt"}; // Disable condition counter name generator V3UniqueNames m_propVarNames{"__Vpropvar"}; // Property-local variable name generator bool m_inAssign = false; // True if in an AssignNode @@ -709,6 +710,99 @@ private: VL_DO_DANGLING(pushDeletep(nodep), nodep); } + // Validate goto repetition count: must be a positive elaboration-time constant. + // On error, replaces nodep with BitFalse placeholder and returns nullptr. + const AstConst* validateGotoRepCount(AstNode* nodep, AstNodeExpr*& countp) { + countp = V3Const::constifyEdit(countp); + const AstConst* const constp = VN_CAST(countp, Const); + if (!constp) { + nodep->v3error("Goto repetition count is not an elaboration-time constant" + " (IEEE 1800-2023 16.9.2)"); + VL_DO_DANGLING(pushDeletep(countp), countp); + nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}}); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + return nullptr; + } + if (constp->isZero()) { + nodep->v3error("Goto repetition count must be greater than zero" + " (IEEE 1800-2023 16.9.2)"); + VL_DO_DANGLING(pushDeletep(countp), countp); + nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}}); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + return nullptr; + } + return constp; + } + + // Lower goto repetition expr[->N] to a counter-based PExpr loop. + // Generated structure: + // begin + // automatic uint32 cnt = 0; + // loop { test(cnt < N); if (sampled(expr)) cnt++; if (cnt < N) @(clk); } + // // consequent check (if rhsp) or pass clause + // end + AstPExpr* createGotoRepPExpr(FileLine* flp, AstNodeExpr* exprp, AstNodeExpr* countp, + AstNodeExpr* rhsp, bool isOverlapped) { + AstSenItem* const sensesp = m_senip; + UASSERT_OBJ(sensesp, exprp, "Goto repetition requires a clock"); + + const std::string name = m_gotoRepNames.get(exprp); + AstVar* const cntVarp = new AstVar{flp, VVarType::BLOCKTEMP, name + "__counter", + exprp->findBasicDType(VBasicDTypeKwd::UINT32)}; + cntVarp->lifetime(VLifetime::AUTOMATIC_EXPLICIT); + + AstBegin* const beginp = new AstBegin{flp, name + "__block", cntVarp, true}; + beginp->addStmtsp( + new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE}, new AstConst{flp, 0}}); + + AstLoop* const loopp = new AstLoop{flp}; + // Loop test: continue while cnt < N + loopp->addStmtsp(new AstLoopTest{flp, loopp, + new AstLt{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, + countp->cloneTreePure(false)}}); + // if ($sampled(expr)) cnt++ + AstSampled* const sampledp = new AstSampled{flp, exprp}; + sampledp->dtypeFrom(exprp); + loopp->addStmtsp( + new AstIf{flp, sampledp, + new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE}, + new AstAdd{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, + new AstConst{flp, 1}}}}); + // if (cnt < N) @(clk) -- only wait if not yet matched + loopp->addStmtsp(new AstIf{ + flp, new AstLt{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, countp}, + new AstEventControl{flp, new AstSenTree{flp, sensesp->cloneTree(false)}, nullptr}}); + + beginp->addStmtsp(loopp); + + if (rhsp) { + if (!isOverlapped) { + beginp->addStmtsp(new AstEventControl{ + flp, new AstSenTree{flp, sensesp->cloneTree(false)}, nullptr}); + } + AstSampled* const sampledRhsp = new AstSampled{flp, rhsp}; + sampledRhsp->dtypeFrom(rhsp); + beginp->addStmtsp(new AstIf{flp, sampledRhsp, new AstPExprClause{flp, true}, + new AstPExprClause{flp, false}}); + } else { + beginp->addStmtsp(new AstPExprClause{flp, true}); + } + + return new AstPExpr{flp, beginp, exprp->findBitDType()}; + } + + void visit(AstSExprGotoRep* nodep) override { + // Standalone goto rep (not inside implication antecedent) + iterateChildren(nodep); + FileLine* const flp = nodep->fileline(); + AstNodeExpr* countp = nodep->countp()->unlinkFrBack(); + if (!validateGotoRepCount(nodep, countp)) return; + AstNodeExpr* const exprp = nodep->exprp()->unlinkFrBack(); + AstPExpr* const pexprp = createGotoRepPExpr(flp, exprp, countp, nullptr, true); + nodep->replaceWith(pexprp); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + } + void visit(AstFuncRef* nodep) override { // IEEE 1800-2023 16.8: Inline sequence instances wherever they appear // in the expression tree (inside implications, boolean ops, nested refs, etc.) @@ -723,6 +817,23 @@ private: void visit(AstImplication* nodep) override { if (nodep->sentreep()) return; // Already processed + // Handle goto repetition as antecedent before iterateChildren, + // so the standalone AstSExprGotoRep visitor doesn't process it + if (AstSExprGotoRep* const gotop = VN_CAST(nodep->lhsp(), SExprGotoRep)) { + iterateChildren(gotop); + iterateAndNextNull(nodep->rhsp()); + FileLine* const flp = nodep->fileline(); + AstNodeExpr* countp = gotop->countp()->unlinkFrBack(); + if (!validateGotoRepCount(nodep, countp)) return; + AstNodeExpr* const exprp = gotop->exprp()->unlinkFrBack(); + AstNodeExpr* const rhsp = nodep->rhsp()->unlinkFrBack(); + AstPExpr* const pexprp + = createGotoRepPExpr(flp, exprp, countp, rhsp, nodep->isOverlapped()); + nodep->replaceWith(pexprp); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + return; + } + iterateChildren(nodep); FileLine* const flp = nodep->fileline(); diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index 9f5323679..a7b7a124f 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -2153,6 +2153,22 @@ public: bool cleanOut() const override { V3ERROR_NA_RETURN(""); } int instrCount() const override { return widthInstrs(); } }; +class AstSExprGotoRep final : public AstNodeExpr { + // Goto repetition: expr [-> count] + // IEEE 1800-2023 16.9.2 + // @astgen op1 := exprp : AstNodeExpr + // @astgen op2 := countp : AstNodeExpr +public: + explicit AstSExprGotoRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp) + : ASTGEN_SUPER_SExprGotoRep(fl) { + this->exprp(exprp); + this->countp(countp); + } + ASTGEN_MEMBERS_AstSExprGotoRep; + string emitVerilog() override { V3ERROR_NA_RETURN(""); } + string emitC() override { V3ERROR_NA_RETURN(""); } + bool cleanOut() const override { V3ERROR_NA_RETURN(""); } +}; class AstSFormatArg final : public AstNodeExpr { // Information for formatting each argument to AstSFormat, // used to pass to (potentially) runtime decoding of format arguments diff --git a/src/V3Width.cpp b/src/V3Width.cpp index 84810a942..75dfed27a 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -1624,6 +1624,14 @@ class WidthVisitor final : public VNVisitor { if (nodep->seedp()) iterateCheckSigned32(nodep, "seed", nodep->seedp(), BOTH); } } + void visit(AstSExprGotoRep* nodep) override { + assertAtExpr(nodep); + if (m_vup->prelim()) { + iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH); + userIterateAndNext(nodep->countp(), WidthVP{SELF, BOTH}.p()); + nodep->dtypeSetBit(); + } + } void visit(AstSExpr* nodep) override { VL_RESTORER(m_underSExpr); m_underSExpr = true; diff --git a/src/verilog.y b/src/verilog.y index 71454ffbb..6495b78e5 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6805,6 +6805,12 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg // // IEEE: expression_or_dist [ boolean_abbrev ] // // Note expression_or_dist includes "expr"! // // sexpr/*sexpression_or_dist*/ --- Hardcoded below + // // IEEE: goto_repetition (single count form) + | ~p~sexpr/*sexpression_or_dist*/ yP_BRAMINUSGT constExpr ']' + { $$ = new AstSExprGotoRep{$2, $1, $3}; } + // // IEEE: goto_repetition (range form -- unsupported) + | ~p~sexpr/*sexpression_or_dist*/ yP_BRAMINUSGT constExpr ':' constExpr ']' + { $$ = $1; BBUNSUP($2, "Unsupported: [-> range goto repetition"); DEL($3); DEL($5); } | ~p~sexpr/*sexpression_or_dist*/ boolean_abbrev { $$ = $1; BBUNSUP($2->fileline(), "Unsupported: boolean abbrev (in sequence expression)"); DEL($2); } // @@ -6906,10 +6912,8 @@ boolean_abbrev: // ==IEEE: boolean_abbrev | yP_BRAEQ constExpr ':' constExpr ']' { $$ = $2; BBUNSUP($1, "Unsupported: [= boolean abbrev expression"); DEL($4); } // // IEEE: goto_repetition - | yP_BRAMINUSGT constExpr ']' - { $$ = $2; BBUNSUP($1, "Unsupported: [-> boolean abbrev expression"); } - | yP_BRAMINUSGT constExpr ':' constExpr ']' - { $$ = $2; BBUNSUP($1, "Unsupported: [-> boolean abbrev expression"); DEL($4); } + // // Goto repetition [->N] handled in sexpr rule (AstSExprGotoRep) + // // Range form [->M:N] also handled there (unsupported) ; //************************************************ diff --git a/test_regress/t/t_assert_goto_rep.py b/test_regress/t/t_assert_goto_rep.py new file mode 100755 index 000000000..b92324a60 --- /dev/null +++ b/test_regress/t/t_assert_goto_rep.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('simulator') + +test.compile(verilator_flags2=['--timing', '--assert']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_assert_goto_rep.v b/test_regress/t/t_assert_goto_rep.v new file mode 100644 index 000000000..ef993d896 --- /dev/null +++ b/test_regress/t/t_assert_goto_rep.v @@ -0,0 +1,67 @@ +// 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 checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0x exp=%0x (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0); +`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); +// verilog_format: on + +module t ( + input clk +); + + int cyc; + reg [63:0] crc; + + // Derive signals from non-adjacent CRC bits (lesson 17: avoid shift correlation) + wire a = crc[0]; + wire b = crc[4]; + wire c = crc[8]; + wire d = crc[12]; + + int count_fail1 = 0; + int count_fail2 = 0; + int count_fail3 = 0; + int count_fail4 = 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; + + // Test 2: a[->1] |-> c (single occurrence, overlapping) + 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; + + // Test 4: standalone goto rep (no implication) -- exercises standalone visitor + assert property (@(posedge clk) b[->2]) + else count_fail4 <= count_fail4 + 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); +`endif + cyc <= cyc + 1; + crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; + if (cyc == 0) begin + crc <= 64'h5aef0c8d_d70a4497; + end + else if (cyc == 99) begin + `checkh(crc, 64'hc77bb9b3784ea091); + `checkd(count_fail1, 20); + `checkd(count_fail2, 40); + `checkd(count_fail3, 19); + `checkd(count_fail4, 0); + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule diff --git a/test_regress/t/t_assert_goto_rep_bad_count.out b/test_regress/t/t_assert_goto_rep_bad_count.out new file mode 100644 index 000000000..994370fed --- /dev/null +++ b/test_regress/t/t_assert_goto_rep_bad_count.out @@ -0,0 +1,10 @@ +%Error: t/t_assert_goto_rep_bad_count.v:16:42: Goto repetition count is not an elaboration-time constant (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 16 | assert property (@(posedge clk) a[->n] |-> b) + | ^~~ + ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. +%Error: t/t_assert_goto_rep_bad_count.v:20:42: Goto repetition count must be greater than zero (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 20 | assert property (@(posedge clk) a[->0] |-> b) + | ^~~ +%Error: Exiting due to diff --git a/test_regress/t/t_assert_goto_rep_bad_count.py b/test_regress/t/t_assert_goto_rep_bad_count.py new file mode 100755 index 000000000..38cf36b43 --- /dev/null +++ b/test_regress/t/t_assert_goto_rep_bad_count.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_goto_rep_bad_count.v b/test_regress/t/t_assert_goto_rep_bad_count.v new file mode 100644 index 000000000..46383a027 --- /dev/null +++ b/test_regress/t/t_assert_goto_rep_bad_count.v @@ -0,0 +1,30 @@ +// 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; + logic clk = 0; + always #5 clk = ~clk; + + int cyc = 0; + logic a, b; + int n; + + // Error: non-constant count + assert property (@(posedge clk) a[->n] |-> b) + else $error("FAIL"); + + // Error: zero count + assert property (@(posedge clk) a[->0] |-> b) + else $error("FAIL"); + + always @(posedge clk) begin + cyc <= cyc + 1; + if (cyc == 5) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule diff --git a/test_regress/t/t_property_sexpr_parse_unsup.out b/test_regress/t/t_property_sexpr_parse_unsup.out index 73d3d9bbc..3aeefadd4 100644 --- a/test_regress/t/t_property_sexpr_parse_unsup.out +++ b/test_regress/t/t_property_sexpr_parse_unsup.out @@ -1,8 +1,19 @@ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:51: Unsupported: [-> boolean abbrev expression - 82 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; - | ^~~ - ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:54: Unsupported: boolean abbrev (in sequence expression) - 82 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; - | ^ -%Error: Exiting due to +%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:60:14: Logical operator IMPLICATION expects 1 bit on the RHS, but RHS's CMETHODHARD 'at' generates 8 bits. + : ... note: In instance 't.ieee' + 60 | $rose(a) |-> q[0]; + | ^~~ + ... For warning description see https://verilator.org/warn/WIDTHTRUNC?v=latest + ... Use "/* verilator lint_off WIDTHTRUNC */" and lint_on around source to disable this message. +%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:65:29: Logical operator SEXPR expects 1 bit on the exprp, but exprp's CMETHODHARD 'at' generates 8 bits. + : ... note: In instance 't.ieee' + 65 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; + | ^~ +%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:86:31: Logical operator SEXPR expects 1 bit on the exprp, but exprp's VARREF 'b' generates 32 bits. + : ... note: In instance 't.ieee' + 86 | assert property (@clk not a ##1 b); + | ^~ +%Error: Internal Error: t/t_property_sexpr_unsup.v:65:29: ../V3AssertProp.cpp:#: Range delay SExpr without clocking event + : ... note: In instance 't.ieee' + 65 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; + | ^~ + ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. diff --git a/test_regress/t/t_sequence_sexpr_unsup.out b/test_regress/t/t_sequence_sexpr_unsup.out index 51fcc05ab..5a0d9a2eb 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.out +++ b/test_regress/t/t_sequence_sexpr_unsup.out @@ -50,18 +50,9 @@ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:98:10: Unsupported: boolean abbrev (in sequence expression) 98 | a [= 1:2]; | ^ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:101:7: Unsupported: [-> boolean abbrev expression - 101 | a [-> 1]; - | ^~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:101:11: Unsupported: boolean abbrev (in sequence expression) - 101 | a [-> 1]; - | ^ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:104:7: Unsupported: [-> boolean abbrev expression +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:104:7: Unsupported: [-> range goto repetition 104 | a [-> 1:2]; | ^~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:104:11: Unsupported: boolean abbrev (in sequence expression) - 104 | a [-> 1:2]; - | ^ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:107:26: Unsupported: sequence argument data type 107 | sequence p_arg_seqence(sequence inseq); | ^~~~~~~~