Tests: Pre-pull for #7946 (#7953)

test_regress/t/t_prop_s_always_eos_count.out

@@ -0,0 +1,9 @@
+*-* All Finished *-*
+[115] %Error: t_prop_s_always_eos_count.v:33: Assertion failed in top.t
+[115] %Error: t_prop_s_always_eos_count.v:40: Assertion failed in top.t
+[115] %Error: t_prop_s_always_eos_count.v:44: Assertion failed in top.t
+[115] %Error: t_prop_s_always_eos_count.v:48: Assertion failed in top.t
+[115] %Error: t_prop_s_always_eos_count.v:56: Assertion failed in top.t
+[115] %Error: t_prop_s_always_eos_count.v:62: Assertion failed in top.t
+[115] %Error: t_prop_s_always_eos_count.v:70: Assertion failed in top.t
+[115] %Error: t_prop_s_always_eos_count.v:73: Assertion failed in top.t

test_regress/t/t_prop_s_always_eos_count.py

@@ -0,0 +1,19 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# This program is free software; you can redistribute it and/or modify it
+# under the terms of either the GNU Lesser General Public License Version 3
+# or the Perl Artistic License Version 2.0.
+# SPDX-FileCopyrightText: 2026 Wilson Snyder
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('vlt')  # UNOPTTHREADS in vltmt due to many small assertion states
+
+# Keep running after an assertion failure so all unfinished strong-property
+# attempts can execute their action block at end of simulation.
+test.compile(verilator_flags2=['--assert', '--no-stop-fail'])
+test.execute(expect_filename=test.golden_filename)
+
+test.passes()

test_regress/t/t_prop_s_always_eos_count.v

@@ -0,0 +1,91 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 PlanV GmbH
+// SPDX-License-Identifier: CC0-1.0
+
+// Per-attempt s_always end-of-simulation failure multiplicity.
+
+module t (
+`ifdef VERILATOR
+    input clk
+`endif
+);
+
+`ifndef VERILATOR
+  logic clk = 1'b0;
+  always #5 clk = ~clk;
+`endif
+
+  int cyc = 0;
+  bit data = 0;
+  bit disable_now = 0;
+  bit abort_now = 0;
+
+  // Finish-edge sample differs from the preceding clock's sample
+  always @(posedge clk) begin
+    if (cyc == 8) data <= 0;
+    else if (cyc == 9) data <= 1;
+    else if (cyc == 10) data <= 0;
+  end
+
+  // s_always [1:3]: three unfinished attempts at $finish, each fires EOS_FAIL.
+  assert property (@(posedge clk) s_always[1: 3] 1'b1)
+  else $display("EOS_FAIL");
+
+  // s_always [2:2]: two distinct unfinished attempts, not one RedOr.
+  assert property (@(posedge clk) s_always[2: 2] 1'b1)
+  else $display("EOS_RING");
+
+  assert property (@(posedge clk) s_always[1: 1] 1'b1)
+  else $display("EOS_PAST=%0d", $past(data));
+
+  // Branch states OR-fold by attempt start cycle before EOS multiplicity
+  assert property (@(posedge clk) (s_always[1: 3] 1'b1) or(s_always[1: 3] 1'b1))
+  else $display("EOS_BRANCH");
+
+  // Exercise the bit-vector pending ring and resolved-attempt depth tracking.
+  assert property (@(posedge clk) (s_always[1: 40] 1'b1) or(s_always[1: 40] 1'b1))
+  else $display("EOS_LARGE_RING");
+
+  // Large lower bounds use bit-vector pending rings and age-indexed resolution.
+  assert property (@(posedge clk) (s_always[300: 300] 1'b1) or(s_always[300: 300] 1'b1))
+  else $display("EOS_DELAY_RING");
+
+  // Attempts resolved by the immediate sibling are not EOS failures
+  assert property (@(posedge clk) 1'b1 or(s_always[1: 3] 1'b1))
+  else $display("EOS_RESOLVED_BAD");
+
+  assert property (@(posedge clk) disable iff (disable_now) s_always[1: 3] 1'b1)
+  else $display("EOS_DISABLE_BAD");
+
+  assert property (@(posedge clk) sync_accept_on (abort_now) s_always[1: 3] 1'b1)
+  else $display("EOS_ABORT_BAD");
+
+  // A kill on the finish edge suppresses stale pending states.
+  assume property (@(posedge clk) s_always[1: 3] 1'b1)
+  else $display("EOS_KILL_BAD");
+
+  // A pending strong cover obligation is not an EOS failure.
+  cover property (@(posedge clk) s_always[1: 3] 1'b1);
+
+  // The default action carries the same per-attempt multiplicity.
+  assert property (@(posedge clk) s_always[1: 3] 1'b1);
+
+  always @(negedge clk) begin
+    if (cyc == 9) abort_now = 1;
+    if (cyc == 10) disable_now = 1;
+  end
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    if (cyc == 10) begin
+      // Kill assumptions only, then verify the standard $assertkill/$asserton flow.
+      $assertcontrol(5, 1, 4);
+      $assertcontrol(3, 1, 4);
+      $display("*-* All Finished *-*");
+      $finish;
+    end
+  end
+
+endmodule

test_regress/t/t_property_nfa_composites.py

@@ -0,0 +1,18 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# This program is free software; you can redistribute it and/or modify it
+# under the terms of either the GNU Lesser General Public License Version 3
+# or the Perl Artistic License Version 2.0.
+# SPDX-FileCopyrightText: 2026 Wilson Snyder
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('vlt_all')
+
+test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing'])
+
+test.execute()
+
+test.passes()

test_regress/t/t_property_nfa_composites.v

@@ -0,0 +1,148 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 PlanV GmbH
+// SPDX-License-Identifier: CC0-1.0
+
+// Per-attempt counts for composite sequence operators.
+
+// verilog_format: off
+`define stop $stop
+`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
+// verilog_format: on
+
+module t (
+    input clk
+);
+
+  // Common-end sequence OR
+  bit or_fail_start = 0, or_both_start = 0;
+  int or_fail_pass = 0, or_fail_count = 0;
+  int or_both_pass = 0, or_both_fail = 0;
+
+  assert property (@(posedge clk) or_fail_start |-> ((1'b1 ##1 1'b0) or(1'b1 ##1 1'b0)))
+    or_fail_pass++;
+  else or_fail_count++;
+
+  assert property (@(posedge clk) or_both_start |-> ((1'b1 ##1 1'b1) or(1'b1 ##1 1'b1)))
+    or_both_pass++;
+  else or_both_fail++;
+
+  // Cross-attempt sequence AND
+  bit cross_l_start = 0, cross_l_end = 0, cross_r_start = 0, cross_r_end = 0;
+  int cross_hits = 0;
+
+  cover property (@(posedge clk) (cross_l_start ##1 cross_l_end) and(cross_r_start ##2 cross_r_end))
+    cross_hits++;
+
+  // Throughout guard composed with sequence AND
+  bit throughout_start = 0, throughout_guard = 0;
+  int throughout_pass = 0, throughout_fail = 0;
+
+  assert property (@(posedge clk) throughout_start |->
+      ((throughout_guard throughout (1'b1 ##2 1'b1)) and
+       (1'b1 ##1 1'b1)))
+    throughout_pass++;
+  else throughout_fail++;
+
+  // Same-end intersect over branching left operands
+  int isect_pass_one = 0, isect_pass_both = 0, isect_pass_zero = 0;
+  int isect_fail_left = 0, isect_fail_right = 0, isect_fail_zero = 0;
+  int isect_unexp_one = 0, isect_unexp_both = 0, isect_unexp_zero_pass = 0;
+  int isect_unexp_zero_fail = 0, isect_unexp_left = 0, isect_unexp_right = 0;
+
+  assert property (@(posedge clk) ((1'b1 ##1 1'b1) or(1'b1 ##1 1'b0)) intersect (1'b1 ##1 1'b1))
+    isect_pass_one <= isect_pass_one + 1;
+  else isect_unexp_one <= isect_unexp_one + 1;
+
+  assert property (@(posedge clk) ((1'b1 ##1 1'b1) or(1'b1 ##1 1'b1)) intersect (1'b1 ##1 1'b1))
+    isect_pass_both <= isect_pass_both + 1;
+  else isect_unexp_both <= isect_unexp_both + 1;
+
+  assert property (@(posedge clk) (1'b1 or 1'b0) intersect 1'b1)
+    isect_pass_zero <= isect_pass_zero + 1;
+  else isect_unexp_zero_pass <= isect_unexp_zero_pass + 1;
+
+  assert property (@(posedge clk) (1'b0 or 1'b0) intersect 1'b1)
+    isect_unexp_zero_fail <= isect_unexp_zero_fail + 1;
+  else isect_fail_zero <= isect_fail_zero + 1;
+
+  assert property (@(posedge clk) ((1'b1 ##1 1'b0) or(1'b1 ##1 1'b0)) intersect (1'b1 ##1 1'b1))
+    isect_unexp_left <= isect_unexp_left + 1;
+  else isect_fail_left <= isect_fail_left + 1;
+
+  assert property (@(posedge clk) ((1'b1 ##1 1'b1) or(1'b1 ##1 1'b0)) intersect (1'b1 ##1 1'b0))
+    isect_unexp_right <= isect_unexp_right + 1;
+  else isect_fail_right <= isect_fail_right + 1;
+
+  initial begin
+    $assertpasson;
+    $assertvacuousoff;
+
+    repeat (2) @(negedge clk);
+
+    // Common-end OR stimulus
+    or_fail_start = 1;
+    or_both_start = 1;
+    @(negedge clk);
+    or_fail_start = 0;
+    or_both_start = 0;
+    repeat (2) @(negedge clk);
+
+    // Cross-attempt SAnd stimulus
+    cross_l_start = 1;
+    cross_r_start = 1;
+    @(negedge clk);
+    cross_l_start = 1;
+    cross_l_end = 0;
+    cross_r_start = 0;
+    cross_r_end = 0;
+    @(negedge clk);
+    cross_l_start = 0;
+    cross_l_end = 1;
+    cross_r_start = 0;
+    cross_r_end = 1;
+    @(negedge clk);
+    cross_l_end = 0;
+    cross_r_end = 0;
+    repeat (2) @(negedge clk);
+
+    // One failed throughout/SAnd attempt
+    throughout_guard = 1;
+    throughout_start = 1;
+    @(negedge clk);
+    throughout_start = 0;
+    throughout_guard = 0;
+    repeat (3) @(negedge clk);
+
+    // One successful throughout/SAnd attempt
+    throughout_guard = 1;
+    throughout_start = 1;
+    @(negedge clk);
+    throughout_start = 0;
+    repeat (3) @(negedge clk);
+
+    `checkd(or_fail_pass, 0);
+    `checkd(or_fail_count, 0);
+    `checkd(or_both_pass, 1);
+    `checkd(or_both_fail, 0);
+    `checkd(cross_hits, 0);
+    `checkd(throughout_pass, 1);
+    `checkd(throughout_fail, 1);
+    `checkd(isect_pass_one, 17);
+    `checkd(isect_pass_both, 17);
+    `checkd(isect_pass_zero, 18);
+    `checkd(isect_fail_left, 0);
+    `checkd(isect_fail_right, 17);
+    `checkd(isect_fail_zero, 18);
+    `checkd(isect_unexp_one, 0);
+    `checkd(isect_unexp_both, 0);
+    `checkd(isect_unexp_zero_pass, 0);
+    `checkd(isect_unexp_zero_fail, 0);
+    `checkd(isect_unexp_left, 0);
+    `checkd(isect_unexp_right, 0);
+    $write("*-* All Finished *-*\n");
+    $finish;
+  end
+
+endmodule

test_regress/t/t_property_nfa_counts.py

@@ -0,0 +1,18 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# This program is free software; you can redistribute it and/or modify it
+# under the terms of either the GNU Lesser General Public License Version 3
+# or the Perl Artistic License Version 2.0.
+# SPDX-FileCopyrightText: 2026 Wilson Snyder
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('vlt_all')
+
+test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing', '--coverage-user'])
+
+test.execute()
+
+test.passes()

test_regress/t/t_property_nfa_counts.v

@@ -0,0 +1,180 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 PlanV GmbH
+// SPDX-License-Identifier: CC0-1.0
+
+// Per-attempt assertion outcome counts.
+
+// verilog_format: off
+`define stop $stop
+`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
+// verilog_format: on
+
+module t (
+    input clk
+);
+
+  int cyc = 0;
+
+  initial $assertpasson;
+
+  // Overlapping attempts maturing in the same time slot
+  bit imp_a = 1, imp_b = 0;
+  bit chain_a = 1, chain_b = 0, chain_c = 0;
+  bit range_a = 1, range_b = 0;
+  int imp_pass = 0, imp_fail = 0;
+  int chain_pass = 0, chain_fail = 0;
+  int range_pass = 0, range_fail = 0, range_cover = 0;
+
+  assert property (@(posedge clk) imp_a |-> ##1 imp_b) imp_pass++;
+  else imp_fail++;
+
+  assert property (@(posedge clk) chain_a ##1 chain_b ##1 chain_c) chain_pass++;
+  else chain_fail++;
+
+  assert property (@(posedge clk) range_a ##[1:2] range_b) range_pass++;
+  else range_fail++;
+  cover property (@(posedge clk) range_a ##[1:2] range_b) range_cover++;
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    if (cyc == 0) begin
+      imp_a <= 0;
+      chain_a <= 1;
+      chain_b <= 1;
+      range_a <= 1;
+      range_b <= 0;
+    end
+    else if (cyc == 1) begin
+      imp_a <= 0;
+      imp_b <= 0;
+      chain_a <= 0;
+      chain_b <= 0;
+      chain_c <= 1;
+      range_a <= 0;
+      range_b <= 1;
+    end
+  end
+
+  // The same multiplicity through the large-range ring-buffer path
+  bit large_a = 0, large_b = 0;
+  int large_pass = 0, large_fail = 0, large_cover = 0, large_imp_at_b = 0;
+
+  assert property (@(posedge clk) large_a ##[1:300] large_b) large_pass++;
+  else large_fail++;
+  cover property (@(posedge clk) large_a ##[1:300] large_b) large_cover++;
+  assert property (@(posedge clk) large_a |-> ##[1:300] large_b) if (large_b) large_imp_at_b++;
+
+  initial begin
+    @(negedge clk) large_a = 1;
+    @(negedge clk) large_a = 1;
+    @(negedge clk) begin
+      large_a = 0;
+      large_b = 1;
+    end
+    @(negedge clk) large_b = 0;
+  end
+
+  // Negation swaps each attempt's verdict at the tagged cycle
+  bit neg_a = 0, neg_b = 0;
+  bit neg_chain_a = 0, neg_chain_b = 0, neg_chain_c = 0, neg_chain_target = 0;
+  bit neg_imp_a = 0, neg_imp_b = 0, neg_imp_c = 0, neg_imp_target = 0;
+  int neg_fail_at_b = 0, neg_large_fail_at_b = 0;
+  int neg_chain_pass = 0, neg_chain_fail = 0, neg_chain_cover = 0;
+  int neg_imp_pass = 0;
+  int vacuous_pass = 0, negated_vacuous_pass = 0;
+
+  assert property (@(posedge clk) not (neg_a ##[1:2] neg_b))
+  else if (neg_b) neg_fail_at_b++;
+  assert property (@(posedge clk) not (neg_a ##[1:300] neg_b))
+  else if (neg_b) neg_large_fail_at_b++;
+
+  assert property (@(posedge clk) not (neg_chain_a ##1 neg_chain_b ##1 neg_chain_c)) begin
+    if (neg_chain_target) neg_chain_pass++;
+  end
+  else begin
+    if (neg_chain_target) neg_chain_fail++;
+  end
+  cover property (@(posedge clk) not (neg_chain_a ##1 neg_chain_b ##1 neg_chain_c))
+    if (neg_chain_target) neg_chain_cover++;
+
+  // One nonvacuous and one vacuous pass in the same clock
+  assert property (@(posedge clk) neg_imp_a |-> not (neg_imp_b ##1 neg_imp_c))
+    if (neg_imp_target) neg_imp_pass++;
+
+  assert property (@(posedge clk) 0 |-> ##1 1) vacuous_pass++;
+  assert property (@(posedge clk) 0 |-> not (##1 1)) negated_vacuous_pass++;
+
+  initial begin
+    @(negedge clk) begin
+      neg_a = 1;
+      neg_chain_a = 1;
+      neg_imp_a = 1;
+      neg_imp_b = 1;
+    end
+    @(negedge clk) begin
+      neg_a = 1;
+      neg_chain_a = 1;
+      neg_chain_b = 1;
+      neg_imp_a = 0;
+      neg_imp_b = 0;
+      neg_imp_target = 1;
+    end
+    @(negedge clk) begin
+      neg_a = 0;
+      neg_b = 1;
+      neg_chain_a = 0;
+      neg_chain_b = 0;
+      neg_chain_c = 1;
+      neg_chain_target = 1;
+      neg_imp_target = 0;
+    end
+    @(negedge clk) begin
+      neg_b = 0;
+      neg_chain_target = 0;
+    end
+  end
+
+  // Property-case branches of different lengths failing on the same tick
+  logic [1:0] selector;
+  int case_fail = 0;
+
+  always_comb begin
+    if (cyc == 2) selector = 0;
+    else if (cyc == 3) selector = 1;
+    else selector = 2;
+  end
+
+  assert property (@(posedge clk) case (selector) 0: 1'b1 ##2 1'b0; 1: 1'b1 ##1 1'b0; default: 1'b1;
+  endcase)
+  else case_fail++;
+
+  always @(negedge clk) begin
+    if (cyc == 12) begin
+      `checkd(imp_pass, 10);
+      `checkd(imp_fail, 1);
+      `checkd(chain_pass, 2);
+      `checkd(chain_fail, 11);
+      `checkd(range_pass, 1);
+      `checkd(range_fail, 10);
+      `checkd(range_cover, 1);
+      `checkd(large_pass, 1);
+      `checkd(large_fail, 10);
+      `checkd(large_cover, 1);
+      `checkd(large_imp_at_b, 2);
+      `checkd(neg_fail_at_b, 1);
+      `checkd(neg_large_fail_at_b, 1);
+      `checkd(neg_chain_pass, 2);
+      `checkd(neg_chain_fail, 2);
+      `checkd(neg_chain_cover, 1);
+      `checkd(neg_imp_pass, 2);
+      `checkd(vacuous_pass, 12);
+      `checkd(negated_vacuous_pass, 12);
+      `checkd(case_fail, 2);
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+
+endmodule

test_regress/t/t_property_nfa_edge_shapes.out

@@ -0,0 +1,4 @@
+*-* All Finished *-*
+[215] %Error: t_property_nfa_edge_shapes.v:27: Assertion failed in top.t
+%Error: t/t_property_nfa_edge_shapes.v:27: Verilog $stop
+Aborting...

test_regress/t/t_property_nfa_edge_shapes.py

@@ -0,0 +1,18 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# This program is free software; you can redistribute it and/or modify it
+# under the terms of either the GNU Lesser General Public License Version 3
+# or the Perl Artistic License Version 2.0.
+# SPDX-FileCopyrightText: 2026 Wilson Snyder
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('vlt_all')
+
+test.compile(verilator_flags2=['--assert', '--timing', '--coverage-user'])
+
+test.execute(fails=True, expect_filename=test.golden_filename)
+
+test.passes()

test_regress/t/t_property_nfa_edge_shapes.v

@@ -0,0 +1,52 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 PlanV GmbH
+// SPDX-License-Identifier: CC0-1.0
+
+// Corner shapes: negated liveness, single-cycle cover abort, strong cover or
+
+// verilog_format: off
+`define stop $stop
+`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
+// verilog_format: on
+
+module t (
+    input clk
+);
+
+  logic a = 0, b = 0, c = 0, x = 0;
+  int cyc = 0;
+  int np1 = 0, nf1 = 0, nc2 = 0, nc3 = 0, nf4 = 0, nc5 = 0;
+
+  // verilog_format: off
+  assert property (@(posedge clk) not (##[1:$] b)) np1 = np1 + 1; else nf1 = nf1 + 1;
+
+  cover property (@(posedge clk) accept_on (x) c) nc2 = nc2 + 1;
+
+  cover property (@(posedge clk) (s_always [1:2] a) or (s_always [1:2] c)) nc3 = nc3 + 1;
+
+  assert property (@(posedge clk) ((a ##2 b) or (c ##2 b)) |-> s_always [1:2] a) else nf4 = nf4 + 1;
+
+  cover property (@(posedge clk) sync_accept_on (x) c) nc5 = nc5 + 1;
+  // verilog_format: on
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    a <= (cyc >= 8 && cyc <= 13);
+    b <= (cyc == 2) || (cyc == 10);
+    c <= (cyc == 4);
+    x <= (cyc == 4);
+    if (cyc == 20) $finish;
+  end
+
+  final begin
+    `checkd(np1, 19);
+    `checkd(nf1, 2);
+    `checkd(nc2, 1);
+    `checkd(nc3, 5);
+    `checkd(nf4, 0);
+    `checkd(nc5, 1);
+    $write("*-* All Finished *-*\n");
+  end
+endmodule

test_regress/t/t_property_nfa_error_limit.out

@@ -0,0 +1,7 @@
+[7] %Error: t_property_nfa_error_limit.v:46: Assertion failed in top.t: 'assert' failed.
+-Info: t/t_property_nfa_error_limit.v:46: Verilog $stop, ignored due to +verilator+error+limit
+[7] %Error: t_property_nfa_error_limit.v:45: Assertion failed in top.t: 'assert' failed.
+[9] %Error: t_property_nfa_error_limit.v:32: Assertion failed in top.t: 'assert' failed.
+[11] %Error: t_property_nfa_error_limit.v:35: Assertion failed in top.t: 'assert' failed.
+[13] %Error: t_property_nfa_error_limit.v:37: Assertion failed in top.t: 'assert' failed.
+*-* All Finished *-*

test_regress/t/t_property_nfa_error_limit.py

@@ -0,0 +1,18 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# This program is free software; you can redistribute it and/or modify it
+# under the terms of either the GNU Lesser General Public License Version 3
+# or the Perl Artistic License Version 2.0.
+# SPDX-FileCopyrightText: 2026 Wilson Snyder
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('vlt_all')
+
+test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing'])
+
+test.execute(all_run_flags=['+verilator+error+limit+10'], expect_filename=test.golden_filename)
+
+test.passes()

test_regress/t/t_property_nfa_error_limit.v

@@ -0,0 +1,88 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 PlanV GmbH
+// SPDX-License-Identifier: CC0-1.0
+
+// Default and counted fail actions under an error limit.
+
+// verilog_format: off
+`define stop $stop
+`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
+// verilog_format: on
+
+module t (
+    input clk
+);
+
+  int cyc = 0;
+
+  // Default actions for property-case branches of different lengths
+  logic [1:0] selector;
+  bit nb = 0;
+  bit abrt = 0;
+  bit zz = 0;
+
+  always_comb begin
+    if (cyc == 2) selector = 0;
+    else if (cyc == 3) selector = 1;
+    else selector = 2;
+  end
+
+  assert property (@(posedge clk) case (selector) 0: 1'b1 ##2 1'b0; 1: 1'b1 ##1 1'b0; default: 1'b1;
+  endcase);
+
+  assert property (@(posedge clk) not (1'b1 ##[1:2] nb));
+
+  assert property (@(posedge clk) sync_reject_on (abrt) always[0: 1] (!zz));
+
+  // Simultaneous negated-consequent failures behind a temporal antecedent
+  bit ant = 0;
+  bit b = 0;
+  int temporal_small_fail = 0, temporal_ring_fail = 0, boolean_ant_fail = 0;
+  int impossible_pass = 0, impossible_fail = 0;
+
+  assert property (@(posedge clk) (1'b1 ##1 ant) |-> not (1'b1 ##[1:2] b));
+  assert property (@(posedge clk) (1'b1 ##1 ant) |-> not (1'b1 ##[1:300] b));
+
+  assert property (@(posedge clk) (1'b1 ##1 ant) |-> not (1'b1 ##[1:2] b))
+  else temporal_small_fail++;
+  assert property (@(posedge clk) (1'b1 ##1 ant) |-> not (1'b1 ##[1:300] b))
+  else temporal_ring_fail++;
+
+  assert property (@(posedge clk) ant |-> not (1'b1 ##[1:2] b))
+  else boolean_ant_fail++;
+
+  assert property (@(posedge clk) not (1'b1 ##1 1'b1)) impossible_pass++;
+  assert property (@(posedge clk) not (1'b1 ##1 1'b0))
+  else impossible_fail++;
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    nb <= (cyc == 4);
+    abrt <= (cyc == 5);
+  end
+
+  initial begin
+    @(negedge clk) ant = 1;
+    @(negedge clk) ant = 1;
+    @(negedge clk) begin
+      ant = 0;
+      b = 1;
+    end
+    @(negedge clk) b = 0;
+  end
+
+  always @(negedge clk) begin
+    if (cyc == 8) begin
+      `checkd(temporal_small_fail, 1);
+      `checkd(temporal_ring_fail, 1);
+      `checkd(boolean_ant_fail, 1);
+      `checkd(impossible_pass, 0);
+      `checkd(impossible_fail, 0);
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+
+endmodule

test_regress/t/t_property_nfa_final_past.py

@@ -0,0 +1,20 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# This program is free software; you can redistribute it and/or modify it
+# under the terms of either the GNU Lesser General Public License Version 3
+# or the Perl Artistic License Version 2.0.
+# SPDX-FileCopyrightText: 2026 Wilson Snyder
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('vlt_all')
+
+test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing'])
+
+test.execute(all_run_flags=['+expect_past=0'])
+
+test.execute(all_run_flags=['+offedge', '+expect_past=0'])
+
+test.passes()

test_regress/t/t_property_nfa_final_past.v

@@ -0,0 +1,49 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 PlanV GmbH
+// SPDX-License-Identifier: CC0-1.0
+
+// $past in 'final' for on-tick and between-tick simulation ends
+
+module t;
+
+  bit clk = 0;
+  bit data = 0;
+  bit offedge = 0;
+  bit exp_past = 0;
+  int cyc = 0;
+
+  always #1 clk = ~clk;
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    data <= ~data;
+    if (!offedge && cyc == 2) begin
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+
+  default clocking cb @(posedge clk);
+  endclocking
+
+  initial begin
+    offedge = $test$plusargs("offedge") != 0;
+    void'($value$plusargs("expect_past=%b", exp_past));
+    if (offedge) begin
+      #6;
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+
+  final begin
+    if ($past(data) !== exp_past) begin
+      $display("%%Error: wrong $past in final: got=%0b exp=%0b offedge=%0b", $past(data), exp_past,
+               offedge);
+      $stop;
+    end
+  end
+
+endmodule

test_regress/t/t_property_nfa_past_sched.py

@@ -0,0 +1,18 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# This program is free software; you can redistribute it and/or modify it
+# under the terms of either the GNU Lesser General Public License Version 3
+# or the Perl Artistic License Version 2.0.
+# SPDX-FileCopyrightText: 2026 Wilson Snyder
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('vlt_all')
+
+test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing'])
+
+test.execute()
+
+test.passes()

test_regress/t/t_property_nfa_past_sched.v

@@ -0,0 +1,75 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 PlanV GmbH
+// SPDX-License-Identifier: CC0-1.0
+
+// $past staging in assertion actions and non-final function/task callers.
+
+// verilog_format: off
+`define stop $stop
+`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0h exp=%0h\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
+// verilog_format: on
+
+module t;
+
+  bit clk = 0;
+  int cyc = 0;
+
+  always #1 clk = ~clk;
+
+  default clocking cb @(posedge clk);
+  endclocking
+
+  // $past in an assertion action returns the previous sampled value
+  bit act_data = 0;
+  bit history[0:4] = '{default: 0};
+  int history_count = 0;
+
+  always @(posedge clk) act_data <= ~act_data;
+
+  assert property (@(posedge clk) 1'b1 ##1 1'b1) begin
+    if (history_count < 5) history[history_count] = $past(act_data);
+    history_count++;
+  end
+
+  // Non-final function/task callers retain the normal $past lowering
+  bit data = 0;
+
+  function automatic bit fpast();
+    return $past(data);
+  endfunction
+
+  task automatic tpast(output bit result);
+    result = $past(data);
+  endtask
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    data <= ~data;
+  end
+
+  always @(negedge clk) begin
+    bit direct;
+    bit via_task;
+    direct = $past(data);
+    tpast(via_task);
+    if (fpast() !== direct || via_task !== direct) begin
+      $display("%%Error: direct=%0b function=%0b task=%0b", direct, fpast(), via_task);
+      $fatal;
+    end
+  end
+
+  initial begin
+    repeat (6) @(negedge clk);
+    `checkd(history_count, 5);
+    `checkd(history[0], 0);
+    `checkd(history[1], 1);
+    `checkd(history[2], 0);
+    `checkd(history[3], 1);
+    `checkd(history[4], 0);
+    $write("*-* All Finished *-*\n");
+    $finish;
+  end
+
+endmodule

test_regress/t/t_property_nfa_stop_error_limit.out

@@ -0,0 +1,2 @@
+-Info: t/t_property_nfa_stop_error_limit.v:29: Verilog $stop, ignored due to +verilator+error+limit
+*-* All Finished *-*

test_regress/t/t_property_nfa_stop_error_limit.py

@@ -0,0 +1,18 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# This program is free software; you can redistribute it and/or modify it
+# under the terms of either the GNU Lesser General Public License Version 3
+# or the Perl Artistic License Version 2.0.
+# SPDX-FileCopyrightText: 2026 Wilson Snyder
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('vlt_all')
+
+test.compile(verilator_flags2=['--assert', '--timing'])
+
+test.execute(all_run_flags=['+verilator+error+limit+10'], expect_filename=test.golden_filename)
+
+test.passes()

test_regress/t/t_property_nfa_stop_error_limit.v

@@ -0,0 +1,45 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 PlanV GmbH
+// SPDX-License-Identifier: CC0-1.0
+
+// Ignored worker-queued $stop against same-slot assertion evaluation.
+
+// verilog_format: off
+`define stop $stop
+`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
+// verilog_format: on
+
+module t (
+    input clk
+);
+
+  int cyc = 0;
+  int passes = 0;
+
+  assert property (@(posedge clk) 1'b1 ##1 1'b1) passes++;
+
+  default clocking cb @(posedge clk);
+  endclocking
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    // A clocked process is emitted inside an eval mtask in threaded models
+    if (cyc == 5) $stop;
+    if (cyc == 10) begin
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+
+  always @(negedge clk) begin
+    if (cyc == 10) `checkd(passes, 9);
+  end
+
+  final begin
+    $stop;
+    `checkd($past(cyc), 10);
+  end
+
+endmodule

test_regress/t/t_property_nfa_stop_error_limit_crossing.out

@@ -0,0 +1,3 @@
+ACTION_RAN
+%Error: t/t_property_nfa_stop_error_limit_crossing.v:23: Verilog $stop
+Aborting...

test_regress/t/t_property_nfa_stop_error_limit_crossing.py

@@ -0,0 +1,20 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# This program is free software; you can redistribute it and/or modify it
+# under the terms of either the GNU Lesser General Public License Version 3
+# or the Perl Artistic License Version 2.0.
+# SPDX-FileCopyrightText: 2026 Wilson Snyder
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('vlt_all')
+
+test.compile(verilator_flags2=['--assert', '--timing'])
+
+test.execute(fails=True,
+             all_run_flags=['+verilator+error+limit+1'],
+             expect_filename=test.golden_filename)
+
+test.passes()

test_regress/t/t_property_nfa_stop_error_limit_crossing.v

@@ -0,0 +1,26 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 PlanV GmbH
+// SPDX-License-Identifier: CC0-1.0
+
+// A worker-queued $stop at the error limit suppresses same-slot assertion actions.
+
+module t (
+    input clk
+);
+
+  int cyc = 0;
+
+  // The exact golden excludes ACTION_RAN for the stopping edge.
+  assert property (@(posedge clk) 1'b1 ##1 1'b1) begin
+    if ($sampled(cyc) == 5) $write("ACTION_RAN\n");
+  end
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    // A clocked process is emitted inside an eval mtask in threaded models.
+    if (cyc == 5) $stop;
+  end
+
+endmodule

test_regress/t/t_property_nfa_throughout_count.py

@@ -0,0 +1,18 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# This program is free software; you can redistribute it and/or modify it
+# under the terms of either the GNU Lesser General Public License Version 3
+# or the Perl Artistic License Version 2.0.
+# SPDX-FileCopyrightText: 2026 Wilson Snyder
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('vlt_all')
+
+test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing', '--coverage-user'])
+
+test.execute()
+
+test.passes()

test_regress/t/t_property_nfa_throughout_count.v

@@ -0,0 +1,91 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 PlanV GmbH
+// SPDX-License-Identifier: CC0-1.0
+
+// Throughout guard-drop failure counts across live attempts.
+
+// verilog_format: off
+`define stop $stop
+`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
+// verilog_format: on
+
+module t (
+    input clk
+);
+
+  bit fixed_start = 0, fixed_guard = 1, drop_tag = 0;
+  int fixed_fail = 0, negated_pass = 0, negated_cover = 0;
+
+  bit range_start = 0, range_guard = 1, range_done = 0;
+  int range_fail = 0;
+
+  bit disable_now = 0, disabled_guard = 1;
+  int disabled_fail = 0;
+
+  bit kill_start = 0, kill_guard = 1;
+  int kill_fail = 0;
+
+  assert property (@(posedge clk) fixed_start |-> (fixed_guard throughout (1'b1 ##300 1'b1)))
+  else fixed_fail++;
+
+  assert property (@(posedge clk) not (fixed_guard throughout (fixed_start ##300 1'b1))) begin
+    if (drop_tag) negated_pass++;
+  end
+  cover property (@(posedge clk) not (fixed_guard throughout (fixed_start ##300 1'b1))) begin
+    if (drop_tag) negated_cover++;
+  end
+
+  assert property (@(posedge clk)
+      range_start |-> (range_guard throughout (1'b1 ##[1:300] range_done)))
+  else range_fail++;
+
+  assert property (@(posedge clk) disable iff (disable_now)
+      fixed_start |-> (disabled_guard throughout (1'b1 ##300 1'b1)))
+  else disabled_fail++;
+
+  assert property (@(posedge clk) kill_start |-> (kill_guard throughout (1'b1 ##300 1'b1)))
+  else kill_fail++;
+
+  initial begin
+    @(negedge clk) begin
+      fixed_start = 1;
+      range_start = 1;
+    end
+    repeat (2) @(negedge clk);
+    @(negedge clk) begin
+      fixed_start = 0;
+      fixed_guard = 0;
+      drop_tag = 1;
+      range_start = 0;
+      range_guard = 0;
+      disable_now = 1;
+      disabled_guard = 0;
+    end
+    #1 disable_now = 0;
+    @(negedge clk) begin
+      `checkd(fixed_fail, 1);
+      `checkd(range_fail, 1);
+      `checkd(negated_pass, 1);
+      `checkd(negated_cover, 1);
+      `checkd(disabled_fail, 0);
+      drop_tag = 0;
+      kill_start = 1;
+    end
+
+    repeat (2) @(negedge clk);
+    @(negedge clk) begin
+      kill_start = 0;
+      kill_guard = 0;
+      $assertkill;
+      $asserton;
+    end
+    @(negedge clk) begin
+      `checkd(kill_fail, 0);
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+
+endmodule