From dfa8453102d6b5d023c151914efe65ecfc2268ca Mon Sep 17 00:00:00 2001 From: George Rennie Date: Thu, 3 Oct 2024 16:34:19 +0200 Subject: [PATCH] tests: remove -seq 1 from sat with -tempinduct where possible * When used with -tempinduct mode, -seq causes assertions to be ignored in the first N steps. While this has uses for reset modelling, for these test cases it is unnecessary and could lead to failures slipping through uncaught --- tests/svtypes/typedef_initial_and_assign.ys | 2 +- tests/svtypes/typedef_struct_port.ys | 4 ++-- tests/various/const_arg_loop.ys | 2 +- tests/various/const_func.ys | 2 +- tests/various/countbits.ys | 2 +- tests/various/param_struct.ys | 2 +- tests/verilog/atom_type_signedness.ys | 2 +- tests/verilog/int_types.ys | 2 +- tests/verilog/mem_bounds.ys | 2 +- tests/verilog/param_no_default.ys | 2 +- tests/verilog/parameters_across_files.ys | 2 +- tests/verilog/typedef_across_files.ys | 2 +- tests/verilog/typedef_legacy_conflict.ys | 2 +- tests/verilog/unbased_unsized.ys | 2 +- tests/verilog/unbased_unsized_shift.ys | 2 +- 15 files changed, 16 insertions(+), 16 deletions(-) diff --git a/tests/svtypes/typedef_initial_and_assign.ys b/tests/svtypes/typedef_initial_and_assign.ys index e778a49bb01..4563ca4919b 100644 --- a/tests/svtypes/typedef_initial_and_assign.ys +++ b/tests/svtypes/typedef_initial_and_assign.ys @@ -11,4 +11,4 @@ logger -expect warning "reg '\\var_19' is assigned in a continuous assignment" 1 read_verilog -sv typedef_initial_and_assign.sv hierarchy; proc; opt; async2sync select -module top -sat -verify -seq 1 -tempinduct -prove-asserts -show-all +sat -verify -tempinduct -prove-asserts -show-all diff --git a/tests/svtypes/typedef_struct_port.ys b/tests/svtypes/typedef_struct_port.ys index dd0775b9ff9..6cd61064cf7 100644 --- a/tests/svtypes/typedef_struct_port.ys +++ b/tests/svtypes/typedef_struct_port.ys @@ -1,6 +1,6 @@ read_verilog -sv typedef_struct_port.sv hierarchy; proc; opt; async2sync select -module top -sat -verify -seq 1 -tempinduct -prove-asserts -show-all +sat -verify -tempinduct -prove-asserts -show-all select -module test_parser -sat -verify -seq 1 -tempinduct -prove-asserts -show-all +sat -verify -tempinduct -prove-asserts -show-all diff --git a/tests/various/const_arg_loop.ys b/tests/various/const_arg_loop.ys index 01bea704499..21554cc0a49 100644 --- a/tests/various/const_arg_loop.ys +++ b/tests/various/const_arg_loop.ys @@ -4,4 +4,4 @@ proc opt -full select -module top async2sync -sat -verify -seq 1 -tempinduct -prove-asserts -show-all +sat -verify -tempinduct -prove-asserts -show-all diff --git a/tests/various/const_func.ys b/tests/various/const_func.ys index d982c3a43fa..e721e0e8157 100644 --- a/tests/various/const_func.ys +++ b/tests/various/const_func.ys @@ -5,4 +5,4 @@ flatten opt -full select -module top async2sync -sat -verify -seq 1 -tempinduct -prove-asserts -show-all +sat -verify -tempinduct -prove-asserts -show-all diff --git a/tests/various/countbits.ys b/tests/various/countbits.ys index f2db9cfe1f6..2d972e2d812 100644 --- a/tests/various/countbits.ys +++ b/tests/various/countbits.ys @@ -5,4 +5,4 @@ flatten opt -full select -module top async2sync -sat -verify -seq 1 -tempinduct -prove-asserts -show-all +sat -verify -tempinduct -prove-asserts -show-all diff --git a/tests/various/param_struct.ys b/tests/various/param_struct.ys index bb26b61d586..96837aafc0c 100644 --- a/tests/various/param_struct.ys +++ b/tests/various/param_struct.ys @@ -48,4 +48,4 @@ endmodule EOF hierarchy; proc; opt async2sync -sat -verify -seq 1 -tempinduct -prove-asserts -show-all +sat -verify -tempinduct -prove-asserts -show-all diff --git a/tests/verilog/atom_type_signedness.ys b/tests/verilog/atom_type_signedness.ys index c8a82f993c5..77a0bd2910a 100644 --- a/tests/verilog/atom_type_signedness.ys +++ b/tests/verilog/atom_type_signedness.ys @@ -16,4 +16,4 @@ endmodule EOT hierarchy; proc; opt; async2sync select -module dut -sat -verify -seq 1 -tempinduct -prove-asserts -show-all +sat -verify -tempinduct -prove-asserts -show-all diff --git a/tests/verilog/int_types.ys b/tests/verilog/int_types.ys index 344f3ee09aa..70c99976cad 100644 --- a/tests/verilog/int_types.ys +++ b/tests/verilog/int_types.ys @@ -5,4 +5,4 @@ flatten opt -full async2sync select -module top -sat -verify -seq 1 -tempinduct -prove-asserts -show-all +sat -verify -tempinduct -prove-asserts -show-all diff --git a/tests/verilog/mem_bounds.ys b/tests/verilog/mem_bounds.ys index 146a6f43302..2c973822a4f 100644 --- a/tests/verilog/mem_bounds.ys +++ b/tests/verilog/mem_bounds.ys @@ -4,4 +4,4 @@ flatten opt -full select -module top async2sync -sat -verify -seq 1 -tempinduct -prove-asserts -show-all -enable_undef +sat -verify -tempinduct -prove-asserts -show-all -enable_undef diff --git a/tests/verilog/param_no_default.ys b/tests/verilog/param_no_default.ys index 0509f6a1aa5..c609987e46d 100644 --- a/tests/verilog/param_no_default.ys +++ b/tests/verilog/param_no_default.ys @@ -5,4 +5,4 @@ flatten opt -full async2sync select -module top -sat -verify -seq 1 -tempinduct -prove-asserts -show-all +sat -verify -tempinduct -prove-asserts -show-all diff --git a/tests/verilog/parameters_across_files.ys b/tests/verilog/parameters_across_files.ys index 94565eb6703..3efe3e68c8c 100644 --- a/tests/verilog/parameters_across_files.ys +++ b/tests/verilog/parameters_across_files.ys @@ -18,4 +18,4 @@ flatten opt -full async2sync select -module top -sat -verify -seq 1 -tempinduct -prove-asserts -show-all +sat -verify -tempinduct -prove-asserts -show-all diff --git a/tests/verilog/typedef_across_files.ys b/tests/verilog/typedef_across_files.ys index baa4b7919dd..8cd578af43c 100644 --- a/tests/verilog/typedef_across_files.ys +++ b/tests/verilog/typedef_across_files.ys @@ -21,4 +21,4 @@ proc opt -full async2sync select -module top -sat -verify -seq 1 -tempinduct -prove-asserts -show-all +sat -verify -tempinduct -prove-asserts -show-all diff --git a/tests/verilog/typedef_legacy_conflict.ys b/tests/verilog/typedef_legacy_conflict.ys index dd1503a852c..d26cc188f81 100644 --- a/tests/verilog/typedef_legacy_conflict.ys +++ b/tests/verilog/typedef_legacy_conflict.ys @@ -35,4 +35,4 @@ flatten opt -full async2sync select -module top -sat -verify -seq 1 -tempinduct -prove-asserts -show-all +sat -verify -tempinduct -prove-asserts -show-all diff --git a/tests/verilog/unbased_unsized.ys b/tests/verilog/unbased_unsized.ys index 75d1bf5e4b5..3290650d531 100644 --- a/tests/verilog/unbased_unsized.ys +++ b/tests/verilog/unbased_unsized.ys @@ -5,4 +5,4 @@ flatten opt -full async2sync select -module top -sat -verify -seq 1 -tempinduct -prove-asserts -show-all +sat -verify -tempinduct -prove-asserts -show-all diff --git a/tests/verilog/unbased_unsized_shift.ys b/tests/verilog/unbased_unsized_shift.ys index 2b5b9d8d082..6a72560b8a1 100644 --- a/tests/verilog/unbased_unsized_shift.ys +++ b/tests/verilog/unbased_unsized_shift.ys @@ -5,4 +5,4 @@ flatten opt -full async2sync select -module top -sat -verify -seq 1 -tempinduct -prove-asserts -show-all +sat -verify -tempinduct -prove-asserts -show-all