Drop redundant width sets, cover low-bound rejection, and add s_always per-cycle parity test

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

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