diff --git a/test_regress/t/t_prop_always.v b/test_regress/t/t_prop_always.v index 6e9fef867..52cfea02c 100644 --- a/test_regress/t/t_prop_always.v +++ b/test_regress/t/t_prop_always.v @@ -38,9 +38,6 @@ module t ( // Bounded weak always over constant-true input. assert property (@(posedge clk) always [0:3] a_high) high_bounded_pass_q.push_back(cyc); - // Strong s_always[m:n] (including its end-of-simulation liveness) is covered - // by t_prop_s_always_liveness; this file stays a pure pass/fail suite. - // Degenerate [0:0]: equivalent to immediate sample. assert property (@(posedge clk) always [0:0] a_high) high_degenerate_pass_q.push_back(cyc); diff --git a/test_regress/t/t_prop_always_wide.v b/test_regress/t/t_prop_always_wide.v index d631ffa6b..742e37d9a 100644 --- a/test_regress/t/t_prop_always_wide.v +++ b/test_regress/t/t_prop_always_wide.v @@ -22,9 +22,6 @@ module t ( assert property (@(posedge clk) always[1: 33] (a_high && b_high && c_high)) wide_pass_q.push_back(cyc); - // Strong wide s_always (and its end-of-simulation liveness) is covered by - // t_prop_s_always_liveness. - always @(posedge clk) begin cyc <= cyc + 1; if (cyc == 49) begin diff --git a/test_regress/t/t_prop_s_always_liveness.out b/test_regress/t/t_prop_s_always_liveness.out index 47e181197..8a1f69c16 100644 --- a/test_regress/t/t_prop_s_always_liveness.out +++ b/test_regress/t/t_prop_s_always_liveness.out @@ -1,4 +1,4 @@ *-* All Finished *-* -[115] %Error: t_prop_s_always_liveness.v:28: Assertion failed in top.t -%Error: t/t_prop_s_always_liveness.v:28: Verilog $stop +[115] %Error: t_prop_s_always_liveness.v:25: Assertion failed in top.t +%Error: t/t_prop_s_always_liveness.v:25: Verilog $stop Aborting... diff --git a/test_regress/t/t_prop_s_always_liveness.v b/test_regress/t/t_prop_s_always_liveness.v index ae4ed8c90..3251b7754 100644 --- a/test_regress/t/t_prop_s_always_liveness.v +++ b/test_regress/t/t_prop_s_always_liveness.v @@ -20,19 +20,11 @@ module t ( int low_s_fail_q[$]; int low_w_fail_q[$]; - // A new attempt starts every tick, so the last hi attempts still have an open - // [2:5] window when the trace ends. Even though a_high is constantly true, - // those unfinished attempts report a liveness failure; Verilator OR-reduces - // them into one end-of-simulation error. (Questa 2022.3: 6 earlier attempts - // complete, the 5 youngest fire the strong else at $finish.) + // The youngest [2:5] windows are still open at $finish, so strong s_always + // reports a liveness failure even with a_high always 1; weak always does not. assert property (@(posedge clk) s_always [2:5] a_high); - // Weak always makes no end-of-trace obligation: silent. assert property (@(posedge clk) always [2:5] a_high); - // Constant-false fails at the first window tick: a safety violation reported - // identically by weak and strong (the strong-only liveness affects just the - // still-open tail). Verilator counts 9 each at cyc 10. (Questa reads 8 -- a - // same-timestep else-vs-read ordering difference, not a semantic one.) assert property (@(posedge clk) s_always [2:5] a_low) else low_s_fail_q.push_back(cyc); assert property (@(posedge clk) always [2:5] a_low)