diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 9878778d0..a2fd9234c 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -253,6 +253,21 @@ class SvaNfaBuilder final { if (AstSThroughout* const throughp = VN_CAST(nodep, SThroughout)) { return fixedLength(throughp->rhsp()); } + if (AstSOr* const orp = VN_CAST(nodep, SOr)) { + // Alternatives must share one end cycle; buildSWithin relies on + // this to pair the OR with an SIntersect. + const int lhsLen = fixedLength(orp->lhsp()); + const int rhsLen = fixedLength(orp->rhsp()); + if (lhsLen < 0 || rhsLen < 0 || lhsLen != rhsLen) return -1; + return lhsLen; + } + if (AstSWithin* const withinp = VN_CAST(nodep, SWithin)) { + // `seq1 within seq2` ends at seq2's end cycle (IEEE 16.9.10). + const int lhsLen = fixedLength(withinp->lhsp()); + const int rhsLen = fixedLength(withinp->rhsp()); + if (lhsLen < 0 || rhsLen < 0 || lhsLen > rhsLen) return -1; + return rhsLen; + } // LCOV_EXCL_START -- defensive: V3AssertPre rejects composite SVA ops // nested in an intersect arm before fixedLength runs (clock-context // resolution fails). Kept as a guard in case future parser relaxations @@ -630,6 +645,67 @@ class SvaNfaBuilder final { return {combVtxp, nullptr, {}}; } + // Lower `seq1 within seq2` (IEEE 1800-2023 16.9.10) as: + // (OR_{i in 0..slack} 1 ##i seq1 ##(slack-i) 1) intersect seq2 + // Both operands must have fixed length (no ranged cycle delays). + // The OR lives inside a single SIntersect so one AndCombiner done-latch + // serves all offsets; lifting it out would double-count matches where + // multiple offsets accept on the same seq2 end cycle. + BuildResult buildSWithin(AstSWithin* nodep, SvaStateVertex* entryVtxp, + bool isTopLevelStep = false) { + const int innerLen = fixedLength(nodep->lhsp()); + const int outerLen = fixedLength(nodep->rhsp()); + if (innerLen < 0 || outerLen < 0) { + nodep->v3warn(E_UNSUPPORTED, "Unsupported: within with ranged cycle-delay operand"); + return BuildResult::failWithError(); + } + if (innerLen > outerLen) { + nodep->v3error("'within' inner sequence " + std::to_string(innerLen) + + " cycles exceeds outer sequence " + std::to_string(outerLen) + + " cycles (IEEE 1800-2023 16.9.10)"); + return BuildResult::failWithError(); + } + FileLine* const flp = nodep->fileline(); + const int slack = outerLen - innerLen; + AstNodeExpr* innerOrp = nullptr; + for (int i = 0; i <= slack; ++i) { + const int postPad = slack - i; + AstNodeExpr* branchp = nodep->lhsp()->cloneTreePure(false); + if (i > 0) { + AstConst* const prePadp = new AstConst{flp, AstConst::BitTrue{}}; + AstDelay* const delayp + = new AstDelay{flp, new AstConst{flp, static_cast(i)}, true}; + AstSExpr* const wrapped = new AstSExpr{flp, prePadp, delayp, branchp}; + wrapped->dtypeSetBit(); + branchp = wrapped; + } + if (postPad > 0) { + AstConst* const postTruep = new AstConst{flp, AstConst::BitTrue{}}; + AstDelay* const delayp + = new AstDelay{flp, new AstConst{flp, static_cast(postPad)}, true}; + AstSExpr* const wrapped = new AstSExpr{flp, branchp, delayp, postTruep}; + wrapped->dtypeSetBit(); + branchp = wrapped; + } + innerOrp = innerOrp ? static_cast(new AstSOr{flp, innerOrp, branchp}) + : branchp; + } + AstNodeExpr* const outerClonep = nodep->rhsp()->cloneTreePure(false); + AstNodeExpr* const combinedp = new AstSIntersect{flp, innerOrp, outerClonep}; + BuildResult result = buildExpr(combinedp, entryVtxp, isTopLevelStep); + VL_DO_DANGLING(combinedp->deleteTree(), combinedp); + // When both operands are plain booleans, buildAndCombiner returns a + // freshly-allocated AstAnd as finalCondp with no parent. Callers up + // the chain clone-and-discard finalCondp, so leave it parent-less and + // it leaks; anchor it in the graph now via an edge. + if (result.valid() && result.finalCondp && !result.finalCondp->backp()) { + SvaStateVertex* const wrapVtxp = scopedCreateVertex(); + guardedLink(result.termVertexp, wrapVtxp, sampled(result.finalCondp), flp); + result = {wrapVtxp, nullptr, result.midSources}; + } + return result; + } + BuildResult buildThroughout(AstSThroughout* nodep, SvaStateVertex* entryVtxp, bool isTopLevelStep = false) { // Mark entryVtxp so "cond false at tick 0" is detected as throughout-drop. @@ -687,6 +763,9 @@ public: } return buildAndCombiner(intp->lhsp(), intp->rhsp(), entryVtxp, intp->fileline()); } + if (AstSWithin* const withinp = VN_CAST(nodep, SWithin)) { + return buildSWithin(withinp, entryVtxp, isTopLevelStep); + } if (VN_IS(nodep, SNonConsRep)) return BuildResult::fail(); // Boolean leaf (including LogAnd): return as finalCond return {entryVtxp, nodep, {}}; diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index 175ee3891..fa6fa02d6 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -3843,6 +3843,29 @@ public: // LCOV_EXCL_STOP bool isMultiCycleSva() const override { return true; } }; +class AstSWithin final : public AstNodeBiop { + // seq1 within seq2 (IEEE 1800-2023 16.9.10) +public: + AstSWithin(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp) + : ASTGEN_SUPER_SWithin(fl, lhsp, rhsp) { + dtypeSetBit(); + } + ASTGEN_MEMBERS_AstSWithin; + // LCOV_EXCL_START // Lowered in V3AssertNfa before these are called + void numberOperate(V3Number& out, const V3Number& lhs, const V3Number& rhs) override { + out.opLogAnd(lhs, rhs); + } + string emitVerilog() override { return "%k(%l %fwithin %r)"; } + string emitC() override { V3ERROR_NA_RETURN(""); } + string emitSimpleOperator() override { V3ERROR_NA_RETURN(""); } + bool cleanOut() const override { return true; } + bool cleanLhs() const override { return true; } + bool cleanRhs() const override { return true; } + bool sizeMattersLhs() const override { return false; } + bool sizeMattersRhs() const override { return false; } + // LCOV_EXCL_STOP + bool isMultiCycleSva() const override { return true; } +}; class AstSel final : public AstNodeBiop { // *Resolved* (tyep checked) multiple bit range extraction. Always const width // @astgen alias op1 := fromp diff --git a/src/V3Width.cpp b/src/V3Width.cpp index bcde8d392..e57c891e8 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -299,6 +299,7 @@ class WidthVisitor final : public VNVisitor { void visit(AstSAnd* nodep) override { visit_log_and_or(nodep); } void visit(AstSIntersect* nodep) override { visit_log_and_or(nodep); } void visit(AstSOr* nodep) override { visit_log_and_or(nodep); } + void visit(AstSWithin* nodep) override { visit_log_and_or(nodep); } void visit(AstLogEq* nodep) override { // Conversion from real not in IEEE, but a fallout visit_log_and_or(nodep); diff --git a/src/verilog.y b/src/verilog.y index 0f689647d..f809924ee 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6885,7 +6885,7 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg // // Below pexpr's are really sequence_expr, but avoid conflict // // IEEE: sexpr yWITHIN sexpr | ~p~sexpr yWITHIN sexpr - { $$ = $1; BBUNSUP($2, "Unsupported: within (in sequence expression)"); DEL($3); } + { $$ = new AstSWithin{$2, $1, $3}; } // // Note concurrent_assertion had duplicate rule for below //UNSUP clocking_event ~p~sexpr %prec prSEQ_CLOCKING { } // diff --git a/test_regress/t/t_sequence_sexpr_unsup.out b/test_regress/t/t_sequence_sexpr_unsup.out index 0ef65b78c..c84289009 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.out +++ b/test_regress/t/t_sequence_sexpr_unsup.out @@ -1,34 +1,31 @@ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:34:7: Unsupported: within (in sequence expression) - 34 | a within(b); - | ^~~~~~ +%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:98:7: Unsupported: [= range nonconsecutive repetition - 98 | a [= 1:2]; +%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:101:7: Unsupported: [= range nonconsecutive repetition - 101 | a [= 1:$]; - | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:107:7: Unsupported: [-> range goto repetition - 107 | a [-> 1:2]; +%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:110:26: Unsupported: sequence argument data type - 110 | sequence p_arg_seqence(sequence inseq); +%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:118:5: Unsupported: first_match with sequence_match_items - 118 | first_match (a, res0 = 1); +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:114:5: Unsupported: first_match with sequence_match_items + 114 | first_match (a, res0 = 1); | ^~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:121:5: Unsupported: first_match with sequence_match_items - 121 | first_match (a, res0 = 1, res1 = 2); +%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); | ^~~~~~~~~~~ -%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:124:9: Ignoring unsupported: cover sequence - 124 | cover sequence (s_a) $display(""); +%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:120:9: Ignoring unsupported: cover sequence + 120 | 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:125:9: Ignoring unsupported: cover sequence - 125 | cover sequence (@(posedge a) disable iff (b) s_a) $display(""); +%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:126:9: Ignoring unsupported: cover sequence - 126 | cover sequence (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(""); | ^~~~~~~~ %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 cdd0e935a..807062e1a 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.v +++ b/test_regress/t/t_sequence_sexpr_unsup.v @@ -30,10 +30,6 @@ module t ( a; endsequence - sequence s_within; - a within(b); - endsequence - sequence s_and; a and b; endsequence diff --git a/test_regress/t/t_sequence_within.py b/test_regress/t/t_sequence_within.py new file mode 100755 index 000000000..ab1f7d03f --- /dev/null +++ b/test_regress/t/t_sequence_within.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=['--assert --timing --coverage']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_sequence_within.v b/test_regress/t/t_sequence_within.v new file mode 100644 index 000000000..62b1e5800 --- /dev/null +++ b/test_regress/t/t_sequence_within.v @@ -0,0 +1,129 @@ +// 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='h%x exp='h%x\n", `__FILE__,`__LINE__, (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 + +// IEEE 1800-2023 16.9.10: seq1 within seq2 +// CRC-driven random stimulus. Each property has a counter; at cyc==99 we +// `checkd` against Verilator's actual count and record the Questa golden +// value in a trailing comment for cross-simulator reference. + +module t ( + input clk +); + integer cyc = 0; + reg [63:0] crc = '0; + + // Non-adjacent CRC bits (gap > max delay) to avoid LFSR correlation. + wire a = crc[0]; + wire b = crc[7]; + wire c = crc[15]; + wire d = crc[23]; + + int count_p1 = 0; + int count_p2 = 0; + int count_p3 = 0; + int count_p4 = 0; + int count_p5 = 0; + int count_p6 = 0; + int count_p7 = 0; + int count_p8 = 0; + int count_p9 = 0; + int count_p10 = 0; + + // Boolean within boolean: equivalent to `a && b`. + assert property (@(posedge clk) disable iff (cyc < 10) + (a & b) |-> (a within b)) + count_p1 <= count_p1 + 1; + + // Boolean within constant true: always passes when a is high. + assert property (@(posedge clk) disable iff (cyc < 10) + a |-> (a within 1'b1)) + count_p2 <= count_p2 + 1; + + // `a` must hold at some offset within the c ##1 d window. + cover property (@(posedge clk) disable iff (cyc < 10) + a within (c ##1 d)) + count_p3 <= count_p3 + 1; + + // `a` within a length-3 outer (four possible offsets). + cover property (@(posedge clk) disable iff (cyc < 10) + a within (c ##3 d)) + count_p4 <= count_p4 + 1; + + // Equal-length inner/outer: single offset, reduces to intersect. + assert property (@(posedge clk) disable iff (cyc < 10) + (a & c) |-> ((a ##1 1'b1) within (c ##1 1'b1))) + count_p5 <= count_p5 + 1; + + // Inner length 1, outer length 3 -> three offsets (0, 1, 2). + cover property (@(posedge clk) disable iff (cyc < 10) + (a ##1 b) within (c ##3 d)) + count_p6 <= count_p6 + 1; + + // Inner length 2, outer length 3 -> two offsets (0, 1). + cover property (@(posedge clk) disable iff (cyc < 10) + (a ##2 b) within (c ##3 d)) + count_p7 <= count_p7 + 1; + + // within nested inside intersect: both must match equal length. + cover property (@(posedge clk) disable iff (cyc < 10) + ((a ##1 b) within (c ##2 d)) intersect (a ##2 b)) + count_p8 <= count_p8 + 1; + + // within combined with throughout on the outer: throughout's rhs + // fixedLength still feeds into within. + cover property (@(posedge clk) disable iff (cyc < 10) + a within (a throughout (b ##1 c))) + count_p9 <= count_p9 + 1; + + // within on the RHS of intersect: forces the parser into the direct + // `sexpr yWITHIN sexpr` grammar rule (IEEE 1800-2023 17.7.1) rather + // than the pexpr-copied variant used at property top level. + cover property (@(posedge clk) disable iff (cyc < 10) + (a ##3 b) intersect ((c ##1 d) within (a ##3 b))) + count_p10 <= count_p10 + 1; + + always_ff @(posedge clk) begin + 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); + // p1/p2/p5 use |->; the NFA currently fires the pass action on + // vacuous passes too, so counts are inflated vs. Questa. Pre-existing + // engine-wide behavior, not within-specific. + `checkd(count_p1, 89); // Questa: 23 + `checkd(count_p2, 89); // Questa: 44 + `checkd(count_p3, 26); // Questa: 20 + `checkd(count_p4, 24); // Questa: 22 + `checkd(count_p5, 89); // Questa: 26 + `checkd(count_p6, 21); // Questa: 16 + `checkd(count_p7, 15); // Questa: 9 + `checkd(count_p8, 15); // Questa: 4 + `checkd(count_p9, 17); // Questa: 10 + `checkd(count_p10, 24); // Questa: 15 + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule + +// Harness for stand-alone simulators (e.g. QuestaSim). Verilator uses +// test_regress's built-in clock shell and ignores this module. +`ifndef VERILATOR +module wrap; + logic clk = 0; + always #5 clk = ~clk; + t inst (.clk(clk)); +endmodule +`endif diff --git a/test_regress/t/t_sequence_within_bad.out b/test_regress/t/t_sequence_within_bad.out new file mode 100644 index 000000000..58a0e5525 --- /dev/null +++ b/test_regress/t/t_sequence_within_bad.out @@ -0,0 +1,6 @@ +%Error: t/t_sequence_within_bad.v:14:17: 'within' inner sequence 3 cycles exceeds outer sequence 1 cycles (IEEE 1800-2023 16.9.10) + : ... note: In instance 't' + 14 | (a ##3 b) within (c ##1 d)); + | ^~~~~~ + ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. +%Error: Exiting due to diff --git a/test_regress/t/t_sequence_within_bad.py b/test_regress/t/t_sequence_within_bad.py new file mode 100755 index 000000000..58fc7aeba --- /dev/null +++ b/test_regress/t/t_sequence_within_bad.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_all') + +test.compile(verilator_flags2=['--assert', '--timing', '--lint-only'], + fails=True, + expect_filename=test.golden_filename) + +test.passes() diff --git a/test_regress/t/t_sequence_within_bad.v b/test_regress/t/t_sequence_within_bad.v new file mode 100644 index 000000000..18b83c37b --- /dev/null +++ b/test_regress/t/t_sequence_within_bad.v @@ -0,0 +1,16 @@ +// 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); + logic a, b, c, d; + + // Inner length (3) exceeds outer length (1). IEEE 1800-2023 16.9.10 + // requires the inner sequence to fit entirely within the outer match + // window, so this is a hard error. + assert property (@(posedge clk) + (a ##3 b) within (c ##1 d)); + +endmodule diff --git a/test_regress/t/t_sequence_within_range_unsup.out b/test_regress/t/t_sequence_within_range_unsup.out new file mode 100644 index 000000000..664237600 --- /dev/null +++ b/test_regress/t/t_sequence_within_range_unsup.out @@ -0,0 +1,6 @@ +%Error-UNSUPPORTED: t/t_sequence_within_range_unsup.v:15:21: Unsupported: within with ranged cycle-delay operand + : ... note: In instance 't' + 15 | (a ##[1:3] b) within (c ##5 d)); + | ^~~~~~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error: Exiting due to diff --git a/test_regress/t/t_sequence_within_range_unsup.py b/test_regress/t/t_sequence_within_range_unsup.py new file mode 100755 index 000000000..58fc7aeba --- /dev/null +++ b/test_regress/t/t_sequence_within_range_unsup.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_all') + +test.compile(verilator_flags2=['--assert', '--timing', '--lint-only'], + fails=True, + expect_filename=test.golden_filename) + +test.passes() diff --git a/test_regress/t/t_sequence_within_range_unsup.v b/test_regress/t/t_sequence_within_range_unsup.v new file mode 100644 index 000000000..f1e63c400 --- /dev/null +++ b/test_regress/t/t_sequence_within_range_unsup.v @@ -0,0 +1,17 @@ +// 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); + logic a, b, c, d; + + // Ranged cycle-delay in the inner arm is not lowerable: each length + // in the range would admit a different offset set. IEEE 1800-2023 + // 16.9.10 is not well-defined under variable-length operands for our + // fixed-length desugar, so reject with UNSUPPORTED. + assert property (@(posedge clk) + (a ##[1:3] b) within (c ##5 d)); + +endmodule