Merge pull request #1589 from YosysHQ/iopad_default

Make iopad option default for all xilinx flows

19 files changed, 61 insertions, 60 deletions

diff --git a/tests/arch/xilinx/add_sub.ys b/tests/arch/xilinx/add_sub.ys
index 9dbddce47..313948cc5 100644
--- a/tests/arch/xilinx/add_sub.ys
+++ b/tests/arch/xilinx/add_sub.ys
@@ -1,7 +1,7 @@
 read_verilog ../common/add_sub.v
 hierarchy -top top
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
 select -assert-count 14 t:LUT2
diff --git a/tests/arch/xilinx/adffs.ys b/tests/arch/xilinx/adffs.ys
index c0ff6a2e2..3328f9edc 100644
--- a/tests/arch/xilinx/adffs.ys
+++ b/tests/arch/xilinx/adffs.ys
@@ -3,7 +3,7 @@ design -save read
 
 hierarchy -top adff
 proc
-equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd adff # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
@@ -15,7 +15,7 @@ select -assert-none t:BUFG t:FDCE %% t:* %D
 design -load read
 hierarchy -top adffn
 proc
-equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd adffn # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
@@ -28,7 +28,7 @@ select -assert-none t:BUFG t:FDCE t:INV %% t:* %D
 design -load read
 hierarchy -top dffs
 proc
-equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd dffs # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
@@ -40,7 +40,7 @@ select -assert-none t:BUFG t:FDSE %% t:* %D
 design -load read
 hierarchy -top ndffnr
 proc
-equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd ndffnr # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
diff --git a/tests/arch/xilinx/attributes_test.ys b/tests/arch/xilinx/attributes_test.ys
index 4c881b280..7bdd94a63 100644
--- a/tests/arch/xilinx/attributes_test.ys
+++ b/tests/arch/xilinx/attributes_test.ys
@@ -1,7 +1,7 @@
 # Check that blockram memory without parameters is not modified
 read_verilog ../common/memory_attributes/attributes_test.v
 hierarchy -top block_ram
-synth_xilinx -top block_ram
+synth_xilinx -top block_ram -noiopad
 cd block_ram # Constrain all select calls below inside the top module
 select -assert-count 1 t:RAMB18E1
  
@@ -9,7 +9,7 @@ select -assert-count 1 t:RAMB18E1
 design -reset
 read_verilog ../common/memory_attributes/attributes_test.v
 hierarchy -top distributed_ram
-synth_xilinx -top distributed_ram
+synth_xilinx -top distributed_ram -noiopad
 cd distributed_ram # Constrain all select calls below inside the top module
 select -assert-count 8 t:RAM32X1D
  
@@ -18,7 +18,7 @@ design -reset
 read_verilog ../common/memory_attributes/attributes_test.v
 prep
 setattr -mod -set ram_style "distributed" block_ram
-synth_xilinx -top block_ram
+synth_xilinx -top block_ram -noiopad
 cd block_ram # Constrain all select calls below inside the top module
 select -assert-count 32 t:RAM128X1D
  
@@ -27,7 +27,7 @@ design -reset
 read_verilog ../common/memory_attributes/attributes_test.v
 prep
 setattr -mod -set logic_block 1 block_ram
-synth_xilinx -top block_ram
+synth_xilinx -top block_ram -noiopad
 cd block_ram # Constrain all select calls below inside the top module
 select -assert-count 0 t:RAMB18E1
 select -assert-count 32 t:RAM128X1D
@@ -35,13 +35,13 @@ select -assert-count 32 t:RAM128X1D
 # Set ram_style block to a distributed memory; will be implemented as blockram
 design -reset
 read_verilog ../common/memory_attributes/attributes_test.v
-synth_xilinx -top distributed_ram_manual
+synth_xilinx -top distributed_ram_manual -noiopad
 cd distributed_ram_manual # Constrain all select calls below inside the top module
 select -assert-count 1 t:RAMB18E1
  
 # Set synthesis, ram_block block to a distributed memory; will be implemented as blockram
 design -reset
 read_verilog ../common/memory_attributes/attributes_test.v
-synth_xilinx -top distributed_ram_manual_syn
+synth_xilinx -top distributed_ram_manual_syn -noiopad
 cd distributed_ram_manual_syn # Constrain all select calls below inside the top module
 select -assert-count 1 t:RAMB18E1
diff --git a/tests/arch/xilinx/blockram.ys b/tests/arch/xilinx/blockram.ys
index bb908cbbf..ed743cf44 100644
--- a/tests/arch/xilinx/blockram.ys
+++ b/tests/arch/xilinx/blockram.ys
@@ -3,28 +3,28 @@
 # Memory bits <= 18K; Data width <= 36; Address width <= 14: -> RAMB18E1
 read_verilog ../common/blockram.v
 chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 1 sync_ram_sdp
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
 
 design -reset
 read_verilog ../common/blockram.v
 chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 18 sync_ram_sdp
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
 
 design -reset
 read_verilog ../common/blockram.v
 chparam -set ADDRESS_WIDTH 14 -set DATA_WIDTH 1 sync_ram_sdp
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
 
 design -reset
 read_verilog ../common/blockram.v
 chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 sync_ram_sdp
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
 
@@ -32,7 +32,7 @@ select -assert-count 1 t:RAMB18E1
 design -reset
 read_verilog ../common/blockram.v
 chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 2 sync_ram_sdp
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 0 t:RAMB18E1
 select -assert-count 4 t:RAM128X1D
@@ -41,7 +41,7 @@ select -assert-count 4 t:RAM128X1D
 design -reset
 read_verilog ../common/blockram.v
 chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 36 sync_ram_sdp
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB36E1
 
@@ -52,7 +52,7 @@ design -reset
 read_verilog ../common/blockram.v
 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 
 setattr -set ram_style "block" m:memory
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
 
@@ -60,7 +60,7 @@ design -reset
 read_verilog ../common/blockram.v
 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 
 setattr -set ram_block 1 m:memory
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
 
@@ -68,7 +68,7 @@ design -reset
 read_verilog ../common/blockram.v
 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 
 setattr -set ram_style "dont_infer_a_ram_pretty_please" m:memory
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 0 t:RAMB18E1
 
@@ -76,7 +76,7 @@ design -reset
 read_verilog ../common/blockram.v
 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 
 setattr -set logic_block 1 m:memory
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 0 t:RAMB18E1
 
@@ -84,7 +84,7 @@ design -reset
 read_verilog ../common/blockram.v
 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1
 setattr -set ram_style "block" m:memory
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
 
@@ -92,6 +92,6 @@ design -reset
 read_verilog ../common/blockram.v
 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1
 setattr -set ram_block 1 m:memory
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
diff --git a/tests/arch/xilinx/bug1460.ys b/tests/arch/xilinx/bug1460.ys
index 2018071cc..09935ccd8 100644
--- a/tests/arch/xilinx/bug1460.ys
+++ b/tests/arch/xilinx/bug1460.ys
@@ -28,7 +28,7 @@ module register_file(
 endmodule
 EOT
 
-synth_xilinx
+synth_xilinx -noiopad
 cd register_file
 select -assert-count 32 t:RAM32M
 select -assert-none t:* t:BUFG %d t:RAM32M %d
diff --git a/tests/arch/xilinx/counter.ys b/tests/arch/xilinx/counter.ys
index 604acdbfc..11c29922e 100644
--- a/tests/arch/xilinx/counter.ys
+++ b/tests/arch/xilinx/counter.ys
@@ -2,7 +2,7 @@ read_verilog ../common/counter.v
 hierarchy -top top
 proc
 flatten
-equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
 
diff --git a/tests/arch/xilinx/dffs.ys b/tests/arch/xilinx/dffs.ys
index 0bba4858f..dc764b033 100644
--- a/tests/arch/xilinx/dffs.ys
+++ b/tests/arch/xilinx/dffs.ys
@@ -3,7 +3,7 @@ design -save read
 
 hierarchy -top dff
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd dff # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
@@ -15,7 +15,7 @@ select -assert-none t:BUFG t:FDRE %% t:* %D
 design -load read
 hierarchy -top dffe
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd dffe # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
diff --git a/tests/arch/xilinx/dsp_cascade.ys b/tests/arch/xilinx/dsp_cascade.ys
index f9185551b..ca6b619b9 100644
--- a/tests/arch/xilinx/dsp_cascade.ys
+++ b/tests/arch/xilinx/dsp_cascade.ys
@@ -19,7 +19,7 @@ EOT
 proc
 design -save read
 
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 design -load postopt
 cd cascade
 select -assert-count 3 t:DSP48E1
@@ -35,7 +35,7 @@ select -assert-none t:DSP48E1 t:BUFG %% t:* %D
 select -assert-count 2 t:DSP48E1 %co:+[PCOUT] t:DSP48E1 %d %co:+[PCIN] w:* %d t:DSP48E1 %i
 
 design -load read
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad
 design -load postopt
 cd cascade
 select -assert-count 3 t:DSP48A1
@@ -65,7 +65,7 @@ EOT
 proc
 design -save read
 
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 design -load postopt
 cd cascade
 select -assert-count 2 t:DSP48E1
@@ -75,7 +75,7 @@ select -assert-none t:DSP48E1 t:BUFG %% t:* %D
 select -assert-count 1 t:DSP48E1 %co:+[PCOUT] t:DSP48E1 %d %co:+[PCIN] w:* %d t:DSP48E1 %i
 
 design -load read
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad
 design -load postopt
 cd cascade
 select -assert-count 2 t:DSP48A1
diff --git a/tests/arch/xilinx/dsp_fastfir.ys b/tests/arch/xilinx/dsp_fastfir.ys
index 0067a822b..57fe49bde 100644
--- a/tests/arch/xilinx/dsp_fastfir.ys
+++ b/tests/arch/xilinx/dsp_fastfir.ys
@@ -63,7 +63,7 @@ module fastfir_dynamictaps(i_clk, i_reset, i_tap_wr, i_tap, i_ce, i_sample, o_re
 endmodule
 EOT
 
-synth_xilinx
+synth_xilinx -noiopad
 cd fastfir_dynamictaps
 select -assert-count 2 t:DSP48E1
 select -assert-none t:* t:DSP48E1 %d t:BUFG %d
diff --git a/tests/arch/xilinx/fsm.ys b/tests/arch/xilinx/fsm.ys
index f03400fe7..3235d5af3 100644
--- a/tests/arch/xilinx/fsm.ys
+++ b/tests/arch/xilinx/fsm.ys
@@ -3,7 +3,7 @@ hierarchy -top fsm
 proc
 flatten
 
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+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 -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
 
diff --git a/tests/arch/xilinx/latches.ys b/tests/arch/xilinx/latches.ys
index c87a8e38b..e226c2ec8 100644
--- a/tests/arch/xilinx/latches.ys
+++ b/tests/arch/xilinx/latches.ys
@@ -3,7 +3,7 @@ design -save read
 
 hierarchy -top latchp
 proc
-equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd latchp # Constrain all select calls below inside the top module
 select -assert-count 1 t:LDCE
@@ -14,7 +14,7 @@ select -assert-none t:LDCE %% t:* %D
 design -load read
 hierarchy -top latchn
 proc
-equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd latchn # Constrain all select calls below inside the top module
 select -assert-count 1 t:LDCE
@@ -26,7 +26,7 @@ select -assert-none t:LDCE t:INV %% t:* %D
 design -load read
 hierarchy -top latchsr
 proc
-equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd latchsr # Constrain all select calls below inside the top module
 select -assert-count 1 t:LDCE
diff --git a/tests/arch/xilinx/logic.ys b/tests/arch/xilinx/logic.ys
index d5b5c1a37..61a9314cc 100644
--- a/tests/arch/xilinx/logic.ys
+++ b/tests/arch/xilinx/logic.ys
@@ -1,7 +1,7 @@
 read_verilog ../common/logic.v
 hierarchy -top top
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
 
diff --git a/tests/arch/xilinx/lutram.ys b/tests/arch/xilinx/lutram.ys
index 6c9d1eae1..3f127a77e 100644
--- a/tests/arch/xilinx/lutram.ys
+++ b/tests/arch/xilinx/lutram.ys
@@ -2,7 +2,7 @@
 #hierarchy -top lutram_1w1r -chparam A_WIDTH 4
 #proc
 #memory -nomap
-#equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+#equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 #memory
 #opt -full
 #
@@ -22,7 +22,7 @@ read_verilog ../common/lutram.v
 hierarchy -top lutram_1w1r -chparam A_WIDTH 5
 proc
 memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 memory
 opt -full
 
@@ -42,7 +42,7 @@ read_verilog ../common/lutram.v
 hierarchy -top lutram_1w1r
 proc
 memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 memory
 opt -full
 
@@ -62,7 +62,7 @@ read_verilog ../common/lutram.v
 hierarchy -top lutram_1w3r
 proc
 memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 memory
 opt -full
 
@@ -82,7 +82,7 @@ read_verilog ../common/lutram.v
 hierarchy -top lutram_1w3r -chparam A_WIDTH 6
 proc
 memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 memory
 opt -full
 
@@ -102,7 +102,7 @@ read_verilog ../common/lutram.v
 hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 6
 proc
 memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 memory
 opt -full
 
@@ -122,7 +122,7 @@ read_verilog ../common/lutram.v
 hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 6
 proc
 memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 memory
 opt -full
 
diff --git a/tests/arch/xilinx/macc.ys b/tests/arch/xilinx/macc.ys
index 11e959976..bf2b36320 100644
--- a/tests/arch/xilinx/macc.ys
+++ b/tests/arch/xilinx/macc.ys
@@ -3,8 +3,8 @@ design -save read
 
 hierarchy -top macc
 proc
-#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
@@ -17,8 +17,8 @@ select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D
 design -load read
 hierarchy -top macc2
 proc
-#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
diff --git a/tests/arch/xilinx/mul.ys b/tests/arch/xilinx/mul.ys
index 6cf994fbf..490846ff1 100644
--- a/tests/arch/xilinx/mul.ys
+++ b/tests/arch/xilinx/mul.ys
@@ -1,7 +1,7 @@
 read_verilog ../common/mul.v
 hierarchy -top top
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
 
@@ -13,7 +13,7 @@ design -reset
 read_verilog ../common/mul.v
 hierarchy -top top
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
 
diff --git a/tests/arch/xilinx/mul_unsigned.ys b/tests/arch/xilinx/mul_unsigned.ys
index c714680af..980263cbd 100644
--- a/tests/arch/xilinx/mul_unsigned.ys
+++ b/tests/arch/xilinx/mul_unsigned.ys
@@ -2,7 +2,7 @@ read_verilog mul_unsigned.v
 hierarchy -top mul_unsigned
 proc
 
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd mul_unsigned # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
@@ -16,7 +16,7 @@ read_verilog mul_unsigned.v
 hierarchy -top mul_unsigned
 proc
 
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd mul_unsigned # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
diff --git a/tests/arch/xilinx/mux.ys b/tests/arch/xilinx/mux.ys
index 388272449..99817738d 100644
--- a/tests/arch/xilinx/mux.ys
+++ b/tests/arch/xilinx/mux.ys
@@ -3,7 +3,7 @@ design -save read
 
 hierarchy -top mux2
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd mux2 # Constrain all select calls below inside the top module
 select -assert-count 1 t:LUT3
@@ -14,7 +14,7 @@ select -assert-none t:LUT3 %% t:* %D
 design -load read
 hierarchy -top mux4
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd mux4 # Constrain all select calls below inside the top module
 select -assert-count 1 t:LUT6
@@ -25,7 +25,7 @@ select -assert-none t:LUT6 %% t:* %D
 design -load read
 hierarchy -top mux8
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd mux8 # Constrain all select calls below inside the top module
 select -assert-count 1 t:LUT3
@@ -37,7 +37,7 @@ select -assert-none t:LUT3 t:LUT6 %% t:* %D
 design -load read
 hierarchy -top mux16
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd mux16 # Constrain all select calls below inside the top module
 select -assert-min 5 t:LUT6
diff --git a/tests/arch/xilinx/shifter.ys b/tests/arch/xilinx/shifter.ys
index 455437f18..3652319a0 100644
--- a/tests/arch/xilinx/shifter.ys
+++ b/tests/arch/xilinx/shifter.ys
@@ -2,7 +2,7 @@ read_verilog ../common/shifter.v
 hierarchy -top top
 proc
 flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
 
diff --git a/tests/arch/xilinx/tribuf.ys b/tests/arch/xilinx/tribuf.ys
index 4697703ca..eaccab126 100644
--- a/tests/arch/xilinx/tribuf.ys
+++ b/tests/arch/xilinx/tribuf.ys
@@ -7,6 +7,7 @@ synth
 equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd tristate # Constrain all select calls below inside the top module
-# TODO :: Tristate logic not yet supported; see https://github.com/YosysHQ/yosys/issues/1225
-select -assert-count 1 t:$_TBUF_
-select -assert-none t:$_TBUF_ %% t:* %D
+select -assert-count 2 t:IBUF
+select -assert-count 1 t:INV
+select -assert-count 1 t:OBUFT
+select -assert-none t:IBUF t:INV t:OBUFT %% t:* %D