diff --git a/test_regress/t/t_prop_s_always_liveness.out b/test_regress/t/t_prop_s_always_liveness.out new file mode 100644 index 000000000..47e181197 --- /dev/null +++ b/test_regress/t/t_prop_s_always_liveness.out @@ -0,0 +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 +Aborting... diff --git a/test_regress/t/t_prop_s_always_liveness.py b/test_regress/t/t_prop_s_always_liveness.py index 9ceaaa7be..e6fa1c51f 100755 --- a/test_regress/t/t_prop_s_always_liveness.py +++ b/test_regress/t/t_prop_s_always_liveness.py @@ -12,6 +12,6 @@ import vltest_bootstrap test.scenarios('vlt') test.compile(verilator_flags2=['--assert']) -test.execute(fails=True) +test.execute(fails=True, expect_filename=test.golden_filename) 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 5ab93809b..ae4ed8c90 100644 --- a/test_regress/t/t_prop_s_always_liveness.v +++ b/test_regress/t/t_prop_s_always_liveness.v @@ -15,24 +15,34 @@ module t ( int cyc = 0; logic a_high = 1'b1; - logic a_low = 1'b0; + 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); + // 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.) + 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); - 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); + // 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) + else low_w_fail_q.push_back(cyc); always @(posedge clk) begin cyc <= cyc + 1; - if (cyc == 4) begin - `checkd(low_s_fail_q.size(), 3); - `checkd(low_w_fail_q.size(), 3); + if (cyc == 10) begin + `checkd(low_s_fail_q.size(), low_w_fail_q.size()); + `checkd(low_w_fail_q.size(), 9); $write("*-* All Finished *-*\n"); $finish; end