diff --git a/src/V3AssertProp.cpp b/src/V3AssertProp.cpp index 5b680b766..9e8ee282e 100644 --- a/src/V3AssertProp.cpp +++ b/src/V3AssertProp.cpp @@ -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; diff --git a/test_regress/t/t_assert_prop_consec_rep.py b/test_regress/t/t_assert_prop_consec_rep.py index 8a938befd..f090e5249 100755 --- a/test_regress/t/t_assert_prop_consec_rep.py +++ b/test_regress/t/t_assert_prop_consec_rep.py @@ -11,7 +11,7 @@ import vltest_bootstrap test.scenarios('simulator') -test.compile() +test.compile(verilator_flags2=['--timing']) test.execute() diff --git a/test_regress/t/t_assert_prop_consec_rep.v b/test_regress/t/t_assert_prop_consec_rep.v index a6f4421e6..512b98706 100644 --- a/test_regress/t/t_assert_prop_consec_rep.v +++ b/test_regress/t/t_assert_prop_consec_rep.v @@ -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 diff --git a/test_regress/t/t_assert_prop_consec_rep_bad.v b/test_regress/t/t_assert_prop_consec_rep_bad.v index df81234e9..7c9a10d3a 100644 --- a/test_regress/t/t_assert_prop_consec_rep_bad.v +++ b/test_regress/t/t_assert_prop_consec_rep_bad.v @@ -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 diff --git a/test_regress/t/t_assert_prop_consec_rep_delay_unsup.out b/test_regress/t/t_assert_prop_consec_rep_delay_unsup.out deleted file mode 100644 index 9b6379796..000000000 --- a/test_regress/t/t_assert_prop_consec_rep_delay_unsup.out +++ /dev/null @@ -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 diff --git a/test_regress/t/t_assert_prop_consec_rep_delay_unsup.v b/test_regress/t/t_assert_prop_consec_rep_delay_unsup.v deleted file mode 100644 index 55cecfef6..000000000 --- a/test_regress/t/t_assert_prop_consec_rep_delay_unsup.v +++ /dev/null @@ -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 diff --git a/test_regress/t/t_assert_prop_consec_rep_range_bad.out b/test_regress/t/t_assert_prop_consec_rep_range_bad.out deleted file mode 100644 index 1e2b2f5bc..000000000 --- a/test_regress/t/t_assert_prop_consec_rep_range_bad.out +++ /dev/null @@ -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 diff --git a/test_regress/t/t_assert_prop_consec_rep_range_bad.py b/test_regress/t/t_assert_prop_consec_rep_range_bad.py deleted file mode 100755 index 38cf36b43..000000000 --- a/test_regress/t/t_assert_prop_consec_rep_range_bad.py +++ /dev/null @@ -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() diff --git a/test_regress/t/t_assert_prop_consec_rep_range_bad.v b/test_regress/t/t_assert_prop_consec_rep_range_bad.v deleted file mode 100644 index 8014fdfa6..000000000 --- a/test_regress/t/t_assert_prop_consec_rep_range_bad.v +++ /dev/null @@ -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 diff --git a/test_regress/t/t_assert_prop_consec_rep_trail_unsup.out b/test_regress/t/t_assert_prop_consec_rep_trail_unsup.out deleted file mode 100644 index 474c5bc40..000000000 --- a/test_regress/t/t_assert_prop_consec_rep_trail_unsup.out +++ /dev/null @@ -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 diff --git a/test_regress/t/t_assert_prop_consec_rep_trail_unsup.py b/test_regress/t/t_assert_prop_consec_rep_trail_unsup.py deleted file mode 100755 index 38cf36b43..000000000 --- a/test_regress/t/t_assert_prop_consec_rep_trail_unsup.py +++ /dev/null @@ -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() diff --git a/test_regress/t/t_assert_prop_consec_rep_unsup.out b/test_regress/t/t_assert_prop_consec_rep_unsup.out new file mode 100644 index 000000000..610a15565 --- /dev/null +++ b/test_regress/t/t_assert_prop_consec_rep_unsup.out @@ -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 diff --git a/test_regress/t/t_assert_prop_consec_rep_delay_unsup.py b/test_regress/t/t_assert_prop_consec_rep_unsup.py old mode 100755 new mode 100644 similarity index 100% rename from test_regress/t/t_assert_prop_consec_rep_delay_unsup.py rename to test_regress/t/t_assert_prop_consec_rep_unsup.py diff --git a/test_regress/t/t_assert_prop_consec_rep_trail_unsup.v b/test_regress/t/t_assert_prop_consec_rep_unsup.v similarity index 51% rename from test_regress/t/t_assert_prop_consec_rep_trail_unsup.v rename to test_regress/t/t_assert_prop_consec_rep_unsup.v index 9c8404c6f..b1f77504c 100644 --- a/test_regress/t/t_assert_prop_consec_rep_trail_unsup.v +++ b/test_regress/t/t_assert_prop_consec_rep_unsup.v @@ -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 diff --git a/test_regress/t/t_sequence_sexpr_unsup.out b/test_regress/t/t_sequence_sexpr_unsup.out index e97f8e521..d5e9fe632 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.out +++ b/test_regress/t/t_sequence_sexpr_unsup.out @@ -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]; | ^~