Add golden file and completing-attempt run to s_always liveness test

This commit is contained in:
Yilou Wang 2026-06-17 20:59:41 +02:00
parent 500d8cb725
commit ba3371a90d
3 changed files with 25 additions and 11 deletions

View File

@ -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...

View File

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

View File

@ -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