luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Trim comments in always property tests and update s_always liveness golden

This commit is contained in:
Yilou Wang 2026-06-17 23:21:12 +02:00
parent 851206f124
commit 065a344bc5
4 changed files with 4 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
test_regress/t/t_prop_always.v
View File

@ -38,9 +38,6 @@ module t (
// Bounded weak always over constant-true input. // Bounded weak always over constant-true input.
assert property (@(posedge clk) always [0:3] a_high) high_bounded_pass_q.push_back(cyc); 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. // Degenerate [0:0]: equivalent to immediate sample.
assert property (@(posedge clk) always [0:0] a_high) high_degenerate_pass_q.push_back(cyc); assert property (@(posedge clk) always [0:0] a_high) high_degenerate_pass_q.push_back(cyc);

3
test_regress/t/t_prop_always_wide.v
View File

@ -22,9 +22,6 @@ module t (
assert property (@(posedge clk) always[1: 33] (a_high && b_high && c_high)) assert property (@(posedge clk) always[1: 33] (a_high && b_high && c_high))
wide_pass_q.push_back(cyc); 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 always @(posedge clk) begin
cyc <= cyc + 1; cyc <= cyc + 1;
if (cyc == 49) begin if (cyc == 49) begin

4
test_regress/t/t_prop_s_always_liveness.out
View File

@ -1,4 +1,4 @@
*-* All Finished *-* *-* All Finished *-*
[115] %Error: t_prop_s_always_liveness.v:28: Assertion failed in top.t [115] %Error: t_prop_s_always_liveness.v:25: Assertion failed in top.t
%Error: t/t_prop_s_always_liveness.v:28: Verilog $stop %Error: t/t_prop_s_always_liveness.v:25: Verilog $stop
Aborting... Aborting...

12
test_regress/t/t_prop_s_always_liveness.v
View File

@ -20,19 +20,11 @@ module t (
int low_s_fail_q[$]; int low_s_fail_q[$];
int low_w_fail_q[$]; int low_w_fail_q[$];
// A new attempt starts every tick, so the last hi attempts still have an open // The youngest [2:5] windows are still open at $finish, so strong s_always
// [2:5] window when the trace ends. Even though a_high is constantly true, // reports a liveness failure even with a_high always 1; weak always does not.
// 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); 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); 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) assert property (@(posedge clk) s_always [2:5] a_low)
else low_s_fail_q.push_back(cyc); else low_s_fail_q.push_back(cyc);
assert property (@(posedge clk) always [2:5] a_low) assert property (@(posedge clk) always [2:5] a_low)