Adding tests for dynamic part select optimisation

1 files changed, 59 insertions, 0 deletions

diff --git a/tests/arch/xilinx/dynamic_part_select.ys b/tests/arch/xilinx/dynamic_part_select.ys
new file mode 100644
index 000000000..597229cc9
--- /dev/null
+++ b/tests/arch/xilinx/dynamic_part_select.ys
@@ -0,0 +1,59 @@
+#### Original testcase ###
+read_verilog ../common/dynamic_part_select/original.v
+hierarchy -top original
+prep -flatten -top original
+design -save gold
+ 
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -seq 10 -prove-skip 1 miter
+ 
+### Multiple blocking assingments ###
+read_verilog ../common/dynamic_part_select/multiple_blocking.v
+hierarchy -top multiple_blocking
+prep -flatten -top multiple_blocking
+design -save gold
+ 
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -seq 10 -prove-skip 1 miter
+ 
+### Non-blocking to the same output register ###
+read_verilog ../common/dynamic_part_select/nonblocking.v
+hierarchy -top nonblocking
+prep -flatten -top nonblocking
+design -save gold
+ 
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -seq 10 -prove-skip 1 miter
+
+### For-loop select, one dynamic input
+read_verilog ../common/dynamic_part_select/forloop_select.v
+hierarchy -top forloop_select
+prep -flatten -top forloop_select
+design -save gold
+ 
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -seq 5 -prove-skip 1 miter
+
+### Double loop (part-select, reset) ### 
+read_verilog ../common/dynamic_part_select/reset_test.v
+hierarchy -top reset_test
+prep -flatten -top reset_test
+design -save gold
+ 
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -seq 10 -prove-skip 1 miter
+
+### Reversed part-select case ###
+read_verilog ../common/dynamic_part_select/reversed.v
+hierarchy -top reversed
+prep -flatten -top reversed
+design -save gold
+ 
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -seq 20 -prove-skip 1 miter