aboutsummaryrefslogtreecommitdiffstats
path: root/tests/various/dynamic_part_select.ys
diff options
context:
space:
mode:
Diffstat (limited to 'tests/various/dynamic_part_select.ys')
-rw-r--r--tests/various/dynamic_part_select.ys106
1 files changed, 106 insertions, 0 deletions
diff --git a/tests/various/dynamic_part_select.ys b/tests/various/dynamic_part_select.ys
new file mode 100644
index 000000000..abc1daad6
--- /dev/null
+++ b/tests/various/dynamic_part_select.ys
@@ -0,0 +1,106 @@
+### Original testcase ###
+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