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

Clock s_eventually unsup test and drop stale unclocked pexpr/first_match tests

This commit is contained in:
Yilou Wang 2026-06-23 15:55:31 +02:00
parent d9d26fa54f
commit e533017060
7 changed files with 6 additions and 181 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
test_regress/t/t_property_pexpr_unsup.out
View File

@ -1,26 +0,0 @@
%Error: t/t_property_pexpr_unsup.v:115:21: Concurrent assertion has no clock; provide a clocking event, a default clocking, or a clocked procedural context (IEEE 1800-2023 16.16)
: ... note: In instance 't'
115 | assert property ((s_eventually a) implies (s_eventually a));
| ^~~~~~~~~~~~
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
%Error: t/t_property_pexpr_unsup.v:115:46: Concurrent assertion has no clock; provide a clocking event, a default clocking, or a clocked procedural context (IEEE 1800-2023 16.16)
: ... note: In instance 't'
115 | assert property ((s_eventually a) implies (s_eventually a));
| ^~~~~~~~~~~~
%Error: t/t_property_pexpr_unsup.v:115:3: Concurrent assertion has no clock; provide a clocking event, a default clocking, or a clocked procedural context (IEEE 1800-2023 16.16)
: ... note: In instance 't'
115 | assert property ((s_eventually a) implies (s_eventually a));
| ^~~~~~
%Error: t/t_property_pexpr_unsup.v:117:21: Concurrent assertion has no clock; provide a clocking event, a default clocking, or a clocked procedural context (IEEE 1800-2023 16.16)
: ... note: In instance 't'
117 | assert property ((s_eventually a) iff (s_eventually a));
| ^~~~~~~~~~~~
%Error: t/t_property_pexpr_unsup.v:117:42: Concurrent assertion has no clock; provide a clocking event, a default clocking, or a clocked procedural context (IEEE 1800-2023 16.16)
: ... note: In instance 't'
117 | assert property ((s_eventually a) iff (s_eventually a));
| ^~~~~~~~~~~~
%Error: t/t_property_pexpr_unsup.v:117:3: Concurrent assertion has no clock; provide a clocking event, a default clocking, or a clocked procedural context (IEEE 1800-2023 16.16)
: ... note: In instance 't'
117 | assert property ((s_eventually a) iff (s_eventually a));
| ^~~~~~
%Error: Exiting due to

18
test_regress/t/t_property_pexpr_unsup.py
View File

@ -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: 2024 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.passes()

15
test_regress/t/t_property_s_eventually_unsup.out
View File

@ -1,15 +1,10 @@
%Error: t/t_property_s_eventually_unsup.v:14:20: Concurrent assertion has no clock; provide a clocking event, a default clocking, or a clocked procedural context (IEEE 1800-2023 16.16) %Error-UNSUPPORTED: t/t_property_s_eventually_unsup.v:14:35: Unsupported: cycle delay in s_eventually
: ... note: In instance 't' : ... note: In instance 't'
14 | assert property (s_eventually ##1 1); 14 | assert property (@(posedge clk) s_eventually ##1 1);
| ^~~~~~~~~~~~ | ^~~~~~~~~~~~
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error: t/t_property_s_eventually_unsup.v:14:3: Concurrent assertion has no clock; provide a clocking event, a default clocking, or a clocked procedural context (IEEE 1800-2023 16.16)
: ... 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 %Error-UNSUPPORTED: t/t_property_s_eventually_unsup.v:15:35: Unsupported: cycle delay in s_eventually
: ... note: In instance 't' : ... note: In instance 't'
15 | assert property (@(negedge clk) s_eventually ##1 1); 15 | assert property (@(negedge clk) s_eventually ##1 1);
| ^~~~~~~~~~~~ | ^~~~~~~~~~~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error: Exiting due to %Error: Exiting due to

2
test_regress/t/t_property_s_eventually_unsup.v
View File

@ -11,7 +11,7 @@ module t;
localparam MAX = 3; localparam MAX = 3;
integer cyc = 1; 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); assert property (@(negedge clk) s_eventually ##1 1);
always @(posedge clk) begin always @(posedge clk) begin

46
test_regress/t/t_sequence_first_match_unsup.out
View File

@ -1,46 +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: t/t_sequence_first_match_unsup.v:51:16: Concurrent assertion has no clock; provide a clocking event, a default clocking, or a clocked procedural context (IEEE 1800-2023 16.16)
: ... note: In instance 'main'
51 | initial p0 : assert property ((##1 1) or(##2 1) |-> x == 1);
| ^~~~~~
%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: t/t_sequence_first_match_unsup.v:54:16: Concurrent assertion has no clock; provide a clocking event, a default clocking, or a clocked procedural context (IEEE 1800-2023 16.16)
: ... 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: t/t_sequence_first_match_unsup.v:57:16: Concurrent assertion has no clock; provide a clocking event, a default clocking, or a clocked procedural context (IEEE 1800-2023 16.16)
: ... 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: t/t_sequence_first_match_unsup.v:60:16: Concurrent assertion has no clock; provide a clocking event, a default clocking, or a clocked procedural context (IEEE 1800-2023 16.16)
: ... 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.

18
test_regress/t/t_sequence_first_match_unsup.py
View File

@ -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()

62
test_regress/t/t_sequence_first_match_unsup.v
View File

@ -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