diff options
| -rw-r--r-- | tests/various/dynamic_part_select.ys | 60 |
1 files changed, 30 insertions, 30 deletions
diff --git a/tests/various/dynamic_part_select.ys b/tests/various/dynamic_part_select.ys index 7db0f62c0..2dc061e89 100644 --- a/tests/various/dynamic_part_select.ys +++ b/tests/various/dynamic_part_select.ys @@ -3,105 +3,105 @@ read_verilog ./dynamic_part_select/original.v proc rename -top gold design -stash gold - + read_verilog ./dynamic_part_select/original_gate.v proc rename -top gate design -stash gate - + design -copy-from gold -as gold gold design -copy-from gate -as gate gate - + miter -equiv -make_assert -make_outcmp -flatten gold gate equiv sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv - + ### Multiple blocking assingments ### design -reset read_verilog ./dynamic_part_select/multiple_blocking.v proc rename -top gold design -stash gold - + read_verilog ./dynamic_part_select/multiple_blocking_gate.v proc rename -top gate design -stash gate - + design -copy-from gold -as gold gold design -copy-from gate -as gate gate - + miter -equiv -make_assert -make_outcmp -flatten gold gate equiv sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv - + ### Non-blocking to the same output register ### design -reset read_verilog ./dynamic_part_select/nonblocking.v proc rename -top gold design -stash gold - + read_verilog ./dynamic_part_select/nonblocking_gate.v proc rename -top gate design -stash gate - + design -copy-from gold -as gold gold design -copy-from gate -as gate gate - + miter -equiv -make_assert -make_outcmp -flatten gold gate equiv sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv - + ### For-loop select, one dynamic input design -reset read_verilog ./dynamic_part_select/forloop_select.v proc rename -top gold design -stash gold - + read_verilog ./dynamic_part_select/forloop_select_gate.v proc rename -top gate design -stash gate - + design -copy-from gold -as gold gold design -copy-from gate -as gate gate - + miter -equiv -make_assert -make_outcmp -flatten gold gate equiv sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv - + #### Double loop (part-select, reset) ### design -reset read_verilog ./dynamic_part_select/reset_test.v proc rename -top gold design -stash gold - + read_verilog ./dynamic_part_select/reset_test_gate.v proc rename -top gate design -stash gate - + design -copy-from gold -as gold gold design -copy-from gate -as gate gate - + miter -equiv -make_assert -make_outcmp -flatten gold gate equiv sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv - + ### Reversed part-select case ### design -reset read_verilog ./dynamic_part_select/reversed.v proc rename -top gold design -stash gold - + read_verilog ./dynamic_part_select/reversed_gate.v proc rename -top gate design -stash gate - + design -copy-from gold -as gold gold design -copy-from gate -as gate gate - + miter -equiv -make_assert -make_outcmp -flatten gold gate equiv sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv @@ -120,8 +120,8 @@ design -stash gate design -copy-from gold -as gold gold design -copy-from gate -as gate gate - -miter -equiv -make_assert -make_outcmp -flatten gold gate equiv + +miter -equiv -make_assert -make_outcmp -flatten gold gate equiv sat -prove-asserts -show-public -verify -set-init-zero equiv ### @@ -139,8 +139,8 @@ design -stash gate design -copy-from gold -as gold gold design -copy-from gate -as gate gate - -miter -equiv -make_assert -make_outcmp -flatten gold gate equiv + +miter -equiv -make_assert -make_outcmp -flatten gold gate equiv sat -prove-asserts -seq 10 -show-public -falsify -set-init-zero equiv ## Part select + latch, with no shift&mask @@ -157,6 +157,6 @@ design -stash gate design -copy-from gold -as gold gold design -copy-from gate -as gate gate - -miter -equiv -make_assert -make_outcmp -flatten gold gate equiv -sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv + +miter -equiv -make_assert -make_outcmp -flatten gold gate equiv +sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv |