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
This commit is contained in:
committed by
Jannis Harder
parent
012ddc2f1e
commit
8fb3f88842
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user