diff --git a/test_regress/t/t_prop_s_always_liveness.py b/test_regress/t/t_prop_s_always_liveness.py index 91b8bb235..9ceaaa7be 100755 --- a/test_regress/t/t_prop_s_always_liveness.py +++ b/test_regress/t/t_prop_s_always_liveness.py @@ -12,12 +12,6 @@ import vltest_bootstrap test.scenarios('vlt') test.compile(verilator_flags2=['--assert']) - -# a is always 1 so there is no per-cycle safety failure: the ONLY failure source -# is the strong end-of-simulation liveness obligation of s_always[1:1] (its window -# is cut off by $finish), so the simulation must exit non-zero. If the in-window -# marking regresses (e.g. the offset-hi vertex stops being flagged), s_always[1:1] -# goes silent, the run succeeds, and this test fails -- catching the regression. test.execute(fails=True) test.passes() diff --git a/test_regress/t/t_prop_s_always_liveness.v b/test_regress/t/t_prop_s_always_liveness.v index f7958f33c..5ab93809b 100644 --- a/test_regress/t/t_prop_s_always_liveness.v +++ b/test_regress/t/t_prop_s_always_liveness.v @@ -4,36 +4,35 @@ // SPDX-FileCopyrightText: 2026 PlanV GmbH // SPDX-License-Identifier: CC0-1.0 +// verilog_format: off +`define stop $stop +`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); +// verilog_format: on + module t ( input clk ); int cyc = 0; - logic a = 1'b1; - logic rst = 1'b1; + logic a_high = 1'b1; + logic a_low = 1'b0; + + int low_s_fail_q[$]; + int low_w_fail_q[$]; + + as_liveness: assert property (@(posedge clk) s_always [2:5] a_high); + as_weak: assert property (@(posedge clk) always [2:5] a_high); + + as_low_s: assert property (@(posedge clk) s_always [2:5] a_low) + ; else low_s_fail_q.push_back(cyc); + as_low_w: assert property (@(posedge clk) always [2:5] a_low) + ; else low_w_fail_q.push_back(cyc); always @(posedge clk) begin cyc <= cyc + 1; - if (cyc == 0) rst <= 1'b0; - end - - // a is always 1, so there is no per-cycle safety failure. The ONLY way these - // can fail is the strong end-of-simulation liveness obligation: attempts whose - // [m:n] window is cut off by $finish must fail (IEEE 1800-2023 16.12.11). - - // Single-tick window s_always[1:1]: its in-window state is ONE registered - // vertex, so a dropped end-of-trace obligation produces total silence (no - // shallower attempt can mask it). It is the most sensitive guard and shares - // the in-window marking with every s_always[m:n], so if it fires the deeper - // windows do too. $finish halts on the first liveness $error, so a single - // strong assertion keeps the failure attributable to this case. - as_mm: assert property (@(posedge clk) disable iff (rst) s_always [1:1] a); - - // Weak twin imposes no end-of-trace obligation: never fails on this trace. - as_weak: assert property (@(posedge clk) disable iff (rst) always [1:4] a); - - always @(posedge clk) begin - if (cyc == 10) begin + if (cyc == 4) begin + `checkd(low_s_fail_q.size(), 3); + `checkd(low_w_fail_q.size(), 3); $write("*-* All Finished *-*\n"); $finish; end