luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Support [*N:$] consecutive repetition (#7940) 

Signed-off-by: Artur Bieniek <abieniek@antmicro.com>
This commit is contained in:
Artur Bieniek 2026-07-16 15:29:30 +02:00 committed by GitHub
parent 877fc1e812
commit 255bcff3ac
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
11 changed files with 119 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/V3AstNodeExpr.h
View File

@ -2262,24 +2262,25 @@ public:
bool cleanOut() const override { V3ERROR_NA_RETURN(false); }
};
class AstSConsRep final : public AstNodeExpr {
// Consecutive repetition [*N], [*N:M], [+], [*] (IEEE 1800-2023 16.9.2)
// Consecutive repetition [*N], [*N:M], [*N:$], [+], [*] (IEEE 1800-2023 16.9.2)
// op1 := exprp -- the repeated expression
// op2 := countp -- min repetition count (N); always a positive constant after V3Width
// op2 := countp -- min repetition count (N); always a non-negative constant after V3Width
// op3 := maxCountp -- max repetition count (M); nullptr when exact or unbounded
//
// Encoding:
// [*N]: countp=N, maxCountp=nullptr, unbounded=false
// [*N:M]: countp=N, maxCountp=M, unbounded=false
// [*N:$]: countp=N, maxCountp=nullptr, unbounded=true
// [+]: countp=1, maxCountp=nullptr, unbounded=true (= [*1:$])
// [*]: countp=0, maxCountp=nullptr, unbounded=true (= [*0:$])
//
// Lowering:
// Exact [*N] standalone: V3AssertPre saturating counter
// All other forms and all SExpr-contained forms: V3AssertProp PExpr loop
// All other forms and all SExpr-contained forms: V3AssertNfa
// @astgen op1 := exprp : AstNodeExpr
// @astgen op2 := countp : AstNodeExpr
// @astgen op3 := maxCountp : Optional[AstNodeExpr]
const bool m_unbounded = false; // True for [+] and [*] (upper bound is $)
const bool m_unbounded = false; // True when the upper bound is $
public:
// Exact [*N]
AstSConsRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp)
@ -2287,7 +2288,7 @@ public:
this->exprp(exprp);
this->countp(countp);
}
// Range [*N:M] or unbounded [+]/[*]
// Range [*N:M] or unbounded [*N:$]/[+]/[*]
AstSConsRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp, AstNodeExpr* maxCountp,
bool unbounded)
: ASTGEN_SUPER_SConsRep(fl)

5
src/V3Width.cpp
View File

@ -1556,7 +1556,7 @@ class WidthVisitor final : public VNVisitor {
}
}
void visit(AstSConsRep* nodep) override {
// IEEE 1800-2023 16.9.2 -- consecutive repetition [*N], [*N:M], [+], [*]
// IEEE 1800-2023 16.9.2 -- consecutive repetition [*N], [*N:M], [*N:$], [+], [*]
assertAtExpr(nodep);
if (m_vup->prelim()) {
userIterateAndNext(nodep->exprp(), WidthVP{SELF, BOTH}.p());
@ -1566,6 +1566,9 @@ class WidthVisitor final : public VNVisitor {
if (!minConstp) {
nodep->v3error("Consecutive repetition count must be constant expression"
" (IEEE 1800-2023 16.9.2)");
} else if (minConstp->toSInt() < 0) {
nodep->v3error("Consecutive repetition count must be non-negative"
" (IEEE 1800-2023 16.9.2)");
} else if (!nodep->unbounded() && !nodep->maxCountp() && minConstp->toSInt() < 1) {
nodep->v3warn(E_UNSUPPORTED, "Unsupported: [*0] consecutive repetition");
}

11
src/verilog.y
View File

@ -6874,9 +6874,16 @@ sexpr<nodeExprp>: // ==IEEE: sequence_expr (The name sexpr is important as reg
// // [*N] exact count
| ~p~sexpr/*sexpression_or_dist*/ yP_BRASTAR constExpr ']'
{ $$ = new AstSConsRep{$<fl>2, $1, $3}; }
// // [*N:M] range
// // [*N:M] bounded range or [*N:$] unbounded range
| ~p~sexpr/*sexpression_or_dist*/ yP_BRASTAR constExpr ':' constExpr ']'
{ $$ = new AstSConsRep{$<fl>2, $1, $3, $5, false}; } // LCOV_EXCL_LINE
{
if (VN_IS($5, Unbounded)) {
DEL($5);
$$ = new AstSConsRep{$<fl>2, $1, $3, nullptr, true};
} else {
$$ = new AstSConsRep{$<fl>2, $1, $3, $5, false};
}
}
// // [+] = [*1:$]
| ~p~sexpr/*sexpression_or_dist*/ yP_BRAPLUSKET
{ $$ = new AstSConsRep{$<fl>2, $1,

44
test_regress/t/t_assert_consec_rep.v
View File

@ -14,6 +14,8 @@ module t (
input clk
);
localparam int MIN_N = 3;
int cyc;
reg [63:0] crc;
@ -34,6 +36,16 @@ module t (
int count_fail9 = 0;
int count_fail10 = 0;
int count_fail11 = 0;
int count_fail12 = 0;
int count_fail13 = 0;
int count_fail14 = 0;
int count_fail15 = 0;
int count_fail16 = 0;
int count_fail17 = 0;
int count_fail18 = 0;
int count_fail19 = 0;
int count_fail20 = 0;
int count_fail21 = 0;
// Test 1: a[*3] |-> b
assert property (@(posedge clk) a [* 3] |-> b)
@ -79,6 +91,32 @@ module t (
assert property (@(posedge clk) a [*] ##1 b)
else count_fail11 <= count_fail11 + 1;
// Tests 12-13: explicit unbounded aliases
assert property (@(posedge clk) a [*0:$] ##1 b)
else count_fail12 <= count_fail12 + 1;
assert property (@(posedge clk) a [*1:$] ##1 b)
else count_fail13 <= count_fail13 + 1;
// Tests 14-17: IEEE 1800-2023 F.3.4.2.1 expansion of arbitrary minima
assert property (@(posedge clk) a [*2:$] ##1 b)
else count_fail14 <= count_fail14 + 1;
assert property (@(posedge clk) a ##1 a [+] ##1 b)
else count_fail15 <= count_fail15 + 1;
assert property (@(posedge clk) a [*MIN_N:$] ##1 b)
else count_fail16 <= count_fail16 + 1;
assert property (@(posedge clk) a [*2] ##1 a [+] ##1 b)
else count_fail17 <= count_fail17 + 1;
// Tests 18-21: unbounded repetition in antecedent and consequent positions
assert property (@(posedge clk) a [*2:$] |-> b)
else count_fail18 <= count_fail18 + 1;
assert property (@(posedge clk) (a ##1 a [+]) |-> b)
else count_fail19 <= count_fail19 + 1;
assert property (@(posedge clk) c |-> a [*2:$])
else count_fail20 <= count_fail20 + 1;
assert property (@(posedge clk) c |-> (a ##1 a [+]))
else count_fail21 <= count_fail21 + 1;
// Counter FSM with M>0: range > kChainLimit (256) forces counter vertex
// creation; min>0 exercises the Gte/active gating path in resolveLinks and
// emitNbaLogic. Cover-only so count_fail values above are undisturbed.
@ -112,6 +150,12 @@ module t (
// a[*] ##1 b: NFA treats unbounded [*] as liveness (no reject);
// Should be definite antecedent
`checkd(count_fail11, 0); // All other sims: 29
`checkd(count_fail12, count_fail11);
`checkd(count_fail13, count_fail7);
`checkd(count_fail14, count_fail15);
`checkd(count_fail16, count_fail17);
`checkd(count_fail18, count_fail19);
`checkd(count_fail20, count_fail21);
$write("*-* All Finished *-*\n");
$finish;
end

12
test_regress/t/t_assert_consec_rep_bad.out
View File

@ -28,4 +28,16 @@
: ... note: In instance 't'
24 | assert property (@(posedge clk) a [*0:0] |-> 1);
| ^~
%Error: t/t_assert_consec_rep_bad.v:27:37: Consecutive repetition count must be non-negative (IEEE 1800-2023 16.9.2)
: ... note: In instance 't'
27 | assert property (@(posedge clk) a [*-1:$] |-> 1);
| ^~
%Error: t/t_assert_consec_rep_bad.v:30:39: Expecting expression to be constant, but variable isn't const: 'n'
: ... note: In instance 't'
30 | assert property (@(posedge clk) a [*n:$] |-> 1);
| ^
%Error: t/t_assert_consec_rep_bad.v:30:37: Consecutive repetition count must be constant expression (IEEE 1800-2023 16.9.2)
: ... note: In instance 't'
30 | assert property (@(posedge clk) a [*n:$] |-> 1);
| ^~
%Error: Exiting due to

6
test_regress/t/t_assert_consec_rep_bad.v
View File

@ -23,4 +23,10 @@ module t (input clk);
// Bad: [*N:0] zero max count
assert property (@(posedge clk) a [*0:0] |-> 1);
// Bad: negative unbounded minimum
assert property (@(posedge clk) a [*-1:$] |-> 1);
// Bad: non-constant unbounded minimum
assert property (@(posedge clk) a [*n:$] |-> 1);
endmodule

4
test_regress/t/t_assert_consec_rep_unroll_limit_bad.out
View File

@ -3,4 +3,8 @@
14 | assert property (@(posedge clk) a [* 25700000] |-> b);
| ^~
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
%Error: t/t_assert_consec_rep_unroll_limit_bad.v:17:37: Concurrent assertion repetition count 25700001 exceeds --assert-unroll-limit (1024); raise '--assert-unroll-limit' to compile
: ... note: In instance 't'
17 | assert property (@(posedge clk) a [* 25700000:$] |-> b);
| ^~
%Error: Exiting due to

3
test_regress/t/t_assert_consec_rep_unroll_limit_bad.v
View File

@ -13,4 +13,7 @@ module t (
// compiler, now an error names the limit so the user can raise it.
assert property (@(posedge clk) a [* 25700000] |-> b);
// The mandatory prefix of an unbounded repetition is subject to the same limit.
assert property (@(posedge clk) a [* 25700000:$] |-> b);
endmodule

4
test_regress/t/t_assert_consec_rep_unsup.out
View File

@ -3,4 +3,8 @@
13 | assert property (@(posedge clk) (a ##1 b) [* 2] |-> a);
| ^~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_assert_consec_rep_unsup.v:16:45: Unsupported: multi-cycle sequence expression inside consecutive repetition (IEEE 1800-2023 16.9.2)
: ... note: In instance 't'
16 | assert property (@(posedge clk) (a ##1 b) [* 2:$] |-> a);
| ^~
%Error: Exiting due to

3
test_regress/t/t_assert_consec_rep_unsup.v
View File

@ -12,4 +12,7 @@ module t (
// Unsupported: multi-cycle sequence expression inside consecutive repetition
assert property (@(posedge clk) (a ##1 b) [* 2] |-> a);
// Unsupported: the same operand restriction applies to unbounded repetition
assert property (@(posedge clk) (a ##1 b) [* 2:$] |-> a);
endmodule

24
test_regress/t/t_cover_sequence.v
View File

@ -14,6 +14,8 @@ module t (
input clk
);
localparam int MIN_N = 3;
logic [63:0] crc = 64'h5aef0c8dd70a4497;
logic rst_n = 1'b0;
logic a, b, c, d, e;
@ -26,6 +28,14 @@ module t (
int hit_consrep_range = 0;
int hit_consrep_2 = 0;
int hit_consrep_3 = 0;
int hit_consrep_unbounded_0 = 0;
int hit_consrep_star = 0;
int hit_consrep_unbounded_1 = 0;
int hit_consrep_plus = 0;
int hit_consrep_unbounded_2 = 0;
int hit_consrep_unbounded_2_expanded = 0;
int hit_consrep_unbounded_param = 0;
int hit_consrep_unbounded_param_expanded = 0;
default clocking cb @(posedge clk);
endclocking
@ -54,6 +64,16 @@ module t (
cover sequence (a [* 2]) hit_consrep_2++;
cover sequence (a [* 3]) hit_consrep_3++;
// Explicit unbounded ranges and their IEEE 1800-2023 equivalents
cover sequence (a [*0:$]) hit_consrep_unbounded_0++;
cover sequence (a [*]) hit_consrep_star++;
cover sequence (a [*1:$]) hit_consrep_unbounded_1++;
cover sequence (a [+]) hit_consrep_plus++;
cover sequence (a [*2:$]) hit_consrep_unbounded_2++;
cover sequence (a ##1 a [+]) hit_consrep_unbounded_2_expanded++;
cover sequence (a [*MIN_N:$]) hit_consrep_unbounded_param++;
cover sequence (a [*2] ##1 a [+]) hit_consrep_unbounded_param_expanded++;
always @(posedge clk) begin
`ifdef TEST_VERBOSE
$write("[%0t] cyc=%0d crc=%x a=%b b=%b c=%b d=%b e=%b\n", $time, cyc, crc, a, b, c, d, e);
@ -84,6 +104,10 @@ module t (
`checkd(hit_consrep_3, 14); // Other sims: 13
// a[*2:3] == a[*2] or a[*3] (IEEE 1800-2023 16.9.2)
`checkd(hit_consrep_range, hit_consrep_2 + hit_consrep_3);
`checkd(hit_consrep_unbounded_0, hit_consrep_star);
`checkd(hit_consrep_unbounded_1, hit_consrep_plus);
`checkd(hit_consrep_unbounded_2, hit_consrep_unbounded_2_expanded);
`checkd(hit_consrep_unbounded_param, hit_consrep_unbounded_param_expanded);
$write("*-* All Finished *-*\n");
end
endmodule