diff --git a/test_regress/t/t_cover_sequence.v b/test_regress/t/t_cover_sequence.v index 20418317a..719a3c1ba 100644 --- a/test_regress/t/t_cover_sequence.v +++ b/test_regress/t/t_cover_sequence.v @@ -37,24 +37,19 @@ module t ( assign d = crc[15]; assign e = crc[20]; - // Form 1: cover sequence ( sexpr ) stmt -- default clocking, no disable + // Form 1: cover sequence ( sexpr ) stmt cover sequence (a | b | c | d | e) hit_simple++; - // Form 2: cover sequence ( clocking_event sexpr ) stmt -- explicit clock, - // bounded range delay (the case where IEEE "every end-of-match" diverges - // from cover_property's "one match per attempt" semantics) + // Form 2: cover sequence ( clocking_event sexpr ) stmt cover sequence (@(posedge clk) (a | b | c | d | e) ##[1:3] b) hit_clocked++; // Form 3: cover sequence ( clocking_event disable iff (expr) sexpr ) stmt cover sequence (@(posedge clk) disable iff (!rst_n) a ##1 b) hit_clocked_disable++; - // Form 4: cover sequence ( disable iff (expr) sexpr ) stmt -- default clock + // Form 4: cover sequence ( disable iff (expr) sexpr ) stmt cover sequence (disable iff (!rst_n) a ##1 c) hit_default_disable++; - // Form 5: consecutive repetition (per-end-of-match). A ranged repetition - // a[*2:3] ends every cycle a 2- or 3-run completes; by IEEE 1800-2023 16.9.2 - // a[*2:3] == a[*2] or a[*3], so the range count equals the sum of the two - // fixed counts -- a Questa-free identity that validates the multiplicity. + // Form 5: consecutive repetition, counted per end-of-match cover sequence (a [* 2: 3]) hit_consrep_range++; cover sequence (a [* 2]) hit_consrep_2++; cover sequence (a [* 3]) hit_consrep_3++; @@ -68,20 +63,28 @@ module t ( if (cyc == 2) rst_n <= 1'b1; if (cyc == 99) begin `checkh(crc, 64'h261a9f1371d7aadf); - `checkd(hit_simple, 96); // Questa: 95 (single-sexpr sample-edge diff) - `checkd(hit_clocked, 149); // IEEE 16.14.3: every end-of-match - `checkd(hit_clocked_disable, 28); // Questa: 27 (sample-edge diff, ##1 single delay) - `checkd(hit_default_disable, 30); // Questa: 30 -`ifdef TEST_VERBOSE - $write("consrep range=%0d 2=%0d 3=%0d sum=%0d\n", hit_consrep_range, hit_consrep_2, - hit_consrep_3, hit_consrep_2 + hit_consrep_3); -`endif - `checkd(hit_consrep_2, 30); - `checkd(hit_consrep_3, 14); - // IEEE 1800-2023 16.9.2: a[*2:3] == a[*2] or a[*3], so the per-end counts add. - `checkd(hit_consrep_range, hit_consrep_2 + hit_consrep_3); // == 44 - $write("*-* All Finished *-*\n"); $finish; end end + + // Read the counters in 'final', not the clocked block: a same-cycle read of a + // cover counter races the cover's increment under --threads (vltmt). Verilator + // counts one more end-of-match than Questa 2022.3 on some forms at the + // simulation boundary; the Questa value is noted per check. + final begin +`ifdef TEST_VERBOSE + $write("simple=%0d clocked=%0d clk_dis=%0d def_dis=%0d range=%0d 2=%0d 3=%0d\n", hit_simple, + hit_clocked, hit_clocked_disable, hit_default_disable, hit_consrep_range, hit_consrep_2, + hit_consrep_3); +`endif + `checkd(hit_simple, 96); // Questa: 95 + `checkd(hit_clocked, 149); // Questa: 149 + `checkd(hit_clocked_disable, 28); // Questa: 27 + `checkd(hit_default_disable, 30); // Questa: 30 + `checkd(hit_consrep_2, 30); // Questa: 29 + `checkd(hit_consrep_3, 14); // Questa: 13 + // a[*2:3] == a[*2] or a[*3] (IEEE 1800-2023 16.9.2) + `checkd(hit_consrep_range, hit_consrep_2 + hit_consrep_3); // 44; Questa: 42 + $write("*-* All Finished *-*\n"); + end endmodule