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

update tests

This commit is contained in:
Yilou Wang 2026-04-05 11:53:51 +02:00
parent eaebb81060
commit d98c5621e3
15 changed files with 56 additions and 105 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/V3AssertProp.cpp
View File

@ -112,15 +112,10 @@ class AssertPropConsRepVisitor final : public VNVisitor {
FileLine* const flp = nodep->fileline();
AstNodeExpr* const exprp = nodep->exprp()->unlinkFrBack();
if (r.minN == 0 && r.unbounded) {
// [*]: always matches (zero or more -- no temporal constraint alone)
VL_DO_DANGLING(exprp->deleteTree(), exprp);
nodep->replaceWith(new AstConst{flp, AstConst::BitTrue{}});
VL_DO_DANGLING(nodep->deleteTree(), nodep);
return;
}
if (r.minN <= 1 && (r.unbounded || !nodep->maxCountp())) {
// [+] or [*1]: just the expression itself
// [+], [*], or [*1]: reduce to the expression itself.
// [*] (zero-or-more) uses the shortest non-vacuous match (length 1 when expr=true),
// matching simulator behavior; zero-length matches do not trigger |-> implications.
nodep->replaceWith(exprp);
VL_DO_DANGLING(nodep->deleteTree(), nodep);
return;

2
test_regress/t/t_assert_prop_consec_rep.py
View File

@ -11,7 +11,7 @@ import vltest_bootstrap
test.scenarios('simulator')
test.compile()
test.compile(verilator_flags2=['--timing'])
test.execute()

34
test_regress/t/t_assert_prop_consec_rep.v
View File

@ -28,27 +28,47 @@ module t (
int count_fail3 = 0;
int count_fail4 = 0;
int count_fail5 = 0;
int count_fail6 = 0;
int count_fail7 = 0;
int count_fail8 = 0;
int count_fail9 = 0;
// Test 1: a[*3] |-> b (3 consecutive, overlapping implication)
// Test 1: a[*3] |-> b
assert property (@(posedge clk) a [* 3] |-> b)
else count_fail1 <= count_fail1 + 1;
// Test 2: a[*1] |-> c (trivial [*1], overlapping)
// Test 2: a[*1] |-> c
assert property (@(posedge clk) a [* 1] |-> c)
else count_fail2 <= count_fail2 + 1;
// Test 3: a[*2] |=> d (2 consecutive, non-overlapping implication)
// Test 3: a[*2] |=> d
assert property (@(posedge clk) a [* 2] |=> d)
else count_fail3 <= count_fail3 + 1;
// Test 4: standalone consecutive rep (no implication)
// Test 4: b[*2] standalone
assert property (@(posedge clk) b [* 2])
else count_fail4 <= count_fail4 + 1;
// Test 5: [*10000] large count -- verifies counter-based lowering compiles
// Test 5: a[*10000] large count
assert property (@(posedge clk) a [* 10000] |-> b)
else count_fail5 <= count_fail5 + 1;
// Test 6: a[*1:3] ##1 b -- bounded range in SExpr
assert property (@(posedge clk) a [* 1:3] ##1 b)
else count_fail6 <= count_fail6 + 1;
// Test 7: a[+] ##1 b -- one-or-more in SExpr
assert property (@(posedge clk) a [+] ##1 b)
else count_fail7 <= count_fail7 + 1;
// Test 8: a[+] |-> b -- standalone [+] (same as a |-> b)
assert property (@(posedge clk) a [+] |-> b)
else count_fail8 <= count_fail8 + 1;
// Test 9: a[*] |-> b -- standalone [*] (shortest non-vacuous match = a)
assert property (@(posedge clk) a [*] |-> b)
else count_fail9 <= count_fail9 + 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);
@ -65,6 +85,10 @@ module t (
`checkd(count_fail3, 9);
`checkd(count_fail4, 74);
`checkd(count_fail5, 0);
`checkd(count_fail6, 65);
`checkd(count_fail7, 65);
`checkd(count_fail8, 20);
`checkd(count_fail9, 20);
$write("*-* All Finished *-*\n");
$finish;
end

4
test_regress/t/t_assert_prop_consec_rep_bad.v
View File

@ -11,7 +11,7 @@ module t (input clk);
// Bad: non-constant repetition count
assert property (@(posedge clk) a [*n] |-> 1);
// Bad: [*0] consecutive repetition unsupported
// Bad: [*0] unsupported exact zero repetition
assert property (@(posedge clk) a [*0] |-> 1);
// Bad: max count < min count
@ -20,7 +20,7 @@ module t (input clk);
// Bad: non-constant max count
assert property (@(posedge clk) a [*1:n] |-> 1);
// Bad: zero max count ([*0:0])
// Bad: [*N:0] zero max count
assert property (@(posedge clk) a [*0:0] |-> 1);
endmodule

6
test_regress/t/t_assert_prop_consec_rep_delay_unsup.out
View File

@ -1,6 +0,0 @@
%Error-UNSUPPORTED: t/t_assert_prop_consec_rep_delay_unsup.v:11:41: Unsupported: consecutive repetition with non-##1 cycle delay
: ... note: In instance 't'
11 | assert property (@(posedge clk) a[*2] ##3 b);
| ^~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error: Exiting due to

13
test_regress/t/t_assert_prop_consec_rep_delay_unsup.v
View File

@ -1,13 +0,0 @@
// 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;
// Bad: consecutive repetition with non-##1 delay
assert property (@(posedge clk) a[*2] ##3 b);
endmodule

6
test_regress/t/t_assert_prop_consec_rep_range_bad.out
View File

@ -1,6 +0,0 @@
%Error-UNSUPPORTED: t/t_assert_prop_consec_rep_range_bad.v:11:37: Unsupported: standalone consecutive repetition range
: ... note: In instance 't'
11 | assert property (@(posedge clk) a [*2:3] |-> 1);
| ^~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error: Exiting due to

16
test_regress/t/t_assert_prop_consec_rep_range_bad.py
View File

@ -1,16 +0,0 @@
#!/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()

13
test_regress/t/t_assert_prop_consec_rep_range_bad.v
View File

@ -1,13 +0,0 @@
// 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;
// Bad: standalone range repetition (no ## delay to anchor the sequence)
assert property (@(posedge clk) a [*2:3] |-> 1);
endmodule

6
test_regress/t/t_assert_prop_consec_rep_trail_unsup.out
View File

@ -1,6 +0,0 @@
%Error-UNSUPPORTED: t/t_assert_prop_consec_rep_trail_unsup.v:11:42: Unsupported: trailing consecutive repetition range in sequence expression (e.g. a ##1 b[+])
: ... note: In instance 't'
11 | assert property (@(posedge clk) b ##1 a[+]);
| ^~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error: Exiting due to

16
test_regress/t/t_assert_prop_consec_rep_trail_unsup.py
View File

@ -1,16 +0,0 @@
#!/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()

14
test_regress/t/t_assert_prop_consec_rep_unsup.out Normal file
View File

@ -0,0 +1,14 @@
%Error-UNSUPPORTED: t/t_assert_prop_consec_rep_unsup.v:11:42: Unsupported: consecutive repetition with non-##1 cycle delay
: ... note: In instance 't'
11 | assert property (@(posedge clk) a [*2] ##3 b);
| ^~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_assert_prop_consec_rep_unsup.v:14:37: Unsupported: standalone consecutive repetition range
: ... note: In instance 't'
14 | assert property (@(posedge clk) a [*2:3] |-> 1);
| ^~
%Error-UNSUPPORTED: t/t_assert_prop_consec_rep_unsup.v:17:42: Unsupported: trailing consecutive repetition range in sequence expression (e.g. a ##1 b[+])
: ... note: In instance 't'
17 | assert property (@(posedge clk) b ##1 a[+]);
| ^~~
%Error: Exiting due to

0
test_regress/t/t_assert_prop_consec_rep_delay_unsup.py → test_regress/t/t_assert_prop_consec_rep_unsup.py Executable file → Normal file
View File

8
test_regress/t/t_assert_prop_consec_rep_trail_unsup.v → test_regress/t/t_assert_prop_consec_rep_unsup.v
View File

@ -7,7 +7,13 @@
module t (input clk);
logic a, b;
// Bad: trailing consecutive repetition range in sequence expression
// Unsupported: non-##1 inter-repetition delay
assert property (@(posedge clk) a [*2] ##3 b);
// Unsupported: standalone range repetition (no ## anchor)
assert property (@(posedge clk) a [*2:3] |-> 1);
// Unsupported: trailing consecutive repetition in sequence
assert property (@(posedge clk) b ##1 a[+]);
endmodule

12
test_regress/t/t_sequence_sexpr_unsup.out
View File

@ -20,18 +20,6 @@
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:82:7: Unsupported: ## [+] cycle delay range expression
82 | a ## [+] b;
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:89:7: Unsupported: [*] boolean abbrev expression
89 | a [*];
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:89:7: Unsupported: boolean abbrev (in sequence expression)
89 | a [*];
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:92:7: Unsupported: [+] boolean abbrev expression
92 | a [+];
| ^~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:92:7: Unsupported: boolean abbrev (in sequence expression)
92 | a [+];
| ^~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:95:7: Unsupported: [= boolean abbrev expression
95 | a [= 1];
| ^~