Fix stale property expression after s_eventually (#8614) (#8619)

This commit is contained in:
Doha Nam
2026-10-05 19:49:34 -04:00
committed by GitHub
parent 303ebe861b
commit 9b7fad3d77
5 changed files with 43 additions and 0 deletions
+1
View File
@@ -1115,6 +1115,7 @@ private:
finalp->addStmtsp(initActiveCountp);
finalp->addStmtsp(finalLoopp);
VL_RESTORER(m_pexprp);
m_pexprp = new AstPExpr{flp, bodyp, finalp, nodep->dtypep()};
VL_RESTORER(m_hasCycleDelay);
m_hasCycleDelay = false;
@@ -18,15 +18,21 @@ module t;
localparam MAX = 1000;
integer cyc = 0;
integer passed = 0;
integer passed_until = 0;
assert property (@(negedge clk) s_eventually 1)
++passed;
// 'until' after 's_eventually' in the same module (#8614)
assert property (@(negedge clk) cyc > 0 until cyc > 0)
++passed_until;
always @(posedge clk) begin
++cyc;
if (cyc == MAX) begin
$display("%d", passed);
if (passed != 999) $stop;
if (passed_until != 999) $stop; // Same as 'passed': each attempt passes on its first edge
$write("*-* All Finished *-*\n");
$finish;
end
@@ -0,0 +1,6 @@
%Error: t/t_property_s_eventually_bad.v:13:10: Usage of cycle delays requires default clocking (IEEE 1800-2023 14.11)
: ... note: In instance 't'
13 | always ##1;
| ^~
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
%Error: Exiting due to
+16
View File
@@ -0,0 +1,16 @@
#!/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, verilator_flags2=['--timing'], expect_filename=test.golden_filename)
test.passes()
@@ -0,0 +1,14 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain.
// SPDX-FileCopyrightText: 2026 Doha Nam
// SPDX-License-Identifier: CC0-1.0
module t (
input clk,
input a
);
// A cycle delay after 's_eventually' still requires default clocking (#8614)
assert property (@(posedge clk) s_eventually a);
always ##1;
endmodule