tests: remove -seq 1 from sat with -tempinduct where possible

* When used with -tempinduct mode, -seq <N> 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
YosysHQ · Oct 3, 2024 · d4546d8 · d4546d8
1 parent 1bf908d
commit d4546d8
Show file tree

Hide file tree

Showing 27 changed files with 17,888 additions and 16 deletions.
diff --git a/tests/simple_abc9/abc9.err b/tests/simple_abc9/abc9.err
diff --git a/tests/simple_abc9/case_large.err b/tests/simple_abc9/case_large.err
diff --git a/tests/simple_abc9/dynslice.err b/tests/simple_abc9/dynslice.err
diff --git a/tests/simple_abc9/generate.err b/tests/simple_abc9/generate.err
diff --git a/tests/simple_abc9/memory.err b/tests/simple_abc9/memory.err
diff --git a/tests/simple_abc9/multiplier.err b/tests/simple_abc9/multiplier.err
diff --git a/tests/simple_abc9/operators.err b/tests/simple_abc9/operators.err
diff --git a/tests/simple_abc9/paramods.err b/tests/simple_abc9/paramods.err
diff --git a/tests/simple_abc9/partsel.err b/tests/simple_abc9/partsel.err
diff --git a/tests/simple_abc9/process.err b/tests/simple_abc9/process.err
diff --git a/tests/simple_abc9/realexpr.err b/tests/simple_abc9/realexpr.err
diff --git a/tests/simple_abc9/repwhile.err b/tests/simple_abc9/repwhile.err
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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