Skip to content

Commit

Permalink
tests: remove -seq 1 from sat with -tempinduct where possible
Browse files Browse the repository at this point in the history
* 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
  • Loading branch information
georgerennie committed Oct 3, 2024
1 parent 1bf908d commit dfa8453
Show file tree
Hide file tree
Showing 15 changed files with 16 additions and 16 deletions.
2 changes: 1 addition & 1 deletion tests/svtypes/typedef_initial_and_assign.ys
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions tests/svtypes/typedef_struct_port.ys
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion tests/various/const_arg_loop.ys
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion tests/various/const_func.ys
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion tests/various/countbits.ys
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion tests/various/param_struct.ys
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion tests/verilog/atom_type_signedness.ys
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion tests/verilog/int_types.ys
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion tests/verilog/mem_bounds.ys
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion tests/verilog/param_no_default.ys
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion tests/verilog/parameters_across_files.ys
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion tests/verilog/typedef_across_files.ys
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion tests/verilog/typedef_legacy_conflict.ys
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion tests/verilog/unbased_unsized.ys
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion tests/verilog/unbased_unsized_shift.ys
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit dfa8453

Please sign in to comment.