Support sequence within operator (#7461)
This commit is contained in:
Yilou Wang
GitHub
parent
e4da16caf0
commit
51eb5346c8
|
|
@ -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<uint32_t>(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<uint32_t>(postPad)}, true};
|
||||
AstSExpr* const wrapped = new AstSExpr{flp, branchp, delayp, postTruep};
|
||||
wrapped->dtypeSetBit();
|
||||
branchp = wrapped;
|
||||
}
|
||||
innerOrp = innerOrp ? static_cast<AstNodeExpr*>(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, {}};
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -6885,7 +6885,7 @@ sexpr<nodeExprp>: // ==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 { }
|
||||
//
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -30,10 +30,6 @@ module t (
|
|||
a;
|
||||
endsequence
|
||||
|
||||
sequence s_within;
|
||||
a within(b);
|
||||
endsequence
|
||||
|
||||
sequence s_and;
|
||||
a and b;
|
||||
endsequence
|
||||
|
|
|
|||
|
|
@ -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()
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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()
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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()
|
||||
|
|
@ -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
|
||||
Loading…
Reference in New Issue