diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 22f4112b7..f45df83f3 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -93,7 +93,10 @@ private: fromAlways = true; } if (!senip) { - nodep->v3warn(E_UNSUPPORTED, "Unsupported: Unclocked assertion"); + nodep->v3error("Concurrent assertion has no clock (IEEE 1800-2023 16.16)\n" + << nodep->warnMore() + << "... Suggest provide a clocking event, a default" + " clocking, or a clocked procedural context"); newp = new AstSenTree{nodep->fileline(), nullptr}; } else { if (cassertp && fromAlways) cassertp->senFromAlways(true); diff --git a/test_regress/t/t_assert_seq_clocking_unsup.out b/test_regress/t/t_assert_seq_clocking_unsup.out index 5ab9bb741..ba12d4ad2 100644 --- a/test_regress/t/t_assert_seq_clocking_unsup.out +++ b/test_regress/t/t_assert_seq_clocking_unsup.out @@ -15,16 +15,20 @@ : ... note: In instance 't' 27 | @clk a | ^ -%Error-UNSUPPORTED: t/t_assert_seq_clocking_unsup.v:32:3: Unsupported: Unclocked assertion - : ... note: In instance 't' +%Error: t/t_assert_seq_clocking_unsup.v:32:3: Concurrent assertion has no clock (IEEE 1800-2023 16.16) + : ... note: In instance 't' + : ... Suggest provide a clocking event, a default clocking, or a clocked procedural context 32 | assert property (s_nest ##1 a); | ^~~~~~ -%Error-UNSUPPORTED: t/t_assert_seq_clocking_unsup.v:33:3: Unsupported: Unclocked assertion - : ... note: In instance 't' + ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. +%Error: t/t_assert_seq_clocking_unsup.v:33:3: Concurrent assertion has no clock (IEEE 1800-2023 16.16) + : ... note: In instance 't' + : ... Suggest provide a clocking event, a default clocking, or a clocked procedural context 33 | assert property (s_level); | ^~~~~~ -%Error-UNSUPPORTED: t/t_assert_seq_clocking_unsup.v:34:3: Unsupported: Unclocked assertion - : ... note: In instance 't' +%Error: t/t_assert_seq_clocking_unsup.v:34:3: Concurrent assertion has no clock (IEEE 1800-2023 16.16) + : ... note: In instance 't' + : ... Suggest provide a clocking event, a default clocking, or a clocked procedural context 34 | assert property (s_level2); | ^~~~~~ %Error: Exiting due to diff --git a/test_regress/t/t_assert_unclocked_bad.out b/test_regress/t/t_assert_unclocked_bad.out new file mode 100644 index 000000000..60590a943 --- /dev/null +++ b/test_regress/t/t_assert_unclocked_bad.out @@ -0,0 +1,22 @@ +%Error: t/t_assert_unclocked_bad.v:9:3: Concurrent assertion has no clock (IEEE 1800-2023 16.16) + : ... note: In instance 't' + : ... Suggest provide a clocking event, a default clocking, or a clocked procedural context + 9 | assert property (a); + | ^~~~~~ + ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. +%Error: t/t_assert_unclocked_bad.v:10:22: Concurrent assertion has no clock (IEEE 1800-2023 16.16) + : ... note: In instance 't' + : ... Suggest provide a clocking event, a default clocking, or a clocked procedural context + 10 | assert property (a |=> b); + | ^~~ +%Error: t/t_assert_unclocked_bad.v:10:3: Concurrent assertion has no clock (IEEE 1800-2023 16.16) + : ... note: In instance 't' + : ... Suggest provide a clocking event, a default clocking, or a clocked procedural context + 10 | assert property (a |=> b); + | ^~~~~~ +%Error: t/t_assert_unclocked_bad.v:11:3: Concurrent assertion has no clock (IEEE 1800-2023 16.16) + : ... note: In instance 't' + : ... Suggest provide a clocking event, a default clocking, or a clocked procedural context + 11 | cover property (a); + | ^~~~~ +%Error: Exiting due to diff --git a/test_regress/t/t_property_pexpr_unsup.py b/test_regress/t/t_assert_unclocked_bad.py similarity index 67% rename from test_regress/t/t_property_pexpr_unsup.py rename to test_regress/t/t_assert_unclocked_bad.py index 9768aebfc..77a0ac64b 100755 --- a/test_regress/t/t_property_pexpr_unsup.py +++ b/test_regress/t/t_assert_unclocked_bad.py @@ -4,15 +4,13 @@ # 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: 2024 Wilson Snyder +# SPDX-FileCopyrightText: 2026 Wilson Snyder # SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 import vltest_bootstrap test.scenarios('vlt') -test.compile(expect_filename=test.golden_filename, - verilator_flags2=['--timing', '--error-limit 1000'], - fails=test.vlt_all) +test.lint(expect_filename=test.golden_filename, fails=True) test.passes() diff --git a/test_regress/t/t_assert_unclocked_bad.v b/test_regress/t/t_assert_unclocked_bad.v new file mode 100644 index 000000000..ae659cf7b --- /dev/null +++ b/test_regress/t/t_assert_unclocked_bad.v @@ -0,0 +1,12 @@ +// 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; + logic a, b; + assert property (a); + assert property (a |=> b); + cover property (a); +endmodule diff --git a/test_regress/t/t_property_pexpr_unsup.out b/test_regress/t/t_property_pexpr_unsup.out deleted file mode 100644 index bae43d802..000000000 --- a/test_regress/t/t_property_pexpr_unsup.out +++ /dev/null @@ -1,26 +0,0 @@ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:115:21: Unsupported: Unclocked assertion - : ... note: In instance 't' - 115 | assert property ((s_eventually a) implies (s_eventually a)); - | ^~~~~~~~~~~~ - ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:115:46: Unsupported: Unclocked assertion - : ... note: In instance 't' - 115 | assert property ((s_eventually a) implies (s_eventually a)); - | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:115:3: Unsupported: Unclocked assertion - : ... note: In instance 't' - 115 | assert property ((s_eventually a) implies (s_eventually a)); - | ^~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:117:21: Unsupported: Unclocked assertion - : ... note: In instance 't' - 117 | assert property ((s_eventually a) iff (s_eventually a)); - | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:117:42: Unsupported: Unclocked assertion - : ... note: In instance 't' - 117 | assert property ((s_eventually a) iff (s_eventually a)); - | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:117:3: Unsupported: Unclocked assertion - : ... note: In instance 't' - 117 | assert property ((s_eventually a) iff (s_eventually a)); - | ^~~~~~ -%Error: Exiting due to diff --git a/test_regress/t/t_property_s_eventually_unsup.out b/test_regress/t/t_property_s_eventually_unsup.out index 6a9be1c3a..e4355f13f 100644 --- a/test_regress/t/t_property_s_eventually_unsup.out +++ b/test_regress/t/t_property_s_eventually_unsup.out @@ -1,12 +1,8 @@ -%Error-UNSUPPORTED: t/t_property_s_eventually_unsup.v:14:20: Unsupported: Unclocked assertion +%Error-UNSUPPORTED: t/t_property_s_eventually_unsup.v:14:35: Unsupported: cycle delay in s_eventually : ... note: In instance 't' - 14 | assert property (s_eventually ##1 1); - | ^~~~~~~~~~~~ + 14 | assert property (@(posedge clk) s_eventually ##1 1); + | ^~~~~~~~~~~~ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error-UNSUPPORTED: t/t_property_s_eventually_unsup.v:14:3: Unsupported: Unclocked assertion - : ... note: In instance 't' - 14 | assert property (s_eventually ##1 1); - | ^~~~~~ %Error-UNSUPPORTED: t/t_property_s_eventually_unsup.v:15:35: Unsupported: cycle delay in s_eventually : ... note: In instance 't' 15 | assert property (@(negedge clk) s_eventually ##1 1); diff --git a/test_regress/t/t_property_s_eventually_unsup.v b/test_regress/t/t_property_s_eventually_unsup.v index 9338a0f4d..02a22a127 100644 --- a/test_regress/t/t_property_s_eventually_unsup.v +++ b/test_regress/t/t_property_s_eventually_unsup.v @@ -11,7 +11,7 @@ module t; localparam MAX = 3; integer cyc = 1; - assert property (s_eventually ##1 1); + assert property (@(posedge clk) s_eventually ##1 1); assert property (@(negedge clk) s_eventually ##1 1); always @(posedge clk) begin diff --git a/test_regress/t/t_sequence_first_match_unsup.out b/test_regress/t/t_sequence_first_match_unsup.out deleted file mode 100644 index e4e3a5d37..000000000 --- a/test_regress/t/t_sequence_first_match_unsup.out +++ /dev/null @@ -1,47 +0,0 @@ -%Error: t/t_sequence_first_match_unsup.v:51:34: Usage of cycle delays requires default clocking (IEEE 1800-2023 14.11) - : ... note: In instance 'main' - 51 | initial p0 : assert property ((##1 1) or(##2 1) |-> x == 1); - | ^~ - ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. -%Error: t/t_sequence_first_match_unsup.v:51:44: Usage of cycle delays requires default clocking (IEEE 1800-2023 14.11) - : ... note: In instance 'main' - 51 | initial p0 : assert property ((##1 1) or(##2 1) |-> x == 1); - | ^~ -%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:51:16: Unsupported: Unclocked assertion - : ... note: In instance 'main' - 51 | initial p0 : assert property ((##1 1) or(##2 1) |-> x == 1); - | ^~~~~~ - ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error: t/t_sequence_first_match_unsup.v:54:47: Usage of cycle delays requires default clocking (IEEE 1800-2023 14.11) - : ... note: In instance 'main' - 54 | initial p1 : assert property (first_match ((##1 1) or(##2 1)) |-> x == 1); - | ^~ -%Error: t/t_sequence_first_match_unsup.v:54:57: Usage of cycle delays requires default clocking (IEEE 1800-2023 14.11) - : ... note: In instance 'main' - 54 | initial p1 : assert property (first_match ((##1 1) or(##2 1)) |-> x == 1); - | ^~ -%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:54:16: Unsupported: Unclocked assertion - : ... note: In instance 'main' - 54 | initial p1 : assert property (first_match ((##1 1) or(##2 1)) |-> x == 1); - | ^~~~~~ -%Error: t/t_sequence_first_match_unsup.v:57:38: Usage of cycle delays requires default clocking (IEEE 1800-2023 14.11) - : ... note: In instance 'main' - 57 | initial p2 : assert property (1 or ##1 1 |-> x == 0); - | ^~ -%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:57:16: Unsupported: Unclocked assertion - : ... note: In instance 'main' - 57 | initial p2 : assert property (1 or ##1 1 |-> x == 0); - | ^~~~~~ -%Error: t/t_sequence_first_match_unsup.v:60:51: Usage of cycle delays requires default clocking (IEEE 1800-2023 14.11) - : ... note: In instance 'main' - 60 | initial p3 : assert property (first_match (1 or ##1 1) |-> x == 0); - | ^~ -%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:60:16: Unsupported: Unclocked assertion - : ... note: In instance 'main' - 60 | initial p3 : assert property (first_match (1 or ##1 1) |-> x == 0); - | ^~~~~~ -%Error: Internal Error: t/t_sequence_first_match_unsup.v:51:34: ../V3Ast.cpp:#: AstSExpr must have non-nullptr delayp() - : ... note: In instance 'main' - 51 | initial p0 : assert property ((##1 1) or(##2 1) |-> x == 1); - | ^~ - ... This fatal error may be caused by the earlier error(s); resolve those first. diff --git a/test_regress/t/t_sequence_first_match_unsup.py b/test_regress/t/t_sequence_first_match_unsup.py deleted file mode 100755 index 235ad76f1..000000000 --- a/test_regress/t/t_sequence_first_match_unsup.py +++ /dev/null @@ -1,18 +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: 2025 Wilson Snyder -# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 - -import vltest_bootstrap - -test.scenarios('simulator') - -test.lint(expect_filename=test.golden_filename, - verilator_flags2=['--assert --error-limit 1000'], - fails=True) - -test.passes() diff --git a/test_regress/t/t_sequence_first_match_unsup.v b/test_regress/t/t_sequence_first_match_unsup.v deleted file mode 100644 index 5f4d08838..000000000 --- a/test_regress/t/t_sequence_first_match_unsup.v +++ /dev/null @@ -1,62 +0,0 @@ -// SPDX-FileCopyrightText: 2001-2020 Daniel Kroening, Edmund Clarke -// SPDX-License-Identifier: BSD-3-Clause -// -// (C) 2001-2020, Daniel Kroening, Edmund Clarke, -// Computer Science Department, University of Oxford -// Computer Science Department, Carnegie Mellon University -// -// All rights reserved. Redistribution and use in source and binary forms, with -// or without modification, are permitted provided that the following -// conditions are met: -// -// 1. Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// -// 2. Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// -// 3. Neither the name of the University nor the names of its contributors -// may be used to endorse or promote products derived from this software -// without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" -// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE -// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE -// ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE -// LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR -// CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF -// SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS -// INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN -// CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) -// ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE -// POSSIBILITY OF SUCH DAMAGE. -// -// You can contact the author at: -// - homepage : https://www.cprover.org/ebmc/ -// - source repository : https://github.com/diffblue/hw-cbmc - -module main ( - input clk -); - - reg [31:0] x = 0; - - always @(posedge clk) x <= x + 1; - - // Starting from a particular state, - // first_match yields the sequence that _ends_ first. - - // fails - initial p0 : assert property ((##1 1) or(##2 1) |-> x == 1); - - // passes - initial p1 : assert property (first_match ((##1 1) or(##2 1)) |-> x == 1); - - // fails - initial p2 : assert property (1 or ##1 1 |-> x == 0); - - // passes - initial p3 : assert property (first_match (1 or ##1 1) |-> x == 0); - -endmodule